Type-Free Lambda Calculus in C#, Pre-4.0 – Defining the Lambda Language Runtime (LLR)

Introduction

A while back, I blogged about (Mis)using C# 4.0 Dynamic – Type-Free Lambda Calculus, Church Numerals, and more which was a fun post and got some good feedback and solid reading numbers. So, let’s continue our journey of brain-exploding theoretical foundational posts with “The Revenge of the Type-Free Lambda Calculus, Now Compatible with C# 3.0”.
Last time around, we truly misused C# 4.0 dynamic to uni-type (not a spelling mistake) functions and values, and went bananas turning basic computation with numerals and Booleans into functions thanks to Church encodings. All in all a great unit test for the Dynamic Language Runtime that sweats under the pressure put on it by our crazy function calls:

//
// Church numerals.
// Basic idea: natural number n gets represented as \fx.f^n(x)
//
var N0 = new Func<dynamic, Func<dynamic, dynamic>>(f => x => x);
var succ = new Func<dynamic, Func<dynamic, Func<dynamic, dynamic>>>(n => f => x => f(n(f)(x)));

Func<dynamic, uint> toInt = x => x(new Func<dynamic, dynamic>(i => i + 1))(0u);
Func<uint, dynamic> fromInt = null;
fromInt = n =>
{
    return (n == 0 ? N0 : succ(fromInt(n - 1)));
};

var plus = new Func<dynamic, Func<dynamic, Func<dynamic, Func<dynamic, dynamic>>>>(m => n => f => x => m(f)(n(f)(x)));

The above allows us to write a simple iterative (ah, I’m cheating) Fibonacci function as follows:

var i = N0;
var prev = N0;
var curr = succ(N0);

while (true /* could have used a Church Boolean as well ;-) */)
{
    Console.WriteLine(toInt(curr));

    var t = curr;
    curr = plus(curr)(prev);
    prev = t;
}

If you don’t believe the above works, or you don’t get it how it does its magic, revisit my previous post on the topic, and check back after you’ve plowed through it.

Exceptions rule the world…

Today, we’ll take a step back and have a look at how we can do all of the above in the pre-.NET 4.0 era, where we don’t have the “convenient” dynamic type to escape from the typed reality. So, how can we make this work? A possible answer can be found in the use of unchecked exceptions, as we have them at our service in the .NET Framework. The underlying idea is to “smuggle out” data out of a function without having to declare it anywhere in the function’s signature (use of checked exceptions prevents this, as the “throws clause” would have to reveal what’s being thrown in a … statically typed manner, aye!).
This is one of the findings described in Mark Lillibridge’s paper entitled “Unchecked Exceptions can be Strictly More Powerful than Call/CC” on page 301, though much more mind-blowing stuff can be found in there (as the title reveals). Once I get into blogging about continuations, most likely in the context of Reactive LINQ (otherwise known as Reactive Framework or Reactive Fx), I may refer to this paper again to assist in blowing out people’s brains (just kidding). Talking about Reactive LINQ, I got the initial reference to this paper by Erik Meijer.
So, what’s the big idea? Let me try to summarize it. You’ll remember we need to define two operations to make the essentials of lambda calculus work: abstraction and application. We also know that both functions and values need to be represented in an equal manner, as functions are first-class: a function can take another function as its input or produce one as its output. So, it’s still clear we need to uni-type things just like we did before. So let’s spoil the beans now without much further ado: that single type we’ll be using today is nothing less than System.Action, as delegate defined as follows:

public delegate void Action();

In fundamentalist functional programming the above is the most useless type for a function: it takes nothing and produces nothing, hence all those guys can be compiled away, right? But as they’ll be our bread and butter for today’s installment, you can guess we’ll joyfully dance the tango of side-effects. One such great side-effect is called an exception.
Let’s take a step back first and summarize the dense info above: values and functions will be represented as System.Action objects. Right, in our lambda calculus “emulator” System.Action is the new System.Object. The careful reader will notice that System.Action plays a dual role here: on the outside we use it as the single type we’re dealing with both for values and functions. But on the inside, we'll leverage its delegate (a “CLR function object” if you will) characteristic somehow. Let’s go there now…
How can we realize abstraction? As we know from the previous time around, all functions of multiple arguments can be represented as functions of one argument through currying. So, to construct this simplest form of a function, all we need is a way for the user to define a function between two of our “first-class” objects (of type System.Action), which is something we can do as a Func<Action, Action> in C#. This allows the users to use the lambda arrow to write such a function. However, since a defined function (through abstraction) needs to be capable of being passed elsewhere as an argument, a Func<Action, Action> is too verbose: we need to morph it into a System.Action again. This is what our lambda abstraction operator will have to do:

