Exposing newtype coercions to Haskell

[Simon Peyton-Jones]

|  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.

Sounds ok to me.

Simon

|  -----Original Message-----
|  From: Richard Eisenberg [mailto:eir at cis.upenn.edu]
|  Sent: 23 July 2013 23:12
|  To: Simon Peyton-Jones
|  Cc: Joachim Breitner; ghc-devs at haskell.org
|  Subject: Re: Exposing newtype coercions to Haskell
|  
|  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-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
|  >
|