The Curry–Howard correspondence

So we have reached the most important part. A program in a language that takes the λ-calculus as its foundation and has solved the problem of non-termination is a theorem: its statement is the type, compilation is the checking of the proof, and execution is guaranteed to return a result of the promised type. The same is possible with imperative languages — program correctness has been proved ever since Hoare logic — but it is much harder: there the proof is not the program itself but a separate superstructure of preconditions, postconditions and invariants.

So: programs written in languages based on the λ-calculus are easier to prove correct than programs in other languages — not necessarily imperative ones; take Python. In this chapter we look at the Curry–Howard correspondence, a bridge between logic and programming: to write a program of type $\tau$ is the same as to prove the proposition $\tau$. Curry noticed it back in the 1930s — in the types of combinators — and it took its precise form in Howard's 1969 manuscript.

Let us look at the types of familiar terms, reading the arrow as the implication “$B$ follows from $A$”. The identity function turns out to prove the tautology “$A$ follows from $A$”:

The combinator $\mathrm{K}$, which discards its second argument, proves the proposition “if $A$ holds, then $A$ follows from anything”:

The combinator $\mathrm{S}$ also proves a theorem — about distributing a premise over two consequences:

Let us, then, give the correspondence table:

A few clarifications. The unit type $()$ is the type with exactly one value. That value can always be constructed, trivially — hence $\top \;$ $\leftrightarrow\; ()$. The empty type $\mathtt{Void}$, by contrast, has no values at all: a program of this type cannot be written. This is falsehood itself: $\bot$ has no proofs.

“Second-order $\forall$ → System F polymorphism” (we will come back to this later). A second-order quantifier ranges over propositions themselves (in the world of types — over types): “for every proposition $A$ …”. In programs this is exactly parametric polymorphism: the type of the identity function $\forall a.\; a$ $\to a$ reads as the theorem “for every $A$: $A$ follows from $A$”. System F is a λ-calculus with such quantification over types built into the language; Haskell's polymorphism is based on it.

“$\forall,\;\exists$ over objects → dependent types”. First-order quantifiers range not over propositions but over objects — concrete values: “for every number $n$ …”, “there exists a list $x$ such that …”. To write this as a type, the type must depend on a value — this is what dependent types are. In Haskell itself $\forall$ ranges only over types, but LiquidHaskell attaches logical predicates to types — refinement types: the signature $\mathtt{head'} : \{\,v : [a] \mid \mathtt{len}\;v$ $> 0\,\}$ $\to a$ reads as “for every list $v$ whose length is greater than zero …”, and the implications between predicates are checked by an SMT solver. The quantifier $\exists$ is expressed by refining the result: $\{\,v : \mathtt{Int} \mid \mathtt{even}\;v\,\}$ is an even number presented together with the guarantee of its evenness. More on this in the “LiquidHaskell” section.

We are back to the problem of Turing completeness. Unrestricted recursion $\mathtt{fix} : (A \to A)$ $\to A$ reads logically as “if $A$ follows from $A$, then $A$ holds”: a vicious circle that proves anything. That is why proof languages must be total: the totality check from the previous section is not an excess of caution but the condition of the logic's honesty. The Agda proof assistant stands on this correspondence: the specification is written as a type, a program of that type is the proof, and proof checking is ordinary type checking.