newtype coercion wrapping status

Richard Eisenberg eir at cis.upenn.edu
Mon Sep 2 18:07:37 CEST 2013 

Yay! I'm really excited to see this coming along so nicely, especially as it has such a nice interaction with roles.

Here are some specific thoughts, upon reviewing your (surprisingly short!) patch:

- I strongly dislike the name NT (and derivatives), for at least two reasons: 1) Someone new to this work won't know what it means, and 2) it's useful for things unrelated to newtypes (because of phantoms). How about "safeCoerce"? The class could have the name "Coercible". Neither of these names conflict on a default search at Hoogle.

- Why box ~R#? Couldn't castEqR just take an unboxed R equality?

- If keeping boxed ~R#, you might want to add an ASSERT in mkEqReprBox ensuring that the coercion passed in has role R. (Use coercionRole.)

- It looks like you plan to make the NT class more wired in (line 507 of TcEvidence). Would this get rid of the Class parameter to EvNT and then simplify mkNT?

- getEqRolePredTys never seems to care about its Role return value. I'm happy about this, because the type-checker doesn't really know about roles. (It assumes everything is Nominal, which is how users would expect type-checking to behave, I think.)

- Without more comments, I get a little lost in the desugaring of EvNT and friends. But, I was able to trace the use of roles, and it looks sensible. In particular, it looks like mkTyConAppCo's preconditions around roles are satisfied, which can be tricky.

- It looks like you left some old code on line 1860 of TcInteract.

- The changes in Coercion are correct -- the use of Nominal that you removed harkened to the days when all CoVars were Nominal.

