Church Encoding, Parametricity, and the Yoneda Lemma

Summary

Church Encoding, Parametricity, and the Yoneda LemmaI 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 NatI 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 FTo 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 funct...