The Curry-Howard Correspondence in C#

It sounds crazy, but every time you instantiate a type in C#, you are proving a logical proposition. This fact is called the Curry-Howard correspondence. It won't be of any practical use in your C# coding, but it's fun and leads to deep ideas in functional programming.

The basic idea is that every type is a logical proposition, and every value is a proof. If you can instantiate a type, you've proved that type's proposition. You don't even have to run any code - if it compiles, it's a proof! We're leveraging the compiler's type checker to create an ad hoc theorem prover. Most such proofs are pretty boring, however. For example, 42 is proof that an integer exists:

int proof_of_int = 42;

That's certainly not very exciting, but the correspondence goes much deeper and will probably surprise you. All our examples will be in C#, so let's dive in!

Logical implication

The first thing interesting correspondence is between logical implication and function types. Logical implication looks like this:

A → B

This means that A and B are logical propositions and that A implies B. This implication might be true or false - we need proof! If I give you a proof that proposition A is true, can you prove that proposition B is also true, for all B? The answer is of course not - it would mean that any proposition implies any other proposition, which we know isn't true.

How do we represent logical implication as a function type in C#? We're going to use a generic function type, like this:

// A implies B
Func<A, B>

This defines the "signature" of a generic function that takes an instance of type A as input and returns an instance of type B as output. So, is it possible to implement a function of generic type Func<A, B>? It would have to look something like this:

B Implication<A, B>(A a)
{
    // implementable?
}

If you can write the body of this function so that it compiles successfully, you've proved that A -> B for all A and B. Note that your code can't use any tricks - it must be type-safe (i.e. no casts) and not rely on runtime mechanisms (e.g. reflection). Can you do it? Take a few minutes to think about it.

The answer is that of course you can't implement this function. If you could, it would mean that there is a way to convert an instance of any type A into an instance of any other type B, which we know isn't possible in general. Just like we can't convert a proof of any logical proposition A into a proof of any other logical proposition B. That's the Curry-Howard correspondence at work.

Modus ponens

But can we use this correspondence to actually prove something useful? Yes, indeed. Let's start with a famous rule of logic called modus ponens:

((A → B) ∧ A) → B

∧ is just the logical symbol for "and", so modus ponens says: If we know that A implies B, and we know A is true, then we also know that B is true. Hopefully, that sounds pretty logical. Is there a general proof of this proposition for all A and B? Yes, there is. Let's see if we can prove it in C#:

/// ((A → B) ∧ A) → B
B ModusPonens<A, B>(
    Func<A, B> A_implies_B,
    A proof_of_A)
{
    // implementation?
}

The signature of this function says: Given a proof that A implies B, and a proof that A is true, we can create a proof that B is true. Can you provide the body of this function? If so, please chime in with a comment! I'll pause here for a while to see if anyone gets it, and then explore other aspects of the correspondence in a future post.

Comments

[seankearon]

I'd say it's going to be this:

B ModusPonens<A, B>(Func<A, B> A_implies_B, A proof_of_A)
{
    A_implies_B(proof_of_A);
}

In the meantime, I'll eagerly await your next article! :)

[Brian Berns]

That's right. Nice work! So modus ponens in logic corresponds to function application in programming. I'll try to follow up with some more interesting correspondences soon. Thanks for responding!

[seankearon]

Woohoo! Thanks, Brian. Looking forward to the next instalment. :)

[Brian Berns]

Part 2 is up here. Thanks for the encouragement to get it done!