Chapter 1: Combinators

Your compiler has refused to run your code before. Not a crash and not a warning: a red line under something that would have gone wrong had the code run. The function was never called. No input was ever tried. And yet the compiler was certain — certain enough to refuse — that it could not vouch for the code. Certainty that has cost nothing is either a swindle or a theorem, and this part of the notes is an attempt to find out which.

First, why there is a checker there at all. Inside the machine everything is bits, and a pattern of thirty-two of them is an integer, or four letters of text, or a colour, or the address of something else, according to nothing but what the program means to do with it. The processor does not know and does not care: asked to add a colour to an address, it will. So the oldest and commonest kind of bug is a thing of one kind put where a thing of another kind was expected. In 1999 the Mars Climate Orbiter was lost because one program reported an impulse in pound-force seconds and the program that read the figure took it for newton-seconds (Mars Climate Orbiter Mishap Investigation Board, 1999): a number of one kind, consumed as a number of another, and a spacecraft flew into the atmosphere of Mars. No test caught it. A checker that knew the kind of each number would have refused to compile the hand-over.

That is why every language you use has a type checker. Java and Rust were born with theirs; JavaScript grew one, called TypeScript, when the untyped web became unmanageable; Python acquired the means for one in 2015. The checker is the part of the compiler whose job is to say no, before anything runs, to every program that would put a thing where a different kind of thing belongs.

Now look at what it claims when it says yes. It claims that the function is safe to run on every input it could ever receive: that it will never add a string to a number, never call something that is not a function, never hand back a value of the wrong shape. A test checks the inputs you thought of. The checker has run none and vouches for all of them. Whatever it is doing, it is not testing. So: what is it looking at, and what is a type?

1.1 Terms and reduction

To understand what the compiler did we must first see what it saw, and the difficulty is that there are hundreds of languages, each with its own checker, and no two of them look alike on the page. The way through is the way a mathematician always takes when the particulars are many and the pattern is one: abstract. Keep only what every checker attends to, and strip away the rest. What does a type checker attend to? Not what your function computes; only what it takes and what it returns. Not the value of an expression; only how it is put together. Not the keywords, the numbers, the names of the library functions; only which thing is applied to which. Strip all of that away and very little is left — less than you would think. There are things that are applied, there are things they are applied to, and there is the act of applying one to the other. Here is a language with exactly that in it and nothing else.

The symbol $\text{:=}$ is read “is defined to be”, and it is not the $=$ of arithmetic: it introduces a name rather than claiming that two things are equal. The last clause of the term definition is what “inductively” means: a term is whatever you can reach from constants and variables by finitely many applications, and nothing you cannot. In one line, with $M$ and $N$ standing for terms already built,

Application groups to the left: $fxy$ is $(fx)y$, a function of two arguments taking them one at a time, and brackets are written only where the grouping is to the right, as in $f(gx)$. In Haskell the term language is data Term = K | S | Var String | App Term Term, one constructor per clause.

A term is closed if no variable occurs in it, and a closed term is what I shall call a program. The word is meant literally: in a closed term there is nothing left to supply. A term with variables in it, such as the body $f(gx)$ of a definition, is a fragment — it says what to do once $f$, $g$ and $x$ are given, and until they are given there is nothing to run. The distinction earns its keep in §1.3, where the checker has to be told the kinds of the variables a fragment leaves open, and it is why the checker’s judgements carry a list of them.

A definition is a rule for rewriting: wherever $f$ stands next to $n$ arguments, the left-hand side may be replaced by the right, with the arguments written in for the parameters. The two constants are the two definitions we take as given, and this is what they do.

So $𝖪$ is the function that keeps its first argument and drops its second, and $𝖲$ is the function that hands its third argument to both of the others and applies the results. Terms built from constants by application, together with rules for rewriting them, make a combinatory algebra; the constants are called combinators, and these two are Schönfinkel’s. Neither looks like anything you would want; the point of the next few pages is that between them they are everything you have ever wanted. One convenience: we shall allow ourselves the integers $0,1,2,\dots$ and the operator $+$ as ready-made constants, with the obvious step $m+n⇝$ the sum. They can be built from $𝖪$ and $𝖲$ alone, and Example 1.6 shows how, but nothing here turns on it.

Two things have been taken on trust in these examples, and it is worth saying which. At the fourth line of the last run there were two steps available, since $\mathrm{𝑖𝑛𝑐}$ could have been unfolded at the outside instead of the inside; I chose the inside. The choice does not matter.

The second is larger, and it is the reason this calculus and not some other is the one to study.

