Some of the most meaningful mathematical realizations that I’ve had have been unexpected connections between two topics; that is, realizing that two concepts that first appeared quite distinct are in fact one and the same. In our first linear algebra courses, we learn that manipulations of matrices is, in fact, equivalent to solving systems of equations. In quantum mechanics, we see that physically observable quantities are, mathematically speaking, linear operators (I still don’t quite grok this one). And, my personal favorite example, we learn in functional analysis that the linear functionals in the dual space of a Hilbert space are themselves in perfect correspondence with the functions in the original space.1
Recently, I’ve stumbled upon another such result, which has captured my attention for a while. The result, often referred to as Curry-Howard correspondence, is the statement that propositions in a formal logical system are equivalent to types in the simply typed lambda calculus. Loosely, this means that logical statements are equivalent to data types!
Let’s unpack that a bit; “propositions” are just statements in a logical
system.2 In mathematics, for example, one might put forward the
proposition “no even numbers are prime,” or “14 is greater than 18”. Note that
propositions need not be true; in fact, some logical systems support
propositions that cannot even be determined to be true or false.3
“Types” can be though of as types in a computing language;
and so on. We will have much more to say about types as we move forward, but for
now, hold in your mind the conventional notion of types as defined in a language
such as Java or Python (or better yet, Haskell).
How on earth could these two be in correspondence? On the surface, they appear entirely separate concepts. In this post, I’ll spend some time unpacking what this equivalence is actually saying, using a simple example. I am far from a full understanding of it, but as usual, I write about it in the hopes that I’ll be forced to clarify what I do understand, or even better, be corrected by someone more knowledgable than myself.
Speaking of those more knowledgable than myself, there are various resources online that I found very helpful in understanding the correspondence: Philip Wadler’s talk on the subject is a great starting point, and there are a number of useful discussions available on StackExchange and various functional programming forums.
I was confused by the idea of propositions as types when I first encountered it,
and after learning more, I believe that the root of my confusion lies in the
fact that types such as
String, which we are
familiar with from programming, correspond to very trivial propositions, making
them poor examples. We’ll have to introduce something a bit fancier; a
conditional type. For example,
OddInt might be odd Integers, and
might be prime integers. We’ll approximate these conditional types with custom
classes in Scala. Classes and types are different beasts, of course, but
we will ignore that distinction in this post.4
Let’s consider one conditional type in particular:
BigInteger. This type
(actually a class in this example) is defined as follows:
One could then instantiate a
BigInteger as follows:
Now the fundemanetal question: what proposition corresponds to this type? In
simple scenarios like this, the corresponding proposition is that the type can
be inhabited; that is, there exists a value that satisfies that type. For
example, the type
BigInteger corresponds to the claim “there exists an integer
\(i\) for which \( i > 10,000 \)”. Obviously, such an integer exists, and the
fact that we can instantiate this type indicates that it corresponds to a true
proposition. Alternatively, consider a type
WeirdInteger, which is an integer
i < 3 && i > 5. We can define the type well enough, but there are
no values which satisfy it; it is an uninhabitable type, and so corresponds to a
Functions and Implication
Let’s make things a little more interesting. In programming languages, there are
not only primitive types like
Boolean, but there are also
function types, which are the types of functions. For example, in Scala, the
def f(x: Int) = x.toString has type
Int => String, which is to say
it is a function that maps integers to strings.
What sort of propositions would functions correspond to? It turns out that
functions naturally map to implication. In some ways, the correspondence here
is very natural. Consider the conditional type
BigInteger, and the conditional
BiggerInteger. The definition of the latter should look familiar, from
Now, we can write a function that maps
Recall that the proposition corresponding to the type
BigInteger is the
statement “there exists an integer greater than 10,000”, and the proposition
Bigger is the statement “there exists an integer greater than
20,000”; the proposition corresponding to the function type
BiggerInteger is then just the statement “the existence of an integer above
10,000 implies the existence of an integer above 20,000”. And note that, as it
should be for an implication, we do not care whether there actually does exist
an integer above 10,000; we simply know that if one exists, then its existence
implies the existence of an integer above 20,000.
To be a bit more explicit, the function that we wrote above can be thought of as a proof of the implication; in particular, if we suppose that there exists an \(i\) such that \(i > 10,000\), then clearly \(2i > 20,000\), and so if we let \(j=2i\), then we have proven the existence of a \(j\) such that \(j > 20,000\). This is what the theoretical computer scientists mean when they say that “programs are proofs”.
Of course, Scala is not a proof-checking language, and cannot tell during
compilation that the function
makeBigger is valid; we would need a much richer
type system to be able to validate such functions. Consider that the following
function compiles with no problem, although there are no input values for which
it will not throw a (runtime) exception:
If you think about it a bit more, it’s sort of a weird example; you
could map any type to
BiggerInteger, just by doing
BiggerInteger = new BiggerInteger(20001). This is because the proposition that
BiggerInteger is true (the type is inhabitable), and if B is
true, then A implies B for any A at all.
Common languages such as Haskell only express very trivial propositions with
their types; there does exist one uninhabitable type (
void), but I have not
found much use for it in practice. The benefit of using conditional types for
these examples is that we can explore at least some types which have
corresponding false propositions, such as
WeirdInteger, which are integers
i which satisfy
i < 3 && i > 5.
Seeing all this, you can begin to get a sense of how computer-assisted proof techniques might arise out of it. If the fact that a program compiles is equivalent to the truth the corrsponding proposition, then all we need is a language with a rich enough type system to express interesting statements. Examples of languages used in this way include Coq and Agda. A thorough discussion of such languages is beyond both the scope of this post and my understanding.
I think what keeps me interested in this subject is that it still remains quite opaque to me; I’ve struggled to even come up with these simple (and flawed) examples of how Curry-Howard correspondence plays out in practice. I hope that anyone reading this who understand the subject better than I do will leave a detailed list of my misunderstandings, so that I can better grasp this mysterious and fascinating topic.
This statement is difficult to understand without background in functional analysis, but it is in fact one of the most beautiful examples of such an equivalence result. ↩