Church Encodings

The lambda calculus has no numbers, no booleans, no pairs — only functions. Yet it is Turing-complete, so it must be able to compute with numbers, booleans and pairs. The resolution is one of the most beautiful ideas in computer science: data is encoded as behaviour. A datum is represented not by a static value but by what it does — how it acts when handed the right arguments. This is Church's encoding, and it is the constructive proof that "functions only" costs us nothing in expressiveness. It is also the ancestor of the Church encoding you meet again in System F, in Böhm–Berarducci encodings, and every time a functional programmer represents a datatype by its fold.

Booleans as choosers

What does a boolean do? It chooses between two alternatives. So encode a boolean as a two-argument function that returns one of its arguments:

\text{TRUE} = \lambda a.\, \lambda b.\, a \qquad \text{FALSE} = \lambda a.\, \lambda b.\, b

\text{TRUE} keeps the first, \text{FALSE} the second. Conditional branching then needs no new machinery — feed the boolean the two branches:

\text{IF} = \lambda p.\, \lambda t.\, \lambda f.\, p\ t\ f

Since \text{IF}\ \text{TRUE}\ t\ f = \text{TRUE}\ t\ f \twoheadrightarrow t, the boolean is the branch selector. The logical connectives fall out too: \text{AND} = \lambda p.\, \lambda q.\, p\ q\ \text{FALSE}, \text{OR} = \lambda p.\, \lambda q.\, p\ \text{TRUE}\ q, \text{NOT} = \lambda p.\, p\ \text{FALSE}\ \text{TRUE}. Watch \text{IF}\ \text{TRUE}\ a\ b reduce to a:

The boolean threads its two arguments through and keeps the first. No primitive if exists; the choosing behaviour is the boolean.

Numbers as iteration

What does a natural number do? It says "do this n times." Encode \overline{n} as the function that applies a given f to a base x exactly n times — the Church numeral:

\overline{0} = \lambda f.\, \lambda x.\, x \qquad \overline{1} = \lambda f.\, \lambda x.\, f\, x \qquad \overline{2} = \lambda f.\, \lambda x.\, f\,(f\, x) \qquad \overline{n} = \lambda f.\, \lambda x.\, f^{\,n}\, x

Arithmetic is now function-plumbing. The successor squeezes in one more application; addition chains m's applications onto n's base; multiplication composes:

\begin{aligned} \text{SUCC} &= \lambda n.\, \lambda f.\, \lambda x.\, f\,(n\, f\, x) \\ \text{PLUS} &= \lambda m.\, \lambda n.\, \lambda f.\, \lambda x.\, m\, f\,(n\, f\, x) \\ \text{MULT} &= \lambda m.\, \lambda n.\, \lambda f.\, m\,(n\, f) \end{aligned}

Notice \text{MULT}\ m\ n feeds m the function "apply f exactly n times" — so f fires m \times n times. Even exponentiation is startlingly terse: \text{EXP} = \lambda m.\, \lambda n.\, n\ m.

Pairs, and the notorious predecessor

A pair does one thing: given a selector, it hands over its two components. So a pair is a function awaiting a selector, and projection just supplies \text{TRUE} or \text{FALSE}:

\text{PAIR} = \lambda a.\, \lambda b.\, \lambda s.\, s\ a\ b \qquad \text{FST} = \lambda p.\, p\ \text{TRUE} \qquad \text{SND} = \lambda p.\, p\ \text{FALSE}

Pairs unlock the hardest classical exercise: the predecessor. Since a numeral can only count up (apply f more times), going down seems impossible. The trick is to carry a pair (a, b) and "shift" it n times, where each shift moves the running counter into first place and advances the second: (a, b) \mapsto (b, b+1). Starting from (0, 0) and shifting n times gives (n-1, n), whose first component is the predecessor:

\text{PRED} = \lambda n.\, \text{FST}\big(n\ (\lambda p.\, \text{PAIR}\ (\text{SND}\ p)\ (\text{SUCC}\,(\text{SND}\ p)))\ (\text{PAIR}\ \overline{0}\ \overline{0})\big)

