Church encoding

Church encoding represents data in the pure λ-calculus, which has nothing but functions, by functions. The natural number $n$ is the function that applies its argument $n$ times, a boolean is a function that chooses between two alternatives, and a pair is a function waiting for a selector. In general a value is represented by its own fold: what it does to a given interpretation of its constructors. Arithmetic, logic and data structures all become λ-terms, which is how Church and Kleene showed that the λ-calculus can express every computable function^[1]^[3]. In typed form the encoding needs polymorphism, and in System F it applies to every algebraic data type^[6].

§ 01

Overview

The λ-calculus has three kinds of term, variables, functions $λ x . e$ and applications $e_{1} e_{2}$ , and one rule of computation, β-reduction, $(λ x . e) a \to e [a / x]$ . It has no numbers, truth values or data structures. Church encoding supplies them by representing each kind of data by what can be done with it. A natural number is used for iteration, so the number $n$ is represented by the operation "iterate $n$ times"; a boolean is used to choose, so it is represented by a choice. Operations on data then become operations on these functions, and computation is β-reduction.

§ 02

Church numerals

The Church numeral $n$ takes a function $f$ and a starting value $x$ and applies $f$ to $x$ $n$ times:

0 = λ f . λ x . x 1 = λ f . λ x . f x 2 = λ f . λ x . f (f x) n = λ f . λ x . f^{n} x

A numeral is converted to an ordinary number by applying it to the successor function and zero, and to anything else by choosing a different $f$ and $x$ .

Arithmetic

The arithmetic operations follow from the laws of iteration, $f^{m} (f^{n} x) = f^{m + n} x$ and $(f^{n})^{m} = f^{mn}$ :

succ plus mult exp = λn . λ f . λ x . f (n f x) = λm . λn . λ f . λ x . m f (n f x) = λm . λn . λ f . m (n f) = λm . λn . n m

Exponentiation is application: $n m$ composes $m$ with itself $n$ times, and the $n$ -fold composite of "iterate $m$ times" iterates $m^{n}$ times. The terms can be checked by reducing them to normal form:

An untyped λ-calculus with normal-order reduction, and Church arithmetic in it.

(* Untyped lambda terms with de Bruijn indices, and normal-order
   reduction to normal form, counting beta-steps. *)
type t = Var of int | Lam of t | App of t * t
 
let rec shift d c = function
  | Var k -> Var (if k >= c then k + d else k)
  | Lam b -> Lam (shift d (c + 1) b)
  | App (a, b) -> App (shift d c a, shift d c b)
 
let rec subst j s = function
  | Var k -> if k = j then s else Var k
  | Lam b -> Lam (subst (j + 1) (shift 1 0 s) b)
  | App (a, b) -> App (subst j s a, subst j s b)
 
let beta body arg = shift (-1) 0 (subst 0 (shift 1 0 arg) body)
 
(* One leftmost-outermost step, if there is a redex. *)
let rec step = function
  | App (Lam b, a) -> Some (beta b a)
  | App (a, b) -> (
      match step a with Some a' -> Some (App (a', b)) | None -> Option.map (fun b' -> App (a, b')) (step b))
  | Lam b -> Option.map (fun b' -> Lam b') (step b)
  | Var _ -> None
 
let normalize t =
  let rec go n t = match step t with Some t' -> go (n + 1) t' | None -> (t, n) in
  go 0 t
 
(* Terms are written with names, a % b for the application a b, and
   converted to indices. *)
type named = V of string | L of string * named | A of named * named
let ( % ) a b = A (a, b)
let rec index env = function
  | V x -> let rec find i = function y :: r -> if x = y then i else find (i + 1) r | [] -> failwith x in Var (find 0 env)
  | L (x, b) -> Lam (index (x :: env) b)
  | A (a, b) -> App (index env a, index env b)
let lam xs b = List.fold_right (fun x b -> L (x, b)) xs b
 
