A Gentle Introduction to Curry-Howard Isomorphism

N.B. This article is best suited for programmers with a basic understanding of at least one pure functional programming language such as Haskell. Idris knowledge (the main programming language used in this article) is not required; if you can read Haskell or a similar language, you should be able to pick up Idris as you read the code examples.

Once upon a time, mathematicians had to prove mathematical theorems by hand. A mathematician would spend days, months or even years writing pages among pages of arguments just to complete a single proof. The proof would then be reviewed by fellow, renowned mathematicians before being accepted by the community. Often times, it would take years for a trained mathematician to spot a logical fallacy in a seemingly correct proof which would undermine the entire proof.

That was until mathematicians / computer scientists in the mid-20th century discovered the Curry-Howard correspondence, sometimes referred to as "Curry-Howard isomorphism". It essentially states that types in a programming language can be seen as mathematical theorems and programs of a certain type can be seen as proofs for the theorem represented by said type. Since then, certain major theorems have been successfully proven using computerized proof assistants, one of the (possibly) most famous proofs being the proof of the Four-Color Theorem. While some mathematicians have raised concerns that the proof assistant(s) being used may be buggy resulting in a compromised proof, others have noted that a proof assistant is no less trustworthy than a human mathematician who may also be prone to human errors.

How is that so, you may ask? Consider a simple program that does not type-check in the traditional Java programming language:

// Wrong.java

public class Wrong {
  public static void main(String[] args) {
    System.out.print("Hello!\n" * 10);
  }
}

And consider another simple program that does type-check in Java:

// Right.java

public class Right {
  public static void main(String[] args) {
    for (int i = 0; i < 10; ++i)
      System.out.println("Hello!");
  }
}

The first program does not type-check because it doesn't make sense to multiply a string by an integer (though it would probably make sense in Python/Ruby and duplicate the string "Hello!\n" 10 times). The second program type-checks because it makes sense - no attempt is made to subtract a string from another string, for example. In a sense, when the Java compiler is type-checking your program, it is proving certain theorems about your program, namely that your program isn't completely nonsensical. But to witness the true power of Curry-Howard correspondence, we will need a much stronger type system than that in Java.

Enter Idris! Idris is a functional programming language which is somewhat similar to Haskell except its type system is even richer. More importantly, it has dependent types which means that types are first-class and can depend on values. This allows us to lift values into the type-level, enabling us to prove theorems about them. But before we begin, let us review the axiom of mathematical induction.

Suppose we have a ladder of infinite height, starting from the ground and reaching up into the sky. The distance between consecutive steps of the ladder is constant - for example, the distance between the 4th and 5th steps is identical to that between the 10th and 11th steps. Then, how do we know that we can reach any given step on the ladder? It suffices to know that we can reach the first step of the ladder, and given that we can reach a certain step k of the ladder, we can always reach the next step k + 1 of the ladder no matter what. And that is proof by induction in a nutshell - if a statement is true for some initial value v (our basis) and if we can show that it is true for some k + 1 th value given that it is true for some k th value (our inductive step) then the statement must hold for all values >= v.

Now, for the interesting topic - suppose we have two counting numbers (e.g. 1, 2, 3) n and m and we add them together. Does it matter which order they are added and why? Intuitively, the order shouldn't matter - for example 3 + 5 = 5 + 3 = 8 and 2 + 3 = 3 + 2 = 5. But how do we know for sure that we can add two arbitrary counting numbers in any order and still get the same result? Perhaps you might say that it's blindingly obvious; however, a mathematician would refuse to accept such a flimsy argument. So how do we settle the score for n + m = m + n once and for all?

In the late nineteenth century, a mathematician called Giuseppe Peano formulated an encoding of the natural numbers (the counting numbers, including zero) as follows:

1. 0 is a natural number
2. For every natural number n, its successor S n is also a natural number
3. There are no other natural numbers (implied)

These are known today as the Peano axioms. While they may seem strange and unnecessary at first sight, their simple structure actually makes it easy for mathematicians to reason about their properties.

To gain an intuition of how the notation above represents the natural numbers, consider the following:

• 1 is the next natural number after 0. So in Peano axioms we would write it as 1 = S 0.
• 2 is the next natural number after 1. So 2 = S 1 = S (S 0).
• Similarly, 3 = S 2 = S (S 1) = S (S (S 0)) and so on.

Intuitively, the successor S n of any natural number n can be thought of as "the next natural number after n". You may be wondering why I didn't call the successor S n as simply 1 + n. That's because we haven't defined addition on the natural numbers yet which we will now do:

1. 0 + m = m
2. S n + m = S (n + m) (the LHS should be read as (S n) + m)

