default roles

[Ganesh Sittampalam]

I think it would be ok to expect the constructors to be visible, even
though it might need to a lot being needed.

BTW I think you might need S1 visible as well otherwise how would you
convert (S1 True :: S Bool Int) into (S1 True :: S Bool Age)?

If you don't derive the role from constructor visibility then I think it
should fail-safe and default to the nominal role - valid Haskell 2010
code shouldn't be exposed to an abstraction leak just because it's GHC
compiling it.


On 08/10/2013 14:23, Richard Eisenberg wrote:
> Pedro is suggesting a way for a Haskell type-level program to gain
> access to role information. This might indeed be useful, but it
> doesn't seem terribly related to the problem of defaults /
> abstraction. The problem has to do with definitions like these:
>
> > module A where
> > data S a b = S1 a | S2 b
> > data T a b = MkT (S a b)
>
> > module B where
> > import A ( {- what goes here? -} )
> >
> > class C a where
> >   mkT :: T Bool a
> >
> > instance C Int where ...
> > newtype Age = MkAge Int deriving C
>
> What constructors do we need in order to convert the (C Int) instance
> to (C Age) by hand? To me, it looks like we need MkT and S2, but not
> S1. Yet, this is not obvious and seems to be quite confusing.
>
> I hope this helps understanding the issue!
> Richard
>
> On Oct 8, 2013, at 4:01 AM, Jos? Pedro Magalh?es <dreixel at gmail.com
> <mailto:dreixel at gmail.com>> wrote:
>
>> Hi,
>>
>> On Tue, Oct 8, 2013 at 3:21 AM, Richard Eisenberg <eir at cis.upenn.edu
>> <mailto: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
>>
>>
>

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