The Simply Typed Lambda Calculus

In the lambda calculus, we built computation from nothing but functions. Three rules, variables, abstraction, application, and from them: arithmetic, logic, recursion, every computable function. But we also built something else. Terms that never stop.

The problem with power#

Remember omega: λx. x x applied to itself. Reduce it and you get the same expression back. Reduce again: the same. It loops forever.

This is not a flaw. It is the price of universality. Lambda calculus can compute anything a Turing machine can, and that includes running forever. Church proved in 1936 that no algorithm can look at an arbitrary term and decide whether it halts. Total freedom comes with total risk.

What if we could rule out the terms that loop, before they ever run?

Types#

The idea is simple: make every expression declare what it expects and what it produces.

Start with base types, just names: α, β, γ. They stand for whatever kinds of values you care about. Then build arrow types: α -> β means "a function that takes an α and returns a β." That is the entire type language. Base types and arrows.

λx. x takes anything and returns the same thing. Its type: α -> α. Read the arrow as "to": alpha to alpha. λx. λy. x takes an α, then a β, and returns the α. Its type: α -> β -> α. Two arrows, one per argument.

Three rules#

How do you know a term has a given type? You derive it, from rules. One rule for each kind of expression.

The variable rule: if x has type α in your context, your current list of assumptions, then x has type α. You look it up.

The abstraction rule: if, after assuming x has type α, you can show the body has type β, then λx. e has type α -> β. You assumed the input, derived the output, and the lambda packages both into a function type.

The application rule: if f has type α -> β and a has type α, then f a has type β. The types must match: the function expects an α, you gave it an α, you get the promised β.

Three rules. That is the entire type system. Derive the identity: by abstraction, assume x : α and show the body, just x, has type α; by the variable rule, it does. Two rules, one derivation. The constant function takes three: assume x : α, assume y : β, the body x has type α from the assumptions, discharge twice. Each step is mechanical, which is exactly what lets a compiler do it for you.

The term with no type#

Now try to type λx. x x, a term that applies x to itself.

For the application x x to work, x has to be a function, so x needs an arrow type, say α -> β. But x is also the argument, so x needs type α. That means x would need to have type α and type α -> β at the same time. In the simply typed lambda calculus, every variable has exactly one type, and no type satisfies both requirements.

Self-application has no type. And without self-application, you cannot build omega. The term that loops forever is simply untypable.

Pause and try: derive a type for λf. λx. f (f x).

Assume types for f and x and let the rules push you around. The inner application f x forces f to be an arrow whose input is the type of x: say x : α and f : α -> β, so f x : β. The outer application feeds f x back into f, so f's input type must also be β, which forces β = α. So f : α -> α, the body has type α, and the whole term has type (α -> α) -> α -> α. Apply-twice only exists where input and output types agree, and the derivation is what told you so.

Every well-typed term halts#

This is not an accident of one example. In 1967, William Tait proved normalization for the simply typed lambda calculus: every well-typed term reduces to a normal form. And the method extends to the stronger fact that no matter what order you reduce in, you reach a term with no more reductions to perform.

Every computation terminates. Not most. Every single one. If it type-checks, it halts.

The proof works by induction on types. Base-type terms always reach a normal form. Arrow types carry a guarantee: apply a terminating function to a terminating argument, and the result terminates too. A type, in this system, is a termination proof.

What you lose#

There is a cost. The Y combinator, the trick that gave lambda calculus recursion, relies on self-application: a function receives a copy of itself as an argument. We just showed self-application cannot be typed. So the Y combinator has no type, and without it you cannot write general recursion. No loops, no fixed points, no programs that might not terminate, because none of them can be expressed. The simply typed lambda calculus is not Turing complete. It computes only total functions, functions that always return an answer.

Step back and look at what happened. Untyped: you can compute anything, but some terms never halt. Simply typed: everything halts, but you cannot compute everything. This is the fundamental tension. Types are constraints; stronger constraints mean more guarantees and less expressiveness. Every type system ever designed lives somewhere on this spectrum.

Recursion, earned back#

You can get recursion back. You just have to earn it.

Add a new kind of type: an inductive type. The natural numbers are the simplest example. A natural number is either zero, or the successor of another natural number. That is the whole definition, and the key is that it is well-founded: every natural number is built from finitely many successors stacked on top of zero. There is no infinite descent.

Now add a recursor, a function that takes a natural number apart the same way it was built. Give it a base case, what to return for zero, and a step, how to turn the result for $n$ into the result for the successor of $n$. The recursor walks down the structure, one constructor at a time, and always reaches the bottom.

This is structural recursion. You can loop, but only over the structure of your data, and each recursive call operates on a strictly smaller piece. The type system can see that the recursion is well-founded, because the data type itself is. Factorial, addition, multiplication: they all come back. Not through the Y combinator's trick of self-application, but through the honest structure of the data.

Gödel's System T is the simply typed lambda calculus plus natural numbers and their recursor. It can compute any function whose totality is provable in first-order arithmetic, far more than the simply typed calculus alone. And everything still terminates.

Where it leads#

Recursion is not the only thing you can add back. Girard's System F adds polymorphism: the identity function does not need to be α -> α for one specific α, it works for all of them, written once and used at any type. Dependent types go further still, letting types mention values: a vector whose type includes its length, a sort function whose type guarantees the output is a permutation of the input. With dependent types you can express propositions in predicate logic, and programs become proofs. This is what Coq, Agda, and Lean are built on. Each extension pushes the boundary of what you can express while preserving a guarantee.

And the simple system is no theoretical curiosity. ML, Haskell, OCaml, Rust: every statically typed language traces part of its type system back to these ideas. When your compiler rejects a program with a type error, it is doing exactly what we did with x x: trying to assign a type and failing because the pieces do not fit. There is a deeper reason it all works, too: the typing rules of the simply typed lambda calculus are exactly the inference rules of the implicational fragment of intuitionistic propositional logic. Types are propositions, programs are proofs, and type checking is proof verification. Your compiler is doing mathematics.

Lambda calculus is three rules and infinite power, including the power to never stop. The simply typed lambda calculus adds one constraint: every expression must have a type. From that single discipline, you get a guarantee no amount of testing could provide.

If you remember three things#

1. Two type formers (base types and arrows) and three typing rules (variable, abstraction, application) are the entire system.
2. Self-application has no type, so omega and the Y combinator are ruled out, and Tait's 1967 theorem says every well-typed term terminates.
3. The cost is Turing completeness; the honest way back is structural recursion over well-founded data, which is how System T, and eventually Coq and Lean, keep both recursion and termination.