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:
iso1 : (A → B) → ∀κ:Functor. κ A → κ B
iso1 x := Λκ. λl. mapκ x l
iso2 : (∀κ:Functor. κ A → κ B) → A → B
iso2 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:
iso2 (iso1 x) a =
mapId x a =
So we see that iso2 (iso1 x) = x as required. The other direction is harder.
iso1 (iso2 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 F1 and F2 and a functor morphism η : ∀α. F1 α → F2 α we have that:
ηB ∘ y F1 = y F2 ∘ ηA
A functor morphism is better known as a natural transformation. A natural transformation η : ∀α. F1 α → F2 α is required to satisfy the following law: For any types C and D and any function g : C → D, we require that,
mapF2 g ∘ ηC = ηD ∘ mapF1 g
My proof will proceed in two stages. The first lemma I will prove is:
- y Id = y (Env A) idA
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 mapId g ∘ η1C = η1D ∘ map(Env A) g:
mapId 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 &eta1 to prove the lemma.
y Id a =
y Id (η1A idA) =
η1B (y (Env A) idA) =
y (Env A) idA a
This completes Lemma 1. To finish our proof of the isomorphism we only need to prove Lemma 2:
- mapκ (y (Env A) idA) 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) idA) l =
η2B (y (Env A) idA) =
y κ (η2A idA) =
y κ (mapκ idA 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.