C++ Template Lambda-Calculus Interpreter

This page is about a lambda-calculus interpreter encoded in the C++ template system. Oh, yes, it's ugly.

What?
This is a rather simple lambda calculus interpreter (with bools, ints, strings, and lists) encoded in the C++ template system. It also includes facilities to automatically project compile-time values as run-time values. This is a proof-of-concept project (i.e., a demonstration of how dreadful it is to encode computations in the type system) and is not intended to be used for anything!

How?
It is well-known that the C++ template system is Turing-complete. By encoding values in the type system (e.g., integers as Peano-encoded types), the template instantiation mechanism can be coöpted to perform purely-functional computations with type-level unification acting as the control constructs (via the "substitution-failure-is-not-an-error" principle). By using the same mechanism, type-encoded values can be converted to appropriate run-time values (e.g., Cons <Succ <Zero> >, Nil> can be converted to a list <int>). This little project demonstrates how an interpreter can be encoded in the template system whose output values can be used at run-time.

Who?
This interpreter is really intended as a demonstration of how the complicated type systems in many modern languages (e.g., C++, Haskell) can be convinced to perform arbitrary computations. Especially, it aims to show how difficult and "inside-out" is the required style of coding to do so.

Example?
Consider the following example program:
let two = S (S Z) in
let x = two + two in
x + x
We can encode this for our interpreter as:
typedef Succ <Succ <Zero> > two ;
typedef Let <1u, Sum <two, two>, Sum <Var <1>, Var <1> > > prog ;
cout << eval <prog> () ;
Which will print "8". Alternately, if we want to use this value for computations, we can write:
typedef Succ <Succ <Zero> > two ;
typedef Let <1u, Sum <two, two>, Sum <Var <1>, Var <1> > > prog ;
eval_type <prog> :: rtt x = eval <prog> () ;
"eval" allows us to refer to the result of our computation; "eval_type" allows us to compute the run-time type into which the output value will be projected.

Where?
You can download C++ source for the interpreter here. The code is licensed under the GPL.