The Curry–Howard Correspondence

Symptom

You write a function signature and it looks like a sentence:

f :: (a -> b) -> (b -> c) -> (a -> c)

Read it aloud: if $a$ implies $b$, and $b$ implies $c$, then $a$ implies $c$. That is transitivity of implication, a rule of logic you have known since school. And the implementation, f g h = h . g, is the proof of it: given evidence for $a$, apply the first, then apply the second.

This keeps happening. A pair type is a conjunction. Either is a disjunction. Void is falsity. It looks like a pun on notation, and every time you dismiss it another instance shows up, until you notice that the type checker is rejecting programs for reasons that sound exactly like invalid proofs.

It is not a pun. It is an isomorphism, and it was found four separate times by people in four different fields who were not looking for each other’s results.

Statement

Propositions are types. Programs are proofs. Evaluation is proof simplification.

The dictionary, which is the whole content:

Argument

Check one row properly. Modus ponens says: from $A \Rightarrow B$ and $A$, conclude $B$. The typing rule for application says: from f : A -> B and x : A, conclude f x : B. These are the same rule. Not analogous, not similar in spirit. Erase the terms from the typing rule and you have modus ponens; erase nothing and you have a proof carrying its own construction.

Implication introduction says: to prove $A \Rightarrow B$, assume $A$ and derive $B$. Lambda abstraction says: to build A -> B, bind a variable of type A and produce a B. The assumption is the bound variable, and discharging the assumption is binding it. Which is why an unbound variable is a type error and an undischarged assumption is an invalid proof: the same defect seen from two sides.

Evaluation is proof simplification. A proof that introduces a connective and immediately eliminates it contains a detour. Prove $A \Rightarrow B$ by assuming $A$, then apply it to an actual proof of $A$. Gentzen’s cut elimination removes the detour by substituting the proof of $A$ into the derivation. On the other side of the dictionary that reads $(\lambda x.M),N \to M[x:=N]$, which is $\beta$-reduction (T041).

Running a program and normalizing a proof are the same operation. This is the part that stops feeling like notation. Gentzen proved cut elimination in 1935 to establish the consistency of his logic. Church built $\beta$-reduction in 1936 to model computation. They wrote down the same rewrite, for unrelated reasons, one year apart.

Why intuitionistic and not classical. The correspondence is with constructive logic, and the missing piece is instructive. The law of excluded middle, $A \vee \neg A$, corresponds to the type forall a. Either a (a -> Void). To inhabit it you would need a program that, for any type, either produces a value of it or produces a proof it is uninhabited. That is a universal decision procedure, which does not exist (T016). A constructive proof of $A \vee B$ must say which, and no program can always say which.

Double-negation elimination ((a -> Void) -> Void) -> a fails for the same reason: knowing a thing cannot fail to exist does not hand you one.

Griffin’s extension is the surprise. In 1990 Griffin showed that classical logic corresponds to control operators: call/cc has the type of Peirce’s law, $((A \Rightarrow B) \Rightarrow A) \Rightarrow A$. A classical proof is a program that can back up and try a different branch. The continuation captures “what I would have had to prove,” and excluded middle becomes the strategy of asserting $A$, running with it, and if it ever fails, jumping back with the counterexample that establishes $\neg A$. Classical logic was not outside the correspondence; it corresponded to a feature nobody had connected to it.

The four independent discoveries. Curry noticed in the 1930s that the types of combinators are axiom schemes of implicational logic. Howard wrote it up for natural deduction in 1969 in a note circulated for years before publication. Lambek found the same structure in cartesian closed categories. De Bruijn built Automath on it while trying to mechanize mathematics. None of them were reading each other. Wadler’s argument, and it is convincing, is that a thing found four times by people looking for four different things is discovered rather than invented.

Forbids

A total functional language proving its own consistency. A language whose types are a logic and whose terms are proofs inherits Gödel (T015). Coq cannot prove Coq’s consistency.

Inhabiting forall a. a. That is a proof of an arbitrary proposition, so a term of that type in a total language collapses the logic. In Haskell you can write one with undefined, and this is exactly why Haskell’s type system is not a sound logic: general recursion inhabits every type, so every proposition is “provable” by a program that loops.

Constructive proof of excluded middle, without control operators. And with them you have left the pure fragment and acquired a program whose meaning depends on evaluation order.

Extracting an algorithm from a classical existence proof. A non-constructive proof that some object exists corresponds to no program producing it. This is a real limitation in practice: many elegant mathematical proofs have no computational content at all.

Does not forbid

It does not mean you must use a proof assistant to benefit. This is the misreading that makes the correspondence look irrelevant. Every use of the type system in an ordinary language is a small proof. Rust’s borrow checker is a substructural logic proving no aliased mutation; TypeScript’s discriminated unions are disjunction elimination with exhaustiveness checking as the proof obligation; Java’s generics are bounded quantification. When the compiler says “non-exhaustive patterns,” it is telling you a case is unproved.

It does not mean dependent types are impractical. Coq produced CompCert, a verified C compiler that Csmith’s fuzzing campaigns could not find a middle-end bug in, while finding hundreds in GCC and LLVM. seL4 is a machine-checked verified microkernel. Lean’s mathlib has formalized a large body of modern mathematics, and Lean was used to check the Liquid Tensor Experiment at Scholze’s request. These are shipped artifacts.

It does not require the whole program to be verified. Liquid Haskell, Dafny, F*, and refinement types in general let you prove the properties worth proving and leave the rest, and this incremental use is how the technique actually enters industrial codebases.

It does not say types must be complicated to be useful. The correspondence holds at every strength. Maybe is disjunction with unit, and using it instead of null is a proof that you handled absence.

It does not mean a well-typed program is correct. The proposition proved is the type, and if your type is Int -> Int you have proved almost nothing. The correspondence tells you exactly how much you proved: precisely the content of the type, no more.

Boundary

• Intuitionistic by default. Classical reasoning requires control operators and their evaluation-order sensitivity.
• Totality is required for soundness. General recursion inhabits every type and destroys the logic. Coq and Agda enforce termination checking, which is why they are logics and Haskell is not.
• Effects break it. A function that logs, throws, or reads a mutable cell is not a proof of anything, because its result is not determined by its argument. Monadic and effect-typed encodings exist to keep the pure core intact.
• Proof relevance. In logic, any two proofs of $A$ are interchangeable. In programming, two terms of type Int -> Int are emphatically not. Homotopy type theory takes this seriously and studies the structure of the space of proofs, which turns out to be the topology of paths.

The idea to carry: a type is a claim, a program is its evidence, and the compiler is a proof checker you have been using all along without calling it one.

Read next