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:
English | Logic | Type |
---|---|---|
A and B | A ∧ B |
Tuple<A, B> |
A or B | A ∨ B |
Either<A, B> |
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
.1
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.2
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!
-
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 typeTuple<Func<A, B>, A>
. Either way, the arguments correspond to(A → B) ∧ A
logically. ↩ -
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'sMain
function. In that case, the logic of the C-H correspondence would match classical logic. But that's not as much fun. ↩
Top comments (8)
@shimmer I see you are transcribing logical relations into C#. If you're not already familiar, you might be interested in playing around with languages that embrace a logical and/or relational programming paradigm! 😄 checkout miniKanren or Prolog
I think the point of this is more towards proving what C# can do from a functional and logical perspective rather than establishing it as the best language for doing these things.
Oh yes, that was my take-away as well👍 It just made me think of some things I thought OP (and their readers) might be interested in 🙂
I also highly recommend Daniel P. Friedman's book The Little Prover 📚
This is a very interesting article. I'm not sure I fully buy that tuple is always and, but I see where you're going with it.
Thanks, glad you're enjoying it. I'm interested in your thoughts on tuples corresponding to logical "and". Can you describe what doesn't seem right about it?
When I think of a tuple, I think more of "a small record" than "two things that are true together". I can definitely squint to see it, but I almost wonder if a new
And
type would be clearer to match theEither
type.I see. It turns out that a custom
And
type would be a small record as well - exactly the same shape asTuple
but with different names (i.e. the two types are "isomorphic").Here's
Tuple<T1, T2>
from the .NET source code:And here's a custom
And
type:Usage: