Exposing newtype coercions to Haskell

[Richard Eisenberg]

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