Monday, August 17, 2009 1:35 AM bart

(Mis)using C# 4.0 Dynamic – Type-Free Lambda Calculus, Church Numerals, and more

Introduction

Sunday morning, time for another episode of the Crazy Sundays series. Again one in the category with risk for exploding brains, but that’s what we like, don’t we? This time around, we’re going to have a look at the type free lambda calculus in C#. But wait a minute, isn’t C# a typed language? True. Does that mean everything you do in it should be statically typed? Not necessarily: typing is there as a tool you can leave or take. In this post we’ll take a look at the new C# 4.0 dynamic feature (which provides a static type to do dynamic dispatch) from a somewhat bizarre angle…

Sometimes types do get in the way: maybe something is intrinsically untyped (like XML documents without a schema, web services without a WSDL contract, etc) or meant to be dynamically typed (like objects coming from a dynamic language like Ruby or Python). And then there are notorious APIs that “peter out” in their typing: one moment you’re statically typed, but all of a sudden you end up with System.Object everywhere (like with COM interop to the Office libraries). All such scenarios are what C# 4.0 dynamic is meant for. The classical sample to illustrate the feature is to talk to an IronPython object from C#. First the Python definition:

class Calc:
    def Add(self, a, b):
        return a + b
def GetCalc():
   return Calc()

The nice thing about this Python-based calculator is that it will work with anything that supports an addition operator. In other words, we could feed it two int objects, two string objects, or even a DateTime and a TimeSpan. To make such calls, we use the dynamic keyword in C#:

var py = Python.CreateEngine();
dynamic script = py.ImportModule("Calc");

dynamic calc = script.GetCalc();
int three = calc.Add(1, 2);

Ignore the few lines of plumbing to load the Python file; what matters here is the fact the calc variable is typed to be “dynamic”, meaning all operations invoked on it will be resolved at runtime:

image

I won’t go into details on how all of this works, maybe another time (outside the scope of Crazy Sundays posts), but that’s the essence of the feature. Instead, we’re going to push this feature to the limits in a “don’t try this at homework” style: enter type free lambda calculus.

 

Type free lambda calculus in a nutshell

The type free lambda calculus, due to Alonzo Church around 1930, is a theory about the computational aspects of functions. It views functions as rules and defines two complimentary operations to work with those: abstraction and application. In essence, that’s all there is but nevertheless the theory gives rise to a whole research area of its own. To convince you about that statement, check the page count for the following book on your favorite online bookshop:

So, allow me to summarize the essentials here, citing/paraphrasing the book above (due to the non-trivial nature of mathematical notation, pasted as images from Word equations). First, we need to define the concept of a lambda term:

image

As a typical exercise, expand the fourth lambda term in the examples above to its fully parenthesized and bloated form.

All there is to lambda terms is they can denote functions, just like lambda expressions in C# do. For example, the second sample above is a function with argument “x”, returning “x”. In other words, it’s the identity function. However, it has no type: it can operate on anything (in particular, any other lambda term). In C# we could write this as follows:

Func<T, T> I = x => x;

where T stands for a generic parameter. It’s clear this function can operate on values but equally well it can operate on functions: given a function, it will return exactly that function:

I(5) // produces 5
I(I) // produces I

In fact, the middle three samples above are closed terms, meaning all symbols used in their “function body” (the part after the dot) are in “scope” by means of the abstraction(s) over it. We call those combinators:

image

The last sample term in the previous sample is not closed though: it returns “x” which is not being abstracted over. This reflects the concept of a closure, just as we have in C#:

R x = …;
Func<T, R> f = z => x;

Let’s not go there for now, but suffice to say that fancy words like “closure” are deeply rooted in theoretical foundations. Praise yourself lucky to work with a language layered on top of solid theoretical foundations :-).

Next, we need the concept of free variables. In short, this allows us to identify those variables not introduced by an abstraction in a given term. The definition is fairly straightforward:

image

For combinators, the free variables set will be empty. In contrast, for our last sample (the one resulting in a closure) the set would be a singleton containing “x”. Nothing too fancy, right?

Finally, we can define how application is carried out, based on the concept of substitution:

image

