default roles

[Richard Eisenberg]

Perhaps I can spot the source of the confusion: there seem to be 2 different conversations going on here!

1: How to fit roles in with the ability to declare a datatype to be abstract. Should a library author be required to use a role annotation to make an abstract datatype, or should a library author be required to use a role annotation to allow GND with a datatype?

2: Some form of role abstraction, where an argument to a type parameter might get a representational role, depending on the role of some other variable. Using typeclasses is the current proposal for how to do this, and it in migmit's email below. Pedro also suggests a type families approach.


My initial email was seeking advice on issue #1.

As for #2: Using typeclasses here might be a decent surface syntax for the feature of role abstraction, but the automatic generation of instances, etc., would seem to require deep and pervasive magic under the hood. Essentially, every type and type variable would need to be annotated with both a kind and a role, significantly complicating GHC's type system. The question would be whether or not this upfront and ongoing investment is worth it.

Thanks,
Richard

On Oct 8, 2013, at 10:49 AM, Miguel <migmit at gmail.com> wrote:

> I don't understand it either.
> 
> Type family solution, however, seems wrong. See, if we, somehow, make something nominal when it has to be representational ? well, some code won't compile, but nothing really bad happens. If, on the other hand, we by some miracle make something representational when in should be nominal ? we can get a runtime error. It seems to be very similar to how type classes work, with "nominal" being the default, and "representational" a type class.
> 
> Consider, for example, the "Tricky" example from the slides, slightly changed:
> 
> data Tricky2 a b c = MkTricky2 (a c) (b c)
> 
> Currently parameter c would be nominal. I suggest that it should be representational if and only if it's representational for BOTH a and b. WIth type classes it would be very simple:
> 
> instance (HasRepresentationalParameter a, HasRepresentationalParameter b) => HasRepresentationalParameter (Tricky2 a b)
> 
> With type families... well, apparently I don't have enough milliolegs to figure out how to do it.
> 
> 
> On Tue, Oct 8, 2013 at 12:01 PM, Jos? Pedro Magalh?es <dreixel at gmail.com> wrote:
> Hi,
> 
> On Tue, Oct 8, 2013 at 3:21 AM, Richard Eisenberg <eir at cis.upenn.edu> wrote:
> We considered this for a while, but it led to a strange design -- to do it right, you would have to import all constructors for all datatypes *recursively* out to the leaves, starting at the datatypes mentioned in the class for which you wanted to use GND. This would mean potentially a whole lot of imports for symbols not actually used in the text of a program.
> 
> I'm not sure I understand why constructors are involved in this. Wouldn't something like
> the following potentially be useful?
> 
> data Role = Nominal | Representational | Phantom | Fun Role Role
> 
> type family HasRole (t :: k) :: Role
> 
> data MyData a b = MyData a
> data MyGADT a b where MyGADT :: MyGADT a Int
> 
> type instance HasRole MyData      = Fun Representational Phantom
> type instance HasRole MyGADT      = Fun Representational Nominal
> type instance HasRole Traversable = Nominal
> 
> HasRole instances would be automatically given by GHC.
> 
> 
> Cheers,
> Pedro
> 
> 
> 
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> 
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20131008/5c20d1fd/attachment.html>