With \text{PRED} in hand, subtraction, comparison and bounded search all follow — enough to program any computable numeric function.

Church arithmetic, running

Every operator above is a genuine higher-order function; the encoding is not a metaphor. Below we build the booleans, numerals, pairs and the predecessor as real closures and decode them back to ordinary integers with toInt. Press Run — the data was functions all along.

type Church = (f: (v: number) => number) => (x: number) => number; const zero: Church = (f) => (x) => x; const succ = (n: Church): Church => (f) => (x) => f(n(f)(x)); const plus = (m: Church, n: Church): Church => (f) => (x) => m(f)(n(f)(x)); const mult = (m: Church, n: Church): Church => (f) => m(n(f)); const toInt = (n: Church): number => n((v) => v + 1)(0); const one = succ(zero), two = succ(one), three = succ(two); console.log("succ, plus, mult:"); console.log(" 3 =", toInt(three)); // 3 console.log(" 2 + 3 =", toInt(plus(two, three))); // 5 console.log(" 2 * 3 =", toInt(mult(two, three))); // 6 // Booleans as choosers. const TRUE = (a: any) => (_b: any) => a; const FALSE = (_a: any) => (b: any) => b; const IF = (p: any) => (t: any) => (f: any) => p(t)(f); console.log("IF:"); console.log(" IF TRUE a b =", IF(TRUE)("a")("b")); // a console.log(" IF FALSE a b =", IF(FALSE)("a")("b")); // b // Pairs and the predecessor via the shifting-pair trick. const PAIR = (a: any) => (b: any) => (s: any) => s(a)(b); const FST = (p: any) => p(TRUE); const SND = (p: any) => p(FALSE); const pred = (n: Church): Church => { const shift = (p: any) => PAIR(SND(p))(succ(SND(p))); const start = PAIR(zero)(zero); // apply `shift` n times to `start`, then take the first component return FST((n as any)(shift)(start)); }; console.log("predecessor:"); console.log(" pred(3) =", toInt(pred(three))); // 2 console.log(" pred(1) =", toInt(pred(one))); // 1 (numeral 1 shifts once → (0,1)) console.log(" pred(0) =", toInt(pred(zero))); // 0 (bottoms out at zero)

pred(3) comes out 2 — climbing down a ladder that only offered rungs up, purely by carrying a pair along for the ride. Church encodings turn the slogan "code is data, data is code" into a working reality with nothing but \lambda.

In the early days Church and his students could encode successor, addition and multiplication almost immediately, but predecessor resisted for months — it felt as though a Church numeral, able only to iterate f forward, simply could not undo a step. Church half-suspected it might be impossible, which would have been catastrophic: without predecessor you cannot do subtraction or bounded loops, and the claim that every computable function is lambda-definable would wobble. The story goes that Stephen Kleene hit on the shifting-pair solution in 1932 in the dentist's chair, mid-extraction, and rushed to write it down. The technique — thread a little extra state (here a pair) through the iteration so that "one step behind" is always available — is the same idea behind computing a Fibonacci pair or a running total in a single fold. A dental emergency, it turns out, secured the foundations of computability.

The pure-calculus \text{IF}\ p\ t\ f = p\ t\ f looks like a drop-in conditional, and under normal order it behaves like one: the unchosen branch, being discarded, is never reduced. But transplant the encoding into a call-by-value host — like the JavaScript the code above compiles to — and both t and f are evaluated before \text{IF} is even called, because CBV evaluates all arguments first. So IF cond expensive loopForever would diverge even when cond is false. This is exactly the evaluation-order hazard from the previous lesson biting in practice. The fix is to pass the branches as thunks (\lambda z.\, t and \lambda z.\, f) and force only the chosen one — which is why real strict languages give if special, non-strict evaluation rather than treating it as an ordinary function.

A second, gentler caution: the Church numeral \overline{2} is not the integer 2. It is a function; only after applying it to a successor and a zero (as toInt does) does an honest integer appear. Do not expect \overline{2} and \overline{3} to be comparable with < — comparison itself must be encoded.