To avoid name clashes (something that can be formally avoided by using a variable convention, using the definition of FV above), we notice careful renames are possible. We all know this from C#, and this is merely a theoretical foundation for scoping:

Func<T, T> I1 = x => x;

and

Func<T, T> I2 = y => y;

are in fact the “same”. Using such a big word in the context of a whole runtime (CLR) and language (C#) is a dangerous business. I’m not saying that I1 and I2 will refer to the same delegate: there’s no identification between delegates that says “x => x” and “y => y” are the same. Rather, what I’m pointing out here is that the behavior of I1 and I2 will be the same when applied to the same object. In the lambda calculus this is referred to as alpha-conversion.

Ignoring the important concern of avoiding name clashes for the time being, have a closer look at the application “beta-conversion” rule above. The idea is simple: “application of an abstraction with another term results in substitution”. This is pretty much like a delegate call in C#, but yet different enough: in the world of the lambda calculus, substitutions are nothing but mechanical rewrites on terms. In languages like C#, code is compiled as-is and delegate calls don’t magically rewrite the delegate’s body on the fly. But more importantly, in C# we get also immediately concerned with call semantics like call-by-value: before making a call, its arguments need to be reduced to a “value” that can be passed to the receiving end of the call (through the delegate invocation mechanism).

 

Untyped or uni-typed?

Now the question of the day: can we type (in the CLR/C# type system sense) all lambda terms? It seems we were successful doing so already with the I combinator, concluding it’s a Func<T, T> with the use of generics: passing a value of a certain type T, the result it the same value and hence of the same type. In fact, what about inferring such signatures? C# doesn’t do so, but F# can (through Hindley-Milner type inference as is done typically in ML-inspired languages):

image

Okay, “I” is inferred to be a type that goes from ‘a to ‘a, where ‘a is the notation for a generic parameter. What about K, the combinator that given two arguments always returns that first one (“constant” value producer):

image

We’re still good to go it seems. F# has inferred the type ought to be “‘a to ‘b to ‘a”. Wow, what’s going on here? In C#, this would look like Func<T1, Func<T2, T1>>: a function that given an argument of type T1 returns a function that given an argument of type T2 returns a value of type T1. Get it? What’s happening here is “currying”, where a function of n arguments is turned into “nested” functions that consume one argument at a time. This means we can write, say, “K 5” to create a new function that will eat the remaining “y” argument (of any type) and will always return 5.

Note: There’s a little complication here in the context of F#, called the “value restriction”. I won’t go there as this is irrelevant for the discussion here. What we’re focusing on is solely whether or not we can type lambda expressions.

Even for the (relatively) complicated beast S, a type can be inferred:

image

Impressive? Not so hard in fact. Follow me as we infer the type ourselves by hand, from the function’s body. First of all, we see x followed by two terms: “z” and “(y z)”. That means “x” is a function with two arguments, and we assume it returns something. Assign type names for those things: the first argument “z” gets type ‘a and the result of “(y z)” will get type ‘b. For the result we write ‘c. In other words, the type of “x” is already inferred to be ’a –> ‘b –> ‘c. Next, we need to infer the type for “y” based on our prior identification of the type for “(y z)” as ’b. We see that “y” is a function with one argument, “z”. We already typed “z” to be ‘a, so the type of “y” becomes ‘a –> ‘b. And finally, our “S” function also takes in “z” as a third argument, which is typed to be ‘a. All of this brought together with the return type of the call to “x” leads to the signature shown above.

So, it looks like we can type all lambda terms, right? Unfortunately, no. Here’s the proof:

image

Here I’ve written a function W that given an argument x applies that to itself. Such a simple lambda term, and yet one can’t find a type for it. Follow me on this brain exercise: W takes one argument x, say of type ‘a. Now, x is applied to x. From this it looks like x is a function type with one argument. The argument is x, which we’ve already typed to be ‘a. What about the return type? Let’s say it’s ‘b, so now we have that x needs to be of type ‘a –> ‘b, which isn’t the same as ‘a we had before: unification fails.

That’s where differences between the type free lambda calculus and typed variants (like the simply typed lambda calculus and for generics and such something called “System F”) crop up. C# being a typed language doesn’t allow us to get rid of types altogether, so there’s no way we can get “untyped”. But what about “uni-typed” (due to Robert Harper): replace all types with one single type. Can we get there? The answer is, with “dynamic” we can!

dynamic W = new Func<dynamic, dynamic>(x => x(x));

The fact we need some ugly delegate constructor call is unfortunate, but notice how we’re assigning the “dynamic –> dynamic” type to a “dynamic” on the left. In other words, we’re treating everything (non-functional values and function “objects” themselves) as dynamic. The code above compiles just fine, but how does the x(x) in the lambda body work? Well, at runtime the system will figure out what the type of x is and ensure it can be used to be called as a unary function. For example:

dynamic W = new Func<dynamic, dynamic>(x => x(x));
W(1);

This will clearly fail. It corresponds to “calling the function integer 1” with argument “integer 1”. Clearly, an integer value cannot be used as a function (a good thing!), so a runtime error results:

Unhandled Exception: Microsoft.CSharp.RuntimeBinder.RuntimeBinderException: Cannot invoke a non-delegate type
   at CallSite.Target(Closure , CallSite , Object , Object )
   at System.Dynamic.UpdateDelegates.UpdateAndExecute2[T0,T1,TRet](CallSite site, T0 arg0, T1 arg1)
   at UntypedLambda.Program.<Main>b__46(Object x)
   at CallSite.Target(Closure , CallSite , Object , Int32 )
   at System.Dynamic.UpdateDelegates.UpdateAndExecuteVoid2[T0,T1](CallSite site, T0 arg0, T1 arg1)
   at UntypedLambda.Program.Main()

How this works internally is beyond the scope of this post (I’m sure I’ll blog about the DLR machinery and the role of the C# and VB compilers in that mix some time in the relatively near future) but the DLR was right to conclude the call above is nonsense.

What about the following?

var I = new Func<dynamic, dynamic>(x => x);
dynamic W = new Func<dynamic, dynamic>(x => x(x));
Console.WriteLine(W(I)(42));

Now, that works. Passing I to W results in I(I), which reduces (using application, or beta-conversion) into I. That function is then used with argument 42 subsequently, returning 42.

You can guess it … we’re going to uni-type our whole programs using dynamic in this Crazy Sundays post. Did I ever mention Scheme? If not, I did now :-).

 

SKI combinators

As we’ve already played with S, K and I in the samples above, let’s see how those look in uni-typed C#:

//
// Where else to start than with ... SKI combinators.
//
var S = new Func<dynamic, Func<dynamic, Func<dynamic, dynamic>>>(x => y => z => x(z)(y(z)));
var K = new Func<dynamic, Func<dynamic, dynamic>>(x => y => x);
var I = new Func<dynamic, dynamic>(x => x);

Notice we’re currying all functions so that we can partially apply functions. For example, we can do the following to create a “constant function” that always returns 42:

var answer = K(42);
Console.WriteLine(answer("Bart"));
Console.WriteLine(answer(DateTime.Now));
Console.WriteLine(answer(-42));
Console.WriteLine(answer(S));

All of the calls above will print 42, regardless of what’s passed in to answer. Follow the reduction in your head: applying 42 to K returns a function from a parameter called “y” to 42. In other words, “y” is discarded altogether. We’re generating the constant 42, no matter what (both in terms of value and type) we throw to the function as an argument. Not just plain values: in the last line we throw S, another function, to the answer function and yet it persists telling us the answer is 42.

It can be shown, as an easy exercise, that SKK (and SKS) are the same as I, so the following is a complicated way of writing 5:

int five = S(K)(K)(5);

See how functions are first-class citizens: they can be passed or returned everywhere. Also notice how functions have to be called one argument at a time because of currying (due to Schonfinkel, not Curry).

While we’re at it, we’ll write a helper function to apply a function to different argument values and print the result to the screen. In subsequent paragraphs we’ll use this function (and a variant thereof) to aid us in printing test results:

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

Quite a signature, but essentially we take a friendly function name, a function to be tested, some function to turn the “dynamic” argument into a print-friendly form (and a similar function for the result of the function call), and an array of values to be fed in. For example:

Console.WriteLine("SKI");
Unary("SKK", S(K)(K), I, I, 5, DateTime.Now, "Bart");
Unary("I", I, I, I, 5, DateTime.Now, "Bart");
Console.WriteLine();

This results in the following:

image

As an exercise, try to do something more meaningful with the S combinator.

 

Church Booleans

Functions and data are very closely related. More closely than you may think. Most programmers think of functions as pieces of code that have a certain behavior and get applied to zero or more arguments, producing some (or none) value. That’s a very code-centric view of the world, while functions in the mathematical sense are obviously not related to “code” at all. Functions are often defined as graphs and are a special kind of relation between two sets. Sets are all about data, aren’t they? Based on such an observation one can establish functions in a computer programs as table lookup = data.

But there’s more, even values themselves (and not mappings between them) can be encoded using functions. Let’s start easy, with Booleans. Easy because there are only two values to distinguish. Here’s the proposed mapping:

//
// Church Booleans.
// Basic idea: true and false are dyadic functions returning respectively
//             the first or second argument, acting as a conditional (?:)
//
var F = new Func<dynamic, Func<dynamic, dynamic>>(a => b => b);
var T = new Func<dynamic, Func<dynamic, dynamic>>(a => b => a);

Okay, the comment reveals it already: the idea is that true and false are encoded as functions with two arguments (again curried) of which one is returned: false returns the second one, true the first one. Sounds familiar, doesn’t it? Right, the conditional operator (sometimes awkwardly referred to as the ternary operator) in C# does exactly that. Notice that using alpha-conversion, T is exactly the same as K.

Notice it’s easy to convert between the untyped world and the typed world using two back-and-forth conversion functions:

Func<dynamic, bool> toBool = x => x(true)(false);
Func<bool, dynamic> fromBool = b => b ? T : F;

We wouldn’t need toBool if we weren’t to print the results to the screen somehow :-). For completeness, I’ve added fromBool to the equation. Both are easy to understand, but let’s start with fromBool. Plain easy: give it true, and it returns T; give it false, and you get F back. The inverse function, toBool, is simple function application (beta conversion) of the defined functions to C# Booleans: if the function bound to x is T, the first argument will be returned (true). If it’s F, the second one (false) will. Clear as crystal. Notice toBool can be applied with any object as its argument: going from untyped to typed will blame the argument if something goes wrong (due to Philip Wadler).

Not very useful yet, if we don’t have a way to define operations between such Booleans. Again functions come to the rescue (we don’t have anything else after all), so let’s have a look at how we define a simple operator: not.

var not = new Func<dynamic, Func<dynamic, Func<dynamic, dynamic>>>(m => a => b => m(b)(a));

Notice all operators on Church Booleans will be higher-order functions in their very nature, since their arguments are functions already. That’s the nature of the beast we’re dealing with. So, how can we turn a Church Boolean “m” in its opposite? We already know that Church Booleans are dyadic functions, so the result of calling not with a Church Boolean should be a function with two arguments: that’s what “a” and “b” are for. The body of the function may look a bit weird: we’re calling “m” (a Church Boolean, but remember everything is a function hence executable) with arguments b and a. That has a flipping effect as proven below:

image

Impressive, isn’t it? A word on notation: before doing a beta-reduction we indicate the abstractions we’re going to apply substitutions for by putting a bar on top of them (e.g. in the second step m, in the fourth step x and y). When doing multiple reductions we write an arrow with a double arrowhead. When substituting terms for their definition (like T and F in the proof above), we carry out alpha-conversion to avoid the risk of name clashes (though strictly speaking for closed terms we could play a more risky game).

How can we do binary operators, like and, or and xor? Turns out those are fairly simple to do as well:

var and = new Func<dynamic, Func<dynamic, dynamic>>(m => n => m(n)(m));
var or = new Func<dynamic, Func<dynamic, dynamic>>(m => n => m(m)(n));
var xor = new Func<dynamic, Func<dynamic, Func<dynamic, Func<dynamic, dynamic>>>>(m => n => a => b => m(n(b)(a))(n(a)(b)));

Agreed, one needs to see a proof of correctness before being convinced those functions have the desired behavior. By the way, outside C#, we could save us some parentheses which mainly come from (dynamic) delegate invocations above. Also notice that the functions for and and or don’t have abstractions in their “body”: the result of calling “mnm” or “mmn” already gives a function of the right arity, as can be seen in the proofs below:

image

The proof for xor is left as an exercise to the reader (feel free to use case analysis of all four combinations of arguments, although you can simplify matters a bit…).

Of course you want to see this in action. We already have our Unary function to test lambda functions with given arguments, let’s define a similar one for binary operators:

static void Binary<T, PArg, PRes>(string name, Func<dynamic, T> f, Func<dynamic, PArg> printArg, Func<dynamic, PRes> printRes, params dynamic[] 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)));
}

