Church Encoding, Parametricity, and the Yoneda Lemma

# Church Encoding, Parametricity, and the Yoneda Lemma Source: [https://blog.wybxc.cc/blog/parametricity/](https://blog.wybxc.cc/blog/parametricity/) I still remember the shock I felt when I first encountered functional programming years ago\. That was the moment I learned that natural numbers can be built within the language itself: ``` data Nat = Zero | Succ Nat ``` I went on to learn that all computation can be expressed through functions \(the lambda calculus\), that recursion itself can be encoded as the mesmerizing Y combinator: ``` Y = λf. (λx. f (x x)) (λx. f (x x)) ``` And then there were Church numerals, where each number becomes a function: ``` 0 = λs. λz. z 1 = λs. λz. s z 2 = λs. λz. s (s z) ``` Church encoding represents natural numbers as functions; each number𝑛takes a successor function and a starting point, then applies the successor𝑛times\. But what is the reasoning behind it? Why these particular lambda terms? There is also Church encoding for lists: ``` nil = λc. λn. n cons = λx. λxs. λc. λn. c x (xs c n) ``` The pattern feels similar, but the details are different\. For a long time I assumed this was just how things were: a clever trick, rediscovered case by case\. It is after many years of learning that I finally understand the deeper story\. Church encoding manifests deep connections between data types, polymorphism, and category theory\. Once you see these connections, the shape of the encoding follows inevitably, and the result is more elegant than the trick itself\. In this article, I want to trace those connections\. We’ll start from the simplest data types in a typed setting, watch a pattern emerge, and gradually build up the machinery \(parametricity, algebraic data types, F\-algebras, and the Yoneda Lemma\) until the Church encoding reveals itself as something the mathematics demands\. ### System F To capture the pattern behind Church encoding, we need types\. The untyped lambda calculus gives us the terms, but it gives us no vocabulary to say*what*those terms are\. That’s the Simply Typed Lambda Calculus \(STLC\), where every term has a type\. The only type constructor in bare STLC is the function arrow𝐴→𝐵11\.To be precise, STLC also includes some base types, like𝚄𝚗𝚒𝚝,𝙱𝚘𝚘𝚕,or𝙸𝚗𝚝;otherwise you cannot give the parameter of the innermost function a type\. But the particular choice of base types is irrelevant to the story; we just need something in the language to talk about\.\. But STLC hits a wall almost immediately\. A Church numeral must accept**any**type as its carrier: the whole point is that2works the same whether you’re counting apples or functions\. STLC can’t say that\. Every function in STLC has a fixed, monomorphic type\. This is where the experienced programmer sits up: we need**generics**\. We need functions that are polymorphic over types\. The calculus that gives us this is**System F**, the polymorphic lambda calculus\. Here’s the idea\. In System F, a function can take a type as an argument\. You write type abstraction asΛ𝑋\.𝑡and type application as𝑓\[𝑋\]\.Types of System F include type variables𝑋,function types𝐴→𝐵,and universal quantification∀𝑋\.𝐴\.22\.Unlike STLC, base types are not necessary in System F\. The polymorphism alone gives us enough structure to build everything we need\. As you can see, our System F starts as an empty universe\. In STLC, we would declare base types like𝚄𝚗𝚒𝚝and𝙱𝚘𝚘𝚕to get started\. But in System F, an interesting thing happens: we can build these types from scratch, using only functions and polymorphism\! We can encode𝚄𝚗𝚒𝚝and𝙱𝚘𝚘𝚕as polymorphic functions, without any special syntax for data types\. Let me state a principle: a data type can be equivalently represented by the ways you consume it\. I cannot yet explain the logic behind this statement, but let’s set it aside for now and see how it works for𝚄𝚗𝚒𝚝\.33\.In the second half of this article, we will ultimately understand the true meaning of this statement through the lens of category theory\. Specifically, the Yoneda Lemma will show that the set of all ways to consume a type fully determines the type itself\. If you’re holding a value of type𝚄𝚗𝚒𝚝,what can you do with it? The only way to consume a𝚄𝚗𝚒𝚝value is to ignore it and return something that has nothing to do with it\. Suppose you want to write a universal consumer: for any target type𝑋,it turns a𝚄𝚗𝚒𝚝into an𝑋\.Because we know nothing about𝑋,we cannot make up any new value of type𝑋\.The only thing we can do is to return an𝑋that we already have\. But where do we get an𝑋from? We don’t have one\! We should receive it as an argument\. Therefore, the type signature of a universal consumer of𝚄𝚗𝚒𝚝is: ∀𝑋\.𝑋→𝑋Read as: “for any type𝑋,give me an𝑋and I’ll give you back an𝑋\.” What is the inhabitant of this type? It is easy to think of one: the identity function\.44\.Later we will see that this is the only possible implementation, as a consequence of parametricity\.It takes an𝑋and returns it unchanged: ``` id = ΛX. λx. x ``` This function is the Church encoding of𝚄𝚗𝚒𝚝\. Let’s try the same reasoning with𝙱𝚘𝚘𝚕\.𝙱𝚘𝚘𝚕has two constructors,𝚃𝚛𝚞𝚎and𝙵𝚊𝚕𝚜𝚎\. What does consuming a𝙱𝚘𝚘𝚕require? You need a target type𝑋,and you need an interpretation for𝚃𝚛𝚞𝚎and one for𝙵𝚊𝚕𝚜𝚎,two values of type𝑋\.Then, depending on which constructor the actual𝙱𝚘𝚘𝚕value represents, you return the appropriate interpretation\. As a type signature: ``` ∀X. X → X → X ``` Read as: “for any type𝑋,give me two𝑋s and I’ll give you back an𝑋\.” We can find two inhabitants of this type, which correspond to the two ways to consume a𝙱𝚘𝚘𝚕: ``` true = ΛX. λx. λy. x false = ΛX. λx. λy. y ``` One chooses the first argument, the other chooses the second\. They correspond exactly to the two values of𝙱𝚘𝚘𝚕\. Looking at these two examples, a pattern emerges: To summarize the pattern so far: the Church encoding of a data type in System F is a polymorphic function whose arguments match the constructors\. It is a universal consumption interface for the type\. This investigation works perfectly for𝚄𝚗𝚒𝚝and𝙱𝚘𝚘𝚕,whose constructors carry no data\. But what about a type like the𝙽𝚊𝚝? Its𝚂𝚞𝚌𝚌constructor has a recursive parameter\. We will talk about how to handle that in the following sections, but before we do, we need to understand the mechanism that makes the pattern work in the first place\. ### Parametricity What is truly remarkable is that for∀𝑋\.𝑋→𝑋,we can only find a single implementation, the identity function\. Likewise, for∀𝑋\.𝑋→𝑋→𝑋,we can only find two implementations,`true`and`false`\. The type system of System F does not permit any other implementations\. Once you have convinced yourself of the fact, let’s move on\. To understand**why**the type system restricts the inhabitants so precisely, we need to examine the mechanism behind System F’s polymorphism\. The polymorphism in System F is**parametric**: a polymorphic function gets a type argument, but it can’t inspect it\. It can’t branch on “am I dealing with Int or Bool?” It must treat the type as a black box\. That restriction turns out to be the source of enormous power\. John Reynolds proved the**parametricity theorem**\(also called the**abstraction theorem**\) in 1983\. Here is a compact statement: > Let𝑓:∀𝑋\.𝜏\(𝑋\)be a closed term of System F, where𝜏\(𝑋\)is a type expression\. For any types𝐴,𝐵and any relation𝑅⊆𝐴×𝐵,let𝜏\(𝑅\)⊆𝜏\(𝐴\)×𝜏\(𝐵\)be the relational lifting defined recursively from the structure of𝜏\.If\(𝑎,𝑏\)∈𝜏\(𝑅\)then\(𝑓\[𝐴\]𝑎,𝑓\[𝐵\]𝑏\)∈𝜏\(𝑅\)\. That formulation may look abstract, but its core message is simple: a polymorphic function must “preserve” whatever relation you associate with the type parameter\. It cannot detect the concrete structure of the type it’s instantiated with\. A consequence is that you can derive equations the function must satisfy purely from its type signature, regardless of implementation\. Philip Wadler later called these “theorems for free\.” Let’s begin with a special case you can verify by hand\. **Claim**:∀𝑋\.𝑋→𝑋has only the identity function, i\.e\., any𝑓:∀𝑋\.𝑋→𝑋must satisfy𝑓\[𝐴\]𝑎=𝑎for all𝐴and𝑎\. **Proof**: Let’s see what parametricity has to say about𝑓:∀𝑋\.𝑋→𝑋\.Take two arbitrary types𝐴and𝐵,and pick any relation𝑅⊆𝐴×𝐵between them\. The theorem requires us to lift𝑅through the type expression𝜏\(𝑋\)=𝑋→𝑋\.Here’s how the lifting works: two functionsℎ𝐴:𝐴→𝐴andℎ𝐵:𝐵→𝐵are related by𝜏\(𝑅\)precisely when they map𝑅\-related inputs to𝑅\-related outputs, that is,\(ℎ𝐴\(𝑥\),ℎ𝐵\(𝑦\)\)∈𝑅whenever\(𝑥,𝑦\)∈𝑅\.Intuitively,ℎ𝐴andℎ𝐵preserve𝑅in lockstep\. Now, parametricity says: because𝑓is polymorphic, its instantiations at𝐴and𝐵must be related by this lifted relation\. In symbols:\(𝑓\[𝐴\],𝑓\[𝐵\]\)∈𝜏\(𝑅\)\.Spelling that out: for any\(𝑥,𝑦\)∈𝑅,we have\(𝑓\[𝐴\]𝑥,𝑓\[𝐵\]𝑦\)∈𝑅\. Here comes the trick\. Fix a type𝐴and a value𝑎:𝐴\.Our goal is to show𝑓\[𝐴\]𝑎=𝑎\.Define a very specific relation: 𝑅=\{\(𝑎,𝑎\)\}⊆𝐴×𝐴This relation pairs𝑎with itself and nothing else\. Take𝐵=𝐴\.Since\(𝑎,𝑎\)∈𝑅,the parametricity condition forces: \(𝑓\[𝐴\]𝑎,𝑓\[𝐴\]𝑎\)∈𝑅But𝑅contains exactly one pair:\(𝑎,𝑎\)\.So𝑓\[𝐴\]𝑎must be𝑎\.Done\. Notice what just happened: parametricity forced𝑓to be the identity function, even though𝑓knows absolutely nothing about the type it’s applied to\. The type signature alone left it no other choice\. A similar argument works for∀𝑋\.𝑋→𝑋→𝑋\.A function of this type receives two values of an unknown type𝑋and must return an𝑋\.With no operations available on𝑋,the only possible behaviors are “always return the first argument” or “always return the second\.” That’s`true`and`false`\.55\.A formal proof follows the same relational strategy, using𝑅=\{\(𝑎,𝑎\),\(𝑏,𝑏\)\}for two distinct values𝑎,𝑏:𝐴\. Now for the payoff\. What does parametricity say about the general shape𝑓:∀𝑋\.\(𝐹𝑋→𝑋\)→𝑋? Here𝐹is any type operator; think of it as describing the structure of a data type\. The free theorem we get is this: for any F\-algebra homomorphism66\.We will explain what an F\-algebra homomorphism is later\.ℎ:\(𝐴,𝑓𝐴\)→\(𝐵,𝑓𝐵\), ℎ\(𝑓\[𝐴\]𝑓𝐴\)=𝑓\[𝐵\]𝑓𝐵This equation will play a central role later when we prove that Church encoding is equivalent to the data type it encodes\. ### Algebraic Data Types and Functors With parametricity in our toolkit, we now return to the main thread\. Recall where we left off:𝚄𝚗𝚒𝚝and𝙱𝚘𝚘𝚕revealed a pattern \(the Church encoding is a polymorphic function whose arguments match the constructors\), but we had no way to handle recursive types like𝙽𝚊𝚝\.To extend the pattern, we need a systematic language for describing the structure of data types, which makes the structure of constructors and their arguments explicit\. This is where**algebraic data types**\(ADT\) enter the picture\. We know that tuples are**product types**and tagged unions are**sum types**\. An algebraic data type is built from these two operations, fundamentally, as a**sum of products**\. Each constructor is a product of its fields; the whole type is the sum among constructors\. If a constructor carries no data, it is the empty product, i\.e\., the𝚄𝚗𝚒𝚝type\. We can make this precise with a small algebraic notation: - 1\(the unit type,𝚄𝚗𝚒𝚝\): a type with exactly one value\. It is the identity of the product:1×𝐴≅𝐴\. - 𝐴\+𝐵\(the sum type\): a value is either an𝐴or a𝐵,tagged with the choice\. - 𝐴×𝐵\(the product type\): a pair of an𝐴and a𝐵\. Under this notation: 𝚄𝚗𝚒𝚝=1𝙱𝚘𝚘𝚕=1\+1𝙽𝚊𝚝=1\+𝙽𝚊𝚝The last line reads: a natural number is either𝚉𝚎𝚛𝚘\(the1branch, carrying no information\) or𝚂𝚞𝚌𝚌\(wrapping another𝙽𝚊𝚝\)\. The equation is recursive, and we make sense of it with the𝜇binder: 𝙽𝚊𝚝=𝜇𝑋\.1\+𝑋The same recipe works for lists: 𝙻𝚒𝚜𝚝\(𝑎\)=𝜇𝑋\.1\+𝑎×𝑋Here,𝙽𝚒𝚕is the1branch and𝙲𝚘𝚗𝚜is the𝑎×𝑋branch\. But the algebra goes deeper than notation\. Types surprisingly obey the familiar laws of algebra\. For example, the distributivity law: 𝑎×\(𝑏\+𝑐\)≅𝑎×𝑏\+𝑎×𝑐Here≅denotes type isomorphism: there exist functions witnessing the equivalence in both directions\. Read the law as types:`\(a, Either b c\)`is isomorphic to`Either \(a, b\) \(a, c\)`\. As evidence, we can write the following functions: ``` f :: (a, Either b c) -> Either (a, b) (a, c) f (a, Left b) = Left (a, b) f (a, Right c) = Right (a, c) g :: Either (a, b) (a, c) -> (a, Either b c) g (Left (a, b)) = (a, Left b) g (Right (a, c)) = (a, Right c) ``` What about function types? Can we express them in terms of algebraic operations? Let me declare:**functions are exponents\.**Consider two finite types𝐴and𝐵,with\|𝐴\|and\|𝐵\|inhabitants respectively\. How many functions𝐴→𝐵exist? For each input𝑎∈𝐴,we can independently choose any output𝑏∈𝐵\.That’s\|𝐵\|choices repeated\|𝐴\|times:\|𝐵\|\|𝐴\|possibilities\. This suggests writing the function type as an exponential: 𝐴→𝐵≅𝐵𝐴Currying then becomes the familiar exponent law: 𝐶𝐴×𝐵≅\(𝐶𝐵\)𝐴And functions out of sums follow their own distributive law: 𝐶𝐴\+𝐵≅𝐶𝐴×𝐶𝐵Now let’s return to the Church encoding of natural numbers\. We have seen Church numerals in untyped lambda calculus: ``` 0 = λs. λz. z 1 = λs. λz. s z 2 = λs. λz. s (s z) ``` We want to give them types in System F\. Assume the type of`z`is𝑋\.We expect the type of`0`and`1`to be the same, so term`s z`should have the same type as`z`\. Therefore,`s`must have type𝑋→𝑋\.That gives us the Church encoding type for natural numbers: ChurchNat=∀𝑋\.𝑋→\(𝑋→𝑋\)→𝑋It looks somewhat different from the Church encoding types for`Unit`and`Bool`\. The second argument is a function rather than a value\. Is there a single shape that captures all of them? Let’s inspect the inner part of the encoding more closely\. Currying tells us that a function𝑋→\(𝑋→𝑋\)→𝑋is equivalent to a function\(𝑋,𝑋→𝑋\)→𝑋\.And we already know that the tuple\(𝐴,𝐵\)can be written as𝐴×𝐵,and the function type𝐴→𝐵can be written as𝐵𝐴\.Then we can do some algebraic manipulation: 𝑋→\(𝑋→𝑋\)→𝑋≅𝑋×𝑋𝑋→𝑋≅𝑋1\+𝑋→𝑋≅\(\(1\+𝑋\)→𝑋\)→𝑋So the full Church encoding becomes: ChurchNat≅∀𝑋\.\(\(1\+𝑋\)→𝑋\)→𝑋Now look at the expression1\+𝑋\.That is precisely the body of the recursive type definition of𝙽𝚊𝚝=𝜇𝑋\.1\+𝑋\.In other words, the Church encoding is of the form: ∀𝑋\.\(𝐹𝑋→𝑋\)→𝑋where𝐹𝑋=1\+𝑋Here,𝐹is a**functor**that captures the shape of the algebraic data type\. Let’s check that this holds for our earlier examples: - For𝚄𝚗𝚒𝚝:the functor is𝐹𝑋=1\.Then\(𝐹𝑋→𝑋\)→𝑋=\(1→𝑋\)→𝑋≅𝑋→𝑋\.Matches∀𝑋\.𝑋→𝑋\. - For𝙱𝚘𝚘𝚕:the functor is𝐹𝑋=1\+1\.Then\(𝐹𝑋→𝑋\)→𝑋=\(1\+1→𝑋\)→𝑋≅\(𝑋×𝑋\)→𝑋≅𝑋→𝑋→𝑋\.Matches∀𝑋\.𝑋→𝑋→𝑋\. Here we get the general pattern: for an algebraic data type𝑇=𝜇𝑋\.𝐹𝑋,its Church encoding is∀𝑋\.\(𝐹𝑋→𝑋\)→𝑋\. In the next section we will see that the Church encoding∀𝑋\.\(𝐹𝑋→𝑋\)→𝑋is the type of universal consumers of**F\-algebras**, and this is the perspective that will lead us, via parametricity and the Yoneda Lemma, to the deepest understanding of what Church encoding really is\. ### F\-Algebra We’ve arrived at a turning point\. The last section ended with a shape,∀𝑋\.\(𝐹𝑋→𝑋\)→𝑋,that unifies the Church encodings of𝚄𝚗𝚒𝚝,𝙱𝚘𝚘𝚕,and𝙽𝚊𝚝under one roof\. But the shape still feels pulled from thin air\. Why this particular arrangement of symbols? To answer that, we need to give names to the pieces\. This is where category theory enters\. Let’s start small\. A**category**is a collection of objects and arrows between them, with sensible rules for*composition*and*identity*\. For a programmer, the natural example is the category𝐒𝐞𝐭:objects are types, arrows are functions, composition is function composition, and the identity arrow is`id`\. A**functor**𝐹is a mapping between categories\. In our world,𝐹maps each type𝐴to a type𝐹𝐴,and each function𝑓:𝐴→𝐵to a function𝐹𝑓:𝐹𝐴→𝐹𝐵,preserving composition and identity: 𝐹\(𝑔∘𝑓\)=𝐹𝑔∘𝐹𝑓𝐹id=idThis is exactly what the𝐹in𝐹𝑋=1\+𝑋has been doing all along: it builds a new type from an old one,**and**it lifts functions to act inside that structure\.77\.For𝙽𝚊𝚝𝙵,given𝑓:𝑋→𝑌,𝙽𝚊𝚝𝙵𝑓maps𝙻𝚎𝚏𝚝\(\)to𝙻𝚎𝚏𝚝\(\)and𝚁𝚒𝚐𝚑𝚝𝑥to𝚁𝚒𝚐𝚑𝚝\(𝑓𝑥\)\.This function\-lifting is the machinery behind structural recursion; we’ll return to it when we define folds\. A**natural transformation**𝜂between two functors𝐹and𝐺is a way of turning𝐹shapes into𝐺shapes, uniformly for all types\. For each type𝑋,you have an arrow𝜂𝑋:𝐹𝑋→𝐺𝑋,and for every functionℎ:𝑋→𝑌the following square commutes:  That is,𝜂𝑌∘𝐹ℎ=𝐺ℎ∘𝜂𝑋\.This is**naturality**: the transformation must work the same way no matter which object you look at\. Here’s the connection that makes all of this tick: the free theorems we got from parametricity are naturality conditions in disguise\. A polymorphic function in System F is a natural transformation when viewed through the right categorical lens\. Parametricity and naturality are two sides of the same coin\. With these three concepts, category, functor, natural transformation, we finally have the language to name the pattern that has been staring at us since the very beginning\. An**F\-algebra**is a triple⟨𝐹,𝑋,𝑓⟩consisting of a functor𝐹,a carrier type𝑋,and a function𝑓:𝐹𝑋→𝑋\. Intuitively,𝑓:𝐹𝑋→𝑋is an**evaluator**that folds the structure described by𝐹into a single value of type𝑋\.For example, the functor of natural numbers is𝙽𝚊𝚝𝙵𝑋=1\+𝑋\.An F\-algebra for this functor consists of a type𝑋and a function𝑓:1\+𝑋→𝑋\.By algebraic manipulation, this becomes a pair of functions\(𝑧:𝑋,𝑠:𝑋→𝑋\),where - 𝑧=𝑓\(𝙻𝚎𝚏𝚝\(\)\)gives what the zero value evaluates to, and - 𝑠𝑛=𝑓\(𝚁𝚒𝚐𝚑𝚝𝑛\)maps the evaluation of𝑛to the evaluation of its successor\. For𝙱𝚘𝚘𝚕𝙵𝑋=1\+1,a𝙱𝚘𝚘𝚕𝙵\-algebra is simply two values of type𝑋:the algebra map𝑓:1\+1→𝑋corresponds to a pair\(𝑥1:𝑋,𝑥2:𝑋\),where𝑥1evaluates`true`and𝑥2evaluates`false`\. The Church encoding type∀𝑋\.\(𝐹𝑋→𝑋\)→𝑋now acquires a precise meaning: it is a**universal consumer of F\-algebras**: given any F\-algebra⟨𝐹,𝑋,𝑓⟩,it takes the evaluator𝑓:𝐹𝑋→𝑋and runs it on the conceptual structure of the data type to produce a value of type𝑋\.It makes rigorous the “consumption interface” idea introduced earlier\. F\-algebras for a fixed functor𝐹themselves form a category\. An arrow in this category is called an**F\-algebra homomorphism**\. If⟨𝐹,𝐴,𝑓⟩and⟨𝐹,𝐵,𝑔⟩are two F\-algebras, a homomorphism between them is a functionℎ:𝐴→𝐵that preserves the algebraic structure: ℎ∘𝑓=𝑔∘𝐹ℎIn diagram form:  The condition says: evaluating a structure in𝐴and then translating the result to𝐵yields the same value as translating the sub\-structure to𝐵first and then evaluating in𝐵\.The two paths through the square produce the same result\. For example, for𝙽𝚊𝚝𝙵𝑋=1\+𝑋,the homomorphism condition becomes: ℎ\(𝑧𝐴\)=𝑧𝐵ℎ\(𝑠𝐴𝑎\)=𝑠𝐵\(ℎ𝑎\)These two equations are exactly the pattern that any structural recursion must obey: the base case maps to the base case, and the recursive case appliesℎto the predecessor and then the successor function\. ### Initial Algebra Among the F\-algebras for a given functor𝐹,one deserves special attention\. In a category, an**initial object**satisfies the**initiality**property: there is a unique arrow from it to every other object\. In the category of F\-algebras, the initial object is called the**initial algebra**, written⟨𝐹,𝜇𝐹,𝚒𝚗⟩,where𝜇𝐹is the carrier and𝚒𝚗:𝐹\(𝜇𝐹\)→𝜇𝐹is the structure map\. By initiality, for any F\-algebra⟨𝐹,𝑋,𝑓⟩,there is exactly one homomorphism from⟨𝐹,𝜇𝐹,𝚒𝚗⟩to it\. We call it𝚏𝚘𝚕𝚍𝑓:𝜇𝐹→𝑋\. To get an intuitive grasp of what the initial algebra is, let’s look at the type of𝚏𝚘𝚕𝚍in System F\. It takes an evaluator𝑓:𝐹𝑋→𝑋and returns a function𝚏𝚘𝚕𝚍𝑓:𝜇𝐹→𝑋\.So its type signature is∀𝑋\.\(𝐹𝑋→𝑋\)→𝜇𝐹→𝑋\. Compare this with the Church encoding type:𝙲𝚑𝚞𝚛𝚌𝚑𝙵=∀𝑋\.\(𝐹𝑋→𝑋\)→𝑋\.They are almost identical\. The only difference is that𝚏𝚘𝚕𝚍has an extra𝜇𝐹→tucked before the final𝑋\.Where Church encoding takes an algebra and produces an𝑋,fold takes an algebra*and*a𝜇𝐹value to produce an𝑋\. This suggests a natural way to move between𝜇𝐹and𝙲𝚑𝚞𝚛𝚌𝚑𝙵\.Given𝑥:𝜇𝐹,we can partially apply𝚏𝚘𝚕𝚍to get a Church encoding:Λ𝑋\.𝜆𝑓\.𝚏𝚘𝚕𝚍𝑓𝑥:𝙲𝚑𝚞𝚛𝚌𝚑𝙵\.Conversely, given𝑐:𝙲𝚑𝚞𝚛𝚌𝚑𝙵,we can feed it the initial algebra’s own structure map:𝑐\[𝜇𝐹\]𝚒𝚗:𝜇𝐹\.These two maps point at each other: one wraps a𝜇𝐹value into a universal consumer, the other unwraps a universal consumer by running it on the initial algebra itself\. We will prove shortly that they are inverses, establishing𝙲𝚑𝚞𝚛𝚌𝚑𝙵≅𝜇𝐹\. Before we do, we still need to understand what𝜇𝐹actually is\. For that we return to initiality\. Take the object𝐹\(𝜇𝐹\)and turn it into an F\-algebra by using𝐹\(𝚒𝚗\):𝐹\(𝐹\(𝜇𝐹\)\)→𝐹\(𝜇𝐹\)as the structure map\. By initiality, we get a unique homomorphism from⟨𝐹,𝜇𝐹,𝚒𝚗⟩to this new algebra; call it𝑔:𝜇𝐹→𝐹\(𝜇𝐹\)\.But𝚒𝚗itself is a homomorphism in the opposite direction:𝐹\(𝜇𝐹\)→𝜇𝐹\.Compose the two:𝚒𝚗∘𝑔is a homomorphism from𝜇𝐹to itself\. Initiality says there is exactly one such homomorphism, namely𝚒𝚍,so𝚒𝚗∘𝑔=𝚒𝚍\.The same argument on the other side gives𝑔∘𝚒𝚗=𝚒𝚍\.So𝚒𝚗and𝑔are inverses:𝚒𝚗is an isomorphism\. This is**Lambek’s theorem**:𝐹\(𝜇𝐹\)≅𝜇𝐹\.The carrier of the initial algebra is the recursive type𝜇𝑋\.𝐹𝑋\.That is why we choose the notation𝜇𝐹\. Now that we know𝜇𝐹is a recursive type, the role of the structure map𝚒𝚗becomes clear\. It is a constructor that builds the recursive type from its components\. Take𝙽𝚊𝚝as an example,𝚒𝚗:1\+𝙽𝚊𝚝→𝙽𝚊𝚝has two cases: - 𝙻𝚎𝚏𝚝\(\)means no predecessor:𝚒𝚗returns𝚉𝚎𝚛𝚘; - 𝚁𝚒𝚐𝚑𝚝𝑛means one predecessor𝑛already built:𝚒𝚗returns𝚂𝚞𝚌𝚌𝑛\. The fold equation now also becomes concrete\. An algebra⟨𝐹,𝑋,𝑓⟩expands to a pair\(𝑧:𝑋,𝑠:𝑋→𝑋\),and the equation𝚏𝚘𝚕𝚍𝑓∘𝚒𝚗=𝑓∘𝐹\(𝚏𝚘𝚕𝚍𝑓\)becomes: 𝚏𝚘𝚕𝚍𝑓\(𝚉𝚎𝚛𝚘\)=𝑧𝚏𝚘𝚕𝚍𝑓\(𝚂𝚞𝚌𝚌𝑛\)=𝑠\(𝚏𝚘𝚕𝚍𝑓𝑛\)This is structural recursion: replace every𝚉𝚎𝚛𝚘with𝑧,every𝚂𝚞𝚌𝚌with an application of𝑠to the recursively processed predecessor\. The fold walks through the value from the bottom up, substituting each constructor with the algebra’s interpretation\. One more consequence of initiality:𝚏𝚘𝚕𝚍𝚒𝚗=𝚒𝚍\.Since𝚒𝚍is a homomorphism from the initial algebra to itself, and initiality says there can only be one, the fold at the initial algebra’s own structure map must be the identity\. This equation will unlock the entire proof\. Now step back\.𝚒𝚗builds values from nothing\.𝚏𝚘𝚕𝚍takes those values and interprets them in any algebra you choose, uniquely\. One end generates; the other end consumes\. This combination is what we call a**universal producer**\. The Church encoding𝙲𝚑𝚞𝚛𝚌𝚑𝙵=∀𝑋\.\(𝐹𝑋→𝑋\)→𝑋is the mirror image: it takes any algebra and returns a value: a**universal consumer**\. Universal producer meets universal consumer\. They are\. Let’s prove𝙲𝚑𝚞𝚛𝚌𝚑𝙵≅𝜇𝐹\.We define two functions between them in System F, and show that they are inverses of each other: ``` fromChurch : ChurchF → μ F fromChurch c = c [μ F] in toChurch : μ F → ChurchF toChurch x = ΛX. λ(f : F X → X). fold f x ``` 𝚏𝚛𝚘𝚖𝙲𝚑𝚞𝚛𝚌𝚑feeds the initial algebra to the universal consumer\.𝚝𝚘𝙲𝚑𝚞𝚛𝚌𝚑takes a concrete value and turns it into a consumer by folding over any algebra you give it\. **Step one:**𝚏𝚛𝚘𝚖𝙲𝚑𝚞𝚛𝚌𝚑∘𝚝𝚘𝙲𝚑𝚞𝚛𝚌𝚑=𝚒𝚍\.For any𝑥:𝜇𝐹: 𝚏𝚛𝚘𝚖𝙲𝚑𝚞𝚛𝚌𝚑\(𝚝𝚘𝙲𝚑𝚞𝚛𝚌𝚑𝑥\)=𝚝𝚘𝙲𝚑𝚞𝚛𝚌𝚑𝑥\[𝜇𝐹\]𝚒𝚗=𝚏𝚘𝚕𝚍𝚒𝚗𝑥=𝑥**Step two:**𝚝𝚘𝙲𝚑𝚞𝚛𝚌𝚑∘𝚏𝚛𝚘𝚖𝙲𝚑𝚞𝚛𝚌𝚑=𝚒𝚍\. We need to show that for any𝑐:𝙲𝚑𝚞𝚛𝚌𝚑𝙵,any𝑋,and any𝑓:𝐹𝑋→𝑋: 𝚏𝚘𝚕𝚍𝑓\(𝑐\[𝜇𝐹\]𝚒𝚗\)=𝑐\[𝑋\]𝑓This is where parametricity earns its keep\. Remember the free theorem we derived: for any F\-algebra homomorphismℎ:\(𝐴,𝑓𝐴\)→\(𝐵,𝑓𝐵\), ℎ\(𝑐\[𝐴\]𝑓𝐴\)=𝑐\[𝐵\]𝑓𝐵Now let𝐴=𝜇𝐹,𝑓𝐴=𝚒𝚗,𝐵=𝑋,𝑓𝐵=𝑓,andℎ=𝚏𝚘𝚕𝚍𝑓\.Since𝚏𝚘𝚕𝚍𝑓is an algebra homomorphism, the free theorem applies directly: 𝚏𝚘𝚕𝚍𝑓\(𝑐\[𝜇𝐹\]𝚒𝚗\)=𝑐\[𝑋\]𝑓That’s the equality we needed\. Both directions are inverses, so𝙲𝚑𝚞𝚛𝚌𝚑𝙵≅𝜇𝐹\. Notice what just happened\. Two completely independent ideas: the uniqueness of the fold from the initial algebra, and the free theorem from parametricity, interlocked to deliver the isomorphism\. Together they’re airtight\. We’ve proved the isomorphism\. But a question lingers:**why**this shape? Why∀𝑋\.\(𝐹𝑋→𝑋\)→𝑋of all things? We arrived at it by following our noses through𝚄𝚗𝚒𝚝,𝙱𝚘𝚘𝚕,𝙽𝚊𝚝,and a bit of algebra\. That’s a fine derivation, but it doesn’t explain why the shape**must**be what it is\. For that, we turn to what is arguably the*most beautiful*theorem in category theory\. ### The Yoneda Lemma Before stating the lemma, one more piece of vocabulary\. The**Hom\-functor**𝖧𝗈𝗆\(𝐴,−\)embodies “the view from𝐴\.” For any object𝑋,𝖧𝗈𝗆\(𝐴,𝑋\)is the set of all arrows from𝐴to𝑋,which in the𝐒𝐞𝐭category is just the function type𝐴→𝑋\.Given a function𝑔:𝑋→𝑌,the Hom\-functor maps it by post\-composition:𝖧𝗈𝗆\(𝐴,𝑔\)=𝜆ℎ\.𝑔∘ℎ\.It’s the formal way of saying “everything you can do with an𝐴\.” Now the Yoneda Lemma: > For any \(locally small\) category𝒞︀,any object𝐴in𝒞︀,and any𝐒𝐞𝐭\-valued functor𝐹:𝒞︀→𝚂𝚎𝚝,there exists a bijection: 𝖭𝖺𝗍\(𝖧𝗈𝗆\(𝐴,−\),𝐹\)≅𝐹\(𝐴\)The left side is the set of natural transformations from𝖧𝗈𝗆\(𝐴,−\)to𝐹;the right side is the value of𝐹at𝐴\.This bijection is natural in both𝐴and𝐹\. Underneath the imposing formalism lives a disarmingly simple idea\. A natural transformation from𝖧𝗈𝗆\(𝐴,−\)to𝐹is completely determined by a single choice: where you send𝚒𝚍𝐴\.Pick any element of𝐹\(𝐴\)as the image of𝚒𝚍𝐴,and naturality does the rest; it uniquely transports that choice to every other object\. Conversely, given a natural transformation, applying it to𝚒𝚍𝐴at𝐴picks out an element of𝐹\(𝐴\)\.That’s the whole correspondence\. Think about what this means\. The Hom\-functor captures everything you can arrow out of𝐴,the “outward view” of𝐴\.Yoneda says this outward view**completely determines**𝐴itself\. Sound familiar? It’s the categorical incarnation of our consumption\-interface principle: a type is fully characterized by how you can consume it\. Let’s try a concrete case\. Set𝐹to the identity functor𝙸𝚍where𝙸𝚍\(𝑋\)=𝑋and𝒞︀to the𝐒𝐞𝐭category\. The Yoneda lemma specializes to: 𝖭𝖺𝗍\(𝖧𝗈𝗆\(𝐴,−\),𝙸𝚍\)≅𝐴Now unpack the left side\.𝖧𝗈𝗆\(𝐴,𝑋\)is𝐴→𝑋\.A natural transformation𝜂:𝖧𝗈𝗆\(𝐴,−\)→𝙸𝚍is a family of functions𝜂𝑋:\(𝐴→𝑋\)→𝑋,one for each𝑋\.So𝜂is necessarily a polymorphic function in System F\. Its type is∀𝑋\.\(𝐴→𝑋\)→𝑋\.So∀𝑋\.\(𝐴→𝑋\)→𝑋≅𝐴\.Yoneda gives us the isomorphism directly\. For𝐴=𝚄𝚗𝚒𝚝,this says∀𝑋\.\(𝚄𝚗𝚒𝚝→𝑋\)→𝑋≅𝚄𝚗𝚒𝚝,which simplifies to∀𝑋\.𝑋→𝑋≅𝚄𝚗𝚒𝚝\.For𝐴=𝙱𝚘𝚘𝚕,we get∀𝑋\.𝑋→𝑋→𝑋≅𝙱𝚘𝚘𝚕\.These are exactly the Church encodings we derived by hand\. Now they fall out of Yoneda for free\. But there’s a catch\. This only works for non\-recursive types:𝐴is a fixed type, not a recursive definition\. To capture𝙽𝚊𝚝and𝙻𝚒𝚜𝚝,we need to level up\. Here’s the move\. Instead of the category of types, we work in the**category of F\-algebras**\. The objects are F\-algebras⟨𝐹,𝑋,𝑓⟩,and the arrows are homomorphisms\. In this category, the initial algebra⟨𝐹,𝜇𝐹,𝚒𝚗⟩is a distinguished object\. Its Hom\-functor𝖧𝗈𝗆\(⟨𝐹,𝜇𝐹,𝚒𝚗⟩,−\)maps any algebra⟨𝐹,𝑋,𝑓⟩to the set of homomorphisms from the initial algebra to it\. By initiality, that set contains exactly one element:𝚏𝚘𝚕𝚍𝑓\. Now introduce the**forgetful functor**𝑈,which takes an algebra⟨𝐹,𝑋,𝑓⟩and discards the structure, keeping only the carrier𝑋\.It’s a functor from the F\-algebra category to𝐒𝐞𝐭category\. Apply Yoneda with𝒞︀as the category of F\-algebras,𝐴=⟨𝐹,𝜇𝐹,𝚒𝚗⟩,and𝐹=𝑈: 𝖭𝖺𝗍\(𝖧𝗈𝗆\(⟨𝐹,𝜇𝐹,𝚒𝚗⟩,−\),𝑈\)≅𝑈\(⟨𝐹,𝜇𝐹,𝚒𝚗⟩\)=𝜇𝐹Let’s decode the left side\. A natural transformation here gives, for each F\-algebra⟨𝐹,𝑋,𝑓⟩,a function from𝖧𝗈𝗆\(⟨𝐹,𝜇𝐹,𝚒𝚗⟩,⟨𝐹,𝑋,𝑓⟩\)to𝑋\.But that Hom\-set is a singleton, it contains only𝚏𝚘𝚕𝚍𝑓\.So specifying this function is equivalent to picking a value of type𝑋for each algebra\. Let’s call it𝑐\[𝑋\]𝑓\.The naturality condition, with the algebra homomorphisms as arrows, becomes exactly: > For any algebra homomorphismℎ:⟨𝐹,𝑋,𝑓⟩→⟨𝐹,𝑌,𝑔⟩,ℎ\(𝑐\[𝑋\]𝑓\)=𝑐\[𝑌\]𝑔\. So the inhabitants of𝙲𝚑𝚞𝚛𝚌𝚑𝙵correspond precisely to the natural transformations on the left side of the Yoneda bijection\. By Yoneda, they are in one\-to\-one correspondence with𝜇𝐹\.Therefore𝙲𝚑𝚞𝚛𝚌𝚑𝙵≅𝜇𝐹\.Put another way: the universal shape of Church encoding,∀𝑋\.\(𝐹𝑋→𝑋\)→𝑋,is a direct translation of “the Yoneda representation of the initial algebra over the forgetful functor\.” This is the full picture\. The Church encoding is Yoneda in disguise\.∀𝑋\.\(𝐹𝑋→𝑋\)→𝑋is the left side of the Yoneda bijection for the initial algebra over the forgetful functor\. Yoneda guarantees it’s isomorphic to𝜇𝐹\.The shape is inevitable\. And here’s the deepest revelation: parametricity and Yoneda are the same idea in two different languages\. The free theoremℎ\(𝑐\[𝐴\]𝑓𝐴\)=𝑐\[𝐵\]𝑓𝐵is the Yoneda naturality square, instantiated in the category of F\-algebras\. The key proof step𝚏𝚘𝚕𝚍𝚒𝚗=𝚒𝚍is Yoneda’s central move: determining the entire natural transformation from a single choice at𝚒𝚍\.88\.The two proofs run in strict parallel: the step𝚏𝚘𝚕𝚍𝑓\(𝑐\[𝜇𝐹\]𝚒𝚗\)=𝑐\[𝑋\]𝑓is the naturality square applied to the homomorphism𝚏𝚘𝚕𝚍𝑓;𝚏𝚘𝚕𝚍𝚒𝚗=𝚒𝚍corresponds to Yoneda’s key step where𝚒𝚍determines the entire transformation\. One path lives inside the type system; the other stands at a higher categorical vantage point\. They are two views of the same structure, mutually reinforcing\.Parametricity is the type\-theoretic shadow of categorical naturality\. ### The Final Recap We can now see the whole arc\. Church encoding begins with a simple intuition: a data type can be replaced by the way you consume it\. From𝚄𝚗𝚒𝚝and𝙱𝚘𝚘𝚕,this yields types like∀𝑋\.𝑋→𝑋and∀𝑋\.𝑋→𝑋→𝑋\.To handle recursive types, we introduce functors𝐹that describe a data type’s one\-layer structure, unifying all Church encodings under a single shape:∀𝑋\.\(𝐹𝑋→𝑋\)→𝑋\. At this point the pieces start locking together\. The inner part𝐹𝑋→𝑋is an**F\-algebra**, and the Church encoding is the universal consumer of F\-algebras: it takes any algebra and produces a value\. Among all F\-algebras, the initial algebra𝜇𝐹\(the recursive data type itself\) plays a special role: its unique fold operation gives us𝚏𝚘𝚕𝚍𝚒𝚗=𝚒𝚍\.Meanwhile, parametricity forces polymorphic functions to behave as natural transformations, yielding the free theoremℎ\(𝑐\[𝐴\]𝑓𝐴\)=𝑐\[𝐵\]𝑓𝐵\.These two facts \(one from initiality, one from parametricity\) interlock cleanly to prove that Church encoding is isomorphic to the original data type:∀𝑋\.\(𝐹𝑋→𝑋\)→𝑋≅𝜇𝐹\. The Yoneda Lemma reveals why the shape must be exactly this\. Applied in the category of F\-algebras, Yoneda states that the natural transformations from the Hom\-functor out of the initial algebra to the forgetful functor are isomorphic to𝜇𝐹itself; and those natural transformations are precisely the inhabitants of∀𝑋\.\(𝐹𝑋→𝑋\)→𝑋\.The Church encoding is thus a direct consequence of one of category theory’s most fundamental results\. Parametricity and Yoneda are two views of the same structure: both rest on naturality, and one is the type\-theoretic shadow of the other\. Returning to the Church numeral𝜆𝑠\.𝜆𝑧\.𝑠\(𝑠𝑧\):it can now be understood as the Church representation of the initial algebra for the functor𝙽𝚊𝚝𝙵\.Church encoding remains an elegant tool in programming, and its shape can be traced along a repeatable path from the consumption intuition all the way to the deep structure of category theory\.