Church Encodings and the Cost of Representing Data as Functions

The untyped lambda calculus has no numbers, no booleans, and no pairs. It has variables, abstraction, and application, and that is all. The claim that this is enough for all computation is not a slogan; it is a construction, and the construction is the subject here. Every data type has to be encoded as a function, and the encodings are not arbitrary. They are chosen so that the elimination form of the type — the operation that consumes a value — becomes the type’s definition.

That principle produces the Church numerals, and it also produces their weaknesses. A numeral is an iterator, so the number n is represented by a term whose normal form has size proportional to n. Arithmetic on those terms costs steps proportional to the values involved, which makes the encoding canonical but a poor basis for a practical runtime. Both facts are worth understanding, because the gap between them explains why real implementations encode numbers as machine words and only use the Church form when the calculus itself is the object of study.

Booleans and pairs as eliminators

Start with the smallest case. A boolean is a value that selects between two alternatives. So the encoding of true takes two arguments and returns the first; false takes two and returns the second.

true  = λt. λf. t
false = λt. λf. f

The eliminator, if, is application: if b then x else y is simply b x y. There is no primitive conditional, and none is needed. true x y →→ x and false x y →→ y by two beta steps each, so the conditional costs one application and no test.

The derived operations fall out of the same idea. Negation applies its argument to false and true, in that order: not = λb. b false true. Conjunction is λp. λq. p q false, which returns q when p is true and false when p is false. Disjunction is λp. λq. p true q. Each reduces in a small fixed number of beta steps at the point of use, and each is a total function on the two encodings.

Pairs follow the same pattern. A pair is a value that, given a selector, applies the selector to both components. So

pair   = λx. λy. λf. f x y
fst    = λp. p (λx. λy. x)
snd    = λp. p (λx. λy. y)

fst (pair a b) →→ a in three steps, and the selector passed to fst is exactly the encoding of true. That coincidence is structural, not accidental: fst is the projection that keeps the first component, and true is the selector that keeps its first argument. The same term serves both roles.

The pattern generalises to any finite sum. A value of type A + B is a function taking two continuations and applying the appropriate one; a value of type A × B is a function taking a continuation of two arguments. The encodings are the eliminators, and the constructors are the terms that supply the arguments. This is the visitor or fold representation, and its typed version is a standard technique in functional programming for exactly this reason: the representation makes it impossible to forget a case, because the type of the value determines which continuations it accepts.

Numerals as iterators

A natural number is a count of repetitions. The Church numeral for n is the function that, given f and x, applies f to x exactly n times:

0 = λf. λx. x
1 = λf. λx. f x
2 = λf. λx. f (f x)
3 = λf. λx. f (f (f x))

The numeral is the iterator, and the eliminator is application to a successor function and a base value. plus is the composition of two iterators:

plus = λm. λn. λf. λx. m f (n f x)

Read it as: iterate f n times starting from x, then iterate f m times on the result. plus 2 3 reduces to 5 after the beta steps that unfold the two numerals, and the step count is linear in the sum. Multiplication composes iterators differently, applying the second numeral’s iterator m times to f:

mult = λm. λn. λf. m (n f)

mult 2 3 f is 2 (3 f), which is f iterated 6 times. Exponentiation is the neatest of the three, because a numeral applied to a function is an iteration, so n m iterates m n times:

exp = λm. λn. n m

exp 2 3 gives 3 2, which applies the numeral 2 as a function three times; a numeral applied to a numeral composes, so the result is 2 ∘ 2 ∘ 2, whose value is 8. The definition is one line and its correctness is immediate from the iterator reading: applying m to x produces the m-fold composite of x, so applying it n times produces the m^n-fold composite.

Addition, multiplication, and exponentiation all cost a number of beta steps proportional to the number of applications in the result, because each step of the reduction is one application of f. That is the fundamental cost of unary representation: the term for 1000 has 1000 applications of f in its normal form, and computing with it moves that many redexes.

Predecessor, and why subtraction is harder

Successor is trivial, because an iterator can be extended by one more application:

succ = λn. λf. λx. f (n f x)

Predecessor is the hard case, and the reason is a mismatch of direction. The numeral describes what to do with f; the predecessor needs to undo one application, and there is no inverse available. The standard solution carries a pair through the iteration, recording the previous value at each step:

pred = λn. λf. λx.
         fst (n (λp. pair (snd p) (f (snd p))) (pair x x))