It basically creates all combinations of input arguments and applies them to the function, putting some pretty printing to the mix. So we write:

Console.WriteLine("Church Booleans");
Unary("toBool", toBool, toBool, I, 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();

The use of toBool allows us to go from a “dynamic” function to a concrete C# Boolean value which is printable by Console.WriteLine. The result looks like this:

image

Looks right, doesn’t it?

 

Church numerals

If we can do Booleans, we can do numeric values too, right? Let’s restrict ourselves to positive natural numbers (including 0) and we end up with the concept of Church numerals. Now we have an infinite domain of values to represent, we need a way to control this complexity somehow (in order to be able to define nice operators over them). One possible solution is the use of repeated function application to encode a numeric value, as follows:

image

Can you see it? Calling f on argument x once corresponds to 1, twice corresponds to 2, etc. Quite nice. What kind of simple operations can we define over such value representation? Clearly we don’t want to define all different N-objects for the whole domain of natural numbers. In fact, we don’t even want to define N1 explicitly. Two basic ingredients should suffice to define every natural number: a representation of 0, and a way to “add one” to a Church numeral (i.e. returning a new function that represents the value of the argument, plus one). This is the much desired successor function:

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)));

The successor function is a function with one argument “n”, returning a function of two arguments “f” and “x” (like all Church numerals being double-abstractions over some term). The definition is “f(nfx)”, with some more parentheses in C#. But how does it work? See it with your own eyes and feed it N0 for starters: “n” is substituted (beta conversion) for “N0” which by itself is a lambda expression of the form shown in the figure above (goes from f and x to x). A few beta-conversions later you’ll end up with f(x), exactly the definition of N1. In other words, succ simply adds an additional “f” application to the existing term’s body. A more formal proof is given below:

