Newtype wrappers

[Simon Peyton-Jones]

Joachim



I was talking to Stepanie about newtype wrappers, and realised that

a) there are two very different ways to use type classes to

   implement the feature, one good and one bad



b) the one I thought we were using is the Bad One



c) the one on the wiki page is sketched in far too little detail

   but is the Good One

   http://ghc.haskell.org/trac/ghc/wiki/NewtypeWrappers



Also, there's an interaction with "roles" which Richard is on the point of committing.



Below are some detailed notes.



Before too long, could you refresh the wiki page to:

* demote rejected ideas

* explain the accepted plan in more detail

* discuss implementation aspects



Thanks



Simon



Bad version

~~~~~~~~~~~

  class NT a b

  rep  :: NT a b => a -> b

  wrap :: NT a b => b -> a



Then for each newtype

  newtype Age = Int

we generate

  axiom axAge :: Age ~ Int

  instance NT Age Int



and for data types

   data (a,b) = (a,b)

we generate

   instance (NT a a', NT b b') => NT (a,b) (a',b')



Internally (NT a b) is implemented as a simple boxing of a

representational equality:

   data NT a b = MkNT (a ~#R b)



There are many problems here

  - It's tiresome for the programmer to remember whether

    to use rep or wrap

  - Many levels of newtype would require repeated application

    of rep (or wrap).  But if I say (rep (rep x)) I immediately

    get ambiguity, unless I also supply a type sig for each

    intermediate level.





Good version (this may be what you are doing already)

~~~~~~~~~~~~

  class NT a b

  ntCast :: NT a b => a -> b



Notice only one ntCast, which will work both ways.



Then for each newtype

  newtype Age = Int

we generate

  axiom axAge :: Age ~ Int

  instance NT Int b => NT Age b

  instance NT a Int => NT b Age



Notice *two* instances



For data types, same as before

   data (a,b) = (a,b)

we generate

   instance (NT a a', NT b b') => NT (a,b) (a',b')



And we have instance NT a a.



Now try this

  f :: (Age, Bool, Int) -> (Int, Bool, Age)

  f x = ntCast x



>From the ntCast we get the wanted constraint

  NT (Age,Bool,Int) (Int,Bool,Age)

Then we simplify as follows

  NT (Age,Bool,Int) (Int,Bool,Age)

---> by instance decl for (,,)

  NT Age Int, NT Bool Bool, NT Int Age

---> by instance NT a a, solves NT Bool Bool

  NT Age Int, NT Int Age

---> by instance NT Int a => NT Age a

  NT Int Int, NT Int Age

---> by instance NT a a, solves NT Int Int

  NT Int Age

...and so on...



In effect, we normalise both arguments of the NT independently

until they match (are equal, or have an outermost list).  This

will even do a good job of

   newtype Moo = MkMoo Age



   f :: Moo -> Age

   f x = ntCast x



Try it.. it'll normalise the (NT Moo Age) to (NT Int Int), so the

coercion we ultimately build wil take x down to Int, then back up

to Age.  But that's fine... the coercion optimiser will remove the

intermediate steps.



This has lots of advantages:

  - No need to remember directions; ntCast does the job in either

    direction or both

  - No need for multiple levels of unwrapping... and hence no

    ambiguity for the intermediate steps.



A note about roles

~~~~~~~~~~~~~~~~~~

We are very keen that if we declare

  data Map key val = [(key,val)]

where the keys are kept ordered, then we do NOT want to allow

a cast from (Map Int val) to (Map Age val)



We were thinking about exercising this control by saying, in

a standalone deriving clause

  deriving NT v1 v2 => NT (Map k v1) (Map k v2)



But another, and more robust, way to express the fact that we

should not allow you to cast (Map Int val) to (Map Age val) is

to give Map the rules

p   Map key at Nominal val at Representational

in Richard's new system (about to be committed).  This gives

Map's first argument a more restrictive role than role inference

would give it.



And for good reason!  If we had



   class C k where

     foo :: Map k Int -> Bool



then we would NOT want to allow



   newtype Age = MkAge Int deriving( C )



And the thing that now prevents us doing that 'deriving( C )' is

precisely the more restrictive role on Map.



So, our proposal is: for every

  data T a = ... deriving( NT )

we get the lifting instance

   instance NT a b => NT (T a) (T b)

whose shape is controlled by T's argument roles.



We probably want to be able to say -XAutoDeriveNT, like -XAutoDeriveTypeable.





-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130802/c33bae6d/attachment.htm>