Continuation passing style in C#
Tags: csharp, dotnet, logic, functional
Published: 2020-01-28 03:02:13

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:

```csharp
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:

```csharp
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) `⊥`.[^1]

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:

```csharp
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`:

```csharp
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:

```csharp
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#.