Exposing newtype coercions to Haskell

[Joachim Breitner]

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


-- 
Joachim “nomeata” Breitner
  mail at joachim-breitner.de • http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130723/d91726e4/attachment.pgp>