# Initial and final encodings of free monads

Free monads are often introduced as an algebraic data type, an initial encoding:

`data Free f a = Pure a | Free (f (Free f a))`

Thanks to that, the term “free monads” tends to be confused with that encoding, even though “free monads” originally refers to a representation-independent idea. Dually, there is a final encoding of free monads:

`type Free' f a = (forall m. MonadFree f m => m a)`

where `MonadFree`

is the following class:

```
class Monad m => MonadFree f m where
free :: f (m a) -> m a
```

The two types `Free`

and `Free'`

are isomorphic.
An explanation *a posteriori* is that free monads are unique up to isomorphism.
In this post, we will prove that they are isomorphic more directly,^{1}
in Coq.

In other words, there are two functions:

```
fromFree' :: Free' f a -> Free f a
toFree' :: Free f a -> Free' f a
```

such that, for all `u :: Free f a`

,

`fromFree' (toFree' u) = u -- easy`

and for all `u :: Free' f a`

,

`toFree' (fromFree' u) = u -- hard`

(Also, these functions are monad morphisms.)

The second equation is hard to prove because it relies on a subtle
fact about polymorphism. If you have a polymorphic function `forall m ...`

,
it can only interact with `m`

via operations provided as parameters—in the
`MonadFree`

dictionary. The equation crashes down if you can perform
some kind of case analysis on types, such as `isinstanceof`

in certain
languages. This idea is subtle because, how do you turn this negative property
“does not use `isinstanceof`

” into a positive, useful fact about the functions
of a language?

Parametricity is the name given to such properties. You can get a good
intuition for it with some practice. For example, most people can convince
themselves that `forall a. a -> a`

is only inhabited by the identity function.
But formalizing it so you can validate your intuition is a more mysterious art.

## Proof sketch

First, unfolding some definitions, the equation we want to prove will simplify to the following:

`foldFree (u @(Free f)) = u @m`

where `u :: forall m. MonadFree f m => m a`

is specialized at `Free f`

on the
left, at an arbitrary `m`

on the right, and `foldFree :: Free f a -> m a`

is a certain function we do not need to look into for now.

The main idea is that those different specializations of `u`

are *related*
by a *parametricity theorem* (aka. *free theorem*).

For all monads`m1`

,`m2`

that are instances of`MonadFree f`

, and for any relation`r`

between`m1`

and`m2`

, if`r`

satisfies`$CERTAIN_CONDITIONS`

, then`r`

relates`u @m1`

and`u @m2`

.

In this case, we will let `r`

relate `u1 :: Free f a`

and `u2 :: m a`

when:

`foldFree u1 = u2`

As it turns out, `r`

will satisfy `$CERTAIN_CONDITIONS`

, so that the
parametricity theorem above applies. This
yields exactly the desired conclusion:

`foldFree (u @(Free f)) = u @m`

It is going to be a **gnarly** exposition of definitions before we can even get
to the proof, and the only reason I can think of to stick around is morbid
curiosity. But I had the proof and I wanted to do something
with it.^{2}

## Formalization in Coq

## Imports and setting options

From Coq Require Import Morphisms. Set Implicit Arguments. Set Contextual Implicit.

### Initial free monads

Right off the bat, the first hurdle is that we cannot actually write the initial `Free`

in Coq.
To guarantee that all functions terminate and to prevent logical
inconsistencies, Coq imposes restrictions about what recursive types can be
defined. Indeed, `Free`

could be used to construct an infinite loop by instantiating
it with a contravariant functor `f`

. The following snippet shows how we can
inhabit the empty type `Void`

, using only non-recursive definitions, so it’s
fair to put the blame on `Free`

:

```
newtype Cofun b a = Cofun (a -> b)
omicron :: Free (Cofun Void) Void -> Void
omicron (Pure y) = y
omicron (Free (Cofun z)) = z (Free (Cofun z))
omega :: Void
omega = omicron (Free (Cofun omicron))
```

To bypass that issue, we can tweak the definition of `Free`

into what you might
know as the *freer monad*, or the *operational monad*.
The key difference is that the recursive occurrence of `Free f a`

is no longer
under an abstract `f`

, but a concrete `(->)`

instead.

```
Inductive Free (f : Type -> Type) (a : Type) : Type :=
| Pure : a -> Free f a
| Bind : forall e, f e -> (e -> Free f a) -> Free f a
.
```

#### Digression on containers

With that definition, it is no longer necessary for `f`

to be a functor—it’s
even undesirable because of size issues. Instead, `f`

should rather be thought
of as a type of “shapes”, containing “positions” of type `e`

, and that induces
a functor by assigning values to those positions (via the function `e -> Free f a`

here); such an `f`

is also known as a “container”.

For example, the `Maybe`

functor consists of two “shapes”: `Nothing`

, with no
positions (indexed by `Void`

), and `Just`

, with one position (indexed by `()`

).
Those shapes are defined by the following GADT, the `Maybe`

container:

```
data PreMaybe _ where
Nothing_ :: PreMaybe Void
Just_ :: PreMaybe ()
```

A container extends into a functor, using a construction that some call `Coyoneda`

:

```
data Maybe' a where
MkMaybe' :: forall a e. PreMaybe e -> (e -> a) -> Maybe' a
data Coyoneda f a where
Coyoneda :: forall f a e. f e -> (e -> a) -> Coyoneda f a
```

`Freer f a`

(where `Freer`

is called `Free`

here in Coq) coincides with
`Free (Coyoneda f) a`

(for the original definition of `Free`

at the top).
If `f`

is already a functor, then it is observationally equivalent to `Coyoneda f`

.

`Monad`

and `MonadFree`

The `Monad`

class hides no surprises. For simplicity we skip the `Functor`

and `Applicative`

classes. Like in C, `return`

is a keyword in Coq, so we have to settle for another name.

Class Monad (m : Type -> Type) : Type := { pure : forall {a}, a -> m a ; bind : forall {a b}, m a -> (a -> m b) -> m b }. (* The braces after `forall` make the arguments implicit. *)

Our `MonadFree`

class below is different than in Haskell because of the switch
from functors to containers (see previous section).
In the original `MonadFree`

, the method `free`

takes an argument of type `f (m a)`

, where the idea is to “interpret” the outer layer `f`