(* Church numerals and arithmetic. *)
let church n = lam [ "f"; "x" ] (let rec go k = if k = 0 then V "x" else V "f" % go (k - 1) in go n)
let succ = lam [ "n"; "f"; "x" ] (V "f" % (V "n" % V "f" % V "x"))
let plus = lam [ "m"; "n"; "f"; "x" ] (V "m" % V "f" % (V "n" % V "f" % V "x"))
let mult = lam [ "m"; "n"; "f" ] (V "m" % (V "n" % V "f"))
let exp = lam [ "m"; "n" ] (V "n" % V "m")
let pair = lam [ "a"; "b"; "s" ] (V "s" % V "a" % V "b")
let fst_ = lam [ "p" ] (V "p" % lam [ "a"; "b" ] (V "a"))
let snd_ = lam [ "p" ] (V "p" % lam [ "a"; "b" ] (V "b"))
 
(* Kleene's predecessor: step (a, b) to (b, b + 1), n times from (0, 0). *)
let pred_pairs =
  lam [ "n" ] (fst_ % (V "n" % lam [ "p" ] (pair % (snd_ % V "p") % (succ % (snd_ % V "p"))) % (pair % church 0 % church 0)))
 
(* The usual predecessor, without pairs. *)
let pred = lam [ "n"; "f"; "x" ] (V "n" % lam [ "g"; "h" ] (V "h" % (V "g" % V "f")) % lam [ "u" ] (V "x") % lam [ "u" ] (V "u"))
 
(* Scott numerals: a number is its own case analysis. *)
let scott n = let rec go k = if k = 0 then lam [ "z"; "s" ] (V "z") else lam [ "z"; "s" ] (V "s" % go (k - 1)) in go n
let scott_pred = lam [ "n" ] (V "n" % scott 0 % lam [ "m" ] (V "m"))
 
(* Printing, with names chosen by binding depth. *)
let names = [| "f"; "x"; "y"; "z"; "u"; "v"; "w" |]
let rec show d = function
  | Var k -> names.(d - 1 - k)
  | Lam b -> "\\" ^ names.(d) ^ ". " ^ show (d + 1) b
  | App (a, b) -> show_fun d a ^ " " ^ show_arg d b
and show_fun d = function Lam _ as t -> "(" ^ show d t ^ ")" | t -> show d t
and show_arg d = function Var _ as t -> show d t | t -> "(" ^ show d t ^ ")"
let show = show 0

Normal forms and the number of β-steps to reach them.

succ 2       ->  \f. \x. f (f (f x))                        3 steps
plus 2 3     ->  \f. \x. f (f (f (f (f x))))                6 steps
mult 2 3     ->  \f. \x. f (f (f (f (f (f x)))))            7 steps
exp 2 3      ->  \f. \x. f (f (f (f (f (f (f (f x)))))))   16 steps
pred 3       ->  \f. \x. f (f x)                           11 steps

Predecessor

Subtracting one is much harder, because a numeral can only apply $f$ more times, never fewer. Kleene's solution iterates on pairs, carrying the previous value along:

step (a, b) = (b, b + 1) step^{n} (0, 0) = (n - 1, n) (n \geq 1) pred n = fst (step^{n} (0, 0))

Kleene later recalled finding it while at the dentist^[4]. The predecessor usually given today avoids pairs, by iterating a function that delays each application of $f$ by one step and discarding the first:

pred = λn . λ f . λ x . n (λ g . λh . h (g f)) (λ u . x) (λ u . u)

Either way the predecessor of $n$ takes a number of β-steps proportional to $n$ , where a unary representation with a direct case analysis would take a constant number. The Scott encoding, which represents a number by its case analysis instead of its fold, has a constant-time predecessor:

β-steps to compute the predecessor of n, Church (with pairs and without) and Scott.

n          pred (pairs)               pred         Scott pred
1                    16                  7                  4
2                    26                  9                  4
4                    46                 13                  4
8                    86                 21                  4
16                  166                 37                  4
32                  326                 69                  4
64                  646                133                  4

Subtraction is iterated predecessor, $sub m n = n pred m$ , and takes time proportional to $m \cdot n$ .

§ 03

Booleans, pairs and sums

A boolean chooses between two alternatives, so $true$ returns the first and $false$ the second, and a conditional is the boolean itself applied to the two branches:

true = λ t . λ f . t false = λ t . λ f . f if b then s else t = b s t

not = λb . λ t . λ f . b f t and = λ p . λ q . p q p iszero = λn . n (λ u . false) true

A pair holds two values until it is given a function to pass them to, and a sum, a value of one of two types, is given one function for each case:

pair = λa . λb . λ s . s a b fst = λ p . p true inl = λa . λ l . λ r . l a inr = λb . λ l . λ r . r b

With numerals, booleans and pairs, together with a fixed-point combinator for general recursion, every partial recursive function can be written as a λ-term. This was the content of Kleene's proof that λ-definability coincides with recursiveness^[3], and with Turing's proof of its equivalence with Turing computability^[14] it supports the Church–Turing thesis.

§ 04

Lists and algebraic data types

A list is represented by its right fold: given a function to combine an element with the folded rest, and a value for the empty list, it returns the result of folding. Every algebraic data type can be encoded in the same way, by abstracting over one function per constructor, each receiving the constructor's arguments with recursive positions already folded. A natural number is the special case with constructors $zero$ and $succ$ , whose fold is iteration.

Church-encoded lists and binary trees in OCaml, where each value is its own fold.

(* A Church list is its own fold: what to do with each element and the
   folded rest, and what to return for the empty list. *)
type 'a clist = { fold : 'r. ('a -> 'r -> 'r) -> 'r -> 'r }
 
let nil = { fold = (fun _ n -> n) }
let cons x xs = { fold = (fun c n -> c x (xs.fold c n)) }
let append xs ys = { fold = (fun c n -> xs.fold c (ys.fold c n)) }
let map f xs = { fold = (fun c n -> xs.fold (fun x r -> c (f x) r) n) }
let filter p xs = { fold = (fun c n -> xs.fold (fun x r -> if p x then c x r else r) n) }
let length xs = xs.fold (fun _ r -> r + 1) 0
let sum xs = xs.fold ( + ) 0
let to_list xs = xs.fold List.cons []
let of_list l = List.fold_right cons l nil
 
(* A binary tree is its fold too. *)
type 'a ctree = { foldt : 'r. 'r -> ('r -> 'a -> 'r -> 'r) -> 'r }
 
let leaf = { foldt = (fun l _ -> l) }
let node a x b = { foldt = (fun l n -> n (a.foldt l n) x (b.foldt l n)) }
let size t = t.foldt 0 (fun a _ b -> a + 1 + b)
let depth t = t.foldt 0 (fun a _ b -> 1 + max a b)
let inorder t = to_list (t.foldt nil (fun a x b -> append a (cons x b)))

Running it.

map square       [1; 4; 9; 16; 25]
filter even      [2; 4]
append           [1; 2; 3; 4; 5; 6; 7]
length, sum      5, 15
tree size 4, depth 3, in order [1; 2; 3; 4]

Operations that fold a structure are simple in this representation, and appending two lists is a composition of folds that does no work until the result is consumed. Operations that inspect a structure and stop are not: taking the tail of a Church list has the same difficulty as the predecessor, and takes time proportional to the length of the list^[15].

§ 05

Typing

Simple types

In the simply typed λ-calculus a numeral can be typed at $Nat_{τ} = (τ \to τ) \to τ \to τ$ for any fixed type $τ$ , but each numeral then iterates over one type only. Schwichtenberg showed that the functions on $Nat_{τ}$ definable in this way are exactly the extended polynomials, built from constants, addition, multiplication and a case distinction on zero^[9]. Predecessor is not among them for a single type $τ$ , nor is exponentiation, which uses a numeral at a different type from its argument.

System F

In System F, the polymorphic λ-calculus of Girard and Reynolds^[7]^[8], the type of numerals quantifies over the type being iterated, and every algebraic data type has an encoding of this form^[6]:

Bool A \times B List A = \forall α . α \to α \to α = \forall α . (A \to B \to α) \to α = \forall α . (A \to α \to α) \to α \to α Nat A + B = \forall α . (α \to α) \to α \to α = \forall α . (A \to α) \to (B \to α) \to α

These are called Böhm–Berarducci encodings, after the authors who gave the general construction for any signature of constructors^[6]. They are impredicative: $Nat$ quantifies over all types, including $Nat$ itself, which is what lets exponentiation and the pair-based predecessor type-check. Every closed normal term of type $Nat$ is, up to η-conversion, a Church numeral, so the encoding contains no junk; parametricity gives the same conclusion semantically and implies that the encoding satisfies the induction principle of the natural numbers^[10].

In OCaml

ML type inference is limited to rank-1 polymorphism: a function's parameter has a single type within the function's body. A numeral passed as an argument therefore cannot be used at two different types:

A function that uses its numeral argument at int and at bool.

(* Without the record, a numeral passed as an argument has one type. *)
let both n = (n (( + ) 1) 0, n not true)

The compiler's error.

File "ch2_bad.ml", line 2, characters 31-34:
2 | let both n = (n (( + ) 1) 0, n not true)
                                   ^^^
Error: This expression has type bool -> bool
       but an expression was expected of type int -> int
       Type bool is not compatible with type int

A record or object with an explicitly polymorphic field restores the quantifier of the System F type, so the numeral can be instantiated at each use:

Church numerals and booleans with polymorphic record fields.

(* In OCaml a numeral must be polymorphic in the type it iterates over, so
   it is wrapped in a record with a polymorphic field. *)
type nat = { 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 -> n.run m.run f) }
let pred n = fst (n.run (fun (_, b) -> (b, succ b)) (zero, zero))
let sub m n = n.run pred m
 
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 choose between two alternatives. *)
type bool_ = { choose : 'a. 'a -> 'a -> 'a }
 
