[Haskell-cafe] Type family signatures

[Dan Weston]

But presumably he can use a data family instead of a type family to 
restore injectivity, at the cost of adding an extra wrapped bottom value 
and one more layer of value constructor?

David Menendez wrote:
> On Fri, Aug 14, 2009 at 11:06 AM, Thomas van Noort<thomas at cs.ru.nl> wrote:
>> Hello,
>>
>> I have a question regarding type family signatures. Consider the following
>> type family:
>>
>>  type family Fam a :: *
>>
>> Then I define a GADT that takes such a value and wraps it:
>>
>>  data GADT :: * -> * where
>>    GADT :: a -> Fam a -> GADT (Fam a)
>>
>> and an accompanying unwrapper:
>>
>>  unwrap :: GADT (Fam a) -> (a, Fam a)
>>  unwrap (GADT x y) = (x, y)
>>
>> When Fam is declared using the first notation,
>>
>>  type family Fam a :: *
>>
>> GHC HEAD gives the following error message:
>>
>>  Main.hs:9:21:
>>    Couldn't match expected type `a' against inferred type `a1'
>>      `a' is a rigid type variable bound by
>>          the type signature for `unwrap' at Main.hs:8:20
>>      `a1' is a rigid type variable bound by
>>           the constructor `GADT' at Main.hs:9:8
>>    In the expression: x
>>    In the expression: (x, y)
>>    In the definition of `unwrap': unwrap (GADT x y) = (x, y)
> 
> This is because type families are not injective. Nothing stops you
> from defining two instances such as,
> 
> type instance Fam Int = Bool
> type instance Fam Char = Bool
> 
> in which case a value of type GADT Bool is ambiguous. Does it contain
> an Int or a Char?
> 
>> However, when Fam is declared as (moving the a to the other side of the ::
>> and changing it into *),
>>
>>  type family Fam :: * -> *
>>
>> everything is ok. So, it seems to me that GHC HEAD considers both signatures
>> to be really different. However, I do not quite understand the semantic
>> difference in my example, other than that Fam needs to be fully satisfied in
>> its named type arguments. Note that GHC 6.10.3 does not accept the latter
>> signature for Fam since it requires at least one index for some reason,
>> that's why I'm using GHC HEAD.
> 
> A type family with no index is equivalent to a type synonym.
> 
> But in answer to your question, these signatures are very different.
> Consider these families.
> 
> type family Foo a b :: *
> type family Bar a :: * -> *
> 
> Foo is indexed by two parameters, but Bar is only indexed by one.
> 
> type instance Foo A B = X
> type instance Foo A C = X
> -- Foo a b ~ Foo a c does not imply b ~ c
> 
> type instance Bar A = []
> -- Bar a b ~ Bar a c does imply b ~ c
> 
> Bar returns a type constructor, so it can be used anywhere a type
> constructor of kind * -> * can be used.
> 
> foo :: (Functor (Foo a)) => ...   -- invalid
> bar :: (Functor (Bar a)) => ...   -- valid
>