This is part 2 of a two-part series on parametricity.

In part 1 we covered the basics: constant types, functions and polymorphism (over types of kind `*`

). In this post we will deal with more advanced material: type constructors, type classes, polymorphism over type constructors and type constructor classes.

## Type constructors (types of kind `* -> *`

)

Before considering the general case, let’s think about lists. Given `a :: A ⇔ A'`

, two lists `xs :: [A]`

and `ys :: [A']`

are related iff their elements are related by `a`

; that is,

` [] ℛ([a]) []`

and

```
:xs') ℛ([a]) (y:ys')
(xand xs' ℛ([a]) ys' iff x ℛ(a) x'
```

For the special case that `a`

is a function `a⃗ :: A -> A'`

, this amounts to saying that `map a⃗ xs ≡ ys`

.

You can imagine a similar relation `F a`

exists for any type constructor `F`

. However, we will not give a general treatment of algebraic data types in this blog post. Doing this would require giving instances for products and sums (which is fine), but also for (least) fixed points, and that would take us much too far afield.

Thankfully, we will not need to be quite so precise. Instead, it will only require the following characterization:

Characterization: Functors.Let

`F`

be a functor. Then for all relations`a :: A ⇔ A'`

,`b :: B ⇔ B'`

and functions`f :: A -> B`

and`g :: A' -> B'`

, such that`f ℛ(a -> b) g`

:where we overload`forall xs :: F A, xs' :: F A'. if xs ℛ(F a) xs' then F f xs ℛ(F b) F g xs'`

`F`

to also mean the “map” function associated with`F`

. (Provided that the`Functor`

type class instance for`F`

is correct,`F f`

should be the same as`fmap f`

.)

(If we had the precise rules for algebraic data types we would be able to prove this characterization for any specific functor `F`

.)

Intuitively, think about `xs`

and `xs'`

as two containers of the same shape with elements related by `a`

, and suppose we have a pair of functions `f`

and `g`

which map `a`

-related arguments to `b`

-related results. Then the characterization states that if we apply function `f`

to the elements of `xs`

and `g`

to the elements of `xs'`

, we must end up with two containers of the same shape with elements related by `b`

.

For the special case that `a`

and `b`

are functions (and `F`

is a functor), the mapping relations characterization simply says that

```
if xs ℛ(F a⃗) xs' then F f xs ℛ(F b⃗) F g xs'
-- simplify
if F a⃗ xs ≡ xs' then F f xs ℛ(F b⃗) F g xs'
-- simplify
F b⃗ (F f xs) ≡ F g (F a⃗ xs)
-- functoriality
F (b⃗ . f) xs ≡ F (g . a⃗) xs
```

which follows immediately from the premise that `b⃗ . f ≡ g . a⃗`

(which in turn is a consequence of `f ℛ(a⃗ -> b⃗) g`

), so the mapping relations characterization is trivially satisfied (provided that the mapping of relations correspond to the functor map in the case for functions).

Technical note.When we use parametricity results, we often say something like: “specializing this result tofunctionsrather thanrelations…”. It is important to realize however that if`F`

is not a functor, then`F a`

may not be a functional relation even if`a`

is.For example, let

`a⃗ :: A -> A'`

, and take`F(a) = a -> a`

. Then`F a⃗) g f ℛ(-- expand definition -> a⃗) g iff f ℛ(a⃗ -- rule for functions forall x :: A, x' :: A'. iff if x ℛ(a⃗) x' then f x ℛ(a⃗) g x' -- simplify (a⃗ is a function) forall x :: A. iff a⃗ (f x) ≡ g (a⃗ x)`

Taking

Given a function`a :: Int -> Int ; a x = 0`

, this would relate two functions`f, g :: Int -> Int`

whenever`0 ≡ g 0`

; it is clear that this is not a functional relation between`f`

and`g`

.`a⃗ :: A -> A'`

,`F a⃗`

is a function`F A -> F A'`

when`F`

is a functor, or a function`F A' -> F A`

if`F`

is a contravariant functor. We will not consider contravariant functors further in this blog post, but there is an analogous Contravariant Functor Characterization that we can use for proofs involving contravariant functors.

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

This is the type of Haskell’s `map`

function for lists of course; the type of `map`

doesn’t fully specify what it should do, but the elements of the result list can only be obtained from applying the function to elements of the input list. Parametricity tells us that

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

Specializing to *functions* `a⃗ :: A -> A'`

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

