Typed type-level programming in Haskell, part I: functional dependencies

The other project I’m working on at MSR this summer is a bit more ambitious: our headline goal is to extend GHC to enable typed, functional, type-level programming. What’s that, you ask? Well, first, let me tell you a little story…

Once upon a time there was a lazy*, pure, functional programming language called Haskell. It was very careful to always keep its values and types strictly separated. So of course “type-level programming” was completely out of the question! …or was it?

In 1997, along came multi-parameter type classes, soon followed by functional dependencies. Suddenly, type-level programming became possible (and even fun and profitable, depending on your point of view). How did this work?

  data Z
  data S n

  class Plus m n r

  instance Plus Z n n
  instance (Plus m n r) => Plus (S m) n (S r)

This says that for any types m, n, and r, (Z,n,n) are in the Plus relation, and (S m, n, S r) are in the Plus relation whenever (m,n,r) are. We can load this into ghci (after enabling a few extensions, namely MultiParamTypeClasses, FlexibleInstances, and EmptyDataDecls), but unfortunately we can’t yet actually use the Plus relation to do any type-level computation:

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

We asked for the type of something which has type r, given that the relation Plus (S Z) (S Z) r holds – but notice that ghci was not willing to simplify that constraint at all. The reason is that type classes are open – there could be lots of instances of the form Plus (S Z) (S Z) r for many different types r, and ghci has no idea which one we might want.

To the rescue come functional dependencies, which let us specify that some type class parameters are determined by others – in other words, that the relation determined by a multi-parameter type class is actually a function.

  class Plus m n r | m n -> r
  instance Plus Z n n
  instance (Plus m n r) => Plus (S m) n (S r)

Here we’ve added the functional dependency m n -> r, which says that knowing m and n also determines r. In practice, this means that we are only allowed to have a single instance of Plus for any particular combination of m and n, and if ghc can determine m and n and finds an instance matching them, it will assume it is the only one and pick r to match. Now we can actually do some computation (after enabling UndecidableInstances):

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

Aha! So 1 + 1 = 2, at the type level!

Type-level programming with multi-parameter type classes and functional dependencies has a strong resemblance to logic programming in languages like Prolog. We declare rules defining a number of relations, and then “running” a program consists of searching through the rules to find solutions for unconstrained variables in a given relation. (The one major difference is that GHC’s type class instance search doesn’t (yet?) do any backtracking.)

This is getting a bit long so I’ll break it up into a few posts. In the next installment, I’ll explain type families, which are a newer, alternative mechanism for type-level programming in Haskell.

• OK, OK, non-strict.