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