The first half is Moses Schönfinkel’s (1924): he noticed that the variables in a definition are bookkeeping, and that two fixed combinations do all the bookkeeping there is. The second half is Alonzo Church’s (1936) and Alan Turing’s (1937), who proved it in Princeton in the year he arrived there to write his doctorate under Church. Between them the two halves say that this small language is not a toy: anything any computer can compute, a program in $𝖪$ and $𝖲$ can compute, and anything you can write with parameters you can write without them. We shall not prove the second half in this course. The first half we shall prove in outline, and it is the surprise of Chapter 2: compiling a definition’s variables away turns out to be a theorem of logic (Theorem 2.7).

Take stock. Nothing has been added to your idea of a program; a great deal has been taken away, and what is left is this. A program is a finite list of definitions together with a term to evaluate. A definition is an equation. To run the term is to replace, over and over, a left-hand side by its right-hand side, until no replacement is left to make. There is no store, no stack, no instruction pointer, and no order of evaluation to settle: which step you take first cannot change the answer you get (Remark 1.7), though Exercise 1.4 shows that it can change whether you get one at all. The constructs you might think are missing have been built in front of you out of nothing — the conditional in Example 1.5, the natural numbers and addition on them in Example 1.6 — recursion is Exercise 1.6, and Theorem 1.8 says that whatever else you want is there too.

So this is not a small language chosen because it is convenient to reason about. It is the general case, reached by deleting from your own languages everything a checker does not read. That is worth holding on to for the next two pages, because something is about to go badly wrong in it, and it will not be a quirk of a toy. It will be a thing that goes wrong in yours.

1.2 Non-termination

Nothing in Definition 1.1 says what may be applied to what. A boolean is a function and a number is a function, so of course a function may be applied to either; and a function may be applied to itself. The definition

is legal: its right-hand side uses nothing but its one parameter. So $\omega$ is the function that applies its argument to itself — an odd thing to want, perhaps, but not a difficult thing to write. Apply it to itself,

and run it. There is one step available, the definition of $\omega$ with $\omega$ written in for $x$, and it gives

The step returns the term it started from. So there is a second step, and it returns it again, and no number of steps ever finishes.

Be exact about what that costs, because “does not terminate” is a phrase the eye slides over. Run $\mathrm{\Omega }$ and there is no output, no error and no crash. The machine is working. It will still be working tomorrow. You have met this: a page that spins; a build that never finishes; a request whose reply never comes, holding its connection open, and then a thousand more behind it, until a server that was answering everybody is answering nobody. The failure here is not that a program returned the wrong answer — a wrong answer can at least be read, and argued with. It is that the program returned nothing and took the machine with it.

Now look at the size of the thing. $\mathrm{\Omega }$ is four symbols. It is not the end of a long chain of subtle mistakes; it is two sensible decisions in a row. Nothing in the three clauses of Definition 1.1 objected, and nothing in them could: they say which strings are terms, and $\omega \omega$ is a perfectly good string. The one rule of Definition 1.3 did not object either. It had a step available, and it took it. (Compiled into the constants, $\omega$ is $𝖲𝖨𝖨$ — check that $𝖲𝖨𝖨x⇝\ast xx$ — and $\mathrm{\Omega }$ is $𝖲𝖨𝖨(𝖲𝖨𝖨)$, which takes three steps to come back to itself instead of one. Nothing is gained by compiling; the loop is in the shape, not the notation.)

Nor can you expect to see it coming. $\mathrm{\Omega }$ announces itself because it is four symbols long. The same self-application, arrived at through three library calls and a type nobody wrote down, announces nothing at all, and the paragraph above is the whole of the warning you are going to get. It is a fact, though not one we are yet in any position to prove, that no checker whatever catches every program that fails to stop. So we shall ask for something weaker, and get something more useful: a checker that refuses a class of programs we can describe exactly, and that has $\mathrm{\Omega }$ inside that class.

1.3 Types and typings

What went wrong is not hard to name. The function $\omega$ takes an argument and returns a result, and nothing anywhere recorded what kind of argument it takes or what kind of result it gives back. So nothing was in a position to notice that when $\omega$ was handed $\omega$, it had been handed something it was never built to take. The language has functions and arguments and no bookkeeping whatever. So here is the idea, and the rest of this chapter is its execution. Write the bookkeeping down. Label every term with what it takes and what it returns; allow an application only when the argument’s label is the one the function asks for; and check, before anything runs, that the labels fit together throughout. Read a label $A\to B$ as a contract: give me an $A$ and I shall return a $B$. The virtue of a contract is that it can be checked without being honoured — without running anything — because it speaks of kinds and not of values, and a verdict in advance is exactly what we are asking for.

Three things must be settled before that is a checker rather than a hope: what the labels are, what it means for a term to carry one, and which labellings are allowed. The labels are called types, and they are built by two clauses, as a term was built by three.

