Church Encoding, Parametricity, and the Yoneda Lemma May 19, 2026<br>29 mins read<br>Table of Contents<br>Church Encoding, Parametricity, and the Yoneda Lemma<br>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:<br>data Nat = Zero | Succ NatI went on to learn that all computation can be expressed through functions (the lambda calculus), that recursion itself can be encoded as the mind-bending Y combinator:<br>Y = λf. (λx. f (x x)) (λx. f (x x))And then there were Church numerals, where each number becomes a function:<br>0 = λs. λz. z<br>1 = λs. λz. s z<br>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.<br>But what is the reasoning behind it? Why these particular lambda terms?<br>There is also Church encoding for lists:<br>nil = λc. λn. n<br>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.<br>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 the connections, the encoding’s shape stops being a trick and starts being inevitable.<br>I want to trace those connections here. We’ll start with the simplest data types, watch a pattern emerge, and build up the machinery: parametricity, algebraic data types, F-algebras, the Yoneda Lemma, until Church encoding looks less like a clever trick and more like something the math demands.<br>System F<br>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..<br>But STLC hits a wall almost immediately. A Church numeral must accept any type as its carrier: the whole point is that 2 works the same whether you’re counting apples or functions. STLC can’t say that. Every function in STLC has a fixed, monomorphic type.<br>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.<br>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.<br>Our System F starts as an empty universe. In STLC, we would declare base types like 𝚄𝚗𝚒𝚝 and 𝙱𝚘𝚘𝚕 to get started. But in System F, it’s interesting that 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.<br>Let me state a principle: a data type can be equivalently represented by the ways you consume it. I can’t yet explain the logic behind this claim, but let’s set it aside and see how it works for 𝚄𝚗𝚒𝚝. 33.In the second half of this article, we’ll see the category-theoretic foundation for this principle. The Yoneda Lemma will show that the set of all ways to consume a type fully determines the type itself.<br>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.<br>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:<br>∀𝑋.𝑋→𝑋Read as: “for any type 𝑋, give me an 𝑋 and I’ll give you back an 𝑋.”<br>What inhabits this type? It is easy to think of one: the identity function.44.Later we’ll see that this is the only possible implementation, as a consequence of parametricity. It takes an 𝑋 and returns it unchanged:<br>id = ΛX. λx. xThis function is the Church encoding of 𝚄𝚗𝚒𝚝.<br>Let’s try the same reasoning with 𝙱𝚘𝚘𝚕. 𝙱𝚘𝚘𝚕 has two constructors, 𝚃𝚛𝚞𝚎 and 𝙵𝚊𝚕𝚜𝚎.<br>What does consuming a...