[Haskell-cafe] Type families and kind signatures
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Thu Apr 2 20:43:57 EDT 2009
> 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
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.
> On Thu, Apr 2, 2009 at 12:47 PM, David Menendez <dave at zednenem.com>
> 2009/4/2 Louis Wasserman <wasserman.louis at gmail.com>:
> > Mkay. One more quick thing -- the wiki demonstrates a place where
> > original attempt worked, with a data family instead. (That is,
> > 'type' with 'data' and adjusting the instance makes this program
> > immediately.)
> > a) Is there a type-hackery reason this is different from data
> 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
> 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
> > 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
> > 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>
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe