Types as propositions, programs as proofs

This post is part of a series called functional fundamentals. See the introduction and index. That's also where you can request specific topics

Note that I am not an authoritative figure on these subjects, if you see something you think might be incorrect or incomplete, please point it out with a comment, let's prevent mistakes from spreading :-)

---

The Curry-Howard correspondence states that formulating a mathematical proof and writing a (typed, functional) program are basically the same thing. It isn't just an analogy, it's an isomorphism, meaning they act exactly the same.

Why does that matter? For programming, it means that if we can compile a program of type a, we have a proof that executing the program will result in a type a. There cannot be any errors or other result that isn't an a.

That is, provided you don't have any infinite recursion in your program, in which case the program will never terminate and you won't get your a.

Now, most of this we already got from typed lambda calculus, which is the foundation of functional programming. However, the Curry-Howard correspondence is a very useful frame of thought when dealing with slightly more advanced types.

To really understand its value, you will have to dive deeper into the subject. In this post specifically, I will explore the isomorphism between intuitionistic, propositional logic and simple types.

A crash course in logic

Do not worry if you don't get all this in the first go, it is a lot to process. University courses tend to spend one or two weeks on propositional logic. Take your time and read it over a few times. Replace symbols with their meaning if it helps you.

---

If you're familiar with classical logic: intuitionistic logic is mostly the same but does not assume ⊢ p ∨ ¬p and ¬¬p ⊢ p.

If you're not familiar with classical logic: don't worry, you were not supposed to understand any of that, the rest of this section is for you.

There are many 'types' of logic around. Each has its own set of rules. We will deal with intuitionistic logic, also called constructive logic. Like many other logic systems, it deals with truth; a proposition can be true or not true.

Essentially, it defines the basis for formulas about truth, much like addition, subtraction, division and multiplication define formulas about numbers.

Much like for numbers in arithmetics, truth values in logic have operators. Each takes truth-values and produces truth-values. Let's take a look at these operators. I'm going to denote true as ⊤ and false as ⊥.

Conjunction

A conjunction, denoted ∧, is like the AND operator in programming; it becomes true when both operands are true.

E.g. p ∧ q has the following truth table:

( As for how to interpret truth-tables: the first line in this truth table means that when p is false (⊥) and q is false (⊥), p ∧ q is also false (⊥). We can substitute other formulas for p and q )

Disjunction

A disjunction, denoted ∨, is like the OR operator in programming; it becomes true when either operand is true.

E.g p ∨ q has the following truth table:

Implication

An implication is denoted →. It means "if the first operand is true, then the second operand must also be true". Note that this "if" is NOT like conditionals in programming, which are more akin to "if and only if" and deal with control flow rather than truth. Implication, on the other hand, does not give a damn about what happens when the condition is false.

E.g. p → q can be read as "p implies q" and has the following truth table:

As you can see, "p implies q" is only false if p is true, but q is not.

An example: if I tell you "I will give you 10 bucks if you fetch me a beer", you have the right to call me a liar if you fetch me a beer but I do not give you 10 bucks. On the other hand, if you don't fetch me a beer but I still give you 10 bucks, you can't really say that I lied because I did not specify what would happen if you wouldn't fetch me a beer. (interesting fact: humans get a lot better at logic when you formulate it as a cheater-detection problem)

Proofs

So far we've learned the basic components of formulas. However, unlike numbers, there aren't many cases in which we need to compute the truth value of some formula. What's more interesting instead, is formulating proofs.

We say A ⊢ B (read: A proves B) to say that B can be proven from A (in whatever proof system we're using, intuitionistic logic in our case).

We can also say A ⊨ B (read: A entails B) to indicate that B must be true if A is true.

A proof system can be incorrect (a logician would say "not sound") or incomplete, so the two are different.

⊢ and ⊨ are operators in the meta-languages, which is a fancy way of saying that they tell something about formulas but are not a part of them. Pretty much in the same way that a for loop cannot be part of an expression (5 + for (...) {...} / 7).

We separate multiple formulas with commas: A ⊢ B, C means we can prove both B and C from A and A, B ⊢ C means we can prove C if we have both A and B.

Now, let's look at a few axioms (an axiom is something that is assumed to be correct):

p ⊢ p: anything is a proof of itself. Well, duhhhh.

p ∧ q ⊢ p: also no surprise, if a conjunction is true, either of its operands must also be true

p, p → q ⊢ q: again, pretty clear, if we know that p is true, and p implies q (p → q), q must also be true.

p → r, q → r ⊢ (p ∨ q) → r If we know that p implies r, and q implies r, so long as either p or q is true, r will be true as well.

We also have associativity and commutativity of conjunction and disjunction but you're likely familiar with those concepts, there's also some more axioms which I've left out because they're less relevant for functional programming.

Of course, we can drop whatever proposition we have proven if we no longer care for them, they're still true, we just don't write them down.

We can now prove e.g. a → (b → c), a, b ⊢ c:

Back to functional programming

From the last example, you may have started to get an inkling as to what on earth this has to do with functional programming. The operators you've seen for logic correspond to type operators in functional programming.

In Elm syntax (≅ is the operator for isomorphism):

A tuple or record is a conjunction
type alias Foo = (A, B)    ≅    Foo = A ∧ B

An enum type is a disjunction
type Foo = Left A | Right B    ≅    Foo = A ∨ B

A function an implication
type alias Foo = A -> B    ≅    Foo = A → B

So when you are writing a function with type String -> Int, you are writing a proof that you can get an Int (Int = ⊤) if you have a String (String = ⊤), or M ⊢ String → Int.
The premise (stuff before the ⊢) M consists of all the functions and variables that are native, imported or that you've written previously.
The compiler will check that your proof is correct (you have no compiler errors).

Take a moment to let that sink in.

Now, imagine that one of the formulas you used in the premise is incorrect, your proof becomes invalid! That's essentially the problem with side-effects. If we have some functions p -> q, that has some side-effect, i.e. it depends on some non-constant 'state' r that we don't know about, what it really corresponds to is a proof of p ∧ r → q (side note: r could be a property of p, but we haven't discussed that kind of logic yet so don't overthink it). Or, if the function throws an error in certain cases, you could say the function proves p → ( q ∨ Error ), just not p → q. The point is: the type signature of an imperative function does not constitute a proof. It's primarily an efficiency feature, not a correctness one.

Other stuff

This isn't all there is to the Curry-Howard correspondence, there are still more advanced type systems, corresponding to more advanced or just different logic. It is a topic of active research today, e.g. in trying to prove that a certain parallel implementation is correct. The main innovation of Rust is linear types, which are derived from linear logic.

I think, however, that this is more than enough information for a first post about the subject.

Further reading:

• implies vs entails vs provable
• I've briefly mentioned infinite recursion and in how that can screw up your proof. This is unavoidable given the halting problem. One possible solution for this problem is to drop Turing completeness and resort to total functional programming.