One type for every use

What a proof about numbers can compute found the limit of the simply typed calculus: with Church numerals of a fixed type as input and output, every function a term computes is an extended polynomial — sums, products and tests on zero — and the predecessor is not among them. One type up then let the input numeral iterate at a higher type than the output, and the predecessor, parity and $2^n$ appeared. Each gain came at a price. A numeral used at a higher type is no longer a numeral of the original type, so the predecessor it computes cannot be fed back into itself, and subtraction — iterating the predecessor — stays out of reach.

That essay ended on the obvious move. Jean-Yves Girard’s system F, introduced in 1972 and discovered independently by John Reynolds in 1974, adds variables that range over types and a quantifier that binds them. A numeral becomes a single term of the single type

$$N = \forall X.\ (X \to X) \to X \to X,$$

and inside any larger term it can be used at whatever type the occasion needs, by applying it to that type. This essay builds a small type-checker and a normaliser for system F and runs the terms that the simply typed calculus could not write.

Terms that take types as arguments #

System F has two new constructions beside the abstraction and application of the simply typed calculus. A term can abstract over a type, $\Lambda X.\ M$, and then has a type of the form $\forall X.\ \sigma$; and a term of type $\forall X.\ \sigma$ can be applied to any type $\tau$, written $M\,[\tau]$, giving a term of type $\sigma$ with $\tau$ put in for $X$. The numeral two is

$$\Lambda X.\ \lambda f : X \to X.\ \lambda x : X.\ f\,(f\,x),$$

and $2\,[X \to X]$ is the same numeral iterating functions, $2\,[N]$ the same numeral iterating numerals. Through the correspondence between derivations and terms, the new constructions are the introduction and elimination rules for a quantifier over propositions: $\forall X.\ (X \to X) \to X \to X$ is the second-order formula “for every proposition $X$, if $X$ implies $X$ then $X$ implies $X$”, and the numerals are its proofs. Applying a numeral to a type is instantiating a universal claim, one level up.

The type-checker behind the figures follows those rules literally: a variable has the type it was declared with, an abstraction has an arrow type, an application requires the argument to match the function’s input type exactly, and a type application substitutes. Types are compared up to renaming of their bound variables, so $\forall X.\ X \to X$ and $\forall Y.\ Y \to Y$ count as the same. The normaliser then erases every type and reduces the remaining untyped term in normal order, counting each step. Types guide what may be written; they play no part in running it.

Ackermann’s function in one line #

The hero’s term is

$$A = \lambda m : N.\ m\,[N \to N]\,\big(\lambda g : N \to N.\ \lambda n : N.\ n\,[N]\,g\,(g\,1)\big)\,S,$$

where $S$ is the successor. Read it from the inside. Given a function $g$ on numerals, the step builds the function that sends $n$ to $g$ applied $n + 1$ times to 1. Starting from the successor, $m$ iterations of that step build the $m$-th level of a hierarchy: adding, then doubling, then exponentiating, then towering. The type-checker confirms $A : N \to N \to N$, and running it gives Wilhelm Ackermann and Rózsa Péter’s function: $A(1, n) = n + 2$, $A(2, n) = 2n + 3$, $A(3, n) = 2^{n+3} - 3$, so $A(3, 4) = 125$, found in 15,765 reduction steps.

The same numeral type appears twice in one term with two different uses: $m$ at type $N \to N$, iterating a function on numerals, and $n$ at type $N$, iterating numerals. In the simply typed calculus the two uses would need two different numeral types, the output of one could not be the input of the other, and Ackermann’s function could not be written with input and output of one type at all. It is the standard example of a function that grows faster than anything the primitive recursive functions can produce, and here it is a single line.

Subtraction, at last #

One type up found the predecessor at a raised type by folding a pair of numbers into a single function. In system F the pair can be its own polymorphic type,

$$P = \forall Y.\ (N \to N \to Y) \to Y,$$

the type of things that, given any way of combining two numerals, combine them. Kleene’s trick of 1932 then reads directly: iterate on pairs, starting from $\langle 0, 0\rangle$ and stepping $\langle a, b\rangle \mapsto \langle b, b + 1\rangle$, and take the first component. The term is checked at type $N \to N$ — numeral in, numeral out, the same type — and computes the predecessor on every input tried.

