Church encoding

In pure λ-calculus there are no numbers, no booleans, no structures — only functions. Church encoding shows that nothing else is needed: data are their own processing operations.

Let’s start with booleans. And notice how practically grounded everything is here. There is no truth or falsehood in itself: these notions make sense only when they presuppose strategies of action. Otherwise there is no point in truth and falsehood existing at all. Feel the formulas.

Here $t$ and $f$ are simply two arguments (mnemonic: the “true” branch and the “false” branch): $\mathbf{tru}$ returns the first, $\mathbf{fls}$ the second. So a boolean value is itself a choice between two — a ready-made $\mathbf{if}$.

Here $\mathbf{if}$ does almost nothing on its own: it takes a boolean $b$ and hands it two branches $t$ and $e$, and $b$ picks the right one. $\mathbf{not}$ is just as simple: it gives the boolean its branches in reverse order, so truth chooses falsehood and falsehood chooses truth.

In $\mathbf{and}$ the first boolean $p$ decides what to return: if $p$ is true, the result depends on $q$; if false, falsehood is returned at once. In $\mathbf{or}$ it is the opposite: if $p$ is true, truth can be returned immediately; if false, we have to look at $q$.

Let’s substitute truth ($1$ $= \mathbf{tru}$, $0$ $= \mathbf{fls}$) and perform the reductions:

Now let’s talk about pairs: a very important type, widely used in Haskell. A pair is a function that holds two values and waits for a “receiver”:

$\mathbf{fst}$ hands the pair $\mathbf{tru}$, $\mathbf{snd}$ hands it $\mathbf{fls}$, and the pair gives back the right component:

Notice how neat this is: $\mathbf{fst}$ and $\mathbf{snd}$ take a pair as their argument and hand control over to it — the pair itself then decides what to return. These are, so to speak, decorator functions.

Now for the most pressing thing — the natural numbers. A number $n$ is “apply a function $n$ times”:

Important: $f$ and $x$ here are arbitrary — they are supplied by whoever uses the number. A numeral fixes only “how many times to apply”, not “what to apply”.

Feed the numeral a function $f$ and an argument $x$ — and it applies $f$ exactly as many times as the number specifies:

Now let’s learn to compute — all arithmetic grows from one trick: “apply $f$ the required number of times”.

Let’s start with adding one: $\mathbf{succ}$ tacks one more application of $f$ onto the number:

Addition continues the idea — it applies $f$ first $\overline{n}$ times, then $\overline{m}$ more:

Multiplication is already repeated addition:

Exponentiation is repeated multiplication, and its notation is very short:

In $\mathbf{pow}$ the arguments simply swap places: $\overline{n}\,\overline{m}$ is $\overline{m}$ applied as a function $n$ times, which yields $\overline{m^{\,n}}$.

Subtraction is surprisingly hard: $\mathbf{pred}$ is built through pairs — we run a pair $(i-1,\,i)$ along the number and take the first component:

By a well-known legend, Stephen Kleene came up with the predecessor function ($\mathbf{pred}$, predecessor) — the key to subtracting Church numerals — right in the dentist’s chair.

Everything “subtractive” rests on $\mathbf{pred}$: subtraction itself is repeated $\mathbf{pred}$, and division is repeated subtraction. We give no separate λ-definition for division: there is no new idea in it — the same $\mathbf{pred}$ in a loop, only a bulkier expression.

Let’s check $\mathbf{pred}$ on a general numeral $\overline{n}$. Denote the step $\sigma$ $= \lambda p.\,\mathbf{pair}\,(\mathbf{snd}\,p)\,(\mathbf{succ}\,(\mathbf{snd}\,p))$ — it shifts the pair: it drops the first component and grows the second:

Substitute $\overline{n}$ into the definition — that means applying $\sigma$ exactly $n$ times to the starting pair $\mathbf{pair}\,\overline{0}\,\overline{0}$:

The pairs run along a chain — the second component counts the steps, the first lags by one:

It only remains to take the first component:

For $\overline{0}$ the chain does not move, so $\mathbf{pred}\,\overline{0}$ $\twoheadrightarrow_\beta \overline{0}$ — we take the predecessor of zero to be zero.

$\mathbf{iszero}$ feeds the number a function that answers $\mathbf{fls}$ at every step, with the start value $\mathbf{tru}$: zero has no steps — $\mathbf{tru}$ remains; any other number has at least one step, which turns it into $\mathbf{fls}$.

A list is its own right fold (the fold encoding):

The same trick in Haskell — the type of $\mathtt{foldr}$: a list is fully determined by how it folds. A Church numeral is “a list of $n$ identical applications”.

-- a list is built by the constructor (:) (cons) and terminated by [] (nil):
[1, 2, 3]  ==  1 : (2 : (3 : []))   -- True

-- Church encoding is the same chain, only (:) and [] become parameters;
-- in Haskell this is exactly foldr:
foldr (:) []  [1, 2, 3]   -- 1 : (2 : (3 : [])) = [1,2,3]   (rebuilt the list)
foldr (+) 0   [1, 2, 3]   -- 1 + (2 + (3 + 0))  = 6         (folded to a sum)

But surely there’s normal programming, with numbers and even floating point. Why cook all this up? I wanted declarative programming, where everything is simple, and instead… Actually the answer is simple: folks, if you don’t like the circus, there’s nothing for you here, don’t come; but if you love the circus…