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/

Louis Wasserman:

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.

No, they are not equivalent. You can see that as follows. Assume, data family T a type family S a Now, given `T a ~ T b', we know that `a ~ b'. (We call this implication "decomposition".) In contrast, given `S a ~ S b' we do *not* know whether `a ~ b'. Why not? Consider the instances type instance S Int = Bool type instance S Float = Bool Clearly, `S Int ~ S Float', but surely not `Int ~ Float'. So, decomposition does not hold for type synonym families, but it does hold for data families. This is actually, not really a property of type *families* alone. It already distinguishes vanilla data types from vanilla type synonyms. We know, say, that if `Maybe a ~ Maybe b', then `a ~ b'. However, given type Const a = Int we have `Const Int ~ Const Float' (and still not `Int ~ Float'). Definitions, such as that of `Const', are rarely used, which is why this issue doesn't come up much until you use type families.

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

You can use newtype instance Foo Int = MkFoo Int So, the instances of a data family can be data or newtype instances., and you can freely mix them. Manuel

...

Mkay. One more quick thing -- the wiki demonstrates a place where

On Thu, Apr 2, 2009 at 12:47 PM, David Menendez wrote: 2009/4/2 Louis Wasserman : 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/

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe