[Haskell-cafe] Type family signatures
westondan at imageworks.com
Fri Aug 14 15:03:48 EDT 2009
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:
>> 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
More information about the Haskell-Cafe