On Fri, Aug 14, 2009 at 11:06 AM, Thomas van Noort
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
--
Dave Menendez