The Curry–Howard isomorphism is a striking relationship connecting two seemingly unrelated areas of mathematics — type theory and structural logic.
IntroductionEdit
The Curry–Howard isomorphism, hereafter referred to as simply CH, tells us that in order to prove any mathematical theorem, all we have to do is construct a certain type which reflects the nature of that theorem, then find a value that has that type. This seems extremely weird at first: what do types have to do with theorems? However, as we shall see, the two are very closely related. A quick note before we begin: for these introductory paragraphs, we ignore the existence of expressions like error
and undefined
whose denotational semantics are ⊥. These have an extremely important role, but we will consider them separately in due time. We also ignore functions that bypass the type system like unsafeCoerce#
.
We can build incredibly complicated types using Haskell's higherorder functions feature. We might want to ask the question: given an arbitrary type, under what conditions does there exist a value with that type (we say the type is inhabited)? A first guess might be 'all the time', but this quickly breaks down under examples. For example, there is no function with type a > b
, because we have no way of turning something of type a
into something of a completely different type b
(unless we know in advance which types a
and b
are, in which case we're talking about a monomorphic function, such as ord :: Char > Int
).
Incredibly, it turns out that a type is only inhabited when it corresponds to a true theorem in mathematical logic. But what is the nature of this correspondence? What does a type like a > b
mean in the context of logic?
A crash course in formal logicEdit
We need some background on formal logic before we can begin to explore its relationship to type theory. This is a very brief introduction; for a wider grounding we recommend you consult an introductory textbook on the subject matter.
In everyday language we use a lot of 'If... then...' sentences. For example, 'If the weather is nice today, then we'll walk into town'. These kinds of statements also crop up in mathematics; we can say things like 'If x is positive, then it has a (real) squareroot'. Formal logic is a way of representing statements which approximate English meanings with a Boolean logic on which we can do computations. We use the A→B sign (read as 'A implies B') to indicate that B is true whenever A is true. For example, our earlier statement could be recast as ' x is positive → x has a real squareroot ', meaning the number's positivity implies the existence of the desired kind of root. We'll often use letters to stand for entire statements, so for example if W is the statement 'the weather is nice', and T is the statement 'we'll walk into town', then we could say W → T.
Our definition of P→Q has some flaws. If Q is some statement that is always true, no matter what the circumstances — like 'the sun is hot' — then it doesn't matter what P is. P could even be a false statement, Q would still be true if P were true, so the implication P → Q is not considered to be proved wrong. P → Q is defined to be true whenever P is false and whenever Q is true. So → doesn't really represent any kind of causeeffect relationship; things like 'the sky is pink → the sun is hot' are defined to be true. There are other logical algebras besides Boolean logic which try to fix these "problems"^{[1]} and we can also construct them in Haskell.
Other things that crop up lots in both everyday language and mathematics are things called conjunctions and disjunctions. The former represent statements involving an 'and', the latter statements involving an 'or'. We could represent the statement 'I will buy this magazine if it's in stock and I have enough money' by the symbolism , where M = 'I have enough money', S = 'The magazine is in stock', B = 'I will buy the magazine'. Essentially, one can just read the symbol as 'and'. Similarly, one can read the symbol as 'or', so that the statement 'I will either walk or get the train to work or both' could be represented as , where W = 'I will walk to work', and T = 'I will get the train to work'.
Using these symbols, and a few more which will be introduced as we go, we can produce arbitrarily complicated symbol strings. There are two classes of these symbol strings: those that represent true statements, often called the theorems; and those which represent false statements, called the nontheorems. Note that whether a symbol string is a theorem or nontheorem depends on what the letters stand for, so is a theorem if, for example, P represents the statement 'It is daytime' and Q represents the statement 'It is night time' (ignoring exceptions like twilight), but it would be a nontheorem if P were 'Trees are blue' and Q were 'All birds can fly'. We'll often call a symbol string a proposition if we don't know whether it's a theorem or not.
There are many more subtleties to the subject of logic (including the fact that when we say 'If you eat your dinner you'll get dessert' we actually mean 'Only if you eat your dinner will you get dessert'). If this is a subject that interests you, there are many textbooks around that comprehensively cover the subject.
Propositions are typesEdit
So, given a type a > b
, what does that mean in terms of symbolistic logic? Handily, it simply means that a → b. Of course, this only makes sense if a
and b
are types which can further be interpreted in our symbolistic logic. This is the essence of CH. Furthermore, as we mentioned before, a → b is a theorem if and only if a > b
is an inhabited type.
Let's see this using one of the simplest of Haskell functions. const
has the type a > b > a
. Translated into logic, we have that a → b → a. This must be a theorem, as the type a > b > a
is inhabited by the value const
. Now, another way of expressing a → b is that 'If we assume a is true, then b must be true.' So a → b → a means that if we assume a is true, then if we further assume that b is true, then we can conclude a. This is of course a theorem; we assumed a, so a is true under our assumptions.
The problem with ⊥Edit
We've mentioned that a type corresponds to a theorem if that type is inhabited. However, in Haskell, every type is inhabited by the value undefined
. Indeed, more generally, anything with type forall a. a
, a value with denotational semantics of ⊥, is a problem. ⊥ in type theory corresponds to inconsistency in logic; we can prove any theorem using Haskell types because every type is inhabited. Therefore, Haskell's type system actually corresponds to an inconsistent logic system. However, if we work with a limited subset of Haskell's type system, and in particular disallow polymorphic types, we have a consistent logic system we can do some cool stuff in. Hereafter it is assumed we are working in such a type system.
Now that we have the basics of CH, we can begin to unpack a little more the relationship between types and propositions.
Logical operations and their equivalentsEdit
The essence of symbolic logic is a set of propositions, such as P and Q, and different ways of combining these propositions such as Q → P or . These ways of combining propositions can be thought of as operations on propositions. By CH, propositions correspond to types, so we should have that the CH equivalents of these proposition combinators are type operations, more normally known as type constructors. We've already seen an example of this: the implication operator → in logic corresponds to the type constructor (>)
. The rest of this section proceeds to explore the rest of the proposition combinators and explain their correspondence.
Conjunction and DisjunctionEdit
In order for to be a theorem, both A and B must be theorems. So a proof for amounts to proving both A and B. Remember that to prove a proposition A we find a value of type A
, where A and A
are CH correspondents. So in this instance we wish to find a value that contains two subvalues: the first whose type corresponds to A, and the second whose type corresponds to B. This sounds remarkably like a pair. Indeed, we represent the symbol string by (a, b)
, where a
corresponds to A and b
corresponds to B.
Disjunction is opposite to conjunction. In order for to be a theorem, either A or B must be a theorem. Again, we search for a value which contains either a value of type A
or a value of type B
. This is Either
. Either A B
is the type which corresponds to the proposition .
FalsityEdit
It is occasionally useful to represent a false statement in our logic system. By definition, a false statement is one that can't be proven. So we're looking for a type which isn't inhabited. Although none of these types exist in the default libraries (don't get confused with the ()
type, which has precisely one value), we can define one (or for older versions of GHC that does not support Haskell2010, we turn on the XEmptyDataDecls
flag):
data Void
The effect of omitting the constructors means that Void
is an uninhabited type. So the Void
type corresponds to a nontheorem in our logic. There are a few handy corollaries here:

