Typed type-level programming in Haskell, part II: type families

In my previous post, we saw how multi-parameter type classes with functional dependencies in Haskell allow us to do type-level programming in a logic programming style. (If you’re not clear on why this corresponds to a logic programming style, see the ensuing discussion on reddit, where others explained it much better than I did in my post.)

However, MPTCs + FDs weren’t the last word on type-level programming. In 2007, along came type families.

Essentially, type families allow us to write functions on types. For example, here’s how we would implement the same Plus function from the last post, this time using type families:

  data Z
  data S n

  type family Plus m n :: *
  type instance Plus Z n = n
  type instance Plus (S m) n = S (Plus m n)

This says that for any types m and n, Plus m n is type of kind *. But it isn’t a new type, it’s just an alias for some existing type. It’s instructive to think carefully about the difference between this and type synonyms. After all, using a type synonym declaration, we can already make Plus m n an alias for some existing type, right?

Well, yes, but the difference is that a type synonym doesn’t get to look at its arguments. The technical term for this is that type synonyms must be parametric. So, for example, we can say

  type Foo m n = [(m, Maybe n)]

which defines the type synonym Foo uniformly for all arguments m and n, but using only type synonyms we cannot say

  type Foo m Int = [m]
  type Foo m Char = Maybe m

where Foo acts differently depending on what its second argument is. However, this is precisely what type families allow us to do — to declare type synonyms that do pattern-matching on their type arguments. Looking back at the Plus example above, we can see that it evaluates to different types depending on whether its first argument is Z or S n. Notice also that it is essentially identical to the way we would implement addition on regular value-level natural numbers, using pattern-matching on the first argument and a recursive call in the successor case:

  data Nat = Z | S Nat

  plus :: Nat -> Nat -> Nat
  plus Z n = n
  plus (S m) n = S (plus m n)

Let’s check that Plus works as advertised:

  *Main> :t undefined :: Plus (S Z) (S Z)
  undefined :: Plus (S Z) (S Z) :: Plus (S Z) (S Z)

Well, unfortunately, as a minor technical point, we can see from the above that ghci doesn’t expand the type family for us. The only way I currently know how to force it to expand the type family is to generate a suitable error message:

  *Main> undefined :: Plus (S Z) (S Z)

  ...No instance for (Show (S (S Z)))...

This is ugly, but it works: S (S Z) is the reduced form of Plus (S Z) (S Z).

So type families let us program in a functional style. This is nice — I daresay most Haskell programmers will be more comfortable only having to use a single coding style for both the value level and the type level. There are a few cases where a logic programming style can be quite convenient (for example, with an additional functional dependency we can use the Plus type class from the last post to compute both addition and subtraction), but in my opinion, the functional style is a huge win in most cases. (And, don’t worry, FDs and TFs are equivalent in expressiveness.)

Of course, there is a lot more to all of this; for example, I haven’t even mentioned data families or associated types. For more, I recommend reading the excellent tutorial by Oleg Kiselyov, Ken Shan, and Simon Peyton Jones, or the page on the GHC wiki. For full technical details, you can look at the System FC paper.

Nothing is ever perfect, though — in my next post, I’ll explain what type families still leave to be desired, and what we’re doing to improve things.