I’m not fond of arguments based on lack of imagination. “There’s no way this code may fail!” might be a sign of great confidence or the result of ignorance. The inability to come up with a counterexample doesn’t prove a theorem. And yet there is one area of programming where such arguments work, and are quite useful. These are parametricity arguments: free theorems about polymorphic functions. Fortunately, there is solid theory behind parametricity. Free theorems are not based on ignorance. So I decided to read the relevant papers (see bibliography at the end of this post) and write a blog about it. How hard could it be? A few months and several failed attempts later I realized how naive I was. But I think I finally understand the basics enough to explain them in relatively simple terms.

## Motivation

Here’s a classic example — a function that takes a list of arbitrary type `a`

and returns a list of the same type:

r :: [a] -> [a]

What can this function do? Since it has to work with any type of list element, it can’t do anything type-specific. It can’t modify the elements or invent new ones. So all it can do is rearrange them, duplicate, or remove. Can you think of anything else?

The questions it a little tricky because it all depends on the kind of polymorphism your language supports. In Haskell, where we have parametric polymorphism, the above statement is for the most part true (modulo termination worries). In C++, which supports ad-hoc polymorphism, a generic function like:

template<class T> list<T> r(list<T>);

can do all kinds of weird things.

*Parametric* polymorphism means that a function will act on all types uniformly, so the declaration at the top indeed drastically narrows down the possibilities.

For instance, try `fmap`

ping any function of the type:

f :: a -> b

over a list of `a`

. You can either apply `fmap`

before or after acting on it with `r`

. It shouldn’t matter whether you first modify the elements of the list and then rearrange them, or first rearrange and then modify them. The result should be the same:

r (fmap f as) = fmap f (r as)

But is it true just because we can’t imagine how it may fail, or can we make a formal argument to prove it?

## Let’s Argue (Denotational) Semantics

One way to understand polymorphism is to have a good model for types. At first approximation types can be modeled as sets of values (strictly speaking, as shown by Reynolds, the set-theoretical model fails in the case of polymorphic lambda calculus, but there are ways around it).

The type `Bool`

is a two-element set of `True`

and `False`

, `Integer`

is a set of integers, and so on. Composite types can also be defined set-theoretically. For instance, a pair type is a cartesian product of two sets. A list of `a`

is a set of lists with elements from the set `a`

. A function type `a->b`

is a set of functions between two sets.

For parametric polymorphism you need to first be able to define functions on types: functions that take a type and produce a new type. In other words, you should be able to define a family of types that is parametrized by another type.

For instance, given some type `a`

, produce a type of pairs: `(a, a)`

. This can be formally written (not in Haskell) as:

Λa . (a, a)

Notice the capital lambda for defining functions on types, as opposed to the lowercase lambda used for functions on values.

To turn a family of types into a family of values, you put the universal quantifier in front of it, as in:

forall a . (a, a)

This is a valid type signature, but you’d be hard pressed to implement it. You’d have to provide a pair of concrete values for every possible type. You can’t do it uniformly across all types.

But there are some types of values that can be specified wholesale. These are *function* values. With one formula you can define a whole family of functions. The following signature, for instance, is perfectly implementable:

forall a . a -> a

Let’s analyze it. It consists of a type function:

Λa . a -> a

which, for any type `a`

, returns a *function type* `a->a`

. When universally quantified with `forall`

, it becomes a family of concrete functions parameterized by type. This is possible because all these functions can be defined with one closed term:

id x = x

In Haskell, we usually omit the `forall`

quantifier when there’s no danger of confusion. Any signature that contains a type variable is automatically universally quantified over it. (You’ll have to use explicit `forall`

, however, with higher-order polymorphism, where a polymorphic function can be passed as an argument to another function.)

So what’s the set-theoretic model for polymorphism? You simply replace types with sets. A function on types becomes a function on sets. Notice that this is not the same as a function *between* sets. The latter assigns elements of one set to elements of another. The former assigns sets to sets. As in: Take any set `a`

and return a cartesian product of the set with itself. (You might be tempted to think of functions on sets as functions between sets of all sets, but this kind of thinking leads to well known paradoxes.)

Or take any set `a`

and return the set of functions from this set to itself. For this one we can easily build a polymorphic function — one which for every type `a`

produces an actual function whose type is `(a->a)`

. So, for instance, if `a`

is `Int`

, we will produce a function `(Int->Int`

); if `a`