, and “carry on” with
a continuation `m a`

. Containers encode that outer layer without the
continuation.^{3}

Class MonadFree {f m : Type -> Type} `{Monad m} : Type := { free : forall {x}, f x -> m x }. (* Some more implicit arguments nonsense. *) Arguments MonadFree f m {_}.

Here comes the final encoding of free monads. The resemblance to the Haskell code above should be apparent in spite of some funny syntax.

```
Definition Free' (f : Type -> Type) (a : Type) : Type :=
forall m `(MonadFree f m), m a.
```

Type classes in Coq are simply types with some extra type inference rules to
infer dictionaries. Thus, the definition of `Free'`

actually desugars to
a function type `forall m, Monad m -> MonadFree f m -> m a`

.
A value `u : Free' f a`

is a function whose arguments are a type
constructor `m`

, followed by two dictionaries of the `Monad`

and `MonadFree`

classes.
We specialize `u`

to a monad `m`

by writing `u m _ _`

, applying `u`

to the type
constructor `m`

and two holes (underscores) for the dictionaries, whose
contents will be inferred via type class resolution.
See for example `fromFree'`

below.

While we’re at it, we can define the instances of `Monad`

and `MonadFree`

for
the initial encoding `Free`

.

Fixpoint bindFree {f a b} (u : Free f a) (k : a -> Free f b) : Free f b := match u with | Pure a => k a | Bind e h => Bind e (fun x => bindFree (h x) k) end. #[global] Instance Monad_Free f : Monad (Free f) := {| pure := @Pure f ; bind := @bindFree f |}. #[global] Instance MonadFree_Free f : MonadFree f (Free f) := {| free A e := Bind e (fun a => Pure a) |}.

### Interpretation of free monads

To show that those monads are equivalent, we must exhibit a mapping going both ways.

The easy direction is from the final `Free'`

to the initial `Free`

: with the
above instances of `Monad`

and `MonadFree`

, just monomorphize the polymorph.

```
Definition fromFree' {f a} : Free' f a -> Free f a :=
fun u => u (Free f) _ _.
```

The other direction is obtained via a fold of `Free f`

, which allows us to interpret it
in any instance of `MonadFree f`

: replace `Bind`

with `bind`

, interpret the
first operand with `free`

, and recurse in the second operand.

Fixpoint foldFree {f m a} `{MonadFree f m} (u : Free f a) : m a := match u with | Pure a => pure a | Bind e k => bind (free e) (fun x => foldFree (k x)) end. Definition toFree' {f a} : Free f a -> Free' f a := fun u M _ _ => foldFree u.

### Equality

In everyday mathematics, equality is a self-evident notion that we take for granted. But if you want to minimize your logical foundations, you do not need equality as a primitive. Equations are just equivalences, where the equivalence relation is kept implicit.

Who even decides what the rules for reasoning about equality are anyway?
You decide, by picking the underlying equivalence relation.
^{4}

Here is a class for equality. It is similar to `Eq`

in Haskell,
but it is propositional (`a -> a -> Prop`

) rather than boolean (`a -> a -> Bool`

),
meaning that equality doesn’t have to be decidable.

Class PropEq (a : Type) : Type := propeq : a -> a -> Prop.

For example, for inductive types, a common equivalence can be defined as
another inductive type which equates constructors and their fields recursively.
Here it is for `Free`

:

Inductive eq_Free f a : PropEq (Free f a) := | eq_Free_Pure x : eq_Free (Pure x) (Pure x) | eq_Free_Bind p (e : f p) k1 k2 : (forall x, eq_Free (k1 x) (k2 x)) -> eq_Free (Bind e k1) (Bind e k2) . (* Register it as an instance of PropEq *)

Having defined equality for `Free`

, we can state and prove one half of the
isomorphism between `Free`

and `Free'`

.

`f`**: **Type -> Type

`a`**: **Type

`u`**: **Free f a

fromFree' (toFree' u) = u

The proof is straightforward by induction, case analysis (which is performed as part of induction), and simplification.

f:Type -> Typea:Typeu:Free f afromFree' (toFree' u) = uf:Type -> Typea:Typea0:afromFree' (toFree' (Pure a0)) = Pure a0f:Type -> Typea, e:Typef0:f ef1:e -> Free f aH:forall e : e, fromFree' (toFree' (f1 e)) = f1 efromFree' (toFree' (Bind f0 f1)) = Bind f0 f1all: constructor; auto. Qed.f:Type -> Typea:Typea0:aPure a0 = Pure a0f:Type -> Typea, e:Typef0:f ef1:e -> Free f aH:forall e : e, fromFree' (toFree' (f1 e)) = f1 eBind f0 (fun x : e => foldFree (f1 x)) = Bind f0 f1

### Equality on final encodings, naive attempts

To state the other half of the isomorphism (`toFree' (fromFree' u) = u`

),
it is less obvious what the right equivalence relation on `Free'`