That one fact is what the simply typed calculus lacked. Because the predecessor’s output has the same type as its input, another numeral can iterate it: $m - n = n\,[N]\,\mathrm{pred}\,m$, type-checked at $N \to N \to N$, and every entry of the table from $0 - 0$ to $7 - 7$ comes out right, the last after 326 reduction steps. In the simply typed calculus no term with inputs and output of one numeral type computes subtraction; here it is a dozen symbols.

What running costs #

The values of Ackermann’s function are large; the work of computing them by reduction is larger. At the first level the steps grow in proportion to the value; at the second, a little faster; at the third, much faster — 61 costs 3,795 steps and 125 costs 15,765. Each level iterates the one below, and the reductions of a numeral iterating numerals multiply. System F defines functions that grow far past Ackermann’s — every function that second-order arithmetic can prove to be total — and for most of them the number of steps needed to compute even a small value exceeds anything physical.

And every run finishes. Girard proved in 1972 that every term of system F reduces to a normal form, whatever order the reductions are taken in, so every term of type $N \to N$ computes a total function. That is the property that made the method of the two previous essays legitimate — list terms, run them, read off the functions — and it survives the move to system F. It survives at a cost that is itself a theorem: the proof cannot be carried out in second-order arithmetic, because the functions system F defines are exactly those that second-order arithmetic can prove total, and a proof of normalisation would prove them all total at once, which by Gödel’s second incompleteness theorem the system cannot do about itself.

Termination has a price that no strengthening of the types can avoid. No algorithm can read what a program does in general because programs in general may run for ever; a language in which every program halts escapes that, and pays by being unable to compute some functions that halt. The argument is a diagonal one. Running a system F term of type $N \to N$ on an input is a total computable process, so the function that takes a code for such a term and a number, and returns one more than the term’s value on that number, is total and computable — and it differs from every function system F defines, at the code of the term defining it. Every total language has functions it cannot write, and the interpreter for the language itself is the first of them.

What lives in a polymorphic type #

A closed term of type $\forall X.\ X \to X \to X$ must produce an $X$ for an $X$ it knows nothing about, and the only values of type $X$ it has are its two arguments. So in normal form it can only return one of them: there are exactly two such terms, and they are true and false. A term of type $\forall X.\ (X \to X) \to X \to X$ can apply its function argument to its value argument any number of times and nothing else: the numerals, one of each size. With two function arguments the normal forms are strings in two letters, $2^n$ of length $n$; with one argument of type $X \to X \to X$ and one of type $X$ they are binary trees, counted by the Catalan numbers 1, 1, 2, 5, 14, 42, 132 — the sequence that counts so many things. Every data structure that can be described as “built from these constructors” has a polymorphic type whose inhabitants are exactly its elements. Corrado Böhm and Alessandro Berarducci worked this out in 1985, and it is how the functional programming languages descended from system F represent data.

The first row is the most important. The type $\forall X.\ X$ has no closed inhabitant at all: a term of it would produce an element of any type from nothing. Read as logic, $\forall X.\ X$ is “every proposition is true”, and the fact that no proof of it exists is the consistency of the system. Normalisation is what guarantees it: a closed normal term of type $\forall X.\ X$ would have to begin with $\Lambda X$ and then produce an $X$ from no arguments, and there is no such term to find.

Why only the identity has the identity’s type #

The counts in the figure are instances of a principle John Reynolds formulated in 1983 and Philip Wadler made famous in 1989 as theorems for free. A term of a polymorphic type cannot inspect the type it is used at, so it must treat every type the same way, and that uniformity constrains what it can do as tightly as a specification would. A term of type $\forall X.\ X \to X$ receives a value of a type it knows nothing about and must return a value of that type; the only one available is the argument, so the term is the identity. The principle, called parametricity, says the same for every type: a function of type $\forall X.\ \mathrm{List}\,X \to \mathrm{List}\,X$ can only rearrange, drop and duplicate the entries of its list, never look at them, and so it commutes with every function applied to the entries — a fact about any such function, derived from its type alone.

The numerals are the cleanest case. The type $\forall X.\ (X \to X) \to X \to X$ is, read through parametricity, the definition of a natural number that Richard Dedekind gave in 1888 and Gottlob Frege before him: a number is whatever belongs to every collection that contains nought and is closed under the successor. Instantiating $X$ at a type is choosing a collection; the numeral’s term is a proof that it belongs. So the second-order quantifier that system F adds is exactly the quantifier over collections that the definition of the natural numbers needs, and the normal forms of $N$ are exactly the numbers.