, we get

```
forall A, A', B, B', a⃗ :: A -> A', b⃗ :: B -> B'.
forall g :: A -> B, g' :: A' -> B', xs :: [A], xs' :: [A'].
if g ℛ(a⃗ -> b⃗) g', xs ℛ([a⃗]) xs' then f g xs ℛ([b⃗]) f g' xs'
-- simplify
forall A, A', B, B', a⃗ :: A -> A', b⃗ :: B -> B'.
iff forall g :: A -> B, g' :: A' -> B'.
if b⃗ . g ≡ g' . a⃗ then map b⃗ . f g ≡ f g' . map a⃗
```

As an aside, `Functor`

instances should satisfy two laws:

`map id ≡ id`

`map f . map g ≡ map (f . g)`

It turns out that the second property follows from the first by parametricity; see The free theorem for `fmap`

.

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

Consider a funtion `f :: ∀a. F a -> G a`

, polymorphic in `a`

but between fixed (constant) type constructors `F`

and `G`

; for example, a function of type `∀a. Maybe a -> [a]`

fits this pattern. What can we tell about `f`

?

```
. F a -> G a) f
f ℛ(∀aforall A, A', a :: A ⇔ A'.
iff @A ℛ(F a -> G a) f@A'
fforall A, A', a :: A ⇔ A', x :: F A, x' :: F A'.
iff if x ℛ(F a) x' then f x ℛ(G a) f x'
```

For the special case where we pick a function `a⃗ :: A -> A'`

for `a`

, this is equivalent to

```
forall A, A', a⃗ :: A -> A'.
G a⃗ . f == f . F a⃗
```

For the categorically inclined, this means that polymorphic functions must be natural transformations.

## Type classes

Now that we’ve covered the basics, it’s time to consider some more advanced language features. We will first consider qualified types, such as `∀a. Eq a => a -> a -> a`

.

The rule for a qualified type is

```
. C a => t) f'
f ℛ(∀ aforall A, A', a :: A ⇔ A'
iff A, A' instances of C and a respects C.
such that @A ℛ(t) f'@A' f
```

What does it mean for a relation `a :: A ⇔ A'`

to respect a type class `C`

? Every type class introduces a new constraint on relations defined by the members of the type class. Let’s consider an example; Haskell’s equality type class is defined by

```
class Eq a where
(==) :: a -> a -> Bool
```

(Let’s ignore (`/=`

) for simplicity’s sake.). Then a relation `a`

*respects* `Eq`

, written `Eq(a)`

, iff all class members are related to themselves. For the specific case of `Eq`

this means that

```
==) ℛ(a -> a -> Bool) (==)
(-- rule for functions, twice
forall x :: A, x' :: A', y :: A, y' :: A'.
iff if x ℛ(a) x', y ℛ(a) y' then x == y ℛ(Bool) x' == y'
-- Bool is a constant type, simplify
forall x :: A, x' :: A', y :: A, y' :: A'.
iff if x ℛ(a) x', y ℛ(a) y' then x == y ≡ x' == y'
```

For the special case where we pick a *function* `a⃗ :: A -> A'`

, the function respects Eq iff

```
forall x :: A, y :: A.
== y ≡ a⃗ x == a⃗ y x
```

I.e., the function maps `(==)`

-equal arguments to `(==)`

-equal results.

Syntactic convention.In the following we will write

`forall A, A', a :: A ⇔ A' A, A' instances of C and a respects C. such that`

more concisely as

`forall C(A), C(A'), C(a) :: A ⇔ A'.`

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

We already considered the free theorem for functions `f :: ∀ a. a -> a -> a`

:

`g (f x y) = f (g x) (g y)`

Is this free theorem still valid for `∀a. Eq a => a -> a -> a`

? No, it’s not. Consider giving this (admittedly somewhat dubious) definition of natural numbers which considers all “invalid” natural numbers to be equal:

```
newtype Nat = Nat Int
deriving (Show)
instance Eq Nat where
Nat n == Nat n' | n <= 0, n' <= 0 = True
| otherwise = n == n'
```

If we define

```
f :: forall a. Eq a => a -> a -> a
= if x == y then y else x
f x y
g :: Nat -> Nat
Nat n) = Nat (n + 1) g (
```

then for `x ≡ Nat (-1)`

and `y ≡ Nat (-2)`

we have that `g (f x y) ≡ Nat (-1)`

but `f (g x) (g y) ≡ Nat 0`

