Re: [Haskell-cafe] Type families and kind signatures

Mkay. I get it now. I was under the impression that, essentially, a data family was precisely equivalent to a type family aliasing to a separately declared datatype. One more question: is there any way to get the low overhead of newtypes for particular instances of a data family? Is this impossible? That is, is there any way to do something like data family Foo a data instance Foo Int = Bar Int -- Bar is actually a newtype Louis Wasserman wasserman.louis@gmail.com On Thu, Apr 2, 2009 at 12:47 PM, David Menendez wrote:

2009/4/2 Louis Wasserman :

...

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 <http://www.eyrie.org/~zednenem/ http://www.eyrie.org/%7Ezednenem/>