So what does it all mean? The first rule 0 + m = m should be rather intuitive - of course zero added to any number is equal to itself! The second rule might not be so obvious, but read it this way, "Suppose we know the result of n + m. Then the sum of the next number after n and the other number m is simply the next number after n + m." How do we know that this describes addition precisely? We can notice that it covers all cases - m is assumed to be an arbitrary natural number and the natural number on the left hand side cannot be anything other than zero or the successor of an arbitrary natural number! Here is an example of evaluating 2 + 3 using the Peano definition of addition to assure you that the definition is correct:

  2 + 3
= S (S 0) + S (S (S 0))
= S (S 0 + S (S (S 0)))
= S (S (0 + S (S (S 0))))
= S (S (S (S (S 0))))
= 5

In Idris, the Peano formulation of the natural numbers is defined in the standard prelude which is implicitly imported in every Idris file. The Peano definition of addition as highlighted above is also defined there. The keyword total in the declaration total plus : (n, m : Nat) -> Nat simply means that Peano addition covers all possible values of n and m and always produces a result (which we would intuitively expect for addition of two arbitrary counting numbers).

Notice in our definition for addition that nowhere did we state n + 0 = n for all n. But intuitively it has to be true! That is because we do not need to state it explicitly - instead, we can deduce (prove) n + 0 = n from the definition of addition given above. But how? This is where induction comes in handy. We will do it on paper first and then see how it can be translated into Idris.

To prove n + 0 = n by mathematical induction, we first need to identify a variable that we can induct on. n is the only such variable here so we will induct on n. Our basis will be n = 0:

When n = 0,
    n + 0
  = 0 + 0
  = 0 (by definition of Peano addition)
  = n

So the basis is trivially true. Notice how the expression 0 + 0 automatically reduced to 0 following the rule 0 + m = m for all m in the definition of addition. So we get 0 = 0 which is obviously true - obviously anything must be equal to itself! In mathematical terms we call this rule, namely x = x for any x, reflexivity (of equality).

Now that we have set foot on the first step on our conceptual ladder, it is time to prove that we can always reach the next step. Suppose n + 0 = n is true for some natural number n (this is called our inductive hypothesis - something we assume to be true for performing mathematical induction). Then showing that the next case S n + 0 = S n follows suffices to prove that n + 0 = n for all natural numbers n:

  S n + 0
= S (n + 0) (by definition of Peano addition)
= S n       (by our inductive hypothesis n + 0 = n)

And we are done! It remains to translate this into Idris.

Before we begin, whip up a file Main.idr:

module Main

%default total

main : IO ()
main = do
  putStrLn "Hello World!"

If you know any Haskell, the syntax should look familiar to you. The only differences are:

1. There is no where following module Main
2. There is an extra statement %default total (explained below)
3. For the type declaration of main, we have a single colon instead of a double colon.

Differences (1) and (3) are trivial - the only one we should be interested in is (2). Recall that total means that a function covers all cases and always produces a result (in finite time). %default total simply means all functions in this module are assumed to be total by default. This is important for proofs as proofs should hold true for all the possible input values that is specified and the "finite time" restriction ensures we do not establish any circular arguments which prevent us from reaching a conclusion, e.g. n + 0 = n because n + 0 = n because ...

First of all, let us figure out the type for this theorem. What we've just proven is essentially the statement "For all natural numbers n, n + 0 = n". This can alternatively be read as "If we have a natural number n then n + 0 = n". So the type of our theorem (let's call it zeroRightId) would be:

zeroRightId : (n : Nat) -> n + 0 = n

Notice how the value n appears in the type signature of zeroRightId. This is possible due to dependent typing in Idris, that is, types can depend on values. In fact, types can be passed to functions, evaluated and returned from functions as well in Idris, i.e. they are first-class, but that will not be explored in this blog post.

Also notice how we defined the natural numbers as data Nat = Z | S n but our type signature has n + 0 = n instead of n + Z = n. In fact, Idris can recognize non-negative integer literals in some cases as natural numbers and sometimes even optimize their representation to aid in efficient computation (after all, evaluating Peano addition takes time proportional to the size of the leftmost natural number which is far from efficient). Another thing - Idris recognises n + m as plus n m when n and m are natural numbers.

Now for the basis. Remember how the base case 0 + 0 = 0 reduces to 0 = 0? As mentioned above, this is called reflexivity in mathematics. Idris also defines equality as follows:

data (=) : a -> b -> Type where
  Refl : x = x

The Refl data constructor in Idris represents reflexivity of equality in mathematics, i.e. that x = x for any x. As for what x is, it is inferred at compile-time depending on the context (and if such inference fails then it results in a type error).

So, for the basis where n = 0, the proof that n + 0 = n simply reduces to mere reflexivity:

zeroRightId Z = Refl