is `Bool`

, we will produce a function `(Bool->Bool)`

; and so on. Now, with ad-hoc polymorphism it’s okay to code the `Int`

function separately from the `Bool`

function; but in parametric polymorphism, you’ll have to use the same code for all types.

Any language that provides some kind of pattern-matching on types (e.g., template specialization in C++) automatically introduces ad-hoc polymorphism. Incidentally, ad-hoc polymorphism is also possible in Haskell with the use of type families.

## Preservation of Relations

Let’s go to our original example and rewrite it using the explicit universal quantifier:

r :: forall a. [a] -> [a]

It defines a family of functions parametrized by the type `a`

. When used in Haskell code, a particular member of this family will be picked automatically by the type inference system, depending on the context. In what follows, I’ll use explicit subscripting for the same purpose. The free theorem I mentioned before can be rewritten as:

r_{b}(fmap f as) = fmap f (r_{a}as)

with the function:

f :: a -> b

serving as a bridge between the types `a`

and `b`

. Specifically, `f`

relates values of type `a`

to values of type `b`

. This relation happens to be functional, which means that there is only one value of type `b`

corresponding to any given value of type `a`

.

But the correspondence between elements of two lists may, in principle, be more general. What’s more general than a function? A relation. A relation between two sets `a`

and `b`

is defined as a set of pairs — a subset of the cartesian product of `a`

and `b`

. A function is a special case of a relation, one that can be represented as a set of pairs of the form `(x, f x)`

, or in relational notation `x <=> f x`

. This relation is often called the *graph* of the function, since it can be interpreted as coordinates of points on a 2-d plane that form the plot the function.

The key insight of Reynolds’ was that you can abstract the shape of a data structure by defining relations between values. For instance, how do we know that two pairs have the same shape — even if one is a pair of integers, say `(1, 7)`

, and the other a pair of colors, say `(Red, Blue)`

? Because we can relate `1`

to `Red`

and `7`

to `Blue`

. This relation may be called: “occupying the same position”.

Notice that the relation doesn’t have to be functional. The pair `(2, 2)`

can be related to the pair `(Black, White)`

using the non-functional relation:

(2 <=> Black), (2 <=> White)

Conversely, given any relation between integers and colors, you can easily test which integer pairs are related to which color pairs. For the above relation, for instance, these are all the pairs that are related:

((2, 2) <=> (Black, Black)), ((2, 2) <=> (Black, White)), ((2, 2) <=> (White, Black)), ((2, 2) <=> (White, White))

This idea is easily extended to lists. Two lists are related if their corresponding elements are related: the first element of one list must be related to the first element of the second list, etc.; and empty lists are always related.

In particular, if the relationship between elements is established by a function `f`

, it’s easy to convince yourself that the lists `as`

and `bs`

are related if

bs = fmap f as

With this in mind, our free theorem can be rewritten as:

r_{b}bs = fmap f (r_{a}as)

In other words, it tells us that the two lists

r_{b}bs

and

r_{a}as

are related under `f`

.

So `r`

transforms related lists into related lists. It may change the shape of the list, but it never touches the values in it. When it acts on two related lists, it rearranges them in exactly the same way, without breaking any of the relations between corresponding elements.

## Reading Types as Relations

The above examples showed that we can define relations between values of composite types in terms of relations between values of simpler types. We’ve seen this with the pair constructor and with the list constructor. Continuing this trend, we can state that two functions:

f :: a -> b

and

g :: a' -> b'

are related iff, for related `x`

and `y`

, `f x`

is related to `g y`

. In other words, related functions map related arguments to related values.

Notice what we are doing here: We are consistently replacing types with relations in type constructors. This way we can read complex types as relations.

But what about primitive types? Let’s consider an example. Two functions from lists to integers that simply calculate the lengths of the lists:

lenStr :: [Char] -> Int lenBool :: [Bool] -> Int

What happens when we call them with two related lists? The first requirement for lists to be related is that they are of equal length. So when called with related lists the two functions will return the same integer value . It makes sense for us to consider these two functions related because they don’t inspect the values stored in the lists — just their shapes. They also look like components of the same parametrically polymorphic function, `length`

.

It therefore makes sense to read a primitive type, such as `Int`

, as an identity relation: two values are related if they are equal. This way our two functions, `lenStr`

and `lenBool`

are indeed related, because they turn related lists to related results.