should be.
When are two polymorphic values `u1, u2 : forall m `(MonadFree f m), m a`

equal?
A fair starting point is that all of their specializations must be equal.
“Equality” requires an instance of `PropEq`

, which must be introduced as an
extra parameter.

(* u1 and u2 are "equal" when all of their specializations (u1 m _ _) and (u2 m _ _) are equal. *) Definition eq_Free'_very_naive f a (u1 u2 : Free' f a) : Prop := forall m `(MonadFree f m) `(forall x, PropEq (m x)), u1 m _ _ = u2 m _ _.

That definition is flagrantly inadequate: so far, a `PropEq`

instance can be
any relation, including the empty relation (which never holds), and the `Monad`

instance
(as a superclass of `MonadFree`

) might be unlawful. In our
desired theorem, `toFree' (fromFree' u) = u`

, the two sides use *a priori*
different combinations of `bind`

and `pure`

, so we expect to rely on laws to
be able to rewrite one side into the other.

In programming, we aren’t used to proving that implementations satisfy their laws,
so there is always the possibility that a `Monad`

instance is unlawful.
In math, the laws are in the definitions; if something doesn’t satisfy the
monad laws, it’s not a monad. Let’s irk some mathematicians and
say that a *lawful monad* is a monad that satisfies the monad laws.
Thus we will have one `Monad`

class for the operations only, and one
`LawfulMonad`

class for the laws they should satisfy.
Separating code and proofs that way helps to organize things.
Code is often much simpler than the proofs about it, since the latter
necessarily involves dependent types.

```
Class LawfulMonad {m} `{Monad m} `{forall a, PropEq (m a)} : Prop :=
{ Equivalence_LawfulMonad :> forall a, Equivalence (propeq (a := m a))
; propeq_bind : forall a b (u u' : m a) (k k' : a -> m b),
u = u' -> (forall x, k x = k' x) -> bind u k = bind u' k'
; bind_pure : forall a (u : m a),
bind u (pure (a := a)) = u
; pure_bind : forall a b (x : a) (k : a -> m b),
bind (pure x) k = k x
; bind_bind : forall a b c (u : m a) (k : a -> m b) (h : b -> m c),
bind (bind u k) h = bind u (fun x => bind (k x) h)
}.
```

The three monad laws should be familiar (`bind_pure`

, `pure_bind`

, `bind_bind`

).
In those equations, “`=`

” denotes a particular equivalence relation, which is now a
parameter/superclass of the class. Once you give up on equality as a primitive notion,
algebraic structures must now carry their own equivalence relations.
The requirement that it is an *equivalence relation* also becomes an explicit law
(`Equivalence_LawfulMonad`

), and we expect that operations (in this case, `bind`

)
preserve the equivalence (`propeq_bind`

). Practically speaking, that last fact
allows us to rewrite subexpressions locally, otherwise we could only apply the
monad laws at the root of an expression.

A less naive equivalence on `Free'`

is thus to restrict the quantification
to lawful instances:

```
Definition eq_Free'_naive f a (u1 u2 : Free' f a) : Prop :=
forall m `(MonadFree f m) `(forall x, PropEq (m x)) `(!LawfulMonad (m := m)),
u1 m _ _ = u2 m _ _.
```

That is a quite reasonable definition of equivalence for `Free'`

. In other circumstances,
it could have been useful. Unfortunately, it is too strong here:
we cannot prove the equation `toFree' (fromFree' u) = u`

with that interpretation of `=`

.
Or at least I couldn’t figure out a solution.
We will need more assumptions to be able to apply the parametricity theorem of
the type `Free'`

. To get there, we must formalize Reynolds’ relational interpretation of types.

### Types as relations

The core technical idea in Reynolds’ take on parametricity is to
interpret a type `t`

as a relation `Rt : t -> t -> Prop`

. Then, the
**parametricity theorem** is that all terms `x : t`

are related to themselves
by `Rt`

(`Rt x x`

is true).
If `t`

is a polymorphic type, that theorem connects different specializations
of a same term `x : t`

, and that allows us to formalize arguments that rely on
“parametricity” as a vague idea.

For example, if `t = (forall a, a -> a)`

, then `Rt`

is the following relation,
which says that two functions `f`

and `f'`

are related if for any relation `Ra`

(on any types), `f`

and `f'`

send related inputs (`Ra x x'`

) to related outputs
(`Ra (f a x) (f' a' x')`

).

```
Rt f f' =
forall a a' (Ra : a -> a' -> Prop),
forall x x', Ra x x' -> Ra (f a x) (f' a' x')
```

If we set `Ra x x'`

to mean “`x`

equals an arbitrary constant `z0`

”
(ignoring `x'`

, i.e., treating `Ra`

as a unary relation), the above relation
`Rt`

amounts to saying that `f z0 = z0`

, from which we deduce that `f`

must be
the identity function.

The fact that `Rt`

is a relation is not particularly meaningful to the parametricity
theorem, where terms are simply related to themselves, but it is a feature of
the construction of `Rt`

: the relation for a composite type `t1 -> t2`

combines
the relations for the components `t1`

and `t2`

, and we could not get the same result
with only unary predicates throughout.^{5} More formally, we define
a relation `R[t]`

by induction on `t`

, between the types `t`

and `t'`

,
where `t'`

is the result of renaming all variables `x`

to `x'`

in `t`

(including binders). The two most interesting cases are:

`t`

starts with a quantifier`t = forall a, _`

, for a type variable`a`

. Then the relation`R[forall a, _]`

between the polymorphic`f`

and`f'`

takes two arbitrary types`a`

and`a'`

to specialize`f`

and`f'`

with, and a relation`Ra : a -> a' -> Prop`

, and relates`f a`

and`f' a'`

(recursively), using`Ra`

whenever recursion reaches a variable`a`

.`t`

is an arrow`t1 -> t2`

, then`R[t1 -> t2]`

relates functions that send related inputs to related outputs.

In summary:

```
R[forall a, t](f, f') = forall a a' Ra, R[t](f a)(f' a')
R[a](f, f') = Ra(f, f')
-- Ra should be in scope when a is in scope.
R[t1 -> t2](f, f') = forall x x', R[t1](x, x') -> R[t2](f x, f' x')
```

That explanation was completely unhygienic, but refer to
Reynolds’ paper or Wadler’s *Theorems for free!* for more formal details.

For sums (`Either`

/`sum`

) and products (`(,)`

/`prod`

), two values are related if
they start with the same constructor, and their fields are related (recursively).
This can be deduced from the rules above applied to the Church encodings of
sums and products.

### Type constructors as relation transformers

While types `t : Type`

are associated to relations `Rt : t -> t -> Prop`

,
type constructors `m : Type -> Type`

are associated to relation transformers
(functions on relations) `Rm : forall a a', (a -> a' -> Prop) -> (m a -> m a' -> Prop)`

.
It is usually clear what’s what from the context, so we will often
refer to “relation transformers” as just “relations”.

For example, the initial `Free f a`

type gets interpreted to the relation `RFree Rf Ra`

defined as follows. Two values `u1 : Free f1 a1`

and `u2 : Free f2 a2`

are related by `RFree`

if either:

`u1 = Pure x1`

,`u2 = Pure x2`

, and`x1`

and`x2`

are related (by`Ra`

); or`u1 = Bind e1 k1`

,`u2 = Bind e2 k2`

,`e1`

and`e2`

are related, and`k1`

and`k2`

are related (recursively).