Here, the value of x is inferred to be Z and our equation type-checks. In this case we cannot replace Z with 0 - the Idris compiler on my end recognizes 0 as an Integer instead of Nat for some unknown reason. Anyway you can read Z as 0 and vice versa.

So now our code becomes:

module Main

%default total

zeroRightId : (n : Nat) -> n + 0 = n
zeroRightId Z = Refl

main : IO ()
main = do
  putStrLn "Hello World!"

Except when we compile it with idris Main.idr -o main it still fails with a compilation error. That is because we have not completed the inductive step of our proof - Idris complains in this case that our program (proof) zeroRightId is not total.

Recall our inductive step:

  S n + 0
= S (n + 0) (by definition of Peano addition)
= S n       (by our inductive hypothesis n + 0 = n)

The first equality S n + 0 = S (n + 0) is true by virtue of the definition of Peano addition. In Idris, equalities that hold true by definition can be deduced by the type-checker so we don't need to explicitly need to state them in Idris. What remains to be proven is the statement S (n + 0) = S n.

Let us first fill in the left-hand side of our inductive step in Idris. We want to prove that our statement n + 0 = n holds true for the next natural number in line S n so this would be:

zeroRightId (S n) = ?proof

?proof is called a typed hole in Idris - use this to fill in an equation when you haven't yet figured out what it should be.

For proving S (n + 0) = S n, we invoked our assumption (inductive hypothesis) that n + 0 = n to transform n + 0 into n within the complex term S (n + 0). The inductive hypothesis in Idris is simply zeroRightId n (exercise: convince yourself that its type is indeed n + 0 = n) so using it gives:

zeroRightId (S n) = zeroRightId n

Except that it doesn't type-check! Notice that the left-hand side of our equality has type S n + 0 = S n which is different from n + 0 = n - after all, they are entirely different statements! So how do we use our inductive hypothesis zeroRightId n within S (n + 0)? We can view the successor operation S as a function of some kind - it receives a natural number n as argument and returns a new result S n which is also a natural number. In Idris there is a lemma (lemma: a theorem used to prove another main theorem of interest) cong : a = b -> f a = f b which states that equality respects function application (source). Again, f is inferred from context - we can apply cong to n + 0 = n with f = S to transform zeroRightId n : n + 0 = n into cong (zeroRightId n) : S (n + 0) = S n. So our inductive step becomes:

zeroRightId (S n) = cong (zeroRightId n)

The full file currently looks like this:

module Main

%default total

zeroRightId : (n : Nat) -> n + 0 = n
zeroRightId Z = Refl
zeroRightId (S n) = cong (zeroRightId n)

main : IO ()
main = do
  putStrLn "Hello World!"

Compiling it again with idris Main.idr -o main confirms that it does indeed type-check. Running the executable main (e.g. by doing $ ./main on my Mac) prints Hello World! as expected. Congratulations, you have successfully proven your first theorem in Idris!

Here are exercises for you if you are interested:

1. Prove that n + S m = S (n + m) for any natural numbers n, m. A good way to go about it would be to first prove it on paper then translate it step-by-step into Idris.
2. Prove the commutative law of addition of natural numbers, namely n + m = m + n for all natural numbers n, m. Hint: the lemmas n + 0 = n and n + S m = S (n + m) you just proved will come in handy ;)

Note that the proofs above (including the first proof I walked you through) are all part of Idris's standard library but try not to peek at them until you have at least attempted to construct the proof.

Some further exercises if you are really interested:

1. Prove n * m = m * n for the natural numbers. You'll have to first define multiplication though ;)
2. Prove a * (b + c) = a * b + a * c for the natural numbers.
3. Prove (a + b) * c = a * c + b * c for the natural numbers. Note that this is a different statement from (2)!
4. List out some properties of exponentiation and try to prove them as well, translating them into Idris in the end. Again, you'll have to first define exponentiation and confirm that your definition matches with intuition.

In this blog post you have personally witnessed Curry-Howard Isomorphism by encoding a proper mathematical proof (albeit a rather simple one) in the programming language Idris. I hope you enjoyed it :D

Further reading:

1. Theorem Proving in Idris
2. A list of proper proof assistants - some even allow you to write proofs step by step (instead of in a single equation) like you would on paper!
3. The Coq Proof Assistant

Comments

[ztyree42]

Nice article, one point to note is that your parenthetical on the 3rd axiom listed for Peano arithmetic is incorrect, that there are no naturals not reachable from 0 via the successor function is not implied by the first two axioms.

[Anti]

Wow thanks! Question, for programs like "factorial", or"add", these are all proofs of nat -> nat. Are these at all useful? I would think inherent in the structure is proof of something, but I can't see what.

[Brian Berns]

I just posted an even gentler introduction to the Curry-Howard correspondence here. I think it's a fascinating topic.