Exposing newtype coercions to Haskell

[Simon Peyton-Jones]

|  - 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:

Excellent point, Richard.

Running example
	deriving instance (NT a b) => NT [a] [b]

The whole point of what Joachim is studying is making it possible for the programmer to generate representational equalities, and use them with ntCast.  
	ntCast :: NT a b -> a -> b
(I'm ignoring the question about the final names for things.)  So we can't use the new (:=:) type because it wraps nominal equality.  To work with the approach Joachim sketches we'd need:

	data REq a b where
 	   REq :: (a ~R# b) -> NT a b

which wraps a *representational* equality.  But as you say, we weren't planning to abstract over representational equalities at all in FC, so that would bring up a range of questions.   One possible response is that we *should* allow abstraction over ~R; there's nothing wrong with it in principle, it's just that we didn't think it was necessary.  The main cost is that we'd need an unboxed type constructor ~R# (to match the existing ~# which is really nominal equalty ~N#), and a boxed one (called NT above) to match (:=:).

So the above instance declaration would somehow generate

	ntList :: REq a b -> REq [a] [b]
	ntList (REq (c :: a  ~R#  b)) = REq ([c] :: [a]  ~R#  [b])

You mention a "magical" approach, but I'm not sure what that is.

The question of how to represent all this in HsSyn, to communicate between TcDeriv and TcInstDcls, is a somewhat separate matter.  We can solve that in several ways.  But first we need be sure what the FC story is.

My instinct is for a 2-param type class.  For 'newtype Age = MkAge Int', it seems odd to have both the newtype axiom
	axiom ax4 : Age ~ Int
and a type family axiom
	axiom ax5 Concrete Age ~ Int

Simon

 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
|  
|  _______________________________________________
|  ghc-devs mailing list
|  ghc-devs at haskell.org
|  http://www.haskell.org/mailman/listinfo/ghc-devs