[Haskell-cafe] Type family signatures

[David Menendez]

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

-- 
Dave Menendez <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>