A type applied to itself #

The polymorphic identity $\Lambda X.\ \lambda x : X.\ x$ has type $\forall X.\ X \to X$, and it can be applied to its own type: $\mathrm{id}\,[\forall X.\ X \to X]$ is an identity function on polymorphic identities, which can be applied to $\mathrm{id}$. The derivation checks, and the result reduces in one step to the identity. In the simply typed calculus the corresponding term $\lambda x.\ x\,x$ has no type at all, since $x$ would need a type $A$ that is also $A \to B$.

This impredicativity — a type quantifies over a collection that includes itself — is what gives system F its power, and it is the reason its normalisation proof is so delicate. Girard’s proof uses reducibility candidates, sets of terms with good behaviour, and defines what it means for a term to be good at type $\forall X.\ \sigma$ by quantifying over all candidates, including the one being defined. The circularity is harmless in second-order logic and fatal in weaker ones, which is exactly why second-order arithmetic is the right measure of the system’s strength.

Normalisation of terms is the same theorem as cut elimination for proofs, seen through the correspondence: a detour in a term — an abstraction immediately applied — is a lemma proved and then used, and removing it is cutting the lemma out. Gaisi Takeuti conjectured in 1953 that cuts can always be eliminated from proofs in second-order logic; William Tait proved a semantic form of it in 1966, and Girard’s normalisation theorem gave the syntactic one. The impredicative step that makes the identity apply to itself is the step that makes the conjecture hard: a cut on a second-order formula can be replaced by cuts on its instances, and the instances can be larger than the formula they came from, so no simple measure of size decreases.

A numeral applied to a numeral #

The shortest striking term in system F is exponentiation: $\lambda m\,n.\ \Lambda X.\ n\,[X \to X]\,(m\,[X])$, give or take two variables that make its normal form read as a numeral. The numeral $n$, used at type $X \to X$, iterates “iterate $m$ times” $n$ times, which is iterating $m^n$ times. In the simply typed calculus the same trick needed $n$ at a higher type than the result, so $2^n$ could not be iterated; here the result is again an $N$, and $2^{2^{2^{\cdots}}}$ can be built by iterating exponentiation. Run on $m = 3$ and $n = 5$ the term returns 243.

What the computations show and assume #

Every type in the figures is checked by an implementation of the rules, and every value is obtained by actually reducing the erased term to a normal form; nothing is computed by a shortcut that would hide a mistake in a term. The counts of inhabitants come from a recurrence over the shapes of normal forms, and every numeral and the small trees were also built as terms and checked. What the computations cannot show is the general theorem behind them: that every term normalises, that the definable functions are exactly the provably total functions of second-order arithmetic, and that the inhabitants of a type are exactly its normal forms. Those are Girard’s, Reynolds’s and others’ theorems, and the figures exhibit instances.

Nor is the type-checker the whole of what system F asks. Writing the types by hand, as here, makes checking easy. Inferring them — given an untyped term, deciding whether some assignment of types makes it a term of system F — was shown undecidable by Joe Wells in 1994, which is why practical languages use restricted forms of polymorphism where inference is possible.

Still open: the definable functions in a picture #

Which functions does system F define with small terms? That every provably total function of second-order arithmetic is definable is a theorem; which ones have short definitions, and how the size of the smallest term grows with the function’s rate of growth, is not mapped. The enumeration that worked for the simply typed calculus is much harder here, because the types inside a term are no longer fixed by the type outside it — a term of type $N \to N$ may instantiate its input at any type, including types larger than the one being checked — so listing all terms of a given size means listing types as well, without bound. Restricted fragments, with quantifiers only at the outside or of bounded rank, have partial maps, and the question of how far the smallest definitions of the fast-growing functions, level by level, actually grow is open.

A single type, used every way #

In system F a numeral is one term of one type, ∀X. (X → X) → X → X, and every use instantiates it at the type that use needs. That one change lets a numeral iterate numerals, functions on numerals, or pairs, all inside one term: the type-checker accepts Ackermann’s function, Kleene’s predecessor and subtraction at a single numeral type, and running them gives the right values, A(3, 4) = 125 among them, after reduction counts that grow faster than the values. The polymorphic types turn out to be data structures, their normal inhabitants counted as booleans, numerals, strings and trees, and $\forall X.\ X$, having none, is the system’s consistency.