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@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Joachim Breitner | Sent: 01 July 2013 13:00 | To: glasgow-haskell-users@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@joachim-breitner.de • http://www.joachim-breitner.de/ | Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C | Debian Developer: nomeata@debian.org