Programs are Proofs: the Curry-Howard Correspondence

In the 1930s, the logician Haskell Curry noticed something odd: the rules for combining functions looked exactly like the rules for combining logical propositions. Three decades later, William Howard wrote it down precisely (in a 1969 manuscript, published only in 1980). Programs and proofs are the same mathematical objects viewed from different angles. This is the Curry-Howard correspondence. We are going to build it from scratch.

The lambda calculus#

We need a precise language for talking about functions. The lambda calculus is a minimal notation for defining and applying them, nothing else, invented by Alonzo Church in the 1930s, around the same time Turing was building his machines.

There are exactly three things in it. Variables: $x$, $y$, $z$, names that stand for values. Abstraction: $\lambda x.e$ means "the function that takes $x$ and returns $e$"; the lambda announces the input and the dot separates it from the body. Application: $fa$ means "apply $f$ to $a$."

That is the whole language. $\lambda x.x$ is the identity function: apply it to some value $a$, substitute $a$ for $x$ in the body, and get $a$ back. $\lambda x.\lambda y.x$ takes two arguments, first $x$ then $y$, and returns the first. Apply it to $a$ and you get $\lambda y.a$, a function that ignores its argument; apply that to $b$ and you get $a$. The second argument is discarded.

Types#

So far we have said nothing about what kinds of values these functions expect. The simply typed lambda calculus fixes this by assigning a type to every expression. We write $\lambda x.x:\alpha \to \alpha$, and read the arrow as "to": give me an $\alpha$, I will give you an $\alpha$. The function $\lambda x.\lambda y.x$ has type $\alpha \to \beta \to \alpha$: give me an $\alpha$, then a $\beta$, and I will give you back that $\alpha$. The $\beta$ is ignored, but the type still records that it was accepted as input.

Now look at the arrow. As a type, $\alpha \to \beta$ says "give me an $\alpha$, I will produce a $\beta$." In logic, $\alpha \to \beta$ says "from $\alpha$, you can conclude $\beta$." Same symbol, same meaning. Let's make that precise.

Typing rules#

How do we know $\lambda x.x$ has type $\alpha \to \alpha$? We derive it from rules, each saying: if you know certain things about the parts, you can conclude something about the whole. Here $\mathrm{\Gamma }$ is the context, your list of assumptions.

The variable rule: if $x:\alpha$ is among your assumptions, then $\mathrm{\Gamma }⊢x:\alpha$. You just look it up.

The abstraction rule: assume the input type, derive the output type, and the lambda packages them together.

$$\frac{\mathrm{\Gamma },x:\alpha ⊢e:\beta }{\mathrm{\Gamma }⊢\lambda x.e:\alpha \to \beta }$$

The application rule: the function expects an $\alpha$, you gave it an $\alpha$, you get the promised $\beta$.

$$\frac{\mathrm{\Gamma }⊢f:\alpha \to \beta \mathrm{\Gamma }⊢a:\alpha }{\mathrm{\Gamma }⊢fa:\beta }$$

To derive $\lambda x.x:\alpha \to \alpha$, the abstraction rule asks us to show $x:\alpha$ assuming $x:\alpha$, and that is the variable rule. Two rules, one derivation.

The same rules, in logic#

In natural deduction, implication has the same two rules. Implication introduction says: if, after assuming $\alpha$, you can derive $\beta$, then you have proven $\alpha \to \beta$.

$$\frac{\mathrm{\Gamma },\alpha ⊢\beta }{\mathrm{\Gamma }⊢\alpha \to \beta }$$

Look at that rule, then look at the abstraction rule. The structure is identical. The typing context $\mathrm{\Gamma }$ is the set of assumptions, the type $\alpha$ is the proposition $\alpha$, and the term $\lambda x.e$ is the proof. The logic rule does not bother naming its proof; it just says a derivation exists. The typing rule tells you what the derivation actually is: the lambda term.

Implication elimination is modus ponens: from $\alpha \to \beta$ and $\alpha$, conclude $\beta$. That is the application rule with the terms erased. Modus ponens is function application.

Pairs are "and", sums are "or"#

Functions are not the only type. If $a:\alpha$ and $b:\beta$, the pair $(a,b)$ has type $\alpha \times \beta$; you need both components to construct it, and you use it by projecting out a component with first or second. In logic this is conjunction: to prove $\alpha \wedge \beta$ you need a proof of each, and from a proof of $\alpha \wedge \beta$ you may conclude $\alpha$, or conclude $\beta$. Pairing is conjunction introduction, and the two projections are the two eliminations.