We thus have one rule for each constructor (`Pure`

and `Bind`

)
in which we relate each field (`Ra x1 x2`

in `RFree_Pure`

; `Rf _ _ _ y1 y2`

and `RFree Rf Ra (k1 x1) (k2 x2)`

in `RFree_Bind`

).
Let us also remark that the existential type `e`

in `Bind`

becomes an existential relation `Re`

in `RFree_Bind`

.

```
Inductive RFree {f₁ f₂ : Type -> Type}
(Rf : forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> f₁ a₁ -> f₂ a₂ -> Prop)
{a₁ a₂ : Type} (Ra : a₁ -> a₂ -> Prop) : Free f₁ a₁ -> Free f₂ a₂ -> Prop :=
| RFree_Pure : forall (x₁ : a₁) (x₂ : a₂),
Ra x₁ x₂ -> RFree Rf Ra (Pure x₁) (Pure x₂)
| RFree_Bind : forall (e₁ e₂ : Type) (Re : e₁ -> e₂ -> Prop) (y₁ : f₁ e₁) (y₂ : f₂ e₂),
Rf e₁ e₂ Re y₁ y₂ ->
forall (k₁ : e₁ -> Free f₁ a₁) (k₂ : e₂ -> Free f₂ a₂),
(forall (x₁ : e₁) (x₂ : e₂),
Re x₁ x₂ -> RFree Rf Ra (k₁ x₁) (k₂ x₂)) ->
RFree Rf Ra (Bind y₁ k₁) (Bind y₂ k₂).
```

Inductive relations such as `RFree`

, indexed by types with existential
quantifications such as `Free`

, are a little terrible to work with
out-of-the-box—especially if you’re allergic to UIP.
Little “inversion lemmas” like the following make them a bit nicer by
reexpressing those relations in terms of some standard building blocks which
leave less of a mess when decomposed.

f₁, f₂:Type -> TypeRf:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> f₁ a₁ -> f₂ a₂ -> Propa₁, a₂:TypeRa:a₁ -> a₂ -> Propu₁:Free f₁ a₁u₂:Free f₂ a₂RFree Rf Ra u₁ u₂ -> match u₁ with | Pure a₁ => match u₂ with | Pure a₂ => Ra a₁ a₂ | Bind _ _ => False end | @Bind _ _ e y₁ k₁ => match u₂ with | Pure _ => False | @Bind _ _ e0 y₂ k₂ => exists Re : e -> e0 -> Prop, Rf e e0 Re y₁ y₂ /\ (forall (x₁ : e) (x₂ : e0), Re x₁ x₂ -> RFree Rf Ra (k₁ x₁) (k₂ x₂)) end endintros []; eauto. Qed.f₁, f₂:Type -> TypeRf:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> f₁ a₁ -> f₂ a₂ -> Propa₁, a₂:TypeRa:a₁ -> a₂ -> Propu₁:Free f₁ a₁u₂:Free f₂ a₂RFree Rf Ra u₁ u₂ -> match u₁ with | Pure a₁ => match u₂ with | Pure a₂ => Ra a₁ a₂ | Bind _ _ => False end | @Bind _ _ e y₁ k₁ => match u₂ with | Pure _ => False | @Bind _ _ e0 y₂ k₂ => exists Re : e -> e0 -> Prop, Rf e e0 Re y₁ y₂ /\ (forall (x₁ : e) (x₂ : e0), Re x₁ x₂ -> RFree Rf Ra (k₁ x₁) (k₂ x₂)) end end

Type classes, which are (record) types, also get interpreted in the same way.
Since `Monad`

is parameterized by a type constructor `m`

, the relation `RMonad`

between `Monad`

instances is parameterized by a relation between two type
constructors `m1`

and `m2`

.
Two instances of `Monad`

, i.e., two values of type `Monad m`

for some `m`

, are related
if their respective fields, i.e., `pure`

and `bind`

, are related.
`pure`

and `bind`

are functions, so two instances are related when they send related inputs
to related outputs.

```
Record RMonad (m₁ m₂ : Type -> Type)
(Rm : forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> m₁ a₁ -> m₂ a₂ -> Prop)
`{Monad m₁} `{Monad m₂} : Prop :=
{ RMonad_pure : forall (t₁ t₂ : Type) (Rt : t₁ -> t₂ -> Prop) (x₁ : t₁) (x₂ : t₂),
Rt x₁ x₂ -> Rm t₁ t₂ Rt (pure x₁) (pure x₂)
; RMonad_bind : forall (t₁ t₂ : Type) (Rt : t₁ -> t₂ -> Prop)
(u₁ u₂ : Type) (Ru : u₁ -> u₂ -> Prop) (x₁ : m₁ t₁) (x₂ : m₂ t₂),
Rm t₁ t₂ Rt x₁ x₂ ->
forall (k₁ : t₁ -> m₁ u₁) (k₂ : t₂ -> m₂ u₂),
(forall (x₁ : t₁) (x₂ : t₂),
Rt x₁ x₂ -> Rm u₁ u₂ Ru (k₁ x₁) (k₂ x₂)) ->
Rm u₁ u₂ Ru (bind x₁ k₁) (bind x₂ k₂)
}.
```

`MonadFree`

also gets translated to a relation `RMonadFree`

. Related inputs, related outputs.

```
Record RMonadFree (f₁ f₂ : Type -> Type)
(Rf : forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> f₁ a₁ -> f₂ a₂ -> Prop)
(m₁ m₂ : Type -> Type)
(Rm : forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> m₁ a₁ -> m₂ a₂ -> Prop)
`{MonadFree f₁ m₁} `{MonadFree f₂ m₂} : Prop :=
{ RMonadFree_free : forall (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (x₁ : f₁ a₁) (x₂ : f₂ a₂),
Rf a₁ a₂ Ra x₁ x₂ -> Rm a₁ a₂ Ra (free x₁) (free x₂)
}.
```

Note that `RMonad`

and `RMonadFree`

are “relation transformer transformers”, since they
take relation transformers as arguments, to produce a relation between class dictionaries.

We can now finally translate the final `Free'`

to a relation.
Two values `u1 : Free' f1 a1`

and `u2 : Free' f2 a2`

are related
if, for any two monads `m1`

and `m2`

, with a relation transformer `Rm`

,
whose `Monad`

and `MonadFree`

instances are related by `RMonad`

and `RMonadFree`

,
`Rm`

