default roles

Richard Eisenberg eir
Tue Oct 8 13:23:56 UTC 2013

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!

On Oct 8, 2013, at 4:01 AM, Jos? Pedro Magalh?es <dreixel at> wrote:

> Hi,
> On Tue, Oct 8, 2013 at 3:21 AM, Richard Eisenberg <eir at> 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: <>

More information about the Glasgow-haskell-users mailing list