The Curry-Howard Correspondence in C#: Part 2

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!

Comments

[John Kazer]

What's the relationship of this concept to Prolog? It's been too long since I used the language but it seems to be conceptually related...
This example Prolog repl seems an nice way to play with the idea. For example, given the propositions

loves(vincent, mia).
loves(marcellus, mia).
loves(pumpkin, honey_bunny).
loves(honey_bunny, pumpkin).

jealous(X, Y) :-
    loves(X, Z),
    loves(Y, Z).

type

loves(X, mia).

in the query terminal and hit 'run'!

[Brian Berns]

Good question. Prolog is a very cool language, but is based on different logical principles. The Curry-Howard correspondence actually leads to theorem-proving languages like Coq, Agda, Idris, and F* that support "dependent types". I might try to blog a little about this in the future.

In the meantime, here's a good Stack Overflow question that goes into the differences between Prolog and C-H correspondence in more detail.

[seankearon]

Thanks, Brian. As a developer, it is quite a shift in thinking to see a value or an instance as proof. But, when you think about it some more you start to wonder "what can be more proof than existence?"!

Those were quite a bit more challenging than the last one. So as not to add spoilers to your article, I've put my efforts here:

gist.github.com/seankearon/dbbd257...

You hinted in your response to John Kazer about theorem proving languages. It would definitely be interesting to see some examples of how this can be used in practice.

[Brian Berns]

Excellent! Your answers are right, and you even correctly named the programming technique that corresponds to syllogism. Thanks again for participating.

when you think about it some more you start to wonder "what can be more proof than existence?"

This is a great point, and leads into one of the key differences between the logic of the C-H correspondence (called constructive or intuitionistic logic) vs. classical logic. Here's something to think about: In classical logic, we accept that either A or ¬A must be true (law of excluded middle). There's no way to prove that using types, so the C-H correspondence just rejects it! Constructive logic is a more limited, skeptical form of logic than classical logic.

I'd love to write about theorem provers and dependent types at some point, but honestly a lot of it is still over my head. :) I might have to build up to it. In the meantime, if you find this topic interesting, I encourage you to:

• Look into functional programming languages (such as F#), where the C-H correspondence is much easier to see. I had fun writing these examples in C#, but the core ideas really belong to the functional programming world.

• Think about what Tuple<A, B> corresponds to in logic. Then take a look at the Either<A, B> type (link) and think about what it corresponds to.

• Bonus: There's actually a totally different correspondence between types and algebraic operations (e.g. addition, multiplication, exponentiation) that will blow your mind yet again, called algebraic data types. I might try to whip up an article or two on that concept as well.

[seankearon]

Thanks, Brian. That was a really interesting challenge, both for the code and also to make me think differently about the meaning of the code.

I've never come across constructive logic before. It feels more natural, more "real world" than the usual binary logic. It also feels close to the statement "the world is all that is the case" in the sense that if we cannot construct it (that is, instantiate it) then in it should not be discussed! All that leading to recognising that statements like "if a tree falls in a forest, does it make a sound?" are not actually real questions.

Having a maths (translation: math! :) ) background, I'm interested in correspondences between maths and programming. So, being also interested in FP I end up reading about Category Theory quite often. There is some work going on (totally inaccessible for all but the best mathematical minds, which is a very, very long way from me!) that is looking at making a change to something that is fundamental in maths - equality. The redefinition of logic you mention seems to be a similar fundamental shift in thinking.

Thanks also for the pointers and links. I'll follow those up. Apart from the F# link, that is, as I am happy to say that I spend half of my time writing F# :) (which is how I came across your articles).

I'll look forward to reading some more from you in the future! :)

[Brian Berns]

Category theory is a fascinating topic. Will read the article. Thanks.

If you find constructive logic interesting, you might also want to look into type theory, which uses constructive logic to replace set theory as the foundation for all math(s).