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 <drei...@gmail.com
> <mailto:drei...@gmail.com>> wrote:
>
>> Hi,
>>
>> On Tue, Oct 8, 2013 at 3:21 AM, Richard Eisenberg <e...@cis.upenn.edu
>> <mailto:e...@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@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
