We need to add role annotations for 7.8

[Edward Kmett]

This puts the constraint on the wrong thing.

I did argue for a pragma-like syntax for the annotations when they were
first proposed, as the need for library authors to hide these behind CPP
pragmas bothers me a great deal, but I think for better or worse that
syntax decision is largely behind us.



A type-class driven approach does have some promise, but that said, it
can't look like what you've written.

What you've written:

data Nominal k => Map k a

is saying something about the argument k, not about if you can turn
Map kinto Map
k', which is actually about Map, k is just along for the ride.

Really what we're talking about is that the next argument is
representational as applied. Also, the right 'open world' version would be
to talk about it as classes would be:

class Representational t where
  rep :: Coercion a b -> Coercion (t a) (t b)

class Representational t => Phantom t where
  phantom :: Coercion (t a) (t b)

With "Nominal" simply being the absence of either of those instances.

data Map k a

would need

instance Representational (Map k)

since the 'a' can be coerced as it has a representational role.

instance Representational (->)
instance Representational ((->) a)

But there are actually still open issues I don't know how to solve, even
with this approach.

-Edward


On Mon, Mar 24, 2014 at 11:36 AM, Mark Lentczner
<mark.lentczner at gmail.com>wrote:

> Again, sorry for the 11:59 meddling....
>
> The syntax of role annotations is very heavy weight, and requires lots of
> CPP where there wasn't need before.  Two thoughts:
>
> 1) Couldn't we do something like use "cue" type constraints? For example,
> assuming the default is representational, and that phantom can just be
> inferred, all we need is a way to indicate nominal:
>
> data (Nominal k) => Map k v = ...
>
>
> This could then probably be easily made to compile in other compilers with
> some null library implementation of Nominal
>
> 2) An alternative to the above. We generally frown on constraints in a
> data / newtype declaration, but perhaps this is exactly the case for them,
> whereby we can now do away with the type role syntax: We can infer nominal
> if there are *any* constraints on a type parameter, *representational* if
> there are none, and *phantom *if there are no mentions in the right hand
> side:
>
> data (Eq k) => Map k v = ...
>
>
> This seems even nicer and just works with all compilers... but perhaps I'm
> missing something. (Yes, I imagine there are type constraints that
> shouldn't force nominal, but perhaps not worth worrying about?)
>
>
> Mind you, this all just about syntax... the issue of what is the
> implication for libraries of the default being representational is still at
> hand.
> ​
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140324/c8c84f93/attachment-0001.html>