image

Based on this, can we create a simple conversions function to promote a C# positive integer value into a corresponding Church numeral? The answer is obviously yes and the idea is fairly easy: we’ll call succ repeatedly, n times for integer with value n, starting with N0 as the base. To go back from a Church numeral to a C# unsigned integer we exploit the repeated function call behavior on argument “f” and use a devilish side-effect to increment a counter whenever we are called:

Func<dynamic, uint> toInt = x =>
{
    uint n = 0;
    x(new Action<dynamic>(_ => { n++; }))(null);
    return n;
};

Func<uint, dynamic> fromInt = null;
fromInt = n =>
{
    return (n == 0 ? N0 : succ(fromInt(n - 1)));
};

If you don’t get this immediately, don’t worry. Just feed it some Church numerals and see what happens. For example, N0 is a function that simply returns its second argument. When calling toInt on N0, x is bound to N0, executed with two arguments of which the second one – null – is returned. The function of type Action<dynamic> in the first argument was never called, so the result is 0. But if N1 is fed in, that function in the first argument will get called how many times? Right, just one time. In other words, the side-effecting n++ will be called once, and the result is 1. In other words, we should be able to “roundtrip” C# integers through Church numerals:

for (uint i = 0; i <= 10; i++)
    Console.WriteLine(toInt(fromInt(i)));

