Last time, we investigated double negation in the Curry-Howard correspondence. We found that we can create a Not<Not<A>> from an A, but we can't create an A from a Not<Not<A>>, because constructive logic doesn't support the law of excluded middle. This means that the two types are not equivalent, which led us to wonder if there's any use for Not<Not<A>> at all. We ended by creating an instance of Not<Not<int>> from the number 5 as a sort of experiment:

Not<Not<int>> proof_of_not_not_int = CreateDoubleNegative(5);

Multiplication, the easy way

First, let's take a quick detour to write a simple C# program that triples a number:

int triple(int n)
{
    var product = n * 3;
    return product;
}

var result = triple(5);
Console.WriteLine($"Result is {result}");

// output:
// Result is 15

The triple function takes an integer (5), triples it, and then returns the resulting product (15), which we then write to the console. This is very basic C#. So here's a question: If we can triple an int, can we also triple a Not<Not<int>>?

Multiplication, the hard way

Remember that Not<A> is just a wrapper around a function of type A → ⊥, which means that Not<Not<A>> is a wrapper around a function of type (A → ⊥) → ⊥. So Not<Not<int>> is essentially a function that takes an int → ⊥ as input and returns an (impossible) ⊥.¹

To call such a function, we need an instance of int → ⊥, which is itself a function that takes an int and returns a ⊥. For example:

Absurd triple_cheat(int n)
{
    var product = n * 3;
    Console.WriteLine($"Product is {product}");
    throw new Exception("Can't ever return");
}

Now, let me be very clear: We've cheated. This function takes an int as input, triples it, and then sends the product on to another function (Console.WriteLine). But it doesn't actually return an Absurd because, by definition, there are no instances of Absurd. Instead, the function blows up with an exception at the end, which is obviously not a reasonable thing to do. But bear with me.

If we overlook this minor issue, we can now invoke proof_of_not_not_int using triple_cheat:

var absurd = proof_of_not_not_int.Apply(new Not<int>(triple_cheat));

// output:
// Product is 15
//
// Unhandled Exception: System.Exception: Can't ever return
// ...

Of course, this doesn't finish successfully, so no value is ever assigned to absurd. But, lo and behold, before it throws an exception, this successfully triples 5 and prints the result, just like the simple C# program.

Continuation passing style

When we passed 5 to CreateDoubleNegative, it came back to us wrapped inside a function of type Not<Not<int>>. Constructive logic doesn't allow us to convert that value back into a plain int, because we can't use the law of excluded middle, but we should remember that the integer really is in there - it's just stuck, waiting to be used somehow. To recognize this, let's call the function represented by Not<Not<A>> an "incomplete" function. To run an incomplete function, we need to send it a "continuation" function that accepts the stuck A instance and does something with it. Strangely, the continuation can do whatever it wants, but it can never legally return.

In this way, logical double negation corresponds to a legitimate programming paradigm called "continuation passing style" (CPS). In order to make CPS practical in C#, we need to make two changes:

• The continuation function should eventually finish (instead of claiming to return Absurd).
• The incomplete function should take the continuation function directly as an argument, so we don't need the Not type and its Apply method.

CPS is the basis for techniques such as async/await in C#. We don't have room to go into asynchronous programming in detail here, so I'll wrap up instead with a simpler example of real-world CPS using the Fibonacci sequence:

static void FibonacciCps(int n, Action<int> continuation)
{
    switch (n)
    {
        case 0: continuation(0); break;
        case 1: continuation(1); break;
        default:
            FibonacciCps(n - 1, fib1 =>
                FibonacciCps(n - 2, fib2 =>
                    continuation(fib1 + fib2)));
            break;
    }
}

static void Main(string[] args)
{
    for (var n = 0; n <= 10; ++n)
        FibonacciCps(n, fib => Console.WriteLine($"{n}: {fib}"));
}

// output:
// 0: 0
// 1: 1
// 2: 1
// 3: 2
// 4: 3
// 5: 5
// 6: 8
// 7: 13
// 8: 21
// 9: 34
// 10: 55

A typical Fibonacci implementation simply returns its result, but our FibonacciCps is an "incomplete" function that does not return a value. Instead, it sends its computed result to the given continuation function, which, in this example, eventually writes the result to the console. Multiple calls to FibonacciCps are chained together using nested continuations. These nested functions tend to pile up in when using CPS in practice, which is why syntactic sugar like async/await is often used to flatten the calls.

For once, the Curry-Howard correspondence has led us from a very abstract notion (logical double-negation) to a programming technique that is actually useful, albeit in modified form. I call that a victory! Thanks again for following along on the journey.

1. To be more precise, Not<A> is a wrapper around a function of type Func<A, Absurd>, which corresponds to the logical proposition A → ⊥. For clarity, I've skipped the Func signature and used logical notation to represent the type of the function instead. This is actually closer to the syntax used to represent function types in functional programming languages like F#. ↩