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 <dave@zednenem.com> wrote:
2009/4/2 Louis Wasserman <wasserman.louis@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@zednenem.com>
<http://www.eyrie.org/~zednenem/>