static Action λ(Func<Action, Action> x)
{
    // But how???}

We’ll see in a moment how we can realize this function. But first, let’s have a look at the contract of a application operator we so badly need to have this come off the ground. Application takes two objects at a time: the first one will be a function, the second one a function or a value. It applies the function to the given argument. Objects are of type System.Action, and the result of the application call is an object too, hence the following signature:

static Action ß(Action x, Action y)
{
    // But how???}

Okay, let’s fill in the voids. How can we smuggle out a function between two Action objects into a single action, to realize abstraction? Well, what about carrying the function on the back of an exception object. We’ll define a useful generic Exception type for this purpose:

class Exception<T> : Exception
{
    public Exception(T data)
    {
        Data = data;
    }

    public new T Data { get; private set; }
}

This allows us to define the lambda function like this:

static Action λ(Func<Action, Action> x)
{
    return () => { throw new Exception<Func<Action, Action>>(x); };
}

In Lillibridge’s paper this is referred to as the “roll” operation. Think of this smuggling operation as rolling the function in a carpet of type Action: nobody will notice from the outside that it contains some dirty secrets. (Tip: don’t try this technique at airport security gates, they won’t allow exceptions.) But what does this mean? Well, from the outside the function can simply construct a proper lambda calculus function, surfaced as an Action object (making it deserve the status of “first-class”). How do we, the “lambda runtime”, get it out of there again? Simply invoke the resulting Action when needed, and catch the generic exception type. That’s precisely what the applicaiton function will have to do:

static Action ß(Action x, Action y)
{
    Func<Action, Action> xe;

    try
    {
        x();
        xe = _ => _;
    }
    catch (Exception<Func<Action, Action>> ex)
    {
        xe = ex.Data;
    }

    return xe(y);
}

This is referred to as the “unroll” operation. In order to apply the function “x” to argument “y”, we first need to evaluate x. We do so by calling the delegate, which (when properly constructed through the lambda operator) will throw an exception allowing us to unroll the underlying function type from our smuggling exception carpet. Then we can feed in the argument ”y” to the resulting Func<Action, Action> to get the result of the function call back. The remaining one-billion dollar question is how we’d ever end up executing the last statement in the try-block:

xe = _ => _;

This is simply an identity function (you could equally well have write z => z or so), which ultimately will cause the application to return its argument. We use this as a convenient mechanism to allow “regular” Action objects as participants in our application operation. At a later point, this will become clear.

Lambda Language Runtime for CLR 2.0 – summary

The “LLR” I’m illustrating here is a way to layer untyped computation on the statically typed foundation of the “CLR”. Contrast to the DLR’s complex infrastructure, we need nothing more than two methods:

static Action λ(Func<Action, Action> x)
{
    return () => { throw new Exception<Func<Action, Action>>(x); };
}

static Action ß(Action x, Action y)
{
    Func<Action, Action> xe;

    try
    {
        x();
        xe = _ => _;
    }
    catch (Exception<Func<Action, Action>> ex)
    {
        xe = ex.Data;
    }

    return xe(y);
}

Reality check: Church Booleans

In the previous post, I’ve explained what Church Booleans are, so I won’t do it again now. Instead, let’s try to redefine those in terms of our lambda and beta operations:

//
// Church Booleans
//
var T = λ(a => λ(b => a)); // \ab.a
var F = λ(a => λ(b => b)); // \ab.b

var Not = λ(m => λ(a => λ(b => ß(ß(m, b), a)))); // \m.\ab.mba
var And = λ(m => λ(n => ß(ß(m, n), m))); // \mn.mnm
var Or = λ(m => λ(n => ß(ß(m, m), n))); // \mn.mmn
var Xor = λ(m => λ(n => λ(a => λ(b => ß(ß(m, ß(ß(n, b), a)), ß(ß(n, a), b)))))); // \mn.\ab.m(nba)(nab)

This should do the trick, shouldn’t it? How to calculate, say, T && F? Here it is:

ß(ß(And, T), F)

Quite easy, but with a bit of beta function noise. To prove all of this works, we’ll have to provide pretty-printing functions. Similarly we may benefit from a function that promotes a CLR Boolean into the corresponding Church Boolean:

Func<Action, bool> toBool = b =>
{
    bool res = false;
    ß(ß(b, () => { res = true; }), () => { res = false; })();
    return res;
};
Func<bool, Action> fromBool = b => b ? T : F;

Those are very comparable to the ones we used in the previous post, using C# 4.0 dynamic. Notice how an impure lambda expression is used as an argument to the beta-application in order to realize toBool.
Based on all of this we’d like to be able to write a testing function that can print results of applying our Boolean operators to various arguments. Again we base this off the functions used in the previous post:

static void Unary<T, PArg, PRes>(string name, Func<Action, T> f, Func<Action, PArg> printArg, Func<T, PRes> printRes, params Action[] values)
{
    foreach (var value in values)
        Console.WriteLine("{0}({1}) = {2}", name, printArg(value), printRes(f(value)));
}

static void Binary<T, PArg, PRes>(string name, Func<Action, Action, T> f, Func<Action, PArg> printArg, Func<T, PRes> printRes, params Action[] values)
{
    foreach (var valueL in values)
        foreach (var valueR in values)
            Console.WriteLine("{0}({1}, {2}) = {3}", name, printArg(valueL), printArg(valueR), printRes(f(valueL, valueR)));
}

For example, Unary could be used with the “Not” operator, using toBool for print-functions which turn the Church Boolean into the corresponding System.Boolean that Console.WriteLine can deal with. Notice one thing though: the above is not pure either, in a sense we’re not passing in plain Action objects for the function “f”, instead we’re using Func<Action, …> types. None of our lambda functions like “Not” and “And” are compatible with this form. How do we do this (purely a cosmetic thing, btw)?

//
// Conversion operations
//
Func<Action, Func<Action, Action>> toFunc1 = f => x => ß(f, x);
Func<Action, Func<Action, Action, Action>> toFunc2 = f => (x, y) => ß(ß(f, x), y);
Func<Action, Func<Action, Action, Action, Action>> toFunc3 = f => (x, y, z) => ß(ß(ß(f, x), y), z);
Func<Func<Action, Action>, Action> fromFunc1 = f => λ(x => f(x));
Func<Func<Action, Action, Action>, Action> fromFunc2 = f => λ(x => λ(y => f(x, y)));
Func<Func<Action, Action, Action, Action>, Action> fromFunc3 = f => λ(x => λ(y => λ(z => f(x, y, z))));

The conversion operators above provide the answer: they allow us to make plain lambda functions callable as if they were CLR functions (Func<…>) and also allow for abstraction based on a CLR functions. In fact, the family of toFunc functions could be called “decurry” (e.g. toFunc3 produces a function of three arguments) while the fromFunc functions are “curry” operators (e.g. fromFunc3 takes a function of three arguments). Based on this we can write “C#-user friendly” forms of our Church Boolean operators:

var not = toFunc1(Not);
var and = toFunc2(And);
var or = toFunc2(Or);
var xor = toFunc2(Xor);

Notice the different casing used. Exercise for the reader: infer the types of the eight objects that appear in the fragment above (i.e. excluding the to* functions).
Now we can write a test procedure as follows:

Console.WriteLine("Church Booleans");
Unary("toBool", toBool, toBool, x => x, F, T);
Unary("not", not, toBool, toBool, F, T);
Binary("and", and, toBool, toBool, F, T);
Binary("or", or, toBool, toBool, F, T);
Binary("xor", xor, toBool, toBool, F, T);
Console.WriteLine();

Here’s the result:

It worked, didn’t it?

Lambda Language Runtime for CLR 2.0 – noise reducing intermezzo

In the sample above, we’ve encountered utterly complicated application calls due to the fact the beta function only takes two arguments at a time (just like classical lambda calculus prescribes):

var Xor = λ(m => λ(n => λ(a => λ(b => ß(ß(m, ß(ß(n, b), a)), ß(ß(n, a), b)))))); // \mn.\ab.m(nba)(nab)

It’s a convention that applications are left-associative, hence we’d like to be able to write the following instead:

var Xor = λ(m => λ(n => λ(a => λ(b => ß(m, ß(n, b, a), ß(n, a, b)))))); // \mn.\ab.m(nba)(nab)

Obviously this is easy to realize as follows, using LINQ’s Aggregate (“left fold”) operator:

static Action ß(Action x, Action y, params Action[] zs)
{
    return zs.Aggregate(ß(x, y), (l, z) => ß(l, z));
}

Can we make the excessive lambda arrows are bit less invasive too? Sure, inspired by our fromFunc objects:

static Action λ(Func<Action, Action, Action> f)
{
    return λ(x => λ(y => f(x, y)));
}

static Action λ(Func<Action, Action, Action, Action> f)
{
    return λ(x => λ(y => λ(z => f(x, y, z))));
}

That puts us in a position to write the Xor operator as:

var Xor = λ((m, n) => λ((a, b) => ß(m, ß(n, b, a), ß(n, a, b)))); // \mn.\ab.m(nba)(nab)

Much cleaner, isn’t it?

Church numerals

If Booleans work, we should get numerals working too. Obviously this is the case:

//
// Church numerals
//
var N0 = λ(f => λ(x => x)); // \fx.x = F
var N1 = λ(f => λ(x => ß(f, x))); // \fx.fx
var N2 = λ(f => λ(x => ß(f, ß(f, x)))); // \fx.f(fx)

var Zero = λ(n => ß(ß(n, λ(x => F)), T)); // \n.n(\x.F)T
var Succ = λ(n => λ(f => λ(x => ß(f, ß(ß(n, f), x))))); // \n.\fx.f(nfx)
var Pred = λ(n => λ(f => λ(x => ß(ß(ß(n, λ(g => λ(h => ß(h, ß(g, f))))), λ(u => x)), λ(u => u)))));
var Plus = λ(m => λ(n => λ(f => λ(x => ß(ß(m, f), ß(ß(n, f), x)))))); // \mn.\fx.mf(nfx)
var Sub = λ(m => λ(n => ß(ß(n, Pred), m)));
var Mul = λ(m => λ(n => λ(f => ß(n, ß(m, f))))); // \mn.\f.n(mf)
var Exp = λ(m => λ(n => ß(n, m))); // \mn.nm

var zero = toFunc1(Zero);
var succ = toFunc1(Succ);
var pred = toFunc1(Pred);
var plus = toFunc2(Plus);
var sub = toFunc2(Sub);
var mul = toFunc2(Mul);
var exp = toFunc2(Exp);

Func<Action, uint> toInt = x =>
{
    uint n = 0;
    ß(ß(x, () => { n++; }), nop)();
    return n;
};
Func<uint, Action> fromInt = null;
fromInt = n =>
{
    return (n == 0 ? N0 : succ(fromInt(n - 1)));
};

The nop helper function used in the toInt function is simply the no-op Action delegate () => {}. To get to know how toInt works (as well as all the other functions, by means of formal proofs), have a look at my previous post again. Either way, a simple test shows all of the above works as well:

Console.WriteLine("Church numerals");
Unary("toInt", toInt, toInt, x => x, Enumerable.Range(0, 3).Select(i => fromInt((uint)i)).ToArray());
Unary("succ", succ, toInt, toInt, Enumerable.Range(0, 3).Select(i => fromInt((uint)i)).ToArray());
Unary("pred", pred, toInt, toInt, Enumerable.Range(1, 3).Select(i => fromInt((uint)i)).ToArray());
Unary("zero", zero, toInt, toBool, Enumerable.Range(0, 2).Select(i => fromInt((uint)i)).ToArray());
Binary("plus", plus, toInt, toInt, Enumerable.Range(0, 3).Select(i => fromInt((uint)i)).ToArray());
Binary("mul", mul, toInt, toInt, Enumerable.Range(0, 3).Select(i => fromInt((uint)i)).ToArray());
Binary("exp", exp, toInt, toInt, Enumerable.Range(1, 3).Select(i => fromInt((uint)i)).ToArray());
Console.WriteLine();

Resulting in:

Church pairs and lists

As an outtake for today’s installment, let’s show how to realize pairs and lists using functions:

//
// Pairs
//
var Pair = λ(x => λ(y => λ(z => ß(ß(z, x), y)))); // \xy.\z.zxy
var Fst = λ(p => ß(p, T)); // \p.pT
var Snd = λ(p => ß(p, F)); // \p.pF

var pair = toFunc2(Pair);
var fst = toFunc1(Fst);
var snd = toFunc1(Snd);

Func<Action, Tuple<object, object>> toPair = a => new Tuple<object, object>(ext(fst(a)), ext(snd(a)));
Func<Tuple<object, object>, Action> fromPair = p => pair(inj(p.Item1), inj(p.Item2));

Assert(toInt(fst(pair(N1, N2))) == 1, "fst(pair(N1, N2))");
Assert(toInt(snd(pair(N1, N2))) == 2, "snd(pair(N1, N2))");

var me = new Tuple<object, object>("Bart", 26);
Assert(toPair(fromPair(me)).Equals(me), "Roundtrip object pair");

var nums = new Tuple<object, object>(N1, N2);
Assert(toPair(fromPair(nums)).Equals(nums), "Roundtrip nums pair");

A pair is constructed by giving it two arguments, resulting in a function that will return one of them by giving it a Boolean (“z” in the Pair function above). The first and second extraction functions are then defined in terms of applying the “pair as a function” to either T or F, which will select the right value out of the pair.
The toPair and fromPair functions are defined to go back and forth between a Church pair and a Tuple<object, object> in CLR-land. This is based on two functions I’m not showing here (left as an exercise for the reader): ext and inj, for extract and inject respectively. The signature of those functions is as follows:

//
// Values
//
Func<object, Action> inj = o => /* left as an exercise */
Func<Action, object> ext = a => /* left as an exercise */

Assert((string)ext(inj("Bart")) == "Bart", "ext(inj(\"Bart\"))");
Assert((int)ext(inj(42)) == 42, "ext(inj(42))");
DateTime now = DateTime.Now;
Assert((DateTime)ext(inj(now)) == now, "ext(inj(now))");

Warning: This is not a trivial exercise, as arbitrary .NET objects need to be able to be “lifted into” lambda land (e.g. the sample above allows to roundtrip a string and a DateTime). Have fun <g>!
Church lists can be defined in terms of Nil and Cons operations, together with extraction functions like Head and Tail, and a test function IsNil:

//
// Lists
//
var Nil = ß(ß(Pair, T), T);
var IsNil = Fst;
var Cons = λ(h => λ(t => ß(ß(Pair, F), ß(ß(Pair, h), t))));
var Head = λ(z => ß(Fst, ß(Snd, z)));
var Tail = λ(z => ß(Snd, ß(Snd, z)));

var nil = Nil;
var isNil = fst;
var cons = toFunc2(Cons);
var head = toFunc1(Head);
var tail = toFunc1(Tail);

Func<Action, List<object>> toList = a =>
{
    List<object> res = new List<object>();

    while (!toBool(isNil(a)))
    {
        res.Add(ext(head(a)));
        a = tail(a);
    }

    return res;
};
Func<List<object>, Action> fromList = l => Enumerable.Reverse(l).Aggregate(nil, (t, o) => cons(inj(o), t));

Assert(toBool(isNil(nil)) == true, "isNil(nil)");
Assert(toBool(isNil(cons(N1, nil))) == false, "isNil(cons(N1, nil))");
Assert(toInt(head(cons(N1, N2))) == 1, "head(cons(N1, N1))");
Assert(toInt(tail(cons(N1, N2))) == 2, "tail(cons(N1, N2))");

var lst = new List<object> { 1, N2, 3 };
Assert(toList(fromList(lst)).SequenceEqual(lst), "Roundtrip list");

Again we provide ways to turn a Church list in a List<object> (again based on ext), and the other way around (using the magical inj). Yes, the above works just fine… As an additional exercise, write a ForEach extension method that can take a Church list (of type … Action) and an Action<Action> delegate as the body of the loop, so we can use it as follows (tip: mirror the toList implementation):

cons(N1, N2).ForEach(x =>
{
    Console.WriteLine(toInt(x));
});

Conclusion

What can I say? This was fun for sure, if nothing more. I hope I’ve convinced the reader that functions are immensely powerful animals capable of representing data. In addition, we’ve shown how powerful exceptions can be (something the “Unchecked Exceptions can be Strictly More Powerful than Call/CC” paper goes much much deeper into). Yeah, performance guys will have the hairs on their back standing upright, but hey: it’s Crazy Sundays after all. And, as an additional excuse I now can claim to be referred to as a “stunt coder” on Twitter (thanks James, also for subtly using the word “fold”):

Enjoy!