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.

## Top comments (4)

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

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

That's right. Nice work! So

modus ponensin logic corresponds tofunction applicationin programming. I'll try to follow up with some more interesting correspondences soon. Thanks for responding!Woohoo! Thanks, Brian. Looking forward to the next instalment. :)

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