Try it at home and you should see the numbers 0 through 10 being printed on the screen. Victory. Oh, and fromInt is simply a recursive function that makes successor calls till n == 0 is reached, at which point N0 is returned. So, fromInt(5) will be encoded as succ(succ(succ(succ(succ(N0)))).

All of this looks good, doesn’t it? Another useful function is a zero-test. In the typed world this would be a function from an integer to a Boolean, but of course in the world of type-free lambda calculus we loose that typing safety net. Nevertheless, here’s how zero looks like:

var zero = new Func<dynamic, dynamic>(n => n(K(F))(T));

Recall that N0 was the same as F, and we know that F returns its second argument for its result. A zero-check on N0 clearly should return T, so the zero function should look like n (???) T. This satisfies the case where N0 is fed in. What about the other cases? Well, the first argument to n (the Church numeral passed in) is the function that gets called repeatedly on the second argument (which we already made T). For all those numerals we want to return F for the zero-check, so the question is whether we know a function that will always return F no matter what argument it’s given? We do, it’s called K with argument F: the constant-generator combinator K which we ask friendly to return hardheadedly F all the time. A formal proof is shown below:

image 

Finally, the real stuff. What about operations like add and multiply, or even exponential? The good thing is they exist indeed :-). And here they are:

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

How they work is another piece of cake. Here’s a proof for plus’s behavior:

