Exposing newtype coercions to Haskell
simonpj at microsoft.com
Tue Jul 2 16:11:56 CEST 2013
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.
| -----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
| this is related to
| 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
| MyList 
| 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)
| 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
| 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
| 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
| Are such traversals re-implemented everywhere or did I just not search well
| * 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?
| 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...
More information about the Glasgow-haskell-users