3
$\begingroup$

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:

  1. 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.
  2. 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 = (run c) p

However, it seems difficult to prove directly that the functions fix, unfix, q satisfy the required properties. I was not able to find a complete proof.

Is it easier to prove that C is an initial algebra, i.e., that q is unique, than to prove that fix . unfix = id?

In the rest of this question, I will show some steps that I was able to make towards the proof that fix . unfix = id.

It is not possible to prove either (1) or (2) simply by using the given code of the functions. We need additional assumptions. Similarly to the Yoneda identity,

 forall r. (A -> r) -> F r   ≅   F A   ,

we need to assume that the functions' code is fully parametric (no side effects, no specially chosen values or fixed types) so that the parametricity theorem can be applied. So, we need to assume that the type C contains only functions of type forall r. (F r -> r) -> r that satisfy the appropriate naturality law (known as "free theorem" after P. Wadler's paper "Theorems for free").

The parametricity theorem gives the following naturality law ("free theorem") for this type signature:

For any types A and B, and for any functions p :: F B -> A and f :: A -> B, the function c :: forall r. (F r -> r) -> r must satisfy the equation

  c (f . p) = f . c (p . fmap f)

Using this naturality law with appropriately chosen p and f, one can show that the composition fix . unfix is a certain function of type C -> C that must be equal to \c -> (run c) fix.

However, further progress in the proof does not seem to be possible; it is not clear why this function must be equal to id.

Let us temporarily define the function m:

 m :: (F C -> C) -> C -> C
 m t c = (run c) t

Then the result I have is written as

fix . unfix  = m fix

One can also show that unfix . fix = fmap (m fix).

It remains to prove that m fix = id. Once that is proved, we will have proved that F C ≅ C.

The same naturality law of c with different choice of p and f gives the strange identity

 m fix . m (m fix . fix) = m (m fix . fix)

But I do not know how to derive from this identity that m fix = id.

$\endgroup$
9
  • 1
    $\begingroup$ Naturality is insufficient except for certain simple cases. You probably need the actual relational parametricity theorem. The difficulty might be stating how $F$ acts on relations abstractly, but the idea is that it should lift a relation between $A$ and $B$ to one between $FA$ and $FB$ that is exact on the $F$ structure and defers to the underlying relation at 'leaves'. $\endgroup$ – Dan Doel Nov 3 '20 at 17:54
  • $\begingroup$ @DanDoel I am trying to prove an equation for functions; how would a relational law help me, other than by replacing some relations by functions and translating a relational law into a law for functions? So, I believe that the naturality law c (f . p) = f . c (p . fmap f) is already the most general result that one would get from the relational law. (It is the dinaturality law for the dinatural transformation c.) $\endgroup$ – winitzki Nov 3 '20 at 18:01
  • $\begingroup$ A related question is cstheory.stackexchange.com/questions/30923/… $\endgroup$ – winitzki Nov 3 '20 at 19:20
  • 2
    $\begingroup$ Also asked on Theoretical Computer Science: cstheory.stackexchange.com/questions/47819/… $\endgroup$ – Yuval Filmus Nov 3 '20 at 20:13
  • $\begingroup$ You also have to assume strict positivity of F. For negative F initial algebras provably don't exist. $\endgroup$ – András Kovács Nov 3 '20 at 20:41
5
$\begingroup$

$\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.

$\endgroup$
5
  • $\begingroup$ Thank you, this has been very educational. I believe it is true that the dinaturality law is not enough. But there is also something called "strong dinaturality", which is a condition similar to what you wrote (but I'll need to go through the calculations to be sure). This paper might be relevant: citeseerx.ist.psu.edu/viewdoc/… $\endgroup$ – winitzki Nov 4 '20 at 16:57
  • 1
    $\begingroup$ I haven't done extensive searching, but it seems like "strong" dinatural transformations aren't something that naturally arise in category theory. They seem like they were invented by CS people specifically to solve this example, because usual categorical notions are inadequate. However, in such a case, thinking about how parametricity might be expanded alongside category theory, as in this paper might be more fruitful. Forcing everything to be superficially category-based is not necessarily optimal. $\endgroup$ – Dan Doel Nov 4 '20 at 17:41
  • $\begingroup$ I suppose if they're also named after Barr, they might not have been first invented for CS. However, I had difficulty finding references to them that aren't on topics related to this sort of problem (for instance, the nlab doesn't seem to mention them). $\endgroup$ – Dan Doel Nov 4 '20 at 18:38
  • $\begingroup$ I found another interesting article that uses strong dinaturality: cs.nott.ac.uk/~pszgmh/pfc.pdf And also these slides: ioc.ee/~tarmo/tday-voore/vene-slides.pdf $\endgroup$ – winitzki Nov 4 '20 at 20:15
  • $\begingroup$ I have succeeded in proving that the Church encoding type C = forall r. (F r -> r) -> r is equivalent to the initial algebra of a (covariant) functor F, if we restrict the type C to allow only functions that satisfy strong dinaturality. I also found some unpublished talk slides here, ioc.ee/~tarmo/tday-voore/vene-slides.pdf that explain how to derive strong dinaturality from parametricity in a large class of type signatures (strong dinaturality probably does not hold for all type signatures). The Church encoding type will have strong dinaturality automatically. $\endgroup$ – winitzki Mar 15 at 10:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.