(Void, A)
and(A, Void)
are both uninhabited types for any typeA
, corresponding to the fact that and are both nontheorems if F is a nontheorem. 
Either Void A
andEither A Void
are essentially the same asA
for any typeA
, ^{[2]} corresponding to the fact that and , where F is a nontheorem, are theorems only if A is a theorem. 
Any type that corresponds to a nontheorem can be replaced with
Void
. This is because any nontheoremtype must be uninhabited, so replacing it withVoid
everywhere doesn't change anything.Void
is really equivalent to any nontheorem type^{[3]}. 
As we remarked in the first section, the implication P → Q is true if Q is true, regardless of the truth value of P. So we should be able to find a term with type
Void > a
. In fact one does exist, but it's somewhat complicated to explain: the answer is the empty function. We can define a functionf :: A > B
as a (probably infinite) set of pairs whose first element is an element ofA
(the domain) and second element isf
's output on this term, an element ofB
(the codomain). For example, the successor function on the naturals is represented as{(0,1), (1,2), (2,3), ...}
. Note that in order to be a (total and welldefined) function, we must have precisely one pair(a, f a)
for each terma
with typeA
.The empty function, let's call it
empty
is represented in this way by the empty set. But as we must have a pair for each element of the domain, and there no pairs in our representation, the domain type must be empty, i.e.Void
. What about the range type?empty
never produces any output, so there are no restrictions placed on the range type. Thus, it is valid to assume that the range type has any type, so we can sayempty :: forall a. Void > a
. Unfortunately, it's not possible to write this function in Haskell; we'd ideally like to write something like:empty :: Void > a
And stop there, but this is illegal Haskell. The closest we can come is the following:
empty :: Void > a empty _ = undefined
Alternatively:
empty :: Void > a empty = empty
Another reasonable way would be to write (valid in GHC with EmptyCase extension):
empty x = case x of { }
The case statement is perfectly well formed since it handles every possible value of
x
.Note that this is perfectly safe, since the righthand side of this function can never be reached (since we have nothing to pass it). So, the conclusion of all this is that
Void > a
is an inhabited type, just as P → Q is true if P is false.
NegationEdit
The ¬ operation in logic turns theorems into nontheorems and vice versa: if A is a theorem then ¬A is a nontheorem; if A is a nontheorem then ¬A is a theorem. How can we represent this in Haskell? The answer's a sneaky one. We define a type synonym:
type Not a = a > Void
So for a type A
, Not A
is just A > Void
. How does this work? Well, if A
was a theoremtype, then A > Void
must be uninhabited: there's no way any function could return any value, because the return type, Void
has no values (The function has to provide values for all inhabitants of A)! On the other hand, if A
was a nontheorem, then A
can be replaced with Void
as we explored in the last section. Then the function id :: Void > Void
is an inhabitant of Not A
, so Not A
is a theorem as required (The function doesn't have to provide any values, since there are no inhabitants in its domain. Nevertheless it's a function — with an empty graph).
Axiomatic logic and the combinatory calculusEdit
So far we've only used some very basic features from Haskell's type system. Indeed, most of the features of logic we've mentioned can be explored using a very basic 'programming language', the combinator calculus. To fully appreciate how closely CH ties together these two areas of mathematics, we need to axiomatise both our discussion of formal logic and our discussion of programming languages.
Axiomatic logicEdit
We start with two axioms about how the → operation should behave (from now on, we assume that → is a rightassociative function, i.e. A → B → C means A → (B → C)):
 A → B → A
 (A → B → C) → (A → B) → A → C