. Dubious or not, free theorems don’t assume anything about the particular implementation of type classes. The free theorem for `∀a. Eq a => a -> a -> a`

however *only* applies to functions `g`

which respect `Eq`

; and this definition of `g`

does not.

## Example: `∀ab. (Show a, Show b) => a -> b -> String`

We promised to look at this type when we considered higher rank types above. If you go through the process, you will find that the free theorem for functions `f`

of this type is

`f x y = f (g x) (h y)`

for any `Show`

-respecting functions `g`

and `h`

. What does it mean for a function to respect `Show`

? Intuitively it means that the function can change the value of its argument but not its string representation:

`show (g x) = show x`

## Type constructor classes

Type constructor classes are classes over types of kind `* -> *`

; a typical example is

```
class Functor f where
fmap :: ∀ab. (a -> b) -> f a -> f b
```

The final rule we will discuss is the rule for universal quantification over a qualified type constructor (universal quantification over a type constructor without a qualifier is rarely useful, so we don’t discuss it separately):

```
. C f => t) g'
g ℛ(∀fforall C(F), C(F'), C(f) :: F ⇔ F'.
iff @F ℛ(t) g'@F' g
```

If `F`

and `F'`

are type constructors rather than types (functions on types), `f :: F ⇔ F'`

is a relational action rather than a relation: that is, it is a function on relations. As before, `C(f)`

means that this function must respect the type class `C`

, in much the same way as for type classes. Let’s consider what this means for the example of `Functor`

:

```
fmap ℛ(∀ab. (a -> b) -> f a -> f b) fmap
forall A, A', B, B', a :: A ⇔ A', b :: B ⇔ B'.
iff @A,B ℛ((a -> b) -> f a -> f b) fmap@A,B
fmapforall A, A', B, B', a :: A ⇔ A', b :: B ⇔ B'.
iff forall g :: A -> B, g' :: A' -> B', x :: F A, x' :: F' A'.
if g ℛ(a -> b) g', x ℛ(f a) x'
then fmap g x ℛ(f b) fmap g' x'
```

#### Example: `∀f. Functor f => f Int -> f Int`

Intuitively, a function `g :: ∀f. Functor f => f Int -> f Int`

can take advantage of the `Int`

type, but only by applying `fmap`

; for example, when we apply `g`

to a list, the order of the list should not matter. Let’s derive the free theorem for functions of this type:

```
. Functor f => f Int -> f Int) g
g ℛ(∀fforall Functor(F), Functor(F'), Functor(f) :: F ⇔ F'.
iff @F ℛ(f Int -> f Int) g@F'
gforall Functor(F), Functor(F'), Functor(f) :: F ⇔ F'.
iff forall x :: F Int, x' :: F' Int.
if x ℛ(f Int) x' then g x ℛ(f Int) g x'
```

As before, we can specialize this to higher order functions, which are special cases of relational actions. Let’s use the notation `f⃗ :: F -> F'`

(with `F`

and `F'`

type constructors) to mean `f⃗ :: ∀ab. (a -> b) -> (F a -> F' b)`

. Then we can specialize the free theorem to

```
forall Functor(F), Functor(F'), Functor(f⃗) :: F -> F'.
iff forall x :: F Int, x' :: F' Int.
if x ℛ(f⃗ Int) x' then g x ℛ(f⃗ Int) g x'
-- `f⃗` is a function; recall that `Int` as a relation is the identity:
forall Functor(F), Functor(F'), Functor(f⃗) :: F -> F'.
iff id . g ≡ g . f⃗ id f⃗
```

for any Functor-respecting `f⃗`

.

#### Example continued: further specializing the free theorem

The free theorem we saw in the previous section has a very useful special case, which we will derive now. Recall that in order to prove that a higher order function `f⃗`

respects `Functor`

we have to prove that

`if g ℛ(a -> b) g', x ℛ(f⃗ a) x' then fmap g x ℛ(f⃗ b) fmap g' x'`

As in the higher rank example, this is a proof obligation (as opposed to the *application* of a free theorem), so that we really have to consider *relations* `a :: A ⇔ A'`

and `b :: B ⇔ B'`

here; it’s not sufficient to consider functions only.

We can however derive a special case of the free theorem which is easier to use. Take some arbitrary polymorphic function `k :: ∀a. F a -> F' a`

, and define the relational action `f :: F ⇔ F'`

by

`= k ⚬ F(a) f(a) `