relates `u1 m1 _ _`

and `u2 m2 _ _`

.

```
Definition RFree' {f₁ f₂} Rf {a₁ a₂} Ra (u₁ : Free' f₁ a₁) (u₂ : Free' f₂ a₂) : Prop :=
forall m₁ m₂ `(MonadFree f₁ m₁) `(MonadFree f₂ m₂) Rm
(pm : RMonad Rm) (pf : RMonadFree Rf Rm),
Rm _ _ Ra (u₁ m₁ _ _) (u₂ m₂ _ _).
```

The above translation of types into relations can be automated by a tool such as
*paramcoq*. However *paramcoq* currently constructs relations in
`Type`

instead of `Prop`

, which got me stuck in universe inconsistencies.
That’s why I’m declaring `Prop`

relations the manual way here.

The parametricity theorem says that any `u : Free' f a`

is related to itself
by `RFree'`

(for some canonical relations on `f`

and `a`

). It is a theorem about
the language Coq which we can’t prove within Coq. Rather than postulate it,
we will simply add the required `RFree' _ _ u u`

assumption to our proposition
(`from_to`

below).
Given a concrete `u`

, it should be straightforward to prove that assumption
case-by-case in order to apply that proposition.

These “relation transformers” are a bit of a mouthful to spell out,
and they’re usually guessable from the type constructor (`f`

or `m`

),
so they deserve a class, that’s a higher-order counterpart to `PropEq`

(like `Eq1`

is to `Eq`

in Haskell).

```
Class PropEq1 (m : Type -> Type) : Type :=
propeq1 : forall a₁ a₂, (a₁ -> a₂ -> Prop) -> m a₁ -> m a₂ -> Prop.
```

Given a `PropEq1 m`

instance, we can apply it to the relation `eq`

to get a plain relation which seems a decent enough default for `PropEq (m a)`

.

```
#[global]
Instance PropEq_PropEq1 {m} `{PropEq1 m} {a} : PropEq (m a) := propeq1 eq.
```

### Really lawful monads

We previously defined a “lawful monad” as a monad with an equivalence relation
(`PropEq (m a)`

). To use parametricity, we will also need a monad `m`

to provide
a relation transformer (`PropEq1 m`

), which subsumes `PropEq`

with the instance
just above.^{6} This extra structure comes with additional laws,
extending our idea of monads to “really lawful monads”.

Class Trans_PropEq1 {m} `{PropEq1 m} : Prop := trans_propeq1 : forall a₁ a₂ (r : a₁ -> a₂ -> Prop) x₁ x₁' x₂ x₂', x₁ = x₁' -> propeq1 r x₁' x₂ -> x₂ = x₂' -> propeq1 r x₁ x₂'. Class ReallyLawfulMonad m `{Monad m} `{PropEq1 m} : Prop := { LawfulMonad_RLM :> LawfulMonad (m := m) ; Trans_PropEq1_RLM :> Trans_PropEq1 (m := m) ; RMonad_RLM : RMonad (propeq1 (m := m)) }. Class ReallyLawfulMonadFree f `{PropEq1 f} m `{MonadFree f m} `{PropEq1 m} : Prop := { ReallyLawfulMonad_RLMF :> ReallyLawfulMonad (m := m) ; RMonadFree_RLMF : RMonadFree (propeq1 (m := f)) (propeq1 (m := m)) }.

We inherit the `LawfulMonad`

laws from before.
The relations `RMonad`

and `RMonadFree`

,
defined earlier, must relate `m`

’s instances of `Monad`

and `MonadFree`

,
for the artificial reason that that’s roughly what `RFree'`

will require.
We also add a generalized transitivity law, which allows us to rewrite
either side of a heterogeneous relation `propeq1 r`

using the homogeneous
one `=`

(which denotes `propeq1 eq`

).

It’s worth noting that there is some redundancy here, that could be avoided
with a bit of refactoring. That generalized transitivity law `Trans_PropEq1`

implies
transitivity of `=`

, which is part of the claim that `=`

is an equivalence
relation in `LawfulMonad`

. And the `bind`

component of `RMonad`

implies
`propeq_bind`

in `LawfulMonad`

, so these `RMonad`

and `RMonadFree`

laws
can also be seen as generalizations of congruence laws to heterogeneous
relations, making them somewhat less artificial than they may seem
at first.

Restricting the definition of equality on the final free monad `Free'`

to
quantify only over really lawful monads yields the right notion of equality
for our purposes, which is to prove the `from_to`

theorem below, validating the
isomorphism between `Free`

and `Free'`

.