let tru = { choose = (fun t _ -> t) }
let fls = { choose = (fun _ f -> f) }
let not_ b = { choose = (fun t f -> b.choose f t) }
let is_zero n = n.run (fun _ -> fls) tru
let leq m n = is_zero (sub m n)
 
(* The same numeral used at two different types. *)
let both n = (n.run (( + ) 1) 0, n.run not true, n.run (fun s -> s ^ "*") "")

Running it.

plus 2 3 = 5   mult 2 3 = 6   exp 2 3 = 8   exp 3 2 = 9
pred 3 = 2   pred 0 = 0   sub 3 2 = 1   sub 2 3 = 0
leq 2 3 = true   leq 3 2 = false
both 3 = (3, false, "***")

Haskell writes the same types with RankNTypes, as newtype Nat = Nat (forall a. (a -> a) -> a -> a).

§ 06

Uses

Church encodings appear in functional programming where representing data by its fold changes the cost of operations. The foldr/build fusion rule of the Glasgow Haskell Compiler removes intermediate lists: build takes a list in Church-encoded form, and a fold applied to it is replaced by an application, so the list is never constructed^[11]. A free monad in Church-encoded form turns left-nested binds, which take quadratic time on the ordinary representation, into linear time^[12]. The encoding of a data type as the type of its fold is also the basis of the Scott encoding, which represents a value by its case analysis instead.

In proof assistants based on impredicative type theories, Church encodings define data types in terms of quantification alone, though they do not give the dependent induction principles that inductive types provide, which is one reason those systems add inductive types as a primitive.

§ 07

History

Church introduced the numerals in his work on the λ-calculus in the early 1930s, and used them in 1936 to state an undecidable problem^[1]; the definitions appear in his 1941 monograph^[2]. Kleene found the predecessor and went on to show that every recursive function is λ-definable^[3]. Girard and Reynolds independently introduced the polymorphic λ-calculus in 1972 and 1974, in which the encodings have types^[7]^[8], and Böhm and Berarducci gave the general encoding of algebraic data types in 1985^[6]. The textbook treatment of the untyped encodings is in Barendregt^[5] and, for programming, Pierce^[13].