Sums mirror disjunction. With a value of type $\alpha$, you can inject it into $\alpha +\beta$ by tagging it left: "I have an $\alpha$, and that is enough for an $\alpha$-or-$\beta$." A $\beta$ tags right. To use a sum, you case-split: if you can handle the $\alpha$ case and the $\beta$ case, you are covered. In logic, from $\alpha$ conclude $\alpha \vee \beta$, and to use $\alpha \vee \beta$ you argue by cases. Proof by cases is pattern matching.

Currying is a theorem#

Let's trace the full correspondence on a specific example. If you have done any functional programming, you have probably curried a function: turned a function expecting a pair of arguments into one that takes them one at a time. The program is

$$\lambda f.\lambda x.\lambda y.f(x,y)$$

with type $\left(\right(\alpha \times \beta )\to \gamma )\to \alpha \to \beta \to \gamma$. Take the bundled function $f$ and return a function that accepts $x$, then $y$, then feeds them to $f$ as a pair.

Read the type as a proposition: if $\alpha$ and $\beta$ together imply $\gamma$, then $\alpha$ implies that $\beta$ implies $\gamma$. You can always unbundle a joint hypothesis into two sequential ones.

Build the typing derivation. Assume $f:(\alpha \times \beta )\to \gamma$, $x:\alpha$, and $y:\beta$. By the pair rule, $(x,y)$ has type $\alpha \times \beta$. By the application rule, $f(x,y)$ has type $\gamma$. Then discharge the assumptions one at a time with three lambdas: first $y$, then $x$, then $f$.

Now read the same tree as a proof. Assume $\alpha \wedge \beta$ implies $\gamma$. Assume $\alpha$. Assume $\beta$. From $\alpha$ and $\beta$, conclude $\alpha \wedge \beta$: conjunction introduction. Apply modus ponens with the first assumption to get $\gamma$. Discharge $\beta$, then $\alpha$, then the original hypothesis. The theorem is proved.

Currying is a theorem in propositional logic. The program is the proof.

Reading programs as theorems#

Once you see this, you can read any typed program as a theorem. The identity function $\lambda x.x:\alpha \to \alpha$ proves that every proposition implies itself. The constant function $\lambda x.\lambda y.x:\alpha \to \beta \to \alpha$ proves that knowing $\alpha$, no additional hypothesis can take it away.

Pause and try: what theorem does function composition prove?

Composition takes $f$ from $\alpha$ to $\beta$ and $g$ from $\beta$ to $\gamma$ and returns $\lambda x.g\left(f\right(x\left)\right)$. Its full type is

$$(\alpha \to \beta )\to (\beta \to \gamma )\to (\alpha \to \gamma ).$$

Read it as a proposition: if $\alpha$ implies $\beta$, and $\beta$ implies $\gamma$, then $\alpha$ implies $\gamma$. Transitivity of implication. The proof is function composition itself: given an $\alpha$, run it through $f$ to get a $\beta$, then through $g$ to get a $\gamma$. Two uses of the application rule under three lambdas.

The correspondence, and where it leads#

Types are propositions. Programs are proofs. A function from $\alpha$ to $\beta$ is a proof that $\alpha$ implies $\beta$, a pair is a proof of "and", a tagged union is a proof of "or", and type checking is proof verification. Your compiler has been verifying theorems every time you build your code.

One precision matters: the logic on the other side is intuitionistic propositional logic. Every proof is a construction, because every proof is a program. Classical principles like the excluded middle and Peirce's law have no lambda term at all; recovering them takes control operators, as Timothy Griffin showed in 1990.

And this is only the beginning. The simply typed lambda calculus corresponds to propositional logic. Add polymorphism and you get second-order propositional logic. Add dependent types, types that can refer to values, and you get predicate logic. Languages like Coq, Agda, and Lean are built on this; in those languages, writing a program and proving a theorem are the same activity.

Every well-typed program you have ever written was a theorem, with one caveat: in a language with general recursion, a looping program inhabits every type, so the logic is inconsistent. The correspondence carries its full weight in total languages, which is why proof assistants demand that every program terminate.

If you remember three things#

1. The lambda calculus has three constructs, and the simply typed version assigns each term a type by three rules: variable, abstraction, and application.
2. Those rules are natural deduction with the proofs written in: abstraction is implication introduction, application is modus ponens, pairs are conjunction, sums are disjunction.
3. A well-typed program is a proof of its type read as a proposition; currying proves that a joint hypothesis can be split, and dependent types extend the idea all the way to Coq, Agda, and Lean.