A powerful feature of Haskell’s type system is that we can deduce properties of functions by looking *only at their type*. For example, a function of type

can only be the identity function: since it must return something of type `a`

, for *any* type `a`

, the only thing it can do is return the argument of type `a`

that it was given (or crash). Similarly, a function of type

can only do one of two things: either return the first argument, or return the second. This kind of reasoning is becoming more and more important with the increasing use of types such as this definition of a “lens”:

Since a lens is just a function of a particular type, the only thing we can conclude about such a function is whatever we can deduce from its type.

To reason about the properties of functions based only on their types we make use of the theory of parametricity, which tells how to derive a so-called “free theorem” from a type. This blog post is a tutorial on how to do this; it won’t explain *why* the theory works, only *how* it works. A Haskell practitioner’s guide to parametricity, if you will.

This is a two-part blog post. In part 1 (this post) we will cover the basics: constant types, functions and polymorphism (over types of kind `*`

).

In part 2 we will deal with more advanced material: type constructor (types of kind `* -> *`

), type classes, polymorphism over type constructors and type constructor classes.

## The Basics

The main theorem of parametricity is the following:

When `t`

is a closed type, `ℛ(t)`

is a relation between two terms of type `t`

(we shall see later that the type of `ℛ`

is actually slightly more general). In words, parametricity states that any term `f`

of type `t`

is related to itself by `ℛ(t)`

. Don’t worry if this all looks incredibly abstract! We shall see lots and lots of examples.

### Constant types (types of kind `*`

)

For any constant type `C`

, the relation `ℛ(C)`

is the identity relation. In other words,

(We will use ≡ throughout to mean mathematical equality, to distinguish it from Haskell’s equality function `(==)`

.)

Let’s see an example. Suppose that `x :: Int`

. Then parametricity tells us that

I.e., it tells us that `x`

is equal to itself. Not very insightful! Intuitively, this makes sense: if all we know about `x`

is that it is an integer, we cannot tell anything about its value.

TOOLING.Many of the examples in this blog post (though sadly not all) can also be auto-derived by one of two tools. On the`#haskell`

IRC channel we can ask`lambdabot`

to derive free theorems for any types not involving type classes or type constructor classes. If you ask`@free x :: Int`

`lambdabot`

will reply with`x = x`

(I recommend starting a private conversation with lambdabot so you avoid spamming the whole

Alternatively, you can also try the online free theorem generator. This free theorem generator is a bit more precise than`#haskell`

channel.)`lambdabot`

(which takes some shortcuts sometimes), and supports type classes, but cannot work with type constructors (`lambdabot`

can work with unknown type constructors but not with quantification over type constructors, unfortunately).

### Functions

For functions we map related arguments to related results:

(The types of `x`

and `x'`

here depend on what precisely `A`

is; see *The type of ℛ*, below.)

Example. Suppose `f :: Int -> Bool`

. By parametricity

```
f ℛ(Int -> Bool) f
iff forall x :: Int, x' :: Int.
if x ℛ(Int) x' then f x ℛ(Bool) f x'
-- both Int and Bool are constant types
iff forall x :: Int, x' :: Int.
if x ≡ x' then f x ≡ f x'
-- simplify
iff f ≡ f
```

Again, not very informative. Parametricity doesn’t tell us anything about functions between constant types. Time to look at something more interesting!

### Polymorphism (over types of kind `*`

)

The definition for polymorphic values is

That is, whenever we pick two types `A`

and `A'`

, and *some* relation `a`

between `A`

and `A'`

, the function `f@A`

obtained by instantiating the type variable by `A`

must be related to the function `f'@A'`

obtained by instantiating the type variable by `A'`

. In what follows we will write explicit type instantiation like this only if the type is not clear from the context; specifically, we will omit it when we supply arguments to the function.

The type of ℛ.

`∀ab. a -> b -> a`

is an example of aclosedtype: all type variables are bound by a universal quantifier. Anopentype is a type with free type variables such as`∀b. a -> b -> a`

or even`a -> b -> a`

. (Note that this distinction is harder to see in Haskell where universal quantifiers are often implicit. We will not follow that convention in this article.)We said in the introduction that if

Given two relations`t`

is a closed type,`ℛ(t)`

relates two terms of type`t`

. As we saw, in order to be able to give a meaning toopentypes we need a mapping from any free variable`a`

to a relation`a :: A ⇔ A'`

. In this article we somewhat informally maintain this mapping simply by using the same name for the type variable and the relation.`a :: A ⇔ A'`

and`b :: B ⇔ B'`

,`ℛ(a -> b -> a)`

relates terms of type`A -> B -> A`

with terms of type`A' -> B' -> A'`

. It is important to realize that`ℛ`

can therefore relate terms of different types. (For a more precise treatment, see my Coq formalization of a part of this blog post.)

