Exposing newtype coercions to Haskell
Simon PeytonJones
simonpj at microsoft.com
Tue Jul 23 07:23:16 CEST 2013
  But, there's a wrinkle here. The (~#) type, along with (~) and (:=:)
 (the last is from the soontobe Data.Type.Equality), all work over
 socalled *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 2param 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 twoparameter class over a oneparameter, as it seems
 more flexible. If the twoparameter version (without any dependencies
 between the two parameters) hinders type inference, users can define an
 explicitlytyped 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 20130722 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 nonnewtypes.
 >
 > After adding the definitions to ghcprim 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
 >
 > _______________________________________________
 > ghcdevs mailing list
 > ghcdevs at haskell.org
 > http://www.haskell.org/mailman/listinfo/ghcdevs

 _______________________________________________
 ghcdevs mailing list
 ghcdevs at haskell.org
 http://www.haskell.org/mailman/listinfo/ghcdevs
More information about the ghcdevs
mailing list