Direct, continuation, Böhm-Berarducci

Direct, continuation, Böhm-Berarducci

Direct

Take a programmer, ask him to write a function that doubles an integer.
It's highly likely that he will give you something similar to the following:

public static int Double(int x) => x * 2;
double :: Int -> Int
double x = x * 2

The solutions are trivial, but can we have a different answer? Something equivalent to the above? Something that can't be reduced to this expression? Something different in how it computes things? Yes, this code is an example of direct style programming, but we can write a similar program in a very unusual way.


Continuation

I have to admint that continuation passing is very strange when first looked at. Here is an implementation that is actually equivalent to the previous code:

public static R Double<R>(int x, Func<int, R> cont) 
    => cont(x * 2);
double :: Int -> (Int -> r) -> r
double x f = f (x * 2)

The function is saying:

Give me an integer and the rest of the program, I'll feed it with the doubled integer and give you the response.

Instead of having to call the function to get the result, we have to give the continuation of the program.

But hey, do we have a 1:1 correspondence between the two styles? I mean, can we transform any direct style function in its continutation passing form? Fortunately, yes, my blog post would be useless otherwise. It's a consequence of the Curry-Howard correspondence.


Böhm-Berarducci

The concept of continuation can be extended to data types with the Böhm-Berarducci encoding (the intuition can be extracted from the Church encoding). In fact, we can transform any data type into a bunch of functions. Pretty strange you may say. Let me show you.

Classic encoding

To start, we define a product type int * int, we usually call it class with two fields in C#:

public sealed class Product
{
    public readonly int X;
    public readonly int Y;
    public Product(int x, int y)
    {
        X = x;
        Y = y;
    }
}

public static int SumProduct(Product product)
    => product.X + product.Y;
    
// call site
var x = SumProduct(new Product(4, 5));
data Product = Product { x :: Int, y :: Int }

sumProduct :: Product -> Int
sumProduct product = x product + y product

-- call site
x = sumProduct (Product 4 5)

I hope that you start to see the difference between C# and Haskell here, the former being far more verbose than the latter (this will hopefully change in C# 8/9 as we will be able to inline classes).

Classic generic encoding

Let's step back for a second. We have a product of two int and a function that, given a product of int, computes the sum of the two parts. We can generalize this concept, having a product of different types A * B associated with an interesting higher order function:

public sealed class Product<A, B>
{
    public readonly A X;
    public readonly B Y;
    public Product(A x, B y)
    {
        X = x;
        Y = y;
    }
}

public static R FoldProduct<A, B, R>(Product<A, B> product,
                                     Func<A, B, R> f)
    => f(product.X, product.Y);
    
public static int SumProduct(Product<int, int> product)
    => FoldProduct<int, int, int>(product, (x, y) => x + y
    
// call site
var x = SumProduct(new Product(4, 5));
data Product a b = Product { x :: a, y :: b }

foldProduct :: Product a b -> (a -> b -> r) -> r
foldProduct product f = f (x product) (y product)

sumProduct :: Product Int Int -> Int
sumProduct product = foldProduct product (\x y -> x + y)

-- call site
x = sumProduct (Product 4 5)

FoldProduct is what we call folding/evaluation/elimination or even destruction of a structure. We are evaluating the whole structure (our product type here) to raise a result. It's the inverse of the structure construction (keyword new in C#).

Generic Böhm-Berarducci encoding

We can go further and transform the whole product into a single function:

public static Func<Func<A, B, R>, R> Product<A, B, R>(A x, B y)
    => f
    => f(x, y);
    
// call site
var result = Product<int, int, int>(5, 6)((x, y) => x + y);
type Product a b = forall r. (a -> b -> r) -> r

product :: a -> b -> Product a b
product x y f = f x y

-- call site
x = product 1 2 (+)

If we pay enough attention, we can notice a big difference between the C# code and its Haskell counterpart. Indeed, in Haskell, the Product type alias does not tell what r will be. In contrast, a and b are known at construction time. We want r to be instantiated later because we may have multiple continuations.

Imagine that you create a Product Int Int and want to fold it using a function that concatenates the two ints like: $$f : \mathbb{Z} \to \mathbb{Z} \to String$$ Imagine that you also want to compute the sum with: $$g : \mathbb{Z} \to \mathbb{Z} \to \mathbb{Z}$$ If we had to fix r while creating our Product Int Int, the continutations would be constrained to the same codomain (r constant after the object creation). This is the case in C#, look at the following:

public static Func<Func<A, B, R>, R> Product<A, B, R>(A x, B y)
    => f
    => f(x, y);
    
// call site
var prod = Product<int, int, int>(5, 6);

// impossible as R is already fixed to int
var str = prod((x, y) => x.ToString() + y.ToString()); // prod(f)

// type checking correctly
var sum = prod((x, y) => x + y); // prod(g);
type Product a b = forall r. (a -> b -> r) -> r

product :: a -> b -> Product a b
product x y f = f x y

-- call site
x = product 1 2 (+)
y = product 1 2 (\x y -> (show x) <> (show y))

While the Haskell code is perfectly right (some type annotations are required as the literals are ambiguous). We are stuck in C# because the generic type R has to be defined when constructing our object.

The limitation is related to something called higher-rank types (we need rank 2 types here but we only have rank 1 types in C#...). In Haskell, the type variable r can be instantiated after the product creation (when calling with our continuation). Yeah, Haskell is supporting arbitrary-rank polymorphism.

Here is an example of a C# implementation if we had rank 2 types:

public static Func<TYPE, Func<Func<A, B, TYPE>, TYPE>> 
    Product<A, B>(A x, B y)
        => TYPE
        => f // public TYPE f(A x, B y)
        => f(x, y);
        
// call site
var prod = Product<int, int>(1, 2);

// we would like to vary R depending on the context
var x = prod<int>((x, y) => x + y);
var y = prod<string>((x, y) => x.ToString() + y.ToString());

You get the idea, we ask for a type TYPE associated with a function f that should have the signature TYPE f(A x, B y). Kinda like giving a type as a classic parameter.

Final

Perhaps you want a more sophisticated example:

/*
    public sealed class Example
    {
        public int X;
        public int Y;
        public int Z;
        public Example(int x, int y, int z)
        {
            X = x;
            Y = y;
            Z = z;
        }
        public int Sum()
            => X + Y + Z;
        public int Prod()
            => X * Y * Z;
        public string ToString()
            => X.ToString();
    }
*/
public static Func<Func<A, B, C, Func<U>, 
                                 Func<V>, 
                                 Func<W>,
                        R>, R>
              Example<A, B, C, U, V, W, R>(A x,
                                           B y, 
                                           C z,
                                           Func<A, B, C, U> sum,
                                           Func<A, B, C, V> prod,
                                           Func<A, B, C, W> toString)
    => f
    => f(x, y, z, 
         () => sum(x, y, z), 
         () => prod(x, y, z), 
         () => toString(x, y, z));
         
// call site
var example = Example<int, int, int, int, int, string, int>(
                1,
                2,
                3,
                (x, y, z) => x + y + z,
                (x, y, z) => x * y * z,
                (x, y, z) => x.ToString());
                
var result = example((x, y, z, sum, prod, toString) => sum());

Voilà! We will dig more into algebraic data types next time. If you want something more theoretical about the subject, you should read Oleg's fantastic article.

Thanks for reading.


http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html
https://en.wikipedia.org/wiki/Church_encoding
https://en.wikipedia.org/wiki/Continuation-passing_style
http://oleg.fi/gists/posts/2019-06-26-linear-church-encodings.html

Show Comments