Types Overview

Adding Types

The simply typed lambda calculus adds type annotations to lambda terms. Each variable gets a type, and the system enforces rules about which terms can be applied to which.

In untyped lambda calculus, any term can be applied to any other term. In the simply typed version, an application f x is only valid if the type of x matches what f expects.

This is a restriction. Some well-formed untyped terms become ill-typed and are rejected by the system.

Types Guarantee

The simply typed lambda calculus has a remarkable property: strong normalization. Every well-typed term reaches a normal form, no matter what reduction strategy is used. There are no infinite reduction sequences.

This means divergence is impossible. The term Ω = (λx.x x)(λx.x x) cannot be typed, so it is excluded from the system entirely. The price of guaranteed termination is that some valid untyped terms are rejected.

Compare this to untyped lambda calculus, which we saw is Turing complete but has terms that never reach normal form.

The Tradeoff

The simply typed lambda calculus guarantees termination but is not Turing complete. Untyped lambda calculus is Turing complete but has terms that diverge. This is not an accident or a limitation to be fixed. It is a fundamental tradeoff.

You cannot have both: a system that guarantees every program terminates and also expresses every computable function. If every program terminates, then "does this program halt?" is trivially decidable (yes, always), which contradicts the undecidability of the halting problem for Turing-complete languages.

Different applications make different choices. A proof assistant needs termination guarantees. A general-purpose programming language needs Turing completeness. The tradeoff is real, and neither side is always right.

Curry-Howard

The Curry-Howard correspondence reveals that typed lambda calculus and constructive logic are the same system seen from two angles:

A type like A → B is simultaneously a function signature and a logical proposition ("if A then B"). A lambda term of that type is simultaneously a function and a proof that the proposition holds.

This is not a metaphor. It is a precise, formal identity. Logic and computation are two views of the same structure.

Proofs Are Programs

The Curry-Howard correspondence establishes a precise identity between typed lambda calculus and constructive logic:

• A type is a proposition
• A program (lambda term) of that type is a proof

To show that a proposition holds, you write a program with the corresponding type. If the program type-checks, the proposition is proved. The program itself is the proof — not a separate artifact, but the very same object viewed from the logic side.

Signpost

This concept has introduced two key ideas:

1. Types as restriction: The simply typed lambda calculus trades Turing completeness for guaranteed termination.
2. Curry-Howard: Types are propositions, programs are proofs. Logic and computation are the same structure.

Both ideas run far deeper than we have explored here. The simply typed lambda calculus is just the first rung of a ladder of increasingly expressive type systems. Richer systems recover more expressive power while maintaining strong guarantees.

Bitwit covers these in dedicated subjects: Type Theory develops the formal systems in depth, and Constructive Logic explores the proofs-as-programs perspective from the logic side.