In one line, $A,B::=p\mid A\to B$. So $\mathrm{𝐼𝑛𝑡}\to \mathrm{𝐵𝑜𝑜𝑙}$ is the type of a test on integers, and $(p\to q)\to p$ is a type too; look at the shape of that one for a moment before reading on. The arrow groups to the right, so $A\to B\to C$ is $A\to (B\to C)$, a function of two arguments taking them one at a time, just as application grouped to the left. Every real checker has more — records, lists, generics — and every one of them has this.

To type a term with variables in it you must know their types.

A checker works down a term a piece at a time, and by Definition 1.1 there are four kinds of piece. The two constants have fixed types, one each. A variable has the type the context gives it. An application is typed from the types of the two terms in it, and it is there that a checker says no. Four cases, then, and the certificate the checker produces is a list of judgements of which every line is one of the four.

Read the four cases as the checker reads your code.

(K)

$𝖪$ takes an $A$, then a $B$, and returns the $A$, and (1.1) says so for every choice of $A$ and $B$.

(S)

$𝖲$ takes a function $M$ of two arguments, a function $N$ of one, and an argument $P$, and returns $MP(NP)$. For that to make sense $P$ must be what both $M$ and $N$ expect:

$$P:A,N:A\to B,M:A\to B\to C,$$

and the result $MP(NP)$ is then a $C$. Schema (1.2) is that sentence written down.

(var)

A variable has the type it was declared with, and the checker has only to look $x$ up in $\mathrm{\Gamma }$.

(app)

An application $MN$ is well typed only if $M$ is a function and $N$ is an argument of exactly the type $M$ expects, and then the result has $M$’s result type. When the types do not match, this is the case that draws the red line.

The ready-made pieces get cases of the same kind: every integer has type $\mathrm{𝐼𝑛𝑡}$, the operator $+$ has type $\mathrm{𝐼𝑛𝑡}\to \mathrm{𝐼𝑛𝑡}\to \mathrm{𝐼𝑛𝑡}$ (so that $y+1$ is $+$ applied to $y$ and then to $1$), and a string such as $\mathtt{\text{"𝚑𝚎𝚕𝚕𝚘"}}$ has type $\mathrm{𝑆𝑡𝑟𝑖𝑛𝑔}$.

What the definition has no case for is a name. It types constants, variables and applications, and a name introduced by a definition is none of the three: to type $\mathrm{𝑎𝑑𝑑}\overline{2}\overline{1}\mathrm{𝑖𝑛𝑐}0$ the checker would need the type of $\mathrm{𝑎𝑑𝑑}$, and nothing above gives it one.

The refusal that matters most is the refusal of $\mathrm{\Omega }$, and to see it we need one fact about $𝖨$: not just that it has type $A\to A$, but that it has no type of any other shape. The argument reads a typing backwards from its last line — the last rule used must have been such-and-such, so the lines above must have looked so — and that shape of argument is the shape of every proof in Chapter 2.

The work was done in two places. The lemma and the first half of the proof only read the four cases backwards; the argument then rests on one fact about types that is not one of the cases, that a type cannot be a proper part of itself. The same fact, seen directly: in a context where $x:A$, the body $xx$ of $\omega$ would need $x:A^{\prime }\to B$ and $x:A^{\prime }$ at once, and (var) gives $x$ the one type $A$, so $A=A\to B$. The parameter was the problem, and compiling it away did not make it go away.

So the checker refuses $\mathrm{\Omega }$, and refuses it by a failure to match, like the red line. That is a refusal of one program. Two theorems say what the checker’s yes is worth for all the others, and the first of them we can prove.

Read what that says. The checker gave its verdict before the program ran. Subject reduction says that the verdict is not overtaken by events: at every step of the run, the term in hand still has the type the checker assigned, so an argument of the wrong kind can never arise part-way through, however long the run. What the checker said stays said. That is the first half of the certificate’s worth. The second half is about $\mathrm{\Omega }$, and about every program like it.

This we take on trust; the proof (Tait, 1967) uses a technique this course does not reach. We have seen the one looping program we know of refused, and Proposition 1.15 says why; the theorem says that no typed program loops, which is a great deal more, and we shall lean on it twice in Chapter 3. Every real language gives the loop back, by adding recursion under another name — Haskell’s fix, a while, a method that calls itself — and Exercise 1.6 asks what that costs.

What Church built it for. Church did not offer this calculus as a programming language. In 1932 there were no programs to write, and what he offered it as was a logic (Church, 1932): a way of writing statements, and of writing the functions that take statements to statements, in exactly the terms of Definition 1.1. The plan was that the whole of mathematics might be done in it. Within three years it was broken, and what broke it was the self-application of §1.2 (Curry, 1942; Kleene and Rosser, 1935). Here is the shape of what went wrong:

