A TypeFamilies Primer

TypeFamilies is a GHC extension that lets you create formerly-impossible abstractions in a very straightforward way. It took me several tries before they clicked for me though, so this is the introduction to TypeFamilies that I wish I had read first (although I just found Brent Yorgey’s, which would have done the trick).

I’m treating the subject very narrowly for most of this post, and try to round things out a little at the very end.

Primal Ignorance

If this isn’t the first thing you’ve read about TypeFamilies, it might be helpful to forget a few things. The question “what precisely is a type family?” isn’t going to be very helpful; in general, the terminology for the constellation of constructions that TypeFamilies gives you is a huge mess, with multiple partially-overlapping terms in the wild, none of which are helpful for developing an intuition about what all of this is about.

I also found various analogies I’d read to be useless, so forget those too.

Type synonyms as type-level functions

Consider the familiar type synonym:

type PairOf a = (a,a)

Normally this is presented as syntactic sugar, with little to do with the type system.

A more interesting way of thinking about PairOf is as a function (as suggested by the =), where evaluation involves substituting occurrences of the left hand side (LHS) with the right, in the usual way. These functions are evaluated in your type signatures at compile time.

The analogous regular term-level function would of course be:

pairOf a = (a,a)

Simple enough. Now let’s think about a simple term-level function, and see what an analogous type-level type synonym/function might look like:

last (a: [])     = a
last (a: (b:bs)) = last (b:bs)

For our type-level Last we need something like lists at the type-level, so we’ll use the common nested tuple representation of (,) as cons and () as the empty list, e.g.:

x :: (Int,(Int,(Int,())))  -- like [1,2,3]

Hopefully I didn’t just lose you. Remember for now we just care about using this list-like tuple thing in our type signatures.

If you were to charge ahead and try to define Last using type synonyms treated as full blown functions, you might come up with:

-- this isn't okay:
type Last (a, ())     = a
type Last (a, (b,bs)) = Last (b,bs)

Unfortunately the compiler will laugh at you. Type synonyms can only have abstract variable arguments on the LHS where above we have tried to deconstruct them using pattern matching, and to define a different RHS for both cases. Further we’ve made the definition recursive. None of that is okay.

In fact the humble type synonym is only a very simple sort of function (a natural transformation or something close) which is very easy to evaluate, but also very limited.

Finally, Enter TypeFamilies

The TypeFamilies extension lets us define Last successfully almost exactly as we did above.

{-# LANGUAGE TypeFamilies #-}

-- we have to "declare" `Last` separately, and the "family"
-- here distinguishes the syntax from a normal type synonym:
type family   Last l  

-- ...and then can define our "cases":
type instance Last (a,())     = a
type instance Last (a,(b,bs)) = Last (b,bs)

At this point when the type-checker sees Last (a,(b,bs)) in a type signature it will replace it with Last (b,bs), and continue until all of these “type functions” are evaluated. I may be fudging things a bit but that’s the general idea.

Since these are a more general sort of type function, they can even be used to replace traditional type synonyms:

type family   PairOf a
type instance PairOf a = (a,a)

But what is that good for?

It would be neat to be able to work with “lists” that look like e.g. (1,('a',("hello",()))); they are heterogeneous, operations like head would be type-safe, etc. So imagine we want to define a last on types of this list-like tuple sort of data.

What would the type of last look like? We know it has to be polymorphic, since its arguments might look like () or (1,(2,())), different types of course. So we’ll need a type-class (and a couple other standard extensions):

{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
class LastOfTupleList l where
    last' :: l -> Last l      -- < we use our `Last` type function

Our instances are trivial:

instance LastOfTupleList (a,()) where
    last' (a,()) = a  -- < the type-checker can see that, indeed, `a`
                      --   is equal to `Last (a,())`

instance (LastOfTupleList (b, bs))=> LastOfTupleList (a,(b,bs)) where
    last' (a,(b,bs)) = last' (b,bs)

Letting us do:

>>> last' (1,(2,()))
2
>>> last' (1,('a',("hello",())))
"hello"

Notice how our instances of Last and last have almost the same structure; this is very common.

Functions… but open!

If you’re a programmer type you were probably irritated by my initial clumsy definition of last; why not:

last (a:[]) = a
last (a:as) = last as -- `as` matches whatever can fall through the pattern
                      -- above; in this case only non-empty lists

Well, I was being sneaky because the type-level analogue isn’t allowed!

type instance Last (a,()) = a
type instance Last (a,as) = Last as -- BAD!

This is because unlike functions, type families are open meaning, like typeclasses, a new instance can be added at any moment. Therefore there’s no way to define a “default” instance to use after all other matches fail, you simply get illegal overlapping synonym instances such as the one above; the order in which we defined the two doesn’t matter.

For some use cases this is what we need, for others (such as our last') we’d really prefer that type synonym families be closed so that we can pattern match in the usual way. This feature is apparently coming soon.

Other details

That should give you an intuition. At this point you might want to stop and read through the following documentation, or continue reading below before coming back to these links for a more refined understanding and additional details:

• Type-families at haskellwiki
• GHC docs

Associated type synonyms

Since we so often define define a type class in terms of one or more type families, we’re given a simplified syntax for combining them in one place.

class LastOfTupleList l  where
    type Last l        -- an *associated* type family
    last' :: l -> Last l

instance LastOfTupleList (a,()) where
    type Last (a,()) = a
    last' (a,()) = a

When people say “associated types” they mean type functions that are associated with a typeclass using the syntax above.

Injectivity

Type synonym family instances are said to be not injective, meaning two different type functions can map to the same type on the RHS, e.g.

type instance F Int  = Bool
type instance F Char = Bool

It’s easy to forget this when building new abstractions, and assume that the typechecker will infer from the RHS (e.g. Bool above) the argument passed in to the type function (Int or Char).

Data families

I’ve completely focused on the type synonym flavor of TypeFamilies above, but there is also a data/newtype flavor in which, for each instance definition the RHS is a brand new type declaration, rather than mapping to an existing type

-- from http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/type-families.html
data family T a
data    instance T Int  = T1 Int | T2 Bool -- new constructors T1 and T2 defined here
newtype instance T Char = TC Bool

Because each instance maps to a unique type, data families are injective allowing the type checker to infer the LHS of the equation knowing the right.

More other things

• TypeFamilies provides the syntax a ~ b to indicate type equality constraints; this is especially useful with type synonym functions, but can be useful on its own as well.
• kind signatures are required for type functions on types taking arguments, e.g. Maybe