The first axiom says that given any two propositions A and B, if we assume both A and B, we know that A is true. The second says that if A implies that B implies C (or equivalently, if C is true whenever A and B are true), and A itself implies B, then knowing A is true would be enough to conclude that C is true. This may seem complicated, but a bit of thought reveals it to be common sense. Imagine we have a collection of boxes of various colours, some with wheels, some with lids, such that all the red boxes with wheels also have lids, and all the red boxes have wheels. Pick one box. Let A = 'The box under consideration is red', B = 'The box under consideration has wheels', C = 'The box under consideration has a lid'. Then the second law tells us that, as A → B → C (all red boxes with wheels also have lids), and A → B (all red boxes have wheels), then if A (if the box is red), then C must be true (the box has a lid).
We also allow one inference law, called modus ponens:
 If A → B, and A, then B.
This law allows us to create new theorems given old one. It should be fairly obvious; it is essentially the definition of what → means. This small basis provides a simple enough logic system which is expressive enough to cover most of our discussions. Here's a sample proof of the law A → A in our system:
Firstly, we know the two axioms to be theorems:
 A → B → A
 (A → B → C) → (A → B) → A → C
You'll notice that the lefthand side of the second axiom looks a bit like the first axiom. The second axiom guarantees that if we know that A → B → C, then we can conclude (A → B) → A → C. In this case, if we let C be the same proposition as A, then we have that if A → B → A, then (A → B) → A → A. But we already know A → B → A, that was the first axiom. Therefore, we have that (A → B) → A → A is a theorem. If we further let B be the proposition C → A, for some other proposition C, then we have that if A → C → A, then A → A. But, again, we know that A → C → A (it's the first axiom again), so A → A, as we wanted.
This example demonstrates that given some simple axioms and a simple way to make new theorems from old, we can derive more complicated theorems. It may take a while to get there — here we had several lines of reasoning to prove just that the obvious statement A → A is a theorem! — but we get there in the end. This kind of formalisation is attractive because we have essentially defined a very simple system, and it is very easy to study how that system works.
Combinator calculusEdit
The lambda calculus is a way of defining a simple programming language from a very simple basis. If you haven't already read the chapter that was just linked to, we recommend you read at least the introductory sections on the untyped version of the calculus. Here's a refresher in case you're feeling dusty. A lambda term is one of three things:
 A value, v.
 A lambda abstraction , where t is another lambda term.
 An application , where and are lambda terms.
