The Idea of My Year: Curry-Howard Correspondence

Edited on September 20, 2015 to add footnote 4.

Curry-Howard Correspondence was first published in 1969, before the author was born, but the author only learned of it in the present year. That alone is enough to induce a desire to go back to everybody one has ever encountered, starting with one's mother and father, grab and shake them, and cry You knew I lived, breathed, thought! Yet, you allowed me to remain in ignorance that such beauty and cleverness existed. How could you have been so cruel and thoughtless? Regardless, it is the idea of the author's year. To rescue the reader from the purgatory that ignorance of Curry-Howard Correspondence is, let one make an inexpert attempt to explain it here.

A notion common to almost all programming language is the function. A function takes an element from one set and returns an element from another, or possibly the same, set. For example, the function plusOne may take an element from the set of integers and yield an element from the same set of integers, specifically the integer one higher. One says that a function \(f\) that takes an element from the set \(A\) and returns an element of the set \(B\) has the type of \(A \to B\). An obvious implication is that \(A \to B\) also describes a set; that of all functions of type \(A \to B\).

One objection to this notion of function is that it is too limited. Many a useful function \(f\) take a fixed number of parameters \(a_0, a_1, \ldots a_n\), each from the sets \(A_0, A_1, \ldots A_n\), and yields a fixed number of results \(b_0, b_1, \ldots b_n\), each from the sets \(B_0, B_1, \ldots B_n\).

One common way to fit such a function \(f\) within the limited notion of functions taking only a single parameter and yielding only a single result is to say that \(f\) really only takes a single parameter from the cartesian product set of the sets \(A_0, A_1, \ldots A_n\) or \((A_0 \times A_1 \times \ldots \times A_n)\) and yields only a single result from the cartesian product set of the sets \(B_0, B_1, \ldots B_n\) or \((B_0 \times B_1 \times \ldots \times B_n)\). So the type of \(f\) is \((A_0 \times A_1 \times \ldots \times A_n) \to (B_0 \times B_1 \times \ldots \times B_n)\).

Another, useful way to describe such a function \(f\)—due to Haskell Curry—is to say that \(f\) takes only a single parameter from the set \(A_0\), but rather than yielding any particular value, it instead yields a function from the set \(A_1 \to \ldots \to A_n \to (B_0, B_1, \ldots B_n)\).

For example, the common function add, rather than taking two parameters \(x\) and \(y\), each from the set of integers \(\mathbb Z\) and yielding their sum \(x+y\), also from \(\mathbb Z\), as programmer conventionally think, or taking a single element from the cartesian product set \((\mathbb Z \times \mathbb Z)\), as the above description went, actually takes a single element of \(\mathbb Z\) and yields a function that takes another single element of \(\mathbb Z\) and yields yet another element of \(\mathbb Z\), the sum of the integer first given to add and the integer given to the function yielded by add. In other words, the type of add is \(\mathbb Z \to (\mathbb Z \to \mathbb Z)\) or, as \(\to\) is defined to be right-associative, just \(\mathbb Z \to \mathbb Z \to \mathbb Z\).

Functions can be arbitrarily complex. For concreteness,¹ consider that somewhere within the bowels of the Social Security Administration there must exist a computer with a function socialSecurity which takes one integer, a Social Security number, and yields another integer, the balance of the Social Security account of the holder of that number,² in cents.

But socialSecurity is only a partial, not a total, function for it will not yield an integer for every integer given to it. For example, if given an invalid Social Security number (one with more or less than 9 digits, or negative, or otherwise never issued), it will, instead of a balance, yield some error message or perhaps, if badly written, just loop forever. Computer scientists denote both of such outcomes by \(\bot\) (pronounced bottom). So the type of the socialSecurity is not really \(\mathbb Z \to \mathbb Z\), but \(\mathbb Z \to \mathbb Z \cup \left\{ \bot \right\}\). In other words, socialSecurity when given an integer will yield either an integer or \(\bot\), i.e., socialSecurity always yields an element from the set union of \(\mathbb Z\) and \(\left\{ \bot \right\}\).

After these preliminaries, Curry-Howard Correspondence can be simply stated:

Every type corresponds to a logical proposition and vice versa. In particular:

1. The empty type corresponds to the false proposition.
2. The union type \(A \cup B\) corresponds to the proposition that proposition \(p_A\) or \(p_B\) or both are true (where \(p_A\) and \(p_B\) are the propositions corresponding to the types \(A\) and \(B\), respectively.)
3. The cartesian product type \(A \times B\) corresponds to the proposition that propositions \(p_A\) and \(p_B\) are both true.
4. The set of functions \(A \to B\) corresponds to the proposition that \(p_B\) follows from \(p_A\).
5. The writing of a total function of type \(A \to B\) (i.e., establishing that the set \(A \to B\) is not empty) corresponds to a proof of the proposition \(p_A \Rightarrow p_B\).³

In other words, programming and mathematical proof are the same thing! Imagine one's shock upon learning that these two activities one had previously devoted a significant part of one's life to and had thought oneself reasonably adept at, were not only related, but actually the same.⁴ It is this shock and the consequent inability to think about the subjects involved in any way but within its terms, that marks Curry-Howard equivalence as one of the genuinely great ideas.

Thus, henceforth it must be the duty of every kindly reader upon encountering a person who may yet live in ignorance of Curry-Howard Correspondence to make it the very first thing mentioned.

¹ Concreteness is helpful in thinking about abstractions to all but Grothendieck. If there is a heaven and the most eccentric geniuses go there, one would like to imagine that they'll have internet access and read this blog (though, sadly, that does not appear to be reflected in the readership statistics). In that case, one apologizes to Grothendieck.

² Readers aware of the actual legal status of the Social Security system will object that, contrary to popular belief, there is no such thing as an individual Social Security account with a balance. That is quite true, as the government lacks such basic honesty and integrity as exhibited, for example, by investment bankers. But for purposes of this discussion, let it pass and imagine instead a function that yields a schedule of promised benefits were the holder to retire today.

³ And so one discovers that the typographical similarity between the symbols \(\rightarrow\) in programming land and \(\Rightarrow\) in proof land is not a coincidence. In the profound Curry-Howard sense, they actually mean the same thing.

⁴ Or imagine that one had two favorite games. One would play the one or the other, as the mood or occasion struck one, eventually accumulating many thousands of hours of play in each and an imagined degree of mastery in both. Then an onlooker would point out that these two games are actually the same, differing only in the color of the counters and some illustrations on the board. The inescapable conclusion would be that, contrary to what one's mother always said, one is not such a clever boy after all.