How to prove that the Church encoding, forall r. (F r -> r) -> r, gives an initial algebra of the functor F?

The well-known Church encoding of natural numbers can be generalized to use an arbitrary (covariant) functor F. The result is the type, call it C, defined by

data C = Cfix { run :: forall r. (F r -> r) -> r }

Here and below, for simplicity, we will assume that F is a fixed, already defined functor.

It is widely known and stated that the type C is a fixpoint of the functor F, and also that C is an initial F-algebra. For example, if the functor F a is defined by

data F a b = Empty | Cons a b

then a fixpoint of F a is [a] (the list of values of type a). Also, [a] is the initial algebra. The Church encoding of lists is well known. But I could not find a rigorous proof of either of these statements (C is a fixpoint, and C is the initial algebra).

The question is, how to prove rigorously one of the two statements:

• The type C is a fixpoint of the type isomorphism F C ≅ C. In other words, we need to prove that there exist two functions, fix :: F C -> C and unfix :: C -> F C such that fix . unfix = id and unfix . fix = id.

• The type C is the initial algebra of the functor F; that is, the initial object in the category of F-algebras. In other words, for any type A such that a function p :: F A -> A is given (that is, A is an F-algebra), we can find a unique function q :: C -> A which is an F-algebra morphism. This means, q must be such that the law q . fix = p . fmap q holds. We need to prove that, given A and p, such q exists and is unique.

These two statements are not equivalent; but proving (2) implies (1). (Lambek's theorem says that an initial algebra is an isomorphism.)

The code of the functions fix and unfix can be written relatively easily:

fix :: F C -> C
 fix fc  = Cfix (forall r. \g -> g . fmap (\h -> h g) fc )
 unfix :: C -> F C
 unfix c = (run c) (fmap fix)

Given a function p :: F A -> A, the code of the function q is written as

```
q :: C -> A
q c =

$\newcommand{\fix}{\mathsf{fix}}$
$\newcommand{\fold}{\mathsf{fold}}$
$\newcommand{\map}{\mathsf{map}}$

Here is, I believe, how one would use parametricity to prove your last lemma. I'm going to rework some stuff slightly for my own understanding. We have: $$C = ∀ r. (F r → r) → r$$ with $F$ functorial. We have: $$\fix : F C → C$$ corresponding to your definition, and I'm going to call a generalization of your m: $$\fold : (F r → r) → C → r \\ \fold\ α\ c = c\ α$$

So, we want to prove that for all $c : C$, $\fold\ \fix\ c = c$

Parametricity looks like this:

$$∀(R : a \Leftrightarrow b).\\ ∀ (α : F a → a) (β : F b → b).\\ (∀ x y. FR(x,y) → R (α\ x, β\ y))\\ → ∀ c. R (c\ α, c\ β)$$

To unpack this a bit, if we have a types $a,b$, a relation $R$ on them, algebra structures $α,β$, and a proof that they preserve the relation, then $R$ relates $c \ α$ to $c \ β$. The idea behind the "preservation" criterion is that $FR(x, y)$ holds if $x$ and $y$ have the same $F$ 'shape', and corresponding occurrences of $a$ and $b$ values are related by $R$.

So, let's make some choices. Suppose we have $ζ : F z → z$. Then: $$a \equiv C \\ b \equiv z \\ R(c, z) \equiv c\ ζ = z \\ α \equiv \fix \\ β \equiv ζ$$ the result of parametricity for these choices will be: $$R(c\ \fix, c\ ζ) \equiv c\ \fix\ ζ = c\ ζ$$

Then by function extensionality we will obtain $c = c\ \fix = \fold\ \fix\ c$. Our obligation is to prove:

$$∀ fc\ fz. FR(fc,fz) → R (\fix\ fc,ζ\ fz)$$

The goal is $$\fix\ fc\ ζ = ζ\ fz$$
By unfolding the definition of $\fix$ we know: $$\fix\ fc\ ζ = ζ (\map_F\ (\fold\ ζ)\ fc)$$

However, the meaning of $FR(fc,fz)$ is actually that $$\map_F\ (\fold\ ζ)\ fc = fz$$ So the result is immediate.

I haven't thought about whether it's possible to make due with dinaturality. I think it is not, but I could be wrong.

Edit:

The free theorem for this scenario is:

$$(∀ x. f (α\ x) = β (\map_F\ f \ x)) \Rightarrow f (c\ α) = c\ β$$

If we choose $$f = \fold\ ζ \\ α = \fix \\ β = ζ$$ then our obligation is:

$$\fold\ ζ\ (\fix\ x) = \fix\ x\ ζ = ζ (\map_F\ (\fold\ ζ)\ x)$$

which is just the definition of $\fix$. The result is:

$$\fold\ ζ\ (c\ \fix) = c\ ζ$$

which again gives us what we wanted. Note that this is also not the same as dinaturality, though. I believe the difference is that dinaturality allows us to shift $f$ around in the expression, but parametricity allows us to absorb it into one of the algebras.

StackExchange Computer Science Q#131901, answer score: 7