Exposing newtype coercions to Haskell

[Simon Peyton-Jones]

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 at haskell.org] On Behalf Of Richard
|  Eisenberg
|  Sent: 23 July 2013 09:51
|  To: Joachim Breitner
|  Cc: ghc-devs at 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 at haskell.org
|  > http://www.haskell.org/mailman/listinfo/ghc-devs
|  
|  _______________________________________________
|  ghc-devs mailing list
|  ghc-devs at haskell.org
|  http://www.haskell.org/mailman/listinfo/ghc-devs