I thought about the design you suggest below, but rejected it because I don't see how to do lifting -- which is really the whole point! In particular, what are you going to write for ntList :: NT a b -> NT [a] [b] ntList (MkNT castNT uncastNT) = MkNT ??? ??? For lists you could write (fmap castNT), but the whole point of this exercise is not to write that -- and the type might not be an instance of Functor. I'm thinking we need (~R#) as a type constructor. Simon | -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Richard | Eisenberg | Sent: 23 July 2013 09:51 | To: Joachim Breitner | Cc: ghc-devs@haskell.org | Subject: Re: Exposing newtype coercions to Haskell | | A few responses: | | - As Simon said, there is no great reason we don't have ~R# in Core. | It's just that we looked through GHC and, without newtype coercions, | there is no need for ~R#, so we opted not to include it. I'm still not | convinced we need it for newtype coercions, though. What if we have this | in Core? | | > class NT a b = MkNT { castNT :: a -> b ; uncastNT :: b -> a } | > NTCo:Age :: Age ~R# Int -- see [1] | > NTAgeInst :: NT Age Int | > NTAgeInst = MkNT { castNT = \(a :: Age). a |> NTCo:Age ; uncastNT = \(x | > :: Int). x |> sym NTCo:Age } | | [1]: We still do have representational coercions, even though it would | be bogus to extract their type, as the type constructor ~R# does not | exist. But, coercionKind, which returns the two coerced types, and the | new coercionRole (which would return Representational in this case) work | just fine. | | Here, we don't need to abstract over ~R#, by just referring to the | global axiom directly. Does this compose well? I think so; you'll just | have to inline all of the coercions. But, the coercions won't ever get | too big, as they will always mirror exactly the structure of the types | being coerced. Simon, this is the sort of "magic" I was thinking of, | magical because I can't imagine a way this could be produced from an | HsExpr. | | Also, nice example of how the one-parameter design might aid the | programmer. I think that thinking about the base case is also | productive, but I don't have a clear enough opinion to express on that | front. | | Richard | | On 2013-07-23 08:21, Joachim Breitner wrote: | > Hi Richard and Simon, | > | > thanks for your detailed notes. | > | > Am Montag, den 22.07.2013, 17:01 +0100 schrieb Richard Eisenberg: | > | >> - 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 ...". | > | > My plan was to make all checks (constructors in scope; IsNT classes for | > all data constructor arguments present) in TcDeriv, so you get nice | > error messages. If it turns out that the actual coercion can only be | > generated in a later pass, then it the checks just need to be strong | > enough to make that pass always succeed. | > | >> - 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. | > | > I know; I was just using them until representational equality is in and | > plan to switch then. | > | >> (Nominal coercions correspond to the "C" coercions from this paper) | > | > I got confused by C and T in my previous mails. In any case, I am only | > concerned with representational equality (T, it seems) for this | > project. | > | >> 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. | > | > Hmm, I must admit I was assuming that once the roles implementation is | > in there will be ~# and ~#/T (or ~R#, which is a less-easy-to-confuse | > moniker) available in Core. | > | > | >> 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! | > | > Exactly. But it is also the reason why we are aiming for deriving | > classes (and not NT values), because it is already an established way | > of | > having the compiler generate code for you. | > | > | >> - I prefer the two-parameter class over a one-parameter, as it seems | >> more flexible. | > | > Thanks for spotting the phantom type replacing example, which is a | > features I’d also like to have. The type family was just a quick idea | > (and it would be neat to be able to ask GHCi via ":kind! (Concrete t)" | > what t looks like with all newtypes unfolded), but it’s not worth the | > loss of flexibility. | > | > | > In some cases, the type family might require less type annotations. | > Consider | > newtype Age = Age Int | > newtype NT1 = NT1 Int | > newtype NT2 = NT2 Int | > | > myCast :: Either NT1 Age -> Either NT2 Age | > myCast = castNT . uncastNT | > | > With two parameters, GHC will not know whether it should cast via | > "Either Int Age" or "Either Int Int", while with a type family there | > will be only one choice, "Concrete (Either NT1 Age) = Either Int Int". | > In general, castNT . uncastNT would have the nice type | > castNT . uncastNT :: Concrete a ~ Concrete b => a -> b | > which plainly expresses „Cast between any to values who have the same | > concrete representation.“. Just as a side remark in case this comes up | > later again. | > | > | > | > BTW, what should the base-case be? I believe most user-friendly is a | > least-specific class | > instance IsNT a a | > so that the cast "Either Age a -> Either Int a" is possible. Or are | > overlapping instances too bad and the user should derive instances for | > all non-container non-newtype types himself: | > instance IsNT Int Int .... | > | > | > Am Dienstag, den 23.07.2013, 05:23 +0000 schrieb Simon Peyton-Jones: | >> 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. | > | > For now what I am doing is that in TcDeriv, I am implementing the | > method | > with a value "unfinishedNTInstance :: a" which I am then replacing in a | > always-run simplCore pass with the real implementation in Core. It is a | > work-around that lets me explore the design-space and implementation | > issues without having to rewire GHC. | > | > 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