After looking at it all, I wonder if shoehorning this feature into the class / instance mechanism is the right way to go. How much is that buying us? The instance lookup mechanism for NT is totally customized (as it should be, it seems). So, how much harder would it be to make this a free-floating feature, separate from classes? This would mean adding a new thing with kind (* -> * -> Constraint) to replace "NT". (In a perfect world, this could be spelled ≈, but I'm not a huge fan of Unicode syntax in reality.) But, there would be no need to worry about user-defined instances, and all the wired-in class stuff could be gotten rid of. It's not that I think the class/instance approach is that bad, but we've had to wander so far away from using GHC's built-in features around instance lookup that I think we should re-examine.

Thoughts?

Thanks,
Richard

On Sep 2, 2013, at 10:42 AM, Joachim Breitner <mail at joachim-breitner.de> wrote:

> Hi,
> 
> after following SPJ’s latest advise and implementing the newtype
> coercion classes directly and ad-hoc in the type checker (in TcInteract,
> similarly to the SingI), this rewrite of the code is now working (for
> some value of working):
> 
> What works now
> ==============
> 
> The setup:
> Prelude> :info GHC.NT.castNT
> castNT :: NT a b => a -> b     -- Defined in ‛GHC.NT’
> 
> Simple cases:
> 
> Prelude> newtype Age = Age Int deriving Show
> Prelude> GHC.NT.castNT (Age 1) :: Int
> 1
> Prelude> GHC.NT.castNT (1::Int) :: Age
> Age 1
> 
> Unrolling several newtypes at the same time:
> 
> Prelude> newtype Bar = Bar Age deriving Show
> Prelude> newtype Baz = Baz Int deriving Show
> Prelude> GHC.NT.castNT (Baz 1) :: Bar
> Bar (Age 1)
> 
> Unrolling newtypes with type arguments, even polymorphically:
> 
> Prelude> newtype MyMB a = MyMB (Maybe a) deriving Show
> Prelude> GHC.NT.castNT (Just ()) :: MyMB ()
> MyMB (Just ())
> Prelude> let f1 = (\x -> GHC.NT.castNT (Just x)) :: a -> MyMB a
> Prelude> f1 True
> MyMB (Just True)
> Prelude> let f2 = (\x -> GHC.NT.castNT (Just x)) :: GHC.NT.NT a b => a -> MyMB b
> Prelude> f2 (Baz 1) :: MyMB Bar
> MyMB (Just (Bar (Age 1)))
> 
> 
> Unrolling inside type constructor arguments, including functions and
> tuples:
> 
> Prelude> GHC.NT.castNT (Just (Age 1)) :: Maybe Int
> Just 1
> Prelude> (GHC.NT.castNT Age :: (Baz -> Bar)) (Baz 1)
> Bar (Age 1)
> Prelude> GHC.NT.castNT (Age 1, Baz 1) :: (Bar, Int)
> (Bar (Age 1),1)
> 
> 
> Arbitrary changing of Phantom types:
> 
> Prelude> data Proxy a = Proxy deriving Show
> Prelude> GHC.NT.castNT (Proxy :: Proxy Int) :: Proxy Bool
> Proxy
> 
> Unwanted casting can be prevented by role annotations:
> 
> Prelude> :set -XRoleAnnotations 
> Prelude> data Map a at N b = Map a b deriving Show
> Prelude> GHC.NT.castNT (Map () (1::Int)) :: Map () Bar
> Map () (Bar (Age 1))
> Prelude> GHC.NT.castNT (Map (1::Int) ()) :: Map Bar ()
> 
> <interactive>:24:1:
>    No instance for (GHC.NT.NT (Map Int ()) (Map Bar ()))
>      arising from a use of ‛GHC.NT.castNT’
>    In the expression: GHC.NT.castNT (Map (1 :: Int) ()) :: Map Bar ()
>    In an equation for ‛it’:
>        it = GHC.NT.castNT (Map (1 :: Int) ()) :: Map Bar ()
> 
> GADTs have the roles set automatically, so this does not work either, as
> expected:
> 
> Prelude> :set -XGADTs -XStandaloneDeriving
> Prelude> data GADT a where GADT :: GADT Int
> Prelude> deriving instance Show (GADT a)
> Prelude> GHC.NT.castNT GADT :: GADT Age
> 
> <interactive>:37:1:
>    No instance for (GHC.NT.NT (GADT Int) (GADT Age))
>      arising from a use of ‛GHC.NT.castNT’
>    In the expression: GHC.NT.castNT GADT :: GADT Age
>    In an equation for ‛it’: it = GHC.NT.castNT GADT :: GADT Age
> 
> 
> What is still missing
> =====================
> 
> * Good error messages (see above)
> * Checking if all involved data constructors are in scope
> * Marking these data constructors as used (to avoid unused import 
>   warnings)
> * Prevent the user from writing NT instances himself.
> * Code documentation
> * User documentation
> * Tests.
> * More testing, especially with weird types and advanced type system 
>   features, e.g. type families.
> 
> What needs more thought
> =======================
> 
> * How to handle recursive newtypes, such as
>   newtype Void = Void Void
>   or worse
>   newtype Foo a = Foo (Foo (a,a))?
>   With the current setup, which is equivalent to an instance
>   instance NT (Foo (a,a)) b => NT (Foo a) b
>   it will cause constraint checking to loop.
> 
>   I’m inclined to simply not create instances for recursive newtypes, 
>   or alternatively only in modules with UndecidableInstances turned on.
> 
> The code
> ========
> 
> The code can be reviewed at
> https://github.com/nomeata/ghc/compare/ntclass-clean
> with the corresponding ghc-prim changes at
> https://github.com/nomeata/packages-ghc-prim/compare/ntclass-clean
> 
> I followed the example of SingI and created a new constructor in data
> EvTerm for NT evidences. There are three kinds of evidence for NT t1 t2:
> One for t1 == t2, one for unfolding a newtype (at t1 or t2), and one if
> t1 and t2 have the same type constructor at the head. This corresponds
> to the the shapes of NT instances one would write by hand.
> 
> The evidence is created in TcInteract, in a function called by
> matchClassInst, and turned into Core by dsEvTerm in DsBinds.
> 
> Currently there is both a type constructor GHC.Types.EqR that boxes EqR#
> and is built-in, and a type class GHC.NT.NT, which has just one method
> of type EqR. This is because it seems to be quite tricky to create a
> built-in class in GHC.Prim, but also causes a bit of extra bookkeeping.
> I guess the final patch will somehow avoid this indirection.
> 
> Richard, can you have a look at my changes to
> compiler/types/Coercion.lhs, if they are sound? I found that there was a
> hardcoded role of Nominal where, with my code, also Representational
> could occur.
> 
> 
> Is this going in the right direction, both design and
> implementation-wise?
> 
> 
> 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
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs

More information about the ghc-devs mailing list