Implementation of a Pure Lazy Functional Language as a Template Metaprogram

What is the smallest system with which we can compute? One simple approach is via lambda calculus. There is only one thing we can do in lambda calculus and that's apply functions. And there's only one type of thing we can apply them to, functions again. And yet lambda calculus allows us to perform complex computations. For example we can represent the number n as the function that maps a function f to fn, i.e. that maps f to its nth iterate. We can also represent booleans, conditionals, lists as functions. In fact, lambda calculus is Turing complete. But lambda calculus has the annoying problem that it needs variables and we have all those issues of variable scope and so on. Can we get simpler? Implementation of Combinatory Logic as C++ templates. Under construction...

Because we know that S and K form a Turing complete system then this code incidentally provides a rigorous proof of the Turing completeness of the C++ template system.


#include <iostream>
#include <typeinfo>

template<class X> class Reduced {
public:
        typedef X value;
};

template<class X,class Y> class cons
        : public Reduced<cons<typename X::value,Y> > { };

class K
        : public Reduced<K> { };
class S
        : public Reduced<S> { };

template<class X,class Y> class cons<cons<K,X>,Y>
        : public Reduced<X> { };

template<class X,class Y,class Z> class cons<cons<cons<S,X>,Y>,Z>
        : public Reduced<cons<cons<X,Z>,cons<Y,Z> > > { };

template<class X,class Y = typename X::value> class FixedPoint
        : public Reduced<typename FixedPoint<Y,typename Y::value>::value> { };

template<class X> class FixedPoint<X,X>
        : public Reduced<X> { };

using std::cout;
using std::endl;

int main() {
        //
        // Run SSSK. Should output SK(SK)
        //
        cout << typeid(FixedPoint<cons<cons<cons<S,S>,S>,K> >::value).name() << endl << endl;

        return 0;
}

Contact

Feel free to email me (Dan Piponi) at stirfry (at) sigfpe.com.
Back to Home.