Suppose you have a function from `Int` to `Char` and an `Int` and you need a `Char`. How can you get one? In other words, how would you implement the function

Easy, just apply the function to the argument:

Okay, now suppose you have a function from `Int` to `Char` and a function from `Char` to `String` and an `Int`. How can you get a `String`? In other words, how can you implement

Easy again, just compose the calls to the functions:

Finally, suppose you have a function from `Int` to `Char` to `String` and a function from `Int` to `Char` and an `Int`. Again, how can you get a `String`? In other words, how can you implement

This one is left for the reader.

You might notice that these functions seem to have an algebraic character, and don’t have anything to do with `Int`, `Char`, or `String` in particular. That’s true, and so the signatures can be rewritten generically (the implementations can be left alone):

At this point you might look at these signatures and notice that they bear a striking similarity to certain theorems of propositional logic, namely modus ponens, hypothetical syllogism, and Frege’s theorem, respectively. If you thought this, then congratulations, you’ve just discovered the first part of the Curry-Howard correspondence. The “correspondence” is the deep isomorphism between types and programs, on the one hand, and propositions and proofs on the other. The first part of the correspondence has to do with propositional logic and was discovered by Curry in the 1930s. The second part has to do with quantificational logic, and was discovered by Howard several decades later. (We’ll ignore the second part for now.)

Here’s a theorem for joining inferences:

We can also prove double negation introduction (where `p -> Void`1 stands in for p → ⊥, which is equivalent to ¬p)2:

What about double negation elimination (DNE)?

Not so fast! It turns out that the type systems used by languages like Idris and Haskell don’t correspond to classical logic, but rather to intuitionistic logic3. Intuitionistic logic is like classical logic except that it doesn’t validate the principle of the excluded middle (PEM): p ∨ ¬p. That is, it’s not the case that for any proposition, either that proposition or its negation holds, and a double negative is not proof positive.

To see why someone might reject PEM, consider the following classic argument.

Claim There are irrational numbers a and b such that ab is rational.

Proof The number √2(√2) is either rational or it isn’t. If it is, let a = b = √2 and we’re done. Otherwise, let a = √2(√2) and let b = √2. Then ab = (√2(√2))(√2) = √2(√2 * √2) = √22 = √2 * √2 = 2. Tada!

There’s something off about this proof. It says that numbers with some property exist, but it doesn’t give witnesses; without witnesses, the knowledge feels hollow. The critical point in the proof is this line: The number √2(√2) is either rational or it isn’t. But this is an instance of PEM! So you might forbid reasoning with PEM in order to preclude proofs like this one.4

Anyway, our type system can’t prove PEM, or DNE, or any of a variety of other equivalent statements, like Peirce’s law or the or the consensus theorem:

On the other hand, it is possible to prove the double negation of any of them, or indeed of any classically valid proposition.5 Here, for instance, is the proof of the double negation of Peirce’s law:

It’s also possible to prove any of those statements given (an instance of) another. For instance, here’s a proof DNE implies PEM (taking PEM itself for p in DNE):

# Exercises

1. Prove the double negations of PEM, DNE, and the consensus theorem.
2. Prove that PEM, DNE, Peirce’s law, and the consensus theorem are equivalent. DNE -> PEM is already done, so there are eleven more implications to prove. Or you could prove them in a circle if that’s too much work.
3. Prove contraposition (`contraposition : (p -> q) -> (q -> Void) -> p -> Void`). Can you prove its converse?
4. Prove the double negation of `(a -> c) -> (b -> c) -> ((a -> b) -> b) -> c`.

# Discussion Questions

1. To what extent should nonconstructive reasoning be accepted?
2. Does any of this types-as-propositions stuff have any bearing on writing real programs in the real world? Does it have any bearing on proving new theorems?

1 In Idris, `Void` is a type with no constructors. It therefore has no instances, and is said to “uninhabited”.