Free theorems were popularized by Wadler in his 1989 paper "Theorems for Free!". In that paper only polymorphism over types is considered. In 2009, Voigtländer illustrates how this can be extended to polymorphism over type constructors with class constraints in his paper "Free Theorems Involving Type Constructor Classes". He uses polymorphism over Monads for his example. In order to learn to apply this theory I will use a very simple exercise only involving Functors. Be aware that our reasoning will be "fast and loose" which is a technical term that means that our results only apply to total values.

The exercise here is to prove that the type `A` → `B` and the polymorphic type ∀`κ`:Functor. `κ` `A` → `κ` `B` are isomorphic. The intuition is that all a polymorphic function of type ∀`κ`:Functor. `κ` `A` → `κ` `B` can do is map some internally held function of type `A` → `B`. The claim is that the following pair of functions witness the isomorphism:

iso_{1} : (`A` → `B`) → ∀`κ`:Functor. `κ` `A` → `κ` `B`

iso_{1} `x` := Λ`κ`. λ`l`. map_{κ} `x` `l`

iso_{2} : (∀`κ`:Functor. `κ` `A` → `κ` `B`) → `A` → `B`

iso_{2} `y` := `y` Id

In the above we use Id, which is the identity functor.

To prove this we need to show that both ways of composing these two functions produce the identity function. One way is easy:

iso_{2} (iso_{1} `x`) `a` =

map_{Id} `x` `a` =
`x` `a`

So we see that iso_{2} (iso_{1} `x`) = `x` as required. The other direction is harder.

iso_{1} (iso_{2} `y`) `κ` `l` =

map_{κ} (`y` Id) `l`

At this point we get stuck. We need to show that map_{κ} (`y` Id) `l` = `y` `κ` `l` for an arbitrary functor `κ` and arbitrary `l` : `κ` `A`. To continue the proof, we are going to have to use the parametricity of `y` : ∀`κ`:Functor. `κ` `A` → `κ` `B`.

Parametricity of `y` gives us a free theorem which states that given two functors `F`_{1} and `F`_{2} and a functor morphism `η` : ∀`α`. `F`_{1} `α` → `F`_{2} `α` we have that:

`η`_{B} ∘ `y` `F`_{1} = `y` `F`_{2} ∘ `η`_{A}

A functor morphism is better known as a natural transformation. A natural transformation `η` : ∀`α`. `F`_{1} `α` → `F`_{2} `α` is required to satisfy the following law: For any types `C` and `D` and any function `g` : `C` → `D`, we require that,

map_{F2} `g` ∘ `η`_{C} = `η`_{D} ∘ map_{F1} `g`

My proof will proceed in two stages. The first lemma I will prove is:

`y`Id =`y`(Env`A`) id_{A}

Here Env `A` is the environment functor (it is also a monad) aka the reader functor, and id is the identity function. To prove our lemma it suffices to show that `y` Id `a` = `y` (Env `A`) id `a` for an arbitrary `a` : A. We will use the free theorem to prove this with a natural transformation from (Env `A`) to Id defined as

`η`_{1} : ∀`α`. Env `A` `α` → Id `α`
`η`_{1} := Λ`α`. λ`h`. `h` `a`

However, we must first prove that this is a natural transformation; i.e. we need to prove that map_{Id} `g` ∘ `η`_{1C} = `η`_{1D} ∘ map_{(Env A)} `g`:

map_{Id} `g` (`η`_{1C} `h`) =
`g` (`h` `a`) =

(`g` ∘ `h`) `a` =
`η`_{1D} (map_{(Env A)} `g` `h`)

Now we can apply our free theorem using the natural transformation `&eta`_{1} to prove the lemma.

`y` Id `a` =
`y` Id (`η`_{1A} id_{A}) =
`η`_{1B} (`y` (Env `A`) id_{A}) =
`y` (Env `A`) id_{A} `a`

This completes Lemma 1. To finish our proof of the isomorphism we only need to prove Lemma 2:

- map
_{κ}(`y`(Env`A`) id_{A})`l`=`y``κ``l`

To prove this we use the free theorem with a new natural transformation from Env `A` to `κ`:

`η`_{2} : ∀`α`. Env `A` `α` → `κ` `α`
`η`_{2} := Λ`α`. λ`h`. (map_{κ} `h` `l`)

Again, we need to show that `η`_{2} is a natural transformation, meaning we need to show that map_{κ} `g` ∘ `η`_{2C} = `η`_{2D} ∘ map_{(Env A)} `g`.

map_{κ} `g` (`η`_{2C} `h`) =

map_{κ} `g` (map_{κ} `h` `l`) =

map_{κ} (`g` ∘ `h`) `l` =
`η`_{2D} (map_{(Env A)} `g` `h`)

Now we can apply our free theorem using the natural transformation `η`_{2} to prove Lemma 2.

map_{κ} (`y` (Env `A`) id_{A}) `l` =
`η`_{2B} (`y` (Env `A`) id_{A}) =
`y` `κ` (`η`_{2A} id_{A}) =
`y` `κ` (map_{κ} id_{A} l) =
`y` `κ` `l`

This completes the proof of the isomorphism. Perhaps it can be simplified by combining the two step into one, but I am satisfied with this two step process.

r6research: ←Instantiating Meaning Formulasr6research: →Lenses Are Exactly the Coalgebras for the Store Comonad