Yes, that's what I got from Joachim's response to my design, also. My only other thought is to have some way to store an _axiom_, instead of an R coercion. But, that seems very fishy and wrong-headed. So, I guess we'll have to have ~R#. I'm tempted to use "~R#" as its name, to make it impossible to write in Haskell code. Would there be any problems with this? I'll go ahead and include the new coercion form when I commit roles.
Richard On Jul 23, 2013, at 7:46 PM, Simon Peyton-Jones wrote: > 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-boun...@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 > _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
