Let's take a look at another interesting aspect of the Curry-Howard correspondence using C#.

"Either" type

First, there's something new we need to introduce: the Either<A, B> type. This is a class with a simple purpose: to hold an instance of either type A or type B. Either is actually very useful to have in your programming toolbox (see details here), but for now we're only interested in the role it plays in the C-H correspondence:

As you can see, Tuple represents logical "and" and our new Either type represents logical "or" (symbolized by ∨). For example, an instance of, say, Tuple<int, string> holds proof of both int and string, while an instance of Either<int, string> holds proof of int or string.¹

OK, now that we know about Either<A, B>, we're ready to put it to use.

Law of excluded middle

In classical logic, it's valid to assume that either A is true or ¬A is true:

A ∨ ¬A

This is called the law of excluded middle. In English, we can read this as "either A is true or A is false", for any proposition A, which seems intuitive enough. Even if we're not yet sure whether a given proposition is actually true or actually false, those are the only two possibilities, so we know one of them must be correct, right? We should be able to convert this law to types using C-H. Let's try:

/// A ∨ ¬A
public static Either<A, Not<A>> ExcludedMiddle<A>()
{
    // implementation?
}

We've represented the law of excluded middle itself as the concrete type Either<A, Not<A>>. If this law is true, we should be able to prove it by creating an instance of this type. Either has two constructors: one that takes an instance of A and another that takes an instance of Not<A>. But we don't yet have proof of A or Not<A> to work with, so how can we call one of Either's constructors?

The answer is: We can't. Which means that the kind of logic we can represent with types is actually not the same as classical logic. The logic of the C-H correspondence is called "constructive" or "intuitionistic". Constructive logic is a more limited, skeptical form of logic than classical logic. Without solid proof of either A or Not<A>, we can't make the leap to showing that one of them must be true.²

Double negation

In classical logic, it's easy to prove that two negations cancel out:

¬¬A → A

In English, if we know that A is not false, then it must be true (because it has to be one or the other). But this proof depends on the law of excluded middle! In constructive logic, we can't prove A merely by knowing that it is not false:

/// ¬¬A → A
A RemoveDoubleNegative<A>(Not<Not<A>> proof_of_not_not_A)
{
    // can't be implemented
}

OK, so if we can't remove a double negative, can we create a double negative? Logically, the proposition is:

A → ¬¬A

Yes, we can prove this constructively:

/// A → ¬¬A
public static Not<Not<A>> CreateDoubleNegative<A>(A proof_of_A)
{
    Absurd not_A_implies_absurd(Not<A> not_A)
        => not_A.Apply(proof_of_A);
    return new Not<Not<A>>(not_A_implies_absurd);
}

It looks complicated, but it just says that if we know A is true, then we know that "not A" is false, so "not (not A)" is true.

Of course, because of the C-H correspondence, this is not just a proof of A → ¬¬A, but also a valid, usable C# function. What happens if we actually use it in a C# program? For example:

Not<Not<int>> proof_of_not_not_int = CreateDoubleNegative(5);

Well, that's interesting. We've created an instance of Not<Not<int>> from the integer 5. What can we do with such a value?

I'll pause here for now and let you ponder that question before we take it up again in the next installment. Thanks for following!

1. You can think of the arguments to a function as being a tuple. We've been using this to avoid explicit tuples when representing logical "and" so far. For example, the arguments to ModusPonens are (A_implies_B, proof_of_A), which you can look at as two separate arguments, or as a single argument of type Tuple<Func<A, B>, A>. Either way, the arguments correspond to (A → B) ∧ A logically. ↩

2. Of course, we could just take the law of excluded middle as an axiom, as though an instance of Either<A, Not<A>> is passed to us via the program's Main function. In that case, the logic of the C-H correspondence would match classical logic. But that's not as much fun. ↩