[Haskell-cafe] Type family signatures
dave at zednenem.com
Fri Aug 14 11:32:56 EDT 2009
On Fri, Aug 14, 2009 at 11:06 AM, Thomas van Noort<thomas at cs.ru.nl> wrote:
> 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:
> 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 <dave at zednenem.com>
More information about the Haskell-Cafe