```
#[global]
Instance eq_Free' f `(PropEq1 f) a : PropEq (Free' f a) :=
fun u₁ u₂ =>
forall m `(MonadFree f m) `(PropEq1 m) `(!ReallyLawfulMonadFree (m := m)),
u₁ m _ _ = u₂ m _ _.
```

Quickly, let’s get the following lemma out of the way, which says
that `foldFree`

commutes with `bind`

. We’re really saying that `foldFree`

is
a monad morphism but no time to say it properly. The proof of the
next lemma will need this, but it’s also nice to look at this on its own.

f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:forall a : Type, PropEq (m a)LawfulMonad0:LawfulMonada, b:Typeu:Free f ak:a -> Free f bfoldFree (bindFree u k) = bind (foldFree u) (fun x : a => foldFree (k x))f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:forall a : Type, PropEq (m a)LawfulMonad0:LawfulMonada, b:Typeu:Free f ak:a -> Free f bfoldFree (bindFree u k) = bind (foldFree u) (fun x : a => foldFree (k x))f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:forall a : Type, PropEq (m a)LawfulMonad0:LawfulMonada, b:Typea0:ak:a -> Free f bfoldFree (k a0) = bind (pure a0) (fun x : a => foldFree (k x))f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:forall a : Type, PropEq (m a)LawfulMonad0:LawfulMonada, b, e:Typef0:f ef1:e -> Free f ak:a -> Free f bH2:forall e : e, foldFree (bindFree (f1 e) k) = bind (foldFree (f1 e)) (fun x : a => foldFree (k x))bind (free f0) (fun x : e => foldFree (bindFree (f1 x) k)) = bind (bind (free f0) (fun x : e => foldFree (f1 x))) (fun x : a => foldFree (k x))f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:forall a : Type, PropEq (m a)LawfulMonad0:LawfulMonada, b:Typea0:ak:a -> Free f bfoldFree (k a0) = bind (pure a0) (fun x : a => foldFree (k x))apply pure_bind with (k := fun x => foldFree (k x)).f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:forall a : Type, PropEq (m a)LawfulMonad0:LawfulMonada, b:Typea0:ak:a -> Free f bbind (pure a0) (fun x : a => foldFree (k x)) = foldFree (k a0)f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:forall a : Type, PropEq (m a)LawfulMonad0:LawfulMonada, b, e:Typef0:f ef1:e -> Free f ak:a -> Free f bH2:forall e : e, foldFree (bindFree (f1 e) k) = bind (foldFree (f1 e)) (fun x : a => foldFree (k x))bind (free f0) (fun x : e => foldFree (bindFree (f1 x) k)) = bind (bind (free f0) (fun x : e => foldFree (f1 x))) (fun x : a => foldFree (k x))f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:forall a : Type, PropEq (m a)LawfulMonad0:LawfulMonada, b, e:Typef0:f ef1:e -> Free f ak:a -> Free f bH2:forall e : e, foldFree (bindFree (f1 e) k) = bind (foldFree (f1 e)) (fun x : a => foldFree (k x))bind (free f0) (fun x : e => foldFree (bindFree (f1 x) k)) = bind (free f0) (fun x : e => bind ((fun x0 : e => foldFree (f1 x0)) x) (fun x0 : a => foldFree (k x0)))f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:forall a : Type, PropEq (m a)LawfulMonad0:LawfulMonada, b, e:Typef0:f ef1:e -> Free f ak:a -> Free f bH2:forall e : e, foldFree (bindFree (f1 e) k) = bind (foldFree (f1 e)) (fun x : a => foldFree (k x))free f0 = free f0f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:forall a : Type, PropEq (m a)LawfulMonad0:LawfulMonada, b, e:Typef0:f ef1:e -> Free f ak:a -> Free f bH2:forall e : e, foldFree (bindFree (f1 e) k) = bind (foldFree (f1 e)) (fun x : a => foldFree (k x))forall x : e, foldFree (bindFree (f1 x) k) = bind (foldFree (f1 x)) (fun x0 : a => foldFree (k x0))reflexivity.f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:forall a : Type, PropEq (m a)LawfulMonad0:LawfulMonada, b, e:Typef0:f ef1:e -> Free f ak:a -> Free f bH2:forall e : e, foldFree (bindFree (f1 e) k) = bind (foldFree (f1 e)) (fun x : a => foldFree (k x))free f0 = free f0auto. Qed.f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:forall a : Type, PropEq (m a)LawfulMonad0:LawfulMonada, b, e:Typef0:f ef1:e -> Free f ak:a -> Free f bH2:forall e : e, foldFree (bindFree (f1 e) k) = bind (foldFree (f1 e)) (fun x : a => foldFree (k x))forall x : e, foldFree (bindFree (f1 x) k) = bind (foldFree (f1 x)) (fun x0 : a => foldFree (k x0))

### Finally the proof

Our goal is to prove an equation in terms of `eq_Free'`

, which gives us
a really lawful monad as an assumption. We open a section to set up
the same context as that and to break down the proof into more digestible pieces.

Section ISOPROOF. Context {f m} `{MonadFree f m} `{PropEq1 m} `{!ReallyLawfulMonad (m := m)}.

As outlined earlier, parametricity will yield an assumption `RFree' _ _ u u`

,
and we will specialize it with a relation `R`

which relates `u1 : Free f a`

and `u2 : m a`

when `foldFree u1 = u2`

. However, `RFree'`

actually expects a relation
transformer rather than a relation, so we instead define `R`

to relate
`u1 : Free f a1`

and `u2 : Free f a2`

when `propeq1 Ra (foldFree u1) u2`

,
where `Ra`

is a relation given between `a1`

and `a2`

.

`Let R := (fun a₁ a₂ (Ra : a₁ -> a₂ -> Prop) u₁ u₂ => propeq1 Ra (foldFree u₁) u₂).`

The following two lemmas are the “`$CERTAIN_CONDITIONS`

” mentioned earlier,
that `R`

must satisfy, i.e., we prove that `R`

, via `RMonad`

(resp.
`RMonadFree`

), relates the `Monad`

(resp. `MonadFree`

) instances for `Free f`

and `m`

.

f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> PropRMonad Rf, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> PropRMonad Rf, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> Propt₁, t₂:TypeRt:t₁ -> t₂ -> Propx₁:t₁x₂:t₂H2:Rt x₁ x₂R Rt (pure x₁) (pure x₂)f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> Propt₁, t₂:TypeRt:t₁ -> t₂ -> Propu₁, u₂:TypeRu:u₁ -> u₂ -> Propx₁:Free f t₁x₂:m t₂H2:R Rt x₁ x₂k₁:t₁ -> Free f u₁k₂:t₂ -> m u₂H3:forall (x₁ : t₁) (x₂ : t₂), Rt x₁ x₂ -> R Ru (k₁ x₁) (k₂ x₂)R Ru (bind x₁ k₁) (bind x₂ k₂)f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> Propt₁, t₂:TypeRt:t₁ -> t₂ -> Propx₁:t₁x₂:t₂H2:Rt x₁ x₂R Rt (pure x₁) (pure x₂)apply RMonad_RLM; auto.f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> Propt₁, t₂:TypeRt:t₁ -> t₂ -> Propx₁:t₁x₂:t₂H2:Rt x₁ x₂R Rt (Pure x₁) (pure x₂)f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> Propt₁, t₂:TypeRt:t₁ -> t₂ -> Propu₁, u₂:TypeRu:u₁ -> u₂ -> Propx₁:Free f t₁x₂:m t₂H2:R Rt x₁ x₂k₁:t₁ -> Free f u₁k₂:t₂ -> m u₂H3:forall (x₁ : t₁) (x₂ : t₂), Rt x₁ x₂ -> R Ru (k₁ x₁) (k₂ x₂)R Ru (bind x₁ k₁) (bind x₂ k₂)f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> Propt₁, t₂:TypeRt:t₁ -> t₂ -> Propu₁, u₂:TypeRu:u₁ -> u₂ -> Propx₁:Free f t₁x₂:m t₂H2:R Rt x₁ x₂k₁:t₁ -> Free f u₁k₂:t₂ -> m u₂H3:forall (x₁ : t₁) (x₂ : t₂), Rt x₁ x₂ -> R Ru (k₁ x₁) (k₂ x₂)propeq1 Ru (foldFree (bind x₁ k₁)) (bind x₂ k₂)f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> Propt₁, t₂:TypeRt:t₁ -> t₂ -> Propu₁, u₂:TypeRu:u₁ -> u₂ -> Propx₁:Free f t₁x₂:m t₂H2:R Rt x₁ x₂k₁:t₁ -> Free f u₁k₂:t₂ -> m u₂H3:forall (x₁ : t₁) (x₂ : t₂), Rt x₁ x₂ -> R Ru (k₁ x₁) (k₂ x₂)foldFree (bind x₁ k₁) = ?x₁'f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> Propt₁, t₂:TypeRt:t₁ -> t₂ -> Propu₁, u₂:TypeRu:u₁ -> u₂ -> Propx₁:Free f t₁x₂:m t₂H2:R Rt x₁ x₂k₁:t₁ -> Free f u₁k₂:t₂ -> m u₂H3:forall (x₁ : t₁) (x₂ : t₂), Rt x₁ x₂ -> R Ru (k₁ x₁) (k₂ x₂)propeq1 Ru ?x₁' ?x₂f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> Propt₁, t₂:TypeRt:t₁ -> t₂ -> Propu₁, u₂:TypeRu:u₁ -> u₂ -> Propx₁:Free f t₁x₂:m t₂H2:R Rt x₁ x₂k₁:t₁ -> Free f u₁k₂:t₂ -> m u₂H3:forall (x₁ : t₁) (x₂ : t₂), Rt x₁ x₂ -> R Ru (k₁ x₁) (k₂ x₂)?x₂ = bind x₂ k₂apply foldFree_bindFree.f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> Propt₁, t₂:TypeRt:t₁ -> t₂ -> Propu₁, u₂:TypeRu:u₁ -> u₂ -> Propx₁:Free f t₁x₂:m t₂H2:R Rt x₁ x₂k₁:t₁ -> Free f u₁k₂:t₂ -> m u₂H3:forall (x₁ : t₁) (x₂ : t₂), Rt x₁ x₂ -> R Ru (k₁ x₁) (k₂ x₂)foldFree (bind x₁ k₁) = ?x₁'eapply RMonad_RLM; eauto.f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> Propt₁, t₂:TypeRt:t₁ -> t₂ -> Propu₁, u₂:TypeRu:u₁ -> u₂ -> Propx₁:Free f t₁x₂:m t₂H2:R Rt x₁ x₂k₁:t₁ -> Free f u₁k₂:t₂ -> m u₂H3:forall (x₁ : t₁) (x₂ : t₂), Rt x₁ x₂ -> R Ru (k₁ x₁) (k₂ x₂)propeq1 Ru (bind (foldFree x₁) (fun x : t₁ => foldFree (k₁ x))) ?x₂reflexivity. Qed. Context (Rf : PropEq1 f). Context (RMonadFree_m : RMonadFree propeq1 propeq1).f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> Propt₁, t₂:TypeRt:t₁ -> t₂ -> Propu₁, u₂:TypeRu:u₁ -> u₂ -> Propx₁:Free f t₁x₂:m t₂H2:R Rt x₁ x₂k₁:t₁ -> Free f u₁k₂:t₂ -> m u₂H3:forall (x₁ : t₁) (x₂ : t₂), Rt x₁ x₂ -> R Ru (k₁ x₁) (k₂ x₂)bind x₂ k₂ = bind x₂ k₂f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> PropRf:PropEq1 fRMonadFree_m:RMonadFree propeq1 propeq1RMonadFree Rf Rf, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> PropRf:PropEq1 fRMonadFree_m:RMonadFree propeq1 propeq1RMonadFree Rf Rf, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> PropRf:PropEq1 fRMonadFree_m:RMonadFree propeq1 propeq1a₁, a₂:TypeRa:a₁ -> a₂ -> Propx₁:f a₁x₂:f a₂H2:Rf Ra x₁ x₂R Ra (free x₁) (free x₂)f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> PropRf:PropEq1 fRMonadFree_m:RMonadFree propeq1 propeq1a₁, a₂:TypeRa:a₁ -> a₂ -> Propx₁:f a₁x₂:f a₂H2:Rf Ra x₁ x₂R Ra (free x₁) (free x₂)f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> PropRf:PropEq1 fRMonadFree_m:RMonadFree propeq1 propeq1a₁, a₂:TypeRa:a₁ -> a₂ -> Propx₁:f a₁x₂:f a₂H2:Rf Ra x₁ x₂propeq1 Ra (foldFree (free x₁)) (free x₂)f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> PropRf:PropEq1 fRMonadFree_m:RMonadFree propeq1 propeq1a₁, a₂:TypeRa:a₁ -> a₂ -> Propx₁:f a₁x₂:f a₂H2:Rf Ra x₁ x₂foldFree (free x₁) = ?x₁'f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> PropRf:PropEq1 fRMonadFree_m:RMonadFree propeq1 propeq1a₁, a₂:TypeRa:a₁ -> a₂ -> Propx₁:f a₁x₂:f a₂H2:Rf Ra x₁ x₂propeq1 Ra ?x₁' ?x₂f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> PropRf:PropEq1 fRMonadFree_m:RMonadFree propeq1 propeq1a₁, a₂:TypeRa:a₁ -> a₂ -> Propx₁:f a₁x₂:f a₂H2:Rf Ra x₁ x₂?x₂ = free x₂apply bind_pure.f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> PropRf:PropEq1 fRMonadFree_m:RMonadFree propeq1 propeq1a₁, a₂:TypeRa:a₁ -> a₂ -> Propx₁:f a₁x₂:f a₂H2:Rf Ra x₁ x₂foldFree (free x₁) = ?x₁'f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> PropRf:PropEq1 fRMonadFree_m:RMonadFree propeq1 propeq1a₁, a₂:TypeRa:a₁ -> a₂ -> Propx₁:f a₁x₂:f a₂H2:Rf Ra x₁ x₂propeq1 Ra (free x₁) ?x₂eassumption.f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> PropRf:PropEq1 fRMonadFree_m:RMonadFree propeq1 propeq1a₁, a₂:TypeRa:a₁ -> a₂ -> Propx₁:f a₁x₂:f a₂H2:Rf Ra x₁ x₂propeq1 Ra x₁ ?Goal0reflexivity. Qed. End ISOPROOF.f, m:Type -> TypeH:Monad mH0:MonadFree f mH1:PropEq1 mReallyLawfulMonad0:ReallyLawfulMonadR:=fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂:forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> Free f a₁ -> m a₂ -> PropRf:PropEq1 fRMonadFree_m:RMonadFree propeq1 propeq1a₁, a₂:TypeRa:a₁ -> a₂ -> Propx₁:f a₁x₂:f a₂H2:Rf Ra x₁ x₂free x₂ = free x₂

Here comes the conclusion, which completes our claim that `toFree'`

/`fromFree'`

is
an isomorphism (we proved the other half `to_from`

on the way here).
This equation is under an assumption which parametricity promises to
fulfill, but we will have to step out of the system if we want it right now.

`f`**: **Type -> Type

`Rf`**: **PropEq1 f

`a`**: **Type

`u`**: **Free' f a

RFree' Rf eq u u -> toFree' (fromFree' u) = u

In the proof, we get the assumption `H : RFree' Rf eq u u`

, which we apply
to the above lemmas, `RMonad_foldFree`

and `RMonadFree_foldFree`

,
using the `specialize`

tactic. That yields exactly our desired goal.

f:Type -> TypeRf:PropEq1 fa:Typeu:Free' f aRFree' Rf eq u u -> toFree' (fromFree' u) = uf:Type -> TypeRf:PropEq1 fa:Typeu:Free' f aH:RFree' Rf eq u um:Type -> TypeH0:Monad mH1:MonadFree f mH2:PropEq1 mReallyLawfulMonadFree0:ReallyLawfulMonadFreetoFree' (fromFree' u) H1 = u m H0 H1f:Type -> TypeRf:PropEq1 fa:Typeu:Free' f aH:RFree' Rf eq u um:Type -> TypeH0:Monad mH1:MonadFree f mH2:PropEq1 mReallyLawfulMonadFree0:ReallyLawfulMonadFreefoldFree (u (Free f) Monad_Free MonadFree_Free) = u m H0 H1f:Type -> TypeRf:PropEq1 fa:Typeu:Free' f aH:forall (m₁ m₂ : Type -> Type) (H : Monad m₁) (H0 : MonadFree f m₁) (H1 : Monad m₂) (H2 : MonadFree f m₂) (Rm : forall a₁ a₂ : Type, (a₁ -> a₂ -> Prop) -> m₁ a₁ -> m₂ a₂ -> Prop), RMonad Rm -> RMonadFree Rf Rm -> Rm a a eq (u m₁ H H0) (u m₂ H1 H2)m:Type -> TypeH0:Monad mH1:MonadFree f mH2:PropEq1 mReallyLawfulMonadFree0:ReallyLawfulMonadFreefoldFree (u (Free f) Monad_Free MonadFree_Free) = u m H0 H1apply H. Qed.f:Type -> TypeRf:PropEq1 fa:Typeu:Free' f am:Type -> TypeH0:Monad mH1:MonadFree f mH2:PropEq1 mH:(fun (a₁ a₂ : Type) (Ra : a₁ -> a₂ -> Prop) (u₁ : Free f a₁) (u₂ : m a₂) => propeq1 Ra (foldFree u₁) u₂) a a eq (u (Free f) Monad_Free MonadFree_Free) (u m H0 H1)ReallyLawfulMonadFree0:ReallyLawfulMonadFreefoldFree (u (Free f) Monad_Free MonadFree_Free) = u m H0 H1

