The Curry-Howard Correspondence in C#
Tags: csharp, dotnet, functional, logic
Published: 2019-12-31 05:13:13

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](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence?oldformat=true). 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:

```csharp
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:

```csharp
// 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:

```csharp
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#:

```csharp
/// ((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.