Because anything may be applied to anything, a statement can be made to talk about itself. Fix any statement $B$ you please — let it be “$0=1$”, if you want something plainly false — and let $X$ be the statement

That $X$ can be written down at all is the self-application of §1.2 over again: $X$ names the very statement it sits inside, as $\omega$ was applied to $\omega$. Now reason about it, in five steps.

1.

Suppose $X$.

2.

$X$ says that $X$ implies $B$, so on that supposition we have $X\to B$.

3.

From $X$ (the supposition) and $X\to B$ (step 2) we get $B$.

4.

Steps 1–3 got $B$ out of the supposition $X$. Discharge it, and conclude $X\to B$ — now with nothing supposed.

5.

But $X\to B$ is exactly what $X$ says. So we have $X$ outright; and then, by step 3’s move once more, $B$, with nothing supposed at all.

Nothing whatever was assumed about $B$, so the logic proves every statement there is; and a logic that proves everything proves nothing, since a proof in it is evidence for nothing. This is Curry’s paradox (1942), and the culprit is the statement that feeds on itself. It is the culprit of §1.2: the one gives a program that never stops, the other a proof of everything, and they are built the same way.

Curry’s is the simple version, and it came second. The inconsistency was found by Kleene and Rosser (1935), who reached it the long way round: they built, inside the calculus, a term that reproduces an old puzzle of Richard’s about naming numbers. The puzzle goes like this. A finite phrase of English can name a real number — “one half”, “the ratio of a circle’s circumference to its diameter” — and the finite phrases themselves can be listed, by length and alphabetically within each length. So the numbers nameable in English can be laid out in order: a first, a second, a third, and so on. Now name a number by this phrase: the number whose $n$th decimal digit differs from the $n$th digit of the $n$th number on the list. That phrase is finite English, so the number it names is itself somewhere on the list, at place $k$ say — and it differs from the $k$th number of the list at the $k$th digit, so it is not that number after all.

Richard’s puzzle is about naming, and Church’s calculus is a calculus of naming: a term is a name for a function, and terms can be taken apart and built up by other terms. Once a calculus can name all of its own names, the list and the diagonal are both available inside it, and that is what Kleene and Rosser assembled. Curry’s achievement was to see which single ingredient had done the damage; his paradox needs that one and nothing else. (The diagonal is not a mistake, and it does not go away. It returns in Chapter 11, where it is put to work rather than defused.)

Church’s repair was types (1940): attach a type to every term and forbid an application unless the types fit, which is rule (app). Proposition 1.15 is the repair working. In the typed calculus $xx$ cannot be written, the self-feeding statement cannot be formed, and the disaster does not occur. It is the repaired calculus, not the original, that your compiler is built around, and that is why the checker’s whole job is to refuse.

Look again at the paragraph in which the logic broke. Statement, suppose, so, discharge, conclude, proves: every word in it is a word about proofs, and we have not said what a proof is. And that is not the only thing pointing the same way. Look at the two types (1.1) and (1.2) give the constants,

Letters and arrows: they are formulas, and logicians have been writing exactly these two for a century, in systems built to say what a proof is. So we have a language in which a program and a logical disaster turned out to be the same object; a checker that refuses both; and two rules whose types a logician would recognise on sight — and no idea yet what it is about those four rules that makes them rules of reasoning. That is the next chapter’s question, and the answer is better than anyone has a right to expect.

Under every language you use is a combinatory algebra: two constants and application, run by two rewrite rules, in which every definition you have ever written can be expressed; and unpoliced it computes everything, including a program that never stops. A type is a contract, a basic type or $A\to B$; the checker’s job is to allow an application only when the contract is met. Its certificate is a typing: a finite list of judgements $\mathrm{\Gamma }⊢M:A$, each justified in one of the four ways (K), (S), (var) and (app). Its no is case (app) failing to match, and $\mathrm{\Omega }$ is refused that way. Its yes mentions no input and so covers every input, and by subject reduction what it says of a program stays said at every step of the program’s run.

Exercises

Reading

Wadler (2015) tells the story of this chapter and the next two in a dozen pages, and is a pleasure to read. Schönfinkel (1924) is where $𝖪$ and $𝖲$ come from; Church (1936) and Turing (1937) are where the calculus is shown to compute everything; Church (1940) is where it gets its types, and Kleene and Rosser (1935) and Curry (1942) are why. Tait (1967) proves Theorem 1.17. Next, Chapter 2: what a proof is, and why the compiler’s rules are its rules. References.