There is one reduction law, too, called betareduction:
 → , where means with all the free occurrences of x replaced with .
As mentioned in the lambda calculus article, the difficulty comes when trying to pin down the notion of a free occurrence of an identifier. The combinator calculus was invented by the American mathematician Haskell Curry (after whom a certain programming language is named) because of these difficulties. There are many variants on the basic combinator calculus, but we consider one of the simplest here. We start with two socalled combinators:
 K takes two values and returns the first. In the lambda calculus, .
 S takes a binary function, a unary function and a value, and applies that value and the value passed into the unary function to the binary function. again, in the lambda calculus: .
The first function you should recognise as const
. The second is more complicated, it is the monadic function ap
in the ((>) e)
monad (which is essentially Reader). These two combinators form a complete basis for the entire lambda calculus. Every lambda calculus program can be written using just these two functions.
Sample proofsEdit
Intuitionistic vs classical logicEdit
So far, all of the results we have proved are theorems of intuitionistic logic. Let's see what happens when we try to prove the basic theorem of classical logic, Not Not A > A
. Recall that this translates as ((A > Void) > Void) > A
. So, given a function of type (A > Void) > Void
we need a function of type A. Now a function of type (A > Void) > Void
exists precisely if type A > Void
is uninhabited, or in other words if type A is inhabited. So we need a function which takes any inhabited type, and returns an element of that type. Although it is simple enough to do this on a computer  we need only find the "simplest" or "first" inhabitant of each type  there is no way to do this using standard lambdacalculus or combinator techniques. So we see that this result cannot be proved using these two techniques, and hence that the underlying logic is intuitionistic rather than classical.
Instead, consider a traditional error handling function which calls throw
when an error occurs, transferring computation to catch
. The throw
function cancels any return value from the original function, so it has type A > Void
, where A
is the type of its arguments. The catch
function then takes the throw
function as its argument, and, if the throw
triggers (i.e. returns a Void
) will return the argument of the throw
function. So the type of catch
is ((A > Void) > Void) > A
. ^{[4]}
Notes
 ↑ Another way of looking at this is that we're trying to define our logical operator → such that it captures our intuition of the "if… then" construct in natural language. So we want statements like for all naturals , " is even" → " is odd" to be true. I.e. that implication must hold when we substitute for any natural including, say, 5. But "5 is even" and "6 is odd" are both false, so we must have that False → False is true. Similarly by considering the statement for all naturals , " is prime" → " is not prime", we must have that False → True is true. And obviously True → True must be true, and True → False is false. So we have that unless is true and false.
 ↑ Technically, the types
Either Void A
andA
are isomorphic. Seeing as you can't have a value of typeVoid
, every value inEither Void A
must be aRight
tagged value, so the transformation just strips theRight
constructors.  ↑ Again, the technical statement is that
Void
is isomorphic to any type which is a nontheorem.  ↑ This argument is taken from Dan Piponi. "Adventures in Classical Land". The Monad Reader (6).