This is a follow-up to my first article on the Curry-Howard correspondence. 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 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:

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:

// (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:

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:

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

/// ¬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:

/// (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!