where we use `k`

also as a relation. Then

```
x ℛ(f a) x'. x ℛ(k) i and i ℛ(F(a)) x'
iff ∃i-- k is a function
F(a)) x'
iff k x ℛ(-- by the Functor Characterization
F g (k x) ℛ(F b) F g' x'
iff -- naturality
F g x) ℛ(F b) F g' x'
iff k (-- use k as a relation again
F g x ℛ(k) k (F g x) ℛ(F b) F g' x'
iff -- pick k (F g x) as the intermediate
then F g x ℛ(f b) F g' x'
-- if we assume that fmap is the "real" functor instance
fmap g x ℛ(f b) fmap g' x' iff
```

In the previous section we derived that the free theorem for `g :: ∀f. Functor f => f Int -> f Int`

was

```
forall Functor(F), Functor(F'), Functor(f⃗) :: F -> F'.
id . g ≡ g . f⃗ id f⃗
```

for any higher order function which respects `Functor`

. The `f`

we defined above *is* a higher order function provided that `a`

if a function, and we just proved that it must respect functor. The identity relation is certainly a function, so we can specialize the free theorem to

`k . g ≡ g . k`

for *any* polymorphic function `k`

(no restrictions on `k`

). As a special case, this means that we must have

`reverse . g ≡ g . reverse`

formalizing the earlier intuition that when we apply such a function to a list, the order of the list cannot matter.

## Example: `∀f. Functor f => (B -> f B) -> f A`

As our last example, we will consider higher-order functions of type `g :: ∀f. Functor f => (B -> f B) -> f A`

. The free theorem for such functions is

```
. Functor f => (B -> f B) -> f A) g
g ℛ(∀fforall Functor(F), Functor(F'), Functor(f) : F ⇔ F'.
iff @F ℛ((B -> f B) -> f A) g@F'
gforall Functor(F), Functor(F'), Functor(f) : F ⇔ F'.
iff forall l :: B -> F B, l' :: B -> F' B.
if l ℛ(B -> f B) l' then g l ℛ(f A) g l'
```

Specializing to *higher order functions* `f⃗ :: ∀ab. (a -> b) -> F a -> F' b`

(rather than a relational action `f`

), we get

```
forall Functor(F), Functor(F'), Functor(f) : F ⇔ F'.
forall l :: B -> F B, l' :: B -> F' B.
if l ℛ(B -> f⃗ B) l' then g l ℛ(f⃗ A) g l'
forall Functor(F), Functor(F'), Functor(f) : F ⇔ F'.
iff forall l :: B -> F B, l' :: B -> F' B.
if f⃗ id . l ≡ l' . id then f⃗ id (g l) ≡ g l'
-- simplify
forall Functor(F), Functor(F'), Functor(f) : F ⇔ F'.
iff forall l :: B -> F B.
id (g l) ≡ g (f⃗ id . l) f⃗
```

for any `Functor`

respecting `f⃗`

; we can now apply the same reasoning as we did in the previous section, and give the following free theorem instead:

`. l) k (g l) ≡ g (k `

for any polymorphic function (that is, natural transformation) `k :: ∀a. F a -> F' a`

and function `l :: B -> F B`

. This property is essential when proving that the above representation of a lens is isomorphic to a pair of a setter and a getter; see Functor is to Lens as Applicative is to Biplate, Section 4, for details.

## Conclusions

Parametricity allows us to formally derive what we can conclude about a function by only looking at its type. We’ve covered a lot of material in this tutorial, but there is a lot more out there still. If you want to know more, here are some additional references.

- Free Theorems Involving Type Constructor Classes is a very accessible paper by Janis Voigtländer that describes how to deal with type constructor classes in free theorems, and gives lots of examples involving monads. If you prefer, you can also watch the video of the presentation. Janis also has a slide set with an introduction to free theorems and some of the underlying theory.
- Proofs for Free: Parametricity for dependent types by Jean-Philippe Bernardy, Patrik Jansson and Ross Paterson extends the theory of parametricity to dependent types.
- Although it’s not about parametricity per se, A Representation Theorem for Second-Order Functionals by Mauro Jaskelioff and Russell O’Connor gives a general (categorical) result that can be used to derive properties of types such as van Laarhoven lenses (sadly, the theorem does not seem to cover prisms).

##### Acknowledgements

Thanks to Auke Booij on `#haskell`

for his helpful feedback on both parts of this blog post.