Scott encoding

Representing 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.

zero succ pred = λ z . λ s . z = λn . λ z . λ s . s n = λn . n zero (λm . m)

The Church numeral 3 is $λ f . λ x . f (f (f x))$ : the whole iteration. The Scott numeral 3 is $λ z . λ s . s 2$ : one layer and the rest. Church's numeral is its own fold, so a match costs a full traversal, which is why its predecessor is linear. Scott's is its own match, so a fold needs recursion:

add = Y (λa . λm . λn . m n (λ m^{'} . succ (a m^{'} n)))

In OCaml the recursive type is a record with a polymorphic field, and the recursion comes from let rec.

(* A Scott numeral is its own case analysis: what to do for zero,
   and what to do with the predecessor. *)
type nat = { case : 'r. 'r -> (nat -> 'r) -> 'r }
 
let zero = { case = (fun z _ -> z) }
let succ n = { case = (fun _ s -> s n) }
 
let pred n = n.case zero (fun m -> m)          (* one step, no iteration *)
let is_zero n = n.case true (fun _ -> false)
 
(* Anything that iterates needs recursion from outside the encoding. *)
let rec add m n = m.case n (fun m' -> succ (add m' n))
let to_int n =
  let rec go acc n = n.case acc (fun m -> go (acc + 1) m) in
  go 0 n
 
let of_int k =
  let rec go acc k = if k = 0 then acc else go (succ acc) (k - 1) in
  go zero k

pred on a numeral a million deep is one step.

pred 1000000     ->  999999
add 2 3          ->  5
is_zero (pred 1) ->  true

The type is recursive, $N ≅ \forall r . r \to (N \to r) \to r$ , so it cannot be written in System F without recursive types. Mogensen used the same encoding for λ-terms themselves, which gives a self-interpreter for the λ-calculus a few lines long.