Exposing newtype coercions to Haskell

[Richard Eisenberg]

Hi Joachim,

A few responses to your plan:

- I think you *do* want HsExprs not CoreExprs. Though I haven't worked 
much in TcDeriv myself, I imagine everything uses HsExprs so that they 
can be type-checked. This allows nice error messages to be reported at 
the site of a user's "deriving instance IsNT ...".

- The type that you've called NT below will soon exist in base, in the 
module Data.Type.Equality. See 
http://ghc.haskell.org/trac/ghc/wiki/TypeLevelReasoning  That 
implementation ran into a little bump this morning, but it should be 
pushed within 24 hours.

- But, there's a wrinkle here. The (~#) type, along with (~) and (:=:) 
(the last is from the soon-to-be Data.Type.Equality), all work over 
so-called *nominal* coercions. (Nominal coercions correspond to the "C" 
coercions from this paper: 
http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf  I hope 
to have an implementation of the ideas in that paper available later 
this week. There are some user-facing features, about which there will 
be wiki page some point quite soon.) A nominal coercion should only 
exist between two types that are nominally equal. Under this definition 
Age and Int are not nominally equal, because they have different names. 
The other interesting equality is "representational". This equality 
considers Age and Int to be representationally equal, because they have 
the same representation. A key point of newtype coercions is that they 
work over representational equality, not only nominal equality. Working 
over representational equality is what makes them interesting and 
useful. Currently, there is no way to abstract over representational 
coercions -- that is, there
is no way to store one, say in a GADT or other Haskelly data type. Of 
course, a data structure within GHC can store a representational 
coercion; you just can't have one be the payload of an Id, say. So, that 
means that the implementation of newtype coercions may have to be a 
little more magical than the design you're writing. Or, it's possible 
that we could add abstraction over representational coercions, but I 
prefer the magical approach, because I don't see a general need for the 
ability to abstract.

Now that I think of it, you may need to generalize the deriving 
mechanism a bit. All current "deriving"s generate code that the user 
could write. (Typeable is something of an exception here.) Here, the 
generated code is something that a user can not write. Maybe that's why 
you wanted CoreExprs in the first place!

Somewhat separately:

- I prefer the two-parameter class over a one-parameter, as it seems 
more flexible. If the two-parameter version (without any dependencies 
between the two parameters) hinders type inference, users can define an 
explicitly-typed wrapper. Why do I want this flexibility? Because, once 
roles are done, the following should be possible:

> data Foo a = MkFoo
> deriving instance IsNT (Foo a) (Foo b)

Note that `a` is a phantom parameter here, and, yes, I meant `data` 
there, not newtype. In other news, I would prefer the name not to 
mention newtypes, because I think the mechanism is somewhat stronger 
than just newtype coercions.

Richard

On 2013-07-22 13:06, Joachim Breitner wrote:
> Hi,
> 
> as discussed, I started to work basing the newtype coercions on classes
> instead of types. I poked around the code, especially TcDeriv.lhs, and 
> I
> have a few questions:
> 
> For my current design I wanted to have
> 
>         class IsNT a where
>         	type Concrete a
>         	coercion :: a ~# Concrete a
> 
> but that does not work, as methods seem to need to have a boxed type.
> Using "a ~ Concrete a" does not work as well, as that has kind
> Constraint. So I wrapped ~# myself and created:
> 
>         data NT a b = NT ((~#) a b)
>         class IsNT a where
>             type Concrete a
>             coercion :: NT a (Concrete a)
> 
> with only IsNT (I’ll think more about the name ;-)) and probably
> Concrete exposed; not or coercion. The interface would then be 
> functions
> 
>         castNT :: IsNT a => Concrete a -> a
>         uncastNT :: IsNT a => a -> Concrete a
> 
> Now we want the user to be able to specify
> 
>         deriving instance IsNT Age -- with Concrete Age = Int
>         deriving instance IsNT a => IsNT [a] -- with Concrete [a] = 
> [Concrete a]
>         deriving instance IsNT v => IsNT (Map k v) -- dito
> and probably also
>         deriving instance IsNT Int -- with Concrete Int = Int
> for all non-newtypes.
> 
> After adding the definitions to ghc-prim and extending PrelNames I 
> tried
> to make the deriving code, starting with the last examle (IsNT Int).
> There, the generated code should be something like
> 
>         instance IsNT Int where
>         	type Concrete Int = Int
>         	coercion = NT (refl Int)
> 
> But here I am stuck: The deriving code mechanism expects me to give the
> method definitions as HsExpr, but I’d like to generate Core here. How
> can I achieve that, or what other options do I have?
> 
> (Of course this will need further adjustments when Richard’s role code
> is in.)
> 
> (If there is a reason to go back to the two parameter type class "NT a
> b", no problem, but the problem of HsExpr vs. CoreExpr would still
> remain.)
> 
> Greetings,
> Joachim
> 
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs