The Curry-Howard Correspondence in C#: Part 2
Tags: csharp, dotnet, functional, logic
Published: 2020-01-10 07:44:48

This is a follow-up to [my first article on the Curry-Howard correspondence](https://dev.to/shimmer/the-curry-howard-correspondence-3obh). As before, all examples will be in C#, so if you're a .NET programmer, take a shot at the challenges!

# Modus Ponens and Syllogism

Shout-out to [Sean Kearon](https://dev.to/seankearon) for his correct answer that modus ponens corresponds to function application. If we have a `proof_of_A` of type `A` and a proof that `A` implies `B` of type `Func<A, B>`, then we can prove `B` by applying the function:

```csharp
B proof_of_B = A_implies_B(proof_of_A);
```
For a slightly more difficult exercise, try proving that *syllogism* is a valid logical argument and then name the programming pattern that it corresponds to:

```csharp
// (A → B) ∧ (B → C) → (A → C)
//
// Example:
// If I do not wake up (A), then I cannot go to work (B).
// If I cannot go to work (B), then I will not get paid (C).
// Therefore, if I do not wake up (A), then I will not get paid (C).
Func<A, C> Syllogism<A, B, C>(
    Func<A, B> A_implies_B,
    Func<B, C> B_implies_C)
{
   // implementation?
}
```

# Negation

Let's move on to something even more mind-bending. In logic, `¬` is the symbol for negation, so `¬A` is the logical negation of `A` (usually read as "not `A`"). We define `¬A` to mean that if we had a proof of `A` then we could prove the impossible:

```
¬A = A → ⊥
```

Where `⊥` is the symbol (usually called "absurd" or "bottom") for a false proposition. In the Curry-Howard correspondence, a type that can't be instantiated represents a false proposition. Can we define such a type in C#? Surprisingly enough, we can:

```csharp
enum Absurd
{
}
```

Yes, this is legal C#! `Absurd` is a type that compiles with no problem, but can never be instantiated (again without using tricks that circumvent the compiler's type checker). Can we actually do anything interesting with such a type?

We know that logical implication (`→`) corresponds to function types in Curry-Howard, so `A → ⊥` corresponds to a function that takes an `A` as input and returns an (impossible) instance of `⊥` as output:

```csharp
/// A → ⊥
Func<A, Absurd> A_implies_absurd;
```

If we can instantiate such a function, then we know for certain that type `A` **cannot** be instantiated (i.e. it corresponds to a false proposition), because if we somehow acquired an actual instance of `A`, we could immediately instantiate `Absurd`, which we know is not possible.

Let's use that knowledge to define a C# type that corresponds to negation:

```csharp
/// ¬A
class Not<A>
{
    public Not(Func<A, Absurd> A_implies_absurd)
    {
        _func = A_implies_absurd;
    }

    public Absurd Apply(A proof_of_A)
        => _func(proof_of_A);

    private readonly Func<A, Absurd> _func;
}
```

`Not` is a generic type that asserts the negation of a type, `A`. We can create an instance of `Not` by supplying the constructor with a proof that `A → ⊥`. We also provide a method called `Apply` that we can use if we were ever to obtain an (impossible) proof of `A`. Look at `Apply` closely: it's a perfectly valid C# function that can never be executed. I bet you've never seen one of those before! 

# Modus tollens

In logic, *modus tollens* states that if we know that `A` implies `B` and we know that `B` is false, then we can conclude that `A` is also false. That makes sense, because if `A` were somehow true, then we could prove that `B` is also true, which would be a contradiction.

Can you use the Curry-Howard correspondence and our amazing `Not` class to prove that modus tollens is true? I'll give you the function signature:

```csharp
/// (A → B) ∧ ¬B → ¬A
Not<A> ModusTollens<A, B>(
    Func<A, B> A_implies_B,
    Not<B> not_B)
{
    // implementation?
}
```

If you've followed the previous examples, you should be able to solve this one as well. Give it a try in the comments!