The interpretation of `ℛ`

for a free type variable `a`

is defined in terms of the corresponding relation:

#### Example: `∀a. a -> a`

Let’s consider a number of examples, starting with an `f :: ∀a. a -> a`

:

```
f ℛ(∀a. a -> a) f
-- parametricity
iff forall A, A', a :: A ⇔ A'.
f@A ℛ(a -> a) f@A'
-- definition for function types
iff forall A, A', a :: A ⇔ A', x :: A, x' :: A'.
if x ℛ(a) x' then f x ℛ(a) f x'
```

It might not be immediately evident from the last line what this actually allows us to conclude about `f`

, so let’s look at this a little closer. A function `g`

is a special kind of relation, relating any argument `x`

to `g x`

; since the property holds for any kind of relation `a : A ⇔ A'`

, it must also hold for a *function* `a⃯ :: A -> A'`

:

```
forall x, x'.
if x ℛ(a⃯) x' then f x ℛ(a⃯) f x'
-- x ℛ(a⃯) x' iff a⃯ x ≡ x'
iff forall x :: A, x' :: A'.
if a⃯ x ≡ x' then a⃯ (f x) ≡ f x'
-- simplify
iff forall x :: A,
a⃯ (f x) ≡ f (a⃯ x)
```

We can apply this result to show that any `f :: ∀a. a -> a`

must be the identity function: picking `a⃯ = const x`

, we get `const x (f x) ≡ f (const x x)`

, i.e. `x ≡ f x`

, as required.

NOTE.We are doing fast and loose reasoning in this tutorial and will completely ignore any totality issues. See Automatically Generating Counterexamples to Naive Free Theorems, or the associated web interface, for some insights about what wrong conclusions we can draw by ignoring totality.

#### Example: `∀a. a -> a -> a`

Intuitively, there are only two things a function `f :: ∀a. a -> a -> a`

can do: it can either return its first argument, or it can return its second argument. What does parametricity tell us? Let’s see:

```
f ℛ(∀a. a -> a -> a) f
iff forall A, A', a :: A ⇔ A'.
f@A ℛ(a -> a -> a) f@A'
-- applying the rule for functions twice
iff forall A, A', a :: A ⇔ A', x :: A, x' :: A', y :: A, y' :: A'.
if x ℛ(a) x', y ℛ(a) y' then f x y ℛ(a) f x' y'
```

Let’s again specialize the last line to pick a function `a⃯ :: A -> A'`

for the relation `a`

:

```
forall x :: A, x' :: A', y :: A, y' :: A'.
if x ℛ(a⃯) x', y ℛ(a⃯) y' then f x y ℛ(a⃯) f x' y'
-- a⃯ is a function
iff forall x :: A, y :: A.
if a⃯ x ≡ x' and a⃯ y ≡ y' then a⃯ (f x y) ≡ f x' y'
-- simplify
iff a⃯ (f x y) = f (a⃯ x) (a⃯ y)
```

So parametricity allows us to “push in” or “distribute” `a⃯`

over `f`

. The fact that `f`

must either return its first or its second argument follows from parametricity, but not in a completely obvious way; see the `reddit`

thread How to use free theorems.

### Example: `∀ab. a -> b`

Other than `undefined`

(which we are ignoring), there can be no function `f :: ∀ab. a -> b`

. Let’s suppose that one *did* exist; what does parametricity tell us?

```
f ℛ(∀ab. a -> b) f
-- applying the rule for universal quantification, twice
iff forall A, A', B, B', a :: A ⇔ A', b :: B ⇔ B'.
f@A,B ℛ(a -> b) f@A',B'
-- applying the rule for functions
iff forall A, A', B, B', a :: A ⇔ A', b :: B ⇔ B', x :: A, x' :: A'.
if x ℛ(a) x' then f x ℛ(b) f x'
```

Picking two functions `a⃯ :: A -> A'`

and `b⃯ :: B -> B'`

for `a`

and `b`

, we get

It’s not too difficult to derive contradiction from this (remember that you can pick any two functions `a⃯`

and `b⃯`

between any types of your choosing). Hence, such a function cannot exist.

#### Example: `∀ab. (a -> b) -> a -> b`

The only thing a function of this type can do is apply the supplied function to the supplied argument (alternatively, if you prefer, this must be the identity function). Let’s spell this example out in a bit of detail because it is our first example of a higher order function.

```
f ℛ(∀ab. (a -> b) -> a -> b) f
-- apply rule for polymorphism, twice
iff forall A, A', B, B', a :: A ⇔ A', b :: B ⇔ B'.
f@A,B ℛ((a -> b) -> a -> b) f@A',B'
-- apply rule for functions, twice
iff forall A, A', B, B', a :: A ⇔ A', b :: B ⇔ B'.
forall g :: A -> B, g' :: A' -> B', x :: A, x' :: A'.
if g ℛ(a -> b) g' and x ℛ(a) x' then f g x ℛ(b) f g' x'
```

