Exposing newtype coercions to Haskell
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 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.
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
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.
| 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
More information about the ghc-devs