## Conclusion

If you managed to hang on so far, treat yourself to some chocolate.

To formalize a parametricity argument in Coq, I had to move the goalposts quite a bit throughout the experiment:

- Choose a more termination-friendly encoding of recursive types.
- Relativize equality.
- Mess around with heterogeneous relations without crashing into UIP.
- Reinvent the definition of a monad, again.
- Come to terms with the externality of parametricity.

It could be interesting to see a “really lawful monad” spelled out fully.

Another similar but simpler exercise is to prove the equivalence between
initial and final encodings of lists. It probably wouldn’t involve “relation
transformers” as much. There are also at least two different variants: is your
final encoding “`foldr`

”- or “`fold`

”-based (the latter mentions monoids, the
former doesn’t)?

I hope that machinery can be simplified eventually, but given the technical sophistication that is currently necessary, prudence is advised when navigating around claims made “by parametricity”.

## Related reading

Church encodings, inductive types, and relational parametricity, by Neel Krishnaswami

Final algebra semantics is observational equivalence, by Max New

Relational parametricity for higher kinds (PDF), by Robert Atkey

Free theorems involving type constructor classes (PDF), by Janis Voigtländer

Parametricity, type equality and higher-order polymorphism (PDF), by Dimitrios Vytiniotis and Stephanie Weirich

Unary parametricity vs binary parametricity, on TCS StackExchange

`(F r -> r) -> r`

gives an initial algebra of`F`

, on CS StackExchange

Answering

*Iceland_Jack*’s question on Twitter.↩︎That idea is also present in Kiselyov and Ishii’s paper.↩︎

Those who do know Coq will wonder, what about

`eq`

(“intensional equality”)? It is a fine default relation for first-order data (`nat`

, pairs, sums, lists, ASTs without HOAS). But it is too strong for computations (functions and coinductive types) and proofs (of`Prop`

s). Then a common approach is to introduce extensionality axioms, postulating that “extensional equality implies intensional equality”. But you might as well just stop right after proving whatever extensional equality you wanted.↩︎Well, if you tried you would end up with the unary variant of the parametricity theorem, but it’s much weaker than the binary version shown here. n-ary versions are also possible and even more general, but you have to look hard to find legitimate uses.↩︎

To be honest, that decision was a little arbitrary. But I’m not sure making things more complicated by keeping

`EqProp1`

and`EqProp`

separate buys us very much.↩︎