Back to explicit Coercible instances?

[Iavor Diatchki]

Hello,


On Sat, Oct 12, 2013 at 5:23 AM, Joachim Breitner
<mail at joachim-breitner.de>wrote:

>
> > Moreover, I'm very keen to give a simple, precise answer to the question
> >       if s is coercible to t
> >       when is (T s) coercible to (T t)
> > I propose that the answer is given by precisely T's roles.  At the
> > moment I don't see why we would want to do anything more complicated.
>
> I’m not sure if „... if the roles allow it“ is any simpler than „if
> there is a Coercible instance for it“, and Haskell programmers might be
> happier if they can think in terms of type class instances without
> learning a new concept.
>

I like the `deriving Coercible` idea, it seems to fit quite naturally with
the rest of the language and does not require programmers to have to know
about roles.
We'd have to be careful that we use the instances consistently though, in
particular, I don't think we can just fall back to using roles behind the
scenes,
because the class mechanism is more general (unles we restrict it somehow).
 Here are some examples:

data T a = T
deriving instance Coercible (T Int) (T Char)
deriving instance Coercible (T Int) (T Bool)

This allows very precise control, but I don't think that we can express it
with roles.  Now consider another declaration like this:

data S a = S (T a)deriving Coercible

Here we'd need some cleverness to determine what instances to derive.

Another question is: are the instances going to be automatically symmetric,
or would one have to write two versions of each rule?
Using the previous example, would I have to also add:

deriving instance Coercible (T Char) (T Int)

This seems a bit tedious and not in the spirit of `Coercible`.  OTOH, if we
were to make `Coercable` automatically symmetric,
we'd have to make sure that the derived user instances are invertible.
 Consider for example:

deriving instance Eq a => Coercible (T a) (T b)

This allows coercing `T Int` to `T (Int -> Int)` but not the other way.

All in all, I like the `deriving Coercible` notation, but I think that we
should restrict it to something that essentially matches the `role`
mechanism under the hood (and get an error saying that we can't derive the
instance otherwise).
Here is a stab at the rules:
  * The head of the instance must be of the form: Coercible (T a1 a2 ...)
(T b1 b2 ...), where `T` is a concrete type, and the `as` and `bs` are
variables.
  * The only constraints in the context may be of the form `Coercible a1
b1`,  or `Coercible a2 b2`, etc...
  * There can be only one instance derived per type `T`

With these restrictions we essentially have another way to specify the
roles.  The role of the Nts parameter of `T` can be determined like this:

role aN bN
  | aN == bN   = Nominal
  | otherwise  = if context has Coercible aN bN then Representational else
Phantom

Hope this helps,
-Iavor
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20131012/57628364/attachment.html>