[Haskell-cafe] Type families and kind signatures

[David Menendez]

2009/4/2 Louis Wasserman <wasserman.louis at gmail.com>:
> Mkay.  One more quick thing -- the wiki demonstrates a place where the
> original attempt worked, with a data family instead. (That is, replacing
> 'type' with 'data' and adjusting the instance makes this program compile
> immediately.)
> a) Is there a type-hackery reason this is different from data families?

It's not type hackery. Data families are different from type families,
and the syntax for declaring instances of higher-kinded families is a
consequence of those differences.

An instance of a data family is a new type constructor, so you have to
provide the additional arguments in order to declare the data
constructors.

data family Foo a :: * -> *
data instance Foo Bool a = FB a a
-- Foo Bool has kind * -> *, like [], so I could make it a Functor

Instance of type families are always pre-existing type constructors.

type family Bar a :: * -> *  -- Bar a must equal something of kind * -> *
type instance Bar () = Maybe

> b) Is there a reason this isn't made a lot clearer in the documentation?
>  GHC's docs say that higher-order type families can be declared with kind
> signatures, but never gives any examples -- which would make it a lot
> clearer that the below program doesn't work.

Here's a higher-kinded type family I've used.

type family Sig t :: * -> *

class (Traversable (Sig t)) => Recursive t where
    roll :: Sig t t -> t
    unroll :: t -> Sig t t


The Traversable context wouldn't be valid if I had declared Sig t a ::
*, because type families must always be fully applied.


The difference is analogous to the difference between

type M0 a = StateT Int IO a
type M1   = StateT Int IO

Since type synonyms (like type and data families) must always be fully
applied, you can use M1 in places where you can't use M0, even though
they're effectively the same thing.

foo :: ErrorT String M1 a -- valid
bar :: ErrorT String M0 a -- not valid



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