Notice that for non-polymorphic functions the relationship that follows from their type is pretty restrictive. For instance, two functions `Int->Int`

are related if and only if their outputs are equal for equal inputs. In other words, the functions must be (extensionally) equal.

Now let’s go back to polymorphic functions. The type of a polymorphic function is specified by universally quantifying a function on types.

f :: forall A. Φ_{A}

The function *Φ* maps types to types. In our set-theoretical model it maps sets to sets, but we want to read it in terms of relations.

A function on relations does two things: it maps input sets to output sets, and it maps pairs from input sets to pairs from output sets. If you pick an arbitrary relation *A* between sets `a`

and `a'`

then *Φ* will map *A* to a relation *Φ _{A}* between sets

`b`

and `b'`

. The connection between `a`

and `b`

, and between `a'`

and `b'`

may, in principle, vary with the input relation.In describing polymorphic functions, we are only interested in functions on relations that “factorize” into functions on sets. It means that *Φ* defines two families of functions on sets, `φ`

and `ψ`

, such that our `b`

is given by `φ`

and _{a}`b'`

is given by `ψ`

. _{a'}*Φ _{A}* then establishes a relation between the sets

`φ`_{a}

and `ψ`_{a'}

.Given that *Φ* maps relations to relations, a universally quantified version of it:

forall A. Φ_{A}

maps pairs of sets to pairs of values.

Now suppose you have two polymorphic functions `g`

and `g'`

:

g :: forall a . φ_{a}g' :: forall a'. ψ_{a'}

They both map types (sets) to values. We can instantiate `g`

at some type `a`

, and it will return a value `g`

of the type _{a}`b=φ`

. We can instantiate _{a}`g'`

at some type `a'`

, and it will return a value `g'`

of the type _{a'}`b'=ψ`

. We can do this for any relation _{a'}*A* between two arbitrary sets `a`

and `a'`

.

We will say that `g`

and `g'`

are related through the relation induced by the type `(forall A. Φ`

iff:_{A})

*Φ*factorizes, as a function on sets, into`φ`

and`ψ`

, and- the results
`g`

and_{a}`g'`

are related by_{a'}*Φ*._{A}

In other words, polymorphic functions are related if they map related types to related values. Notice that in the interesting examples these values are themselves functions.

With these definitions, we can now reinterpret any type signature as a relation between values.

# The Parametricity Theorem

Reynolds’ second key insight was that any term is in a relation with itself — the relation being defined by the term’s type. We have indeed defined the mapping of types to relations to make this work. Primitive types turn into identity relations, so obviously a primitive value is in relation with itself. A function between primitive types is in relation with itself because it maps related (equal) arguments into related (equal) results. A list or a pair of primitive types is in relation with itself because each element of it is equal to itself. You can recurse and consider a list of functions, or a pair of lists, etc., building the proof inductively, proceeding from simpler types to more and more complex types. The proof goes over all possible term construction rules and typing rules in a given theory.

Formally, this kind of proof is called “structural induction,” because you’re showing that more complex structures will satisfy the theorem as long as the simpler ones from which they are constructed, do. The only tricky part is dealing with polymorphic functions, because they are quantified over *all types*. In fact, this is the reason why the naive interpretation of types as sets breaks down (see, however, Pitts’ paper). It is possible, however, to prove the parametricity theorem in a more general setting, for instance, using frames, or in the framework of operational semantics.

Wadler’s key insight was to interpret Reynolds’ theorem not only as a way of identifying different implementations of the same type — for instance, cartesian and polar representations of complex numbers — but also as a source of free theorems for polymorphic types.

Let’s try applying parametricity theorem to some simple examples. Take a constant term: an integer like 5. Its type `Int`

can be interpreted as a relation, which we defined to be the identity relation (it’s one of the primitive types). And indeed, 5 is in this relation with 5.

Take a function like:

ord :: Char -> Int

Its type defines a relation between functions: Two functions of the type `Char->Int`

are related if they return equal integers for equal characters. Obviously, `ord`

is in this relation with itself.

Those were trivial examples. The interesting ones involve polymorphic functions. So let’s go back to our starting example. The term now is the polymorphic function `r`

whose type is:

forall a . [a] -> [a]

Parametricity tells us that `r`

is in relation with itself. However, comparing a polymorphic function to itself involves comparing the instantiations of the same function at two arbitrary types (sets), say `a`

and `a'`

:

r_{a}<=> r_{a'}

We are free to pick an arbitrary relation *A* between elements of these sets. *A* will be mapped to another relation by *Φ _{A}* which, in our case, is induced by the type:

[a] -> [a]

By our definition, two functions r_{a} and r_{a’} are related if they map related arguments to related results. In this case the arguments and the results are lists. So if we have two related lists:

as :: [a] as' :: [a']

they must, by parametricity, be mapped to two related lists:

bs = r_{a}as bs' = r_{a'}as'

This must be true for any type of relation, so let’s pick a functional relation generated by some `(f :: a -> a')`

. We have:

as' = fmap f as

The results of applying `r`

, therefore, must be related through the same relation:

bs' = fmap f bs

Putting it all together, we get our expected result:

r_{a'}(fmap f as) = fmap f (r_{a}as)

## Parametricity and Natural Transformations

The free theorem I used as the running example is interesting for another reason: The list constructor is a functor. You may think of functors as generalized containers for storing arbitrary types of values. You can imagine that they have shapes; and for two containers of the same shape you may establish a correspondence between “positions” at which the elements are stored. This is quite easy for traditional containers like lists or trees, and with a leap of faith it can be stretched to non-traditional “containers” like functions. We used the intuition of relations corresponding to the idea of “occupying the same position” within a data structure. This notion can be readily generalized to any polymorphic containers. Two trees, for instance, are related if they are both empty, or if they have the same shape and their corresponding elements are related.

Let’s try another functor: You can also think of `Maybe`

as having two shapes: `Nothing`

and `Just`

. Two `Nothings`

are always related, and two `Just`

s are related if their contents are related.

This observation immediately gives us a free theorem about polymorphic functions of the type:

r :: forall a. [a] -> Maybe a

an example of which is `safeHead`

. The theorem is:

fmap h . safeHead == safeHead . fmap h

Notice that the `fmap`

on the left is defined by the `Maybe`

functor, whereas the one on the right is the list one.

If you accept the premise that an appropriate relation can be defined for any functor, then you can derive a free theorem for all polymorphic functions of the type:

r :: forall a. f a -> g a

where `f`

and `g`

are functors. This type of function is known as a natural transformation between the two functors, and the free theorem:

fmap h . r == r . fmap h

is the naturality condition. That’s how naturality follows from parametricity.

## Acknowledgments

I’d like to thank all the people I talked to about parametricity at the ICFP in Gothenburg, and Edward Kmett for reading and commenting on the draft of this blog.

## Appendix: Other Examples

Here’s a list of other free theorems from Wadler’s paper. You might try proving them using parametricity.

r :: [a] -> a -- for instance, head f . r == r . fmap f

r :: [a] -> [a] -> [a] -- for instance, (++) fmap f (r as bs) == r (fmap f as) (fmap f bs)

r :: [[a]] -> [a] -- for instance, concat fmap f . r == r . fmap (fmap f)

r :: (a, b) -> a -- for instance, fst f . r == r . mapPair (f, g)

r :: (a, b) -> b -- for instance, snd g . r == r . mapPair (f, g)

r :: ([a], [b]) -> [(a, b)] -- for instance, uncurry zip fmap (mapPair (f, g)) . r == r . mapPair (fmap f, fmap g)

r :: (a -> Bool) -> [a] -> [a] -- for instance, filter fmap f . r (p . f) = r p . fmap f

r :: (a -> a -> Ordering) -> [a] -> [a] -- for instance, sortBy -- assuming: f is monotone (preserves order) fmap f . r cmp == r cmp' . fmap f

r :: (a -> b -> b) -> b -> [a] -> b -- for instance, foldl -- assuming: g (acc x y) == acc (f x) (g y) g . foldl acc zero == foldl acc (g zero) . fmap f

r :: a -> a -- id f . r == r . f

r :: a -> b -> a -- for instance, the K combinator f (r x y) == r (f x) (g y)

where:

mapPair :: (a -> c, b -> d) -> (a, b) -> (c, d) mapPair (f, g) (x, y) = (f x, g y)

## Bibliography

- John C Reynolds, Types, Abstraction and Parametric Polymorphism
- Philip Wadler, Theorems for Free!
- Claudio Hermida, Uday S. Reddy, Edmund P. Robinson, Logical Relations and Parametricity – A Reynolds Programme for Category Theory and Programming Languages
- Derek Dreyer, Paremetricity and Relational Reasoning, Oregon Programming Languages Summer School