Exposing newtype coercions to Haskell

[Simon Peyton-Jones]

Good stuff.  The basic idea seems good to me.



I'm not sure that a plugin is the way to go here, though it's a good start.

·        Exactly which programs are type-correct?  Eg
    coerce (listNT createNT)

It all depends on exactly what type args createNT is applied to.

·        A function f = createNT probably would not be accepted.  But if ‘f’ was inlined sufficiently early (before the plugin) it might.

·        Giving an error message in terms of exactly the text the user wrote is harder.

·        I’m not sure how you expect to deal with essential NT arguments:

newtype T a = MkT a a

tNT :: NT a b -> NT (T a) (T b)

tNT n = createNT ???



On the whole I think a ‘deriving’ form would be preferable.  And then yes, you’ll need to build HEAD.



To your questions:

·        To do these kind of things, CoreM will need more reader stuff.  In particular:

o   The global TypeEnv

o   The GlobalRdrEnv

·        I don’t think we have generic Core traversal functions, perhaps because almost every such pass needs to deal with binders.



Simon





|  -----Original Message-----

|  From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-

|  bounces at haskell.org] On Behalf Of Joachim Breitner

|  Sent: 01 July 2013 13:00

|  To: glasgow-haskell-users at haskell.org

|  Subject: Exposing newtype coercions to Haskell

|

|  Hi,

|

|  this is related to

|  http://hackage.haskell.org/trac/ghc/wiki/NewtypeWrappers#Proposal3.

|  I tried to hack up a little prototype of this, and this “works” now:

|

|          import GHC.NT

|

|          newtype Age = Age Int deriving Show

|

|          ageNT :: NT Age Int

|          ageNT = createNT

|

|          newtype MyList a = MyList [a] deriving Show

|

|          myListNT :: NT (MyList a) [a]

|          myListNT = createNT

|

|

|          main = do

|              let n = 1 :: Int

|              let a = coerce (sym ageNT) 1

|              let l1 = [a]

|              let l2 = coerce (listNT ageNT) l1

|              let l3 = coerce (sym myListNT) l2

|              print a

|              print l2

|              print l3

|

|  will print

|

|          Age 1

|          [1]

|          MyList [1]

|

|  and no unsafeCoerce and no map is used in the production of this output.

|

|

|  The GHC.NT module provides:

|

|  data NT a b

|  coerce :: NT a b -> a -> b

|  refl   :: NT a a

|  sym    :: NT a b -> NT b a

|  trans  :: NT a b -> NT b c -> NT a c

|  createNT :: NT a b

|  listNT :: NT a b -> NT [a] [b]

|

|  where createNT takes the place of the "deriving foo :: NT a b" syntax:

|  At compile time, it is checked if its first type argument is a newtype of the second,

|  and the corresponding coercion is inserted, otherwise an error is (well, will be)

|  printed.

|

|  The idea is that these coercions will be guaranteed to be free (or almost free; I am

|  not sure if the coercion witness (NT a b) will actually be optimized away).

|

|

|  The prototype can be found at

|  https://github.com/nomeata/nt-coerce

|  and is implemented as a GHC plugin compatible with GHC 7.6.3 (I chose this

|  route as it means not having to compile GHC). You can check if it works for you via

|  $ ghc  -dcore-lint -package ghc --make test.hs  && ./test

|

|  The code itself is, well, at most prototype code quality and contains quite a

|  number of hacks and other warts, mostly due to my inexperience with GHC

|  hacking, and I could make use of some advice. Some more concrete questions:

|

|   * How do I look up a module (here GHC.NT.Type) and a name therein (NT) in

|  CoreM? I tried to go via getOrigNameCache, but passing the ModuleName name to

|  lookupModuleEnv yielded Nothing, although it seems to me to be precisely the

|  same name that I find in moduleEnvKeys. If I take the ModuleName from that list,

|  it works. Similar problems with the OccEnv.

|  Please see

|  https://github.com/nomeata/nt-

|  coerce/blob/edef9f4d4889dde651bb086e76c576f84e8f8aec/GHC/NT/Plugin.hs#L9

|  9

|  for what I tried (and how I worked around it). This work-around also prevents

|  building the package with cabal right now.

|

|   * I did not find generic Core traversal functions like traverse :: (Monad m) =>

|  (Expr a -> m (Maybe (Expr a))) -> Expr a -> m (Expr a) which  I defined in

|  https://github.com/nomeata/nt-

|  coerce/blob/edef9f4d4889dde651bb086e76c576f84e8f8aec/GHC/NT/Plugin.hs#L2

|  31.

|  Are such traversals re-implemented everywhere or did I just not search well

|  enough?

|

|   * On the core level, once I have a TyCon, I also have all DataCons available. Is

|  there already code present that checks if the currently compiled module really

|  should see the data constructors, i.e. if they are exported? I see code in

|  normaliseFfiType, but that seems to be integrated in the type checker, and it

|  seems I need a GlobalRdrEnv; can I get such a thing in a Core2Core pass?

|

|

|  Thanks,

|  Joachim

|

|  --

|  Joachim “nomeata” Breitner

|    mail at joachim-breitner.de • http://www.joachim-breitner.de/

|    Jabber: nomeata at joachim-breitner.de  • GPG-Key: 0x4743206C

|    Debian Developer: nomeata at debian.org
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20130702/c40bc9d8/attachment-0001.htm>