Church encoding

Representing data as functions in the pure lambda calculus: the numeral n applies its argument n times, true and false choose between two arguments, and a pair waits for a selector. Addition, multiplication and exponentiation are one line each; the predecessor needs a trick and takes time linear in n.

Each is a fact about iteration. Applying $f$ $n$ times and then $m$ times applies it $m+n$ times. Iterating $nf$ a total of $m$ times applies $f$ $mn$ times, so multiplication is composition of numerals. And $nm$ composes $m$ with itself $n$ times, which is $m^n$.

A numeral can only iterate; it has no access to the number it was built from. Kleene's predecessor iterates on pairs instead, $(a,b)\mapsto (b,b+1)$ starting from $(0,0)$.^[2] After $n$ steps the pair is $(n-1,n)$, and the first component is the answer:

It takes $n$ steps to go down by one.

(* A numeral is "apply f n times", for every type of f. *)
type church = { run : 'a. ('a -> 'a) -> 'a -> 'a }
 
let zero = { run = (fun _ x -> x) }
let succ n = { run = (fun f x -> f (n.run f x)) }
let plus m n = { run = (fun f x -> m.run f (n.run f x)) }
let mult m n = { run = (fun f -> m.run (n.run f)) }
let exp m n = { run = (fun f x -> n.run m.run f x) }
 
(* Predecessor: iterate (a, b) -> (b, b + 1) from (0, 0), keep the first. *)
let pred n = fst (n.run (fun (_, b) -> (b, succ b)) (zero, zero))
 
let to_int n = n.run (( + ) 1) 0
let rec of_int k = if k = 0 then zero else succ (of_int (k - 1))
 
(* Booleans and pairs: a choice, and a function waiting for a selector. *)
let tru t _ = t
let fls _ f = f
let pair a b sel = sel a b

plus 2 3   ->  5
mult 2 3   ->  6
exp 2 3    ->  8
pred 3     ->  2
pred 0     ->  0
pair 1 2 fls  ->  2

Typed as $\forall \alpha .(\alpha \to \alpha )\to \alpha \to \alpha$, these are System F's natural numbers, and Böhm and Berarducci showed every inductive type can be encoded the same way:^[3] the encoding of a value is its own fold.

• Scott encodingRepresenting data by its case analysis rather than its fold: a Scott numeral takes what to do for zero and what to do with the predecessor. Pattern matching and the predecessor take one step; iteration needs recursion from outside, such as a fixed-point combinator.
• Y combinatorA lambda term Y with Y f = f (Y f) for every f, which gives recursion to a language with no named definitions. Under call-by-value it loops before f is ever called; the Z combinator puts the self-application behind a lambda and works in strict languages.
• SKI combinatorsThree combinators, S x y z = x z (y z), K x y = x and I x = x, from which every closed lambda term can be built by application alone, with no variables. I is redundant, since S K K x = x. The translation from lambda terms is called bracket abstraction.
• HylomorphismA function that unfolds a seed into a recursive structure and folds that structure into a result, written so the structure is never built: hylo f g = f . fmap (hylo f g) . g. The call tree of the recursion is the intermediate structure.
• Algebraic data typeA type built from sums (a value is one of several cases) and products (a value has several fields at once), possibly recursively. The name comes from counting: the number of values of a sum is the sum of the counts, and of a product the product, so types obey the laws of algebra.
• CurryingTurning a function of several arguments into a function of the first argument that returns a function of the rest: f : A * B -> C becomes curry f : A -> (B -> C). In OCaml and Haskell every function is curried, so applying it to fewer arguments than it takes, partial application, is ordinary.
• De Bruijn indicesA representation of lambda terms without variable names: each variable is the number of binders between it and the lambda that binds it. Alpha-equivalent terms become identical and substitution cannot capture a variable, at the price of shifting indices when a term moves under a binder.

1. [1]A. Church, The Calculi of Lambda-Conversion, Princeton University Press (1941).
2. [2]S. C. Kleene, “A theory of positive integers in formal logic”, American Journal of Mathematics 57 (1935).
3. [3]C. Böhm, A. Berarducci, “Automatic synthesis of typed Λ-programs on term algebras”, Theoretical Computer Science 39 (1985).