The state is a pair (previous, current). One step of the iterated function keeps the current value as the new first component and applies f to it for the new second component, so after n steps the pair holds (f^(n-1) x, f^n x), and the first projection is the predecessor. The base case seeds the pair with (x, x), which makes pred 0 equal to 0: the first projection of the seed is x, so the encoding has no negative numbers and predecessor saturates at zero.

The step count is what the encoding costs. Each of the n iterations performs a pair construction and two projections, so predecessor is linear in n with a constant factor of several beta steps per iteration, where successor is linear with a constant of one. Subtraction is then repeated predecessor, which makes minus m n cost O(m·n) beta steps. Comparison is worse: deciding m ≤ n requires iterating a test that itself iterates, and the straightforward encoding is O(m·n) with a large constant. None of these are efficient, and none of them are wrong.

The deeper point is that the predecessor encoding is not canonical in the way the numerals are. Several encodings exist — the pair-based one above, a version using a fold over a two-element sum, and variants that use the numeral applied to a term that returns a function of the “seen a zero yet” flag. They all compute the same function, and they differ in step count by constant factors. The numerals themselves are canonical up to beta-eta equivalence, which is what makes them a useful specification and a poor implementation.

What the encoding costs in practice

Three numbers characterise the representation.

Size of the normal form. The Church numeral for n has a number of nodes proportional to n: two binders, n application nodes, and n+1 occurrences of f. A 64-bit integer occupies 8 bytes in a machine register and constant space in a term. The Church numeral for 2^64 would need on the order of 10^19 nodes, which is beyond the memory of any machine that could hold it.

Step count for arithmetic. Addition and multiplication are linear in the result magnitude. Exponentiation is not: exp m n reduces to the numeral for m^n, so the normal form has m^n applications in it, and the number of beta steps to reach that normal form is proportional to m^n. A doubling in n squares the work. This is not an implementation defect; it is what the encoding means.

Sharing. The pure calculus has no sharing. Reducing (λx. x x) N duplicates N, and if N is a large numeral, every use duplicates the whole unary structure. Implementations that use graph reduction or environments avoid the duplication by sharing, which is what makes it possible to run Church-encoded programs at all. Without sharing, a program that applies the same large numeral twice produces two copies of it, and repeated doubling squares the size of the normal form at each step, so a few dozen doublings produce a term with more nodes than any machine could hold.

The typed version of the encoding has a further property worth noting: in System F, the Church numeral type is ∀α. (α → α) → α → α, and the encoding is parametric, meaning a function of that type can only iterate. That is a theorem, not a convention, and it is the basis of the “free theorems” results. In the untyped calculus the guarantee vanishes: a term of the numeral shape can inspect its arguments in arbitrary ways, so nothing forces it to behave like a number. Typing is what restores the invariant.

Encoding as a design decision

The choice of encoding is a choice about which operations are cheap. Church numerals make iteration cheap and inspection expensive; a different encoding — binary numerals as lists of bits, or Scott numerals as case-eliminators — trades those costs differently. Scott numerals, where the numeral is a fold that immediately returns its base case or recurses, make pattern matching cheap and iteration comparatively awkward. Binary encodings make the term size logarithmic in the value but require the arithmetic to carry.

All of these are correct, and they are not equivalent as programs. The lambda calculus defines functions up to beta-eta equivalence, and two encodings of the same number are not beta-eta equivalent unless they are the same term; they are merely observationally equivalent when used through the standard operations. A program that inspects the structure of a numeral — for instance, one that counts the number of applications in its normal form — distinguishes them, which is why the encodings are a genuine interface and not a notational variant.

The elimination principle also explains why the encoding is stable under extension. Adding a new operation to a data type means writing a function that consumes the eliminator form, and the existing values need not change. That is the same property the visitor pattern has, and the same cost: adding a new constructor requires changing every consumer, because the eliminator’s arity is baked into the encoding. The expression problem appears in the lambda calculus before it appears in any programming language, and it appears as a choice about how to write the encoding.

Iteration with no base case that terminates is where the encodings meet the fixed points. A numeral always terminates because it applies f a finite number of times; the general recursion operator has no such guarantee, and its encoding requires a term that reproduces itself, which no finite normal form can do. That construction is the subject of fixed-point combinators and recursion. The typed reading of these encodings, where parametricity restores the guarantees the untyped calculus lacks, is a separate subject; what matters here is that the untyped encoding is a total function only when the terms it consumes terminate, and the confluence result is what makes “the numeral it reduces to” a well-defined thing to ask about.