Free as in theorems

In a nutshell, the parametricity theorem states that when you see a "forall" in a Haskell type, it really means "for all". It means that you can put any type in there, and it works. It doesn't matter what the type is, or what it can do.

Here's an example. Consider this type signature:

> id :: forall a. a -> a

What that means is that id has the type a -> a for all types a.

Since a can have any type, id can't make any assumptions about what operations it supports. It can't construct a value of that type, it can't compare types for equality, and it can't make decisions based on what specific value that a value of type a has. And, crucially, you can perform any type substitution, and the meaning of id is unchanged.

Let's see what that means. Suppose that you have some substitution f :: A1 -> A2, and let x :: A1 be an arbitrary value. If y is the substitution performed on x, then id y is the same substitution performed in id x. In other words:

If f x = y,
then f (id x) = id y.

You can substitute the first equation into the second and do some point-free conversion to get the following nice form:

f . id = id . f

That is, for any function f, f commutes with id.

One important thing to notice here is that the concrete types for id are different on the left-hand side and the right-hand side. On the left-hand side, id has type A1->A1, and on the right-hand side, it has type A2->A2. This distinction is important if you're expressing the theorem in a system where this is explicit, such as System F or GHC core.

(Incidentally, I computed all of the free theorems presented here with my own free theorem generator. It's also built into the current lambdabot, using the command free. However, by the end of this blog entry, you may be able to have a good guess as to what the free theorem is for most polymorphic functions with only one type variable (which is what I'll be largely concentrating on).)

Let's look at another example. Consider the type declaration:

> simpleFst :: forall a. (a,Int) -> a

Let's introduce the morphism product, just to make things a little clearer:

> (><) :: (a -> b) -> (c -> d) -> (a,c) -> (b,d)
> (f >< g) ~(a,b) = (f a, g b)

Suppose f :: A1 -> A2 is an arbitrary type substitution, and let x :: (a,Int) be an arbitrary value. Then the free theorem for simpleFst is:

If (f >< id) x = y,
then f (simpleFst x) = simpleFst y

Substituting y and points-freeing gives the nice form:

f . simpleFst = simpleFst . (f >< id)

Which, once again, kind of looks like f commutes with simpleFst.

Another way of looking at this is to note that the type (a,Int) is a functor. If you declared a Functor instance for it:

> newtype F a = F (a,Int)

> instance Functor F where

>     fmap f = (F (x,n)) = F (f x, n)

then the free theorem would be:

f . simpleFst = simpleFst . fmap f

This always works for functors. In fact, if you have a mapping between functors:

> trans :: forall a. F a -> G a

then the free theorem is:

fmap f . trans = trans . fmap f

Interestingly, this is just the axiom that must be satisfied by a natural transformation. If you didn't understand what "natural" means before, now you do: you can't avoid writing them in Haskell. Haskell type-correctness corresponds to the category notion of "naturality".

Higher-order functions also obey free theorems. The idea is that if func has a function as its argument, then the free theorem states that if the function that you pass obeys the type substitution, then so does the function that it's passed to. For example:

> substFirst :: forall a. (a -> a) -> (a,Int) -> (a,Int)

Suppose that you have a substitution f :: A1 -> A2. Then the free theorem is:

Let g :: A1 -> A1 and h :: A2 -> A2 be arbitrary functions.

If for all x, f (g x) = h (f x)
then (f >< id) . substFst g = substFst h . (f >< id)

In other words, if g and h essentially "do the same thing" when the substitution is applied, then f commutes with substFst.

What, exactly, does "do the same thing" mean, though? It might be clearer if we look at a few examples. Consider sortBy, which sorts a list according to a supplied ordering:

> sortBy :: forall a. (a -> a -> Ordering) -> [a] -> [a]

(Note that list is just a functor, so we can use map.)

Intuitively, what we want is for the ordering not to change under the substitution. That is, if f :: A1 -> A2 is a substitution, we'd like ord1 :: A1 -> A1 -> Ordering and ord2 :: A1 -> A1 -> Ordering to obey:

For all x, y :: A1
, ord1 x y = ord2 (f x) (f y)

And, it turns out, that this is precisely the precondition required. If the above is true, then f commutes with sortBy:

map f . sortBy ord1 = sortBy ord2 . map f

Let's try a trickier example:

foldl1 :: forall. (a -> a -> a) -> [a] -> a

If f :: A1 -> A2 is a substitution, then the free theorem is:

Let g :: A1 -> A1 -> A1 and h :: A2 -> A2 -> A2. Let x, y :: A1 be arbitrary values. Then:

If f (g x y) = h (f x) (f y),

then f . foldl1 g = foldl1 h . map f

So far, so good. It says that if g does the "same thing" as h, then f commutes with foldl1.

Now step back for a moment and think about what foldl1 actually does. Generally speaking, you have some kind of combining operation that combines two "values" into one "value", and you use this to reduce a finite, non-empty list of values into one.

Ignoring associativity for a moment, you can think of this as a mathematical semigroup. In fact, we can define a type class:

> class Semigroup s where
>     (<*>) :: s -> s -> s

And then define a foldl1-like operation:

> semigroupCombine :: (Semigroup s) => [s] -> s

Remember that the type class context here is exactly like passing in a function of type s -> s -> s, so this is conceptually the same as foldl1.

So what would the free theorem for semigroupCombine be?

Let f :: S1 -> S2 be an arbitrary mapping between two semigroups. Then the free theorem looks like this:

Let x, y :: S1 be arbitrary values. Then:

If f (x <*> y) = (f x) <*> (f y),

then f . semigroupCombine = semigroupCombine . map f

The condition on f says that f must be a semigroup homomorphism! If that's true, then f commutes with semigroupCombine.

Now what do you suppose the free theorem for this function is?

> restrictedFoldl :: forall. (a -> a -> a) -> a -> [a] -> a

I won't bother to work it all out, but you can probably guess: the first two arguments define a monoid. The free theorem states that if your type substitution is a monoid homomorphism, then it commutes with restrictedFoldl.

This suggests a bunch of interesting stuff, but from the point of view of obtaining theorems for free, the most practical one is this: There are a bunch of built-in Haskell type classes, like Ord, Enum and Show. Each one of these defines an algebra, and has the notion of a homomorphism. And, so, any function which uses those type classes has a free theorem.

It might be a complicated one. It might have so many preconditions on it that it's useless. But nonetheless, it's a theorem that you didn't have to pay for.