Let’s expand what that premise `g ℛ(a -> b) g'`

means:

For the special case that we pick *functions* `a⃯ :: A -> A'`

and `b⃯ :: B -> B'`

for `a`

and `b`

, that premise collapses to

```
forall y :: A, y' :: A'.
if y ℛ(a⃯) y' then g y ℛ(b⃯) g' y'
-- a⃯ and b⃯ are functions
iff forall y :: A, y' :: A'.
if a⃯ y ≡ y' then b⃯ (g y) ≡ g' y'
-- simplify
iff forall y :: A.
b⃯ (g y) ≡ g' (a⃯ y)
-- simplify (extensionality)
iff b⃯ . g ≡ g' . a⃯
```

So that the free theorem for `f :: ∀ab. (a -> b) -> a -> b`

becomes

Picking `b⃯ = const g`

, `g' = g`

, and `a⃯ = id`

(verify that the premise holds) we get that indeed `g ≡ f g`

, as expected.

whenever

Useful shortcut.This pattern is worth remembering:`a⃯`

and`b⃯`

are function(al relation)s.

#### Example: `∀ab. (∀c. c -> String) -> a -> b -> String`

A function `f :: ∀ab. (∀c. c -> String) -> a -> b -> String`

is not only higher order, but has a rank-2 type: it insists that the function it is given is *itself* polymorphic. This makes it possible to write, for example

`f g x y = g x ++ g y`

Note that since `x`

and `y`

have different types, it is important that `g`

is polymorphic. What is the free theorem for `f`

?

```
f ℛ(∀ab. (∀c. c -> String) -> a -> b -> String) f
-- apply rule for polymorphism, twice
iff forall A, A', B, B', a :: A ⇔ A', b :: B ⇔ B'.
f ℛ((∀c. c -> String) -> a -> b -> String) f
-- apply rule for functions three times, and simplify ℛ(String) to (≡)
iff forall A, A', B, B', a :: A ⇔ A', b :: B ⇔ B'.
forall g :: ∀c. c -> String, g' :: ∀c. c -> String.
forall x :: A, x' :: A', y :: B, y' :: B'.
if
g ℛ(∀c. c -> String) g', x ℛ(a) x', y ℛ(b) y'
then
f g x y ≡ f g' x' y'
```

Specializing this theorem to *functions* `a⃯ :: A -> A'`

and `b⃯ :: B -> B'`

we get

```
forall A, A', B, B', a⃯ :: A -> A', b⃯ :: B -> B'.
forall g :: ∀c. c -> String, g' :: ∀c. c -> String.
forall x :: A, y :: B.
if
g ℛ(∀c. c -> String) g'
then
f g x y ≡ f g' (a⃯ x) (b⃯ y)
```

But that is somewhat surprising, because it seems to say that the values of `x`

and `y`

cannot matter at all! What is going on? Expanding the first premise:

```
g ℛ(∀c. c -> String) g'
iff forall C, C', c :: C ⇔ C',
g ℛ(c -> String) g'
iff forall C, C', c :: C ⇔ C', z :: C, z' :: C'.
if z ℛ(c) z' then g z = g' z'
```

Let’s stop for a moment to ponder what this requirement for `g`

and `g'`

really says: given *any* relation `c`

, and *any* elements `z`

and `z'`

that are related by `c`

—in other words, for any `z`

and `z'`

at all—we must have that `g z`

and `g' z'`

give us equal results. This means that `g`

and `g'`

must be constant functions, and the *same* constant function at that. As a consequence, for any function `f`

of the above type, `f g`

must itself be constant in `x`

and `y`

. In part two we will see a more useful variation which uses the `Show`

type class.

Incidentally, note that this quantification over an arbitrary relation `c`

is a *premise* to the free theorem, not a conclusion; hence we cannot simply choose to consider only *functions* c.

TOOLING.Indeed, if you enterin the online free theorem generator you will see that it first gives the free theorem using relations only, and then says it will reduce all “permissible” relation variables to functions; in this example, that is all relations except for`(forall c. c -> String) -> a -> b -> String`

`c`

;`lambdabot`

doesn’t make this distinction andalwaysreduces relations to functions, which is not correct.

## To be continued

Part 2 covers type constructors, type classes and type constructor classes. Meanwhile, here are some links to papers on the subject if you want to read more.

- Theorems for free! by Philip Wadler is the seminal paper on the topic. It doesn’t however cover general type classes, higher types, or type constructors.
- Type-safe cast does no harm: Syntactic parametricity for Fω and beyond by Dimitrios Vytiniotis and Stephanie Weirich is a more theoretical paper about free theorems in a calculus with higher rank types and representation types.