Re: 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@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