image

That was fairly easy, wasn’t it? Feel free to feed it a couple of values to confirm the behavior, but we’ll run it through some tests in just a while. For mul and exp, proofs need some inductive reasoning as shown below:

image

Notice how beautiful the definition of exp is: apply n with argument m, and you got an exponential. Wow. If I’d drink alcohol, this would be a reason to get drunk. I’ll stick with Diet Coke anyhow, but suffice to say I absolutely love it. And far that matter, mul is nice too, don’t you agree?

What about a predecessor and subtract function? Unfortunately those are quite ugly in this Church numeral encoding system:

var pred = new Func<dynamic, Func<dynamic, Func<dynamic, dynamic>>>(n => f => x => n(new Func<dynamic, Func<dynamic, dynamic>>(a => b => b(a(f))))(K(x))(I));

Bweik. It’s so disgusting I’ll leave the definition of a “sub” function (tip: use pred) to the reader. Oh, and if you’re really fearsome, prove the correctness of “pred” using induction.

Anyway, here’s a test-application for Church numerals:

Console.WriteLine("Church numerals");
Unary("toInt", toInt, toInt, I, 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();

We use our beloved fromInt function in combination with some LINQ operators to produce an array of test inputs, for which all combinations will be fed to the passed-in functions:

image 

Wonderful. (Don’t bother to ask about performance…)

 

Going nuts – recursive functions

We could go much further and define pairs, tuples and lists using Church encodings as well, but as I have another rabbit in my hat for another time, I won’t spoil the beans at this point. A little sneak peak though (this is without C# 4.0 dynamic…), for pairs:

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

and for 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)));

Instead, let’s conclude this post with two recursive functions:

//
// The icing on the cake.
//
Func<Func<Func<dynamic, dynamic>, Func<dynamic, dynamic>>, Func<dynamic, dynamic>> Fix = null;
Fix = f => x => f(Fix(f))(x);

var fact = Fix(new Func<dynamic, Func<dynamic, dynamic>>(f => x => zero(x)(new Func<dynamic, dynamic>(_ => succ(N0)))(new Func<dynamic, dynamic>(_ => mul(x)(f(pred(x)))))(I)));
var fib = Fix(new Func<dynamic, Func<dynamic, dynamic>>(f => x => zero(x)(new Func<dynamic, dynamic>(_ => N0))(new Func<dynamic, dynamic>(_ => zero(pred(x))(new Func<dynamic, dynamic>(__ => succ(N0)))(new Func<dynamic, dynamic>(__ => plus(f(pred(x)))(f(pred(pred(x))))))(I)))(I)));

Unary("fact", fact, toInt, toInt, Enumerable.Range(0, 10).Select(i => fromInt((uint)i)).ToArray());
Unary("fib", fib, toInt, toInt, Enumerable.Range(0, 10).Select(i => fromInt((uint)i)).ToArray());

This gets quite ugly due to the use of a fixpoint combinator and the chase to circumvent call-by-value semantics (exercise: where and how does that happen precisely in the fragments above?) causing endless evaluations (exhausting the stack), but rest assured those functions work just fine:

image

Finally, an outtake :-). What does the following result in?

var Omega = new Func<dynamic, dynamic>(x => x(x))(new Func<dynamic, dynamic>(x => x(x)));
Omega(I);

Got a headache? Click here.

Del.icio.us | Digg It | Technorati | Blinklist | Furl | reddit | DotNetKicks

Filed under: , , ,

Comments

# Dew Drop &#8211; August 15, 2009 | Alvin Ashcraft's Morning Dew

Pingback from  Dew Drop &#8211; August 15, 2009 | Alvin Ashcraft's Morning Dew

# re: (Mis)using C# 4.0 Dynamic – Type-Free Lambda Calculus, Church Numerals, and more

Monday, August 17, 2009 6:33 AM by Nick Palladinos

I love Lambda Calculus, it's so simple so elegant!!!( Barendregt's book is the bible)

Here is my attempt to define the famous Y combinator

           Func<Func<dynamic, dynamic>, dynamic> fd = x => x;

           dynamic Y = fd(f => fd(x => f(fd(y => x(x)(y))))(fd(x => f(fd(y => x(x)(y))))));

           Y(fd(f => fd(x => f(x))))(42);

Crazy beautiful code :)

# A dynanic Y Combinator

Monday, August 17, 2009 7:10 AM by Thoughts and Code

Ο Bart de Smet έγραψε ένα πολύ καλο blog post για όσους θέλουν να πάρουν μια μικρή γεύση από την ομορφιά

# (Mis)using C# 4.0 Dynamic – Type-Free Lambda Calculus, Church Numerals, and more - Bart De Smet

Monday, August 17, 2009 7:24 AM by DotNetShoutout

Thank you for submitting this cool story - Trackback from DotNetShoutout

# re: (Mis)using C# 4.0 Dynamic – Type-Free Lambda Calculus, Church Numerals, and more

Monday, August 17, 2009 3:34 PM by kvb

Nice post!  Any reason toInt shouldn't look more like x => x(i => i+1)(0) rather than your side-effecting version?

-Keith

# re: (Mis)using C# 4.0 Dynamic – Type-Free Lambda Calculus, Church Numerals, and more

Monday, August 17, 2009 3:46 PM by bart

Hi Keith,

Sure - was a little too much in the mood of Action<dynamic> at the time of writing that part :-). But yes, you could write something along the lines of:

x => x(new Func<dynamic, dynamic>(i => i + 1))(0u)

Much cleaner - I like it!

Thanks,

-Bart

# Reflective Perspective - Chris Alcock &raquo; The Morning Brew #414

Pingback from  Reflective Perspective - Chris Alcock  &raquo; The Morning Brew #414

# (Mis)using C# 4.0 Dynamic – Type-Free Lambda Calculus, Church Numerals, and more - B# .NET Blog

Tuesday, August 18, 2009 8:32 AM by progg.ru

Thank you for submitting this cool story - Trackback from progg.ru

# re: (Mis)using C# 4.0 Dynamic – Type-Free Lambda Calculus, Church Numerals, and more

Tuesday, August 18, 2009 9:50 AM by Bones Justice

eul me up, boys, it's [lambda] calculus time!

# Introducing System.Linq.Expressions v4.0

Monday, August 24, 2009 3:47 PM by Introducing System.Linq.Expressions v4.0

Pingback from  Introducing System.Linq.Expressions v4.0

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

Sunday, August 30, 2009 5:18 AM by B# .NET Blog

Introduction A while back, I blogged about (Mis)using C# 4.0 Dynamic – Type-Free Lambda Calculus, Church

# More LINQ with System.Interactive – Exploiting the code = data relationship

Tuesday, December 29, 2009 3:44 AM by B# .NET Blog

With the recent release of the Reactive Extensions for .NET (Rx) on DevLabs , you’ll hear quite a bit

# Top 9 Posts from 2009

Sunday, January 03, 2010 1:08 AM by B# .NET Blog

select top 9 [Subject] from dbo . cs_Posts where postlevel = 1 and usertime &lt; &#39;01/01/2010&#39;

# Lambda Calculus: Links, News and Resources (1) &laquo; Angel &#8220;Java&#8221; Lopez on Blog

Pingback from  Lambda Calculus: Links, News and Resources (1) &laquo; Angel &#8220;Java&#8221; Lopez on Blog