Untyped lambda calculus interpreter implemented in C++ templates

fact.cpp

////////////////////////////////////////////////////////////////////////////////
/// Kernel definitions

template <char  Var>            struct Ref;
template <char  Var, class Exp> struct Lam;
template <class Fun, class Arg> struct App;

                                          struct NullEnv;
template <char Var, class Env>            struct Lookup;
template <char Var, class Val, class Env> struct Bind;

template <char Var>
struct Lookup<Var, NullEnv>;

template <char Var, class Val, class Env>
struct Lookup<Var, Bind<Var, Val, Env>>
{
    typedef Val result;
};

template <char Var, char OtherVar, class Val, class Env>
struct Lookup<Var, Bind<OtherVar, Val, Env>>
{
    typedef typename Lookup<Var, Env>::result result;
};

template <class Abs, class Env> struct Closure;
template <class Exp, class Env> struct Eval;
template <class Fun, class Arg> struct Apply;

template <char Var, class Env>
struct Eval<Ref<Var>, Env>
{
    typedef typename Lookup<Var, Env>::result value;
};

template <char Var, class Exp, class Env>
struct Eval<Lam<Var, Exp>, Env>
{
    typedef Closure<Lam<Var, Exp>, Env> value;
};

template <class Fun, class Arg, class Env>
struct Eval<App<Fun, Arg>, Env>
{
    typedef typename Apply<typename Eval<Fun, Env>::value,
                           typename Eval<Arg, Env>::value>::result value;
};

template <char Var, class Exp, class Env, class Arg>
struct Apply<Closure<Lam<Var, Exp>, Env>, Arg>
{
    typedef typename Eval<Exp, Bind<Var, Arg, Env>>::value result;
};

////////////////////////////////////////////////////////////////////////////////
/// Macroexpand : Kernel

template <class Exp> struct Expand;

template <class Exp, class Env>
struct Compute
{
    typedef typename Eval<typename Expand<Exp>::result, Env>::value value;
};

template <char Var>
struct Expand<Ref<Var>>
{
    typedef Ref<Var> result;
};

template <char Var, class Exp>
struct Expand<Lam<Var, Exp>>
{
    typedef Lam<Var, typename Expand<Exp>::result> result;
};

template <class Fun, class Arg>
struct Expand<App<Fun, Arg>>
{
    typedef App<typename Expand<Fun>::result,
                typename Expand<Arg>::result> result;
};

////////////////////////////////////////////////////////////////////////////////
/// Macroexpand : Variadic abstraction

template <char... Vars> struct Args;
template <class Args, class Exp> struct Lam_;

template <char Var, class Exp>
struct Expand<Lam_<Args<Var>, Exp>>
{
    typedef typename Expand<Lam<Var, Exp>>::result result;
};

template <char Var, char... Vars, class Exp>
struct Expand<Lam_<Args<Var, Vars...>, Exp>>
{
    typedef Lam<Var, typename Expand<Lam_<Args<Vars...>, Exp>>::result> result;
};

////////////////////////////////////////////////////////////////////////////////
/// Macroexpand : Variadic application : Ref-list

struct Nil;
template <class First, class Rest> struct RefList;

template <char... Vars> struct ToRefList_s;

template <char Var>
struct ToRefList_s<Var>
{
    typedef RefList<Ref<Var>, Nil> result;
};

template <char Var, char... Vars>
struct ToRefList_s<Var, Vars...>
{
    typedef RefList<Ref<Var>, typename ToRefList_s<Vars...>::result> result;
};

template <class... Exps> struct ToRefList_i;

template <class Exp>
struct ToRefList_i<Exp>
{
    typedef RefList<Exp, Nil> result;
};

template <class Exp, class... Exps>
struct ToRefList_i<Exp, Exps...>
{
    typedef RefList<Exp, typename ToRefList_i<Exps...>::result> result;
};

////////////////////////////////////////////////////////////////////////////////
/// Macroexpand : Variadic application : Ref-list processing

template <class Apps, class RefList> struct App_wrap;

template <class A, class D, class R>
struct App_wrap<Nil, RefList<A, RefList<D, R>>>
{
    typedef typename App_wrap<App<A, D>, R>::result result;
};

template <class Apps, class A>
struct App_wrap<Apps, RefList<A, Nil>>
{
    typedef typename App_wrap<App<Apps, A>, Nil>::result result;
};

template <class Apps, class A, class D>
struct App_wrap<Apps, RefList<A, D>>
{
    typedef typename App_wrap<App<Apps, A>, D>::result result;
};

template <class Apps>
struct App_wrap<Apps, Nil>
{
    typedef Apps result;
};

////////////////////////////////////////////////////////////////////////////////
/// Macroexpand : Variadic application : Actual implementation

template <char...  Exps> struct App_s;
template <class... Exps> struct App_i;

template <char... Exps>
struct Expand<App_s<Exps...>>
{
    typedef typename Expand<
                typename App_wrap<Nil,
                    typename ToRefList_s<Exps...>::result
            >::result
        >::result result;
};

template <class... Exps>
struct Expand<App_i<Exps...>>
{
    typedef typename Expand<
                typename App_wrap<Nil,
                    typename ToRefList_i<Exps...>::result
            >::result
        >::result result;
};

///////////////////////////////////////////////////////////////////////////////
/// Macroexpand : Recursion support : Lazy If

template <class Cond, class Then, class Else> struct If;

template <class Cond, class Then, class Else>
struct Expand<If<Cond, Then, Else>>
{
    typedef typename Expand<
        App_i<Cond, Lam<'.', Then>, Lam<'.', Else>, Lam<'.', Ref<'.'>>>
    >::result result;
};

///////////////////////////////////////////////////////////////////////////////
/// Churchifier

template <unsigned int N, char f, char x> struct Church_Inner;

template <unsigned int N>
struct Church
{
    typedef Lam_<Args<'f', 'x'>,
                typename Church_Inner<N, 'f', 'x'>::result > num;
};

template <char f, char x>
struct Church_Inner<0, f, x>
{
    typedef Ref<x> result;
};

template <unsigned int N, char f, char x>
struct Church_Inner
{
    typedef App<Ref<f>, typename Church_Inner<N - 1, f, x>::result> result;
};

#define MakeChurch(n) typename Church<n>::num

////////////////////////////////////////////////////////////////////////////////
/// Foreign term injection

template <class T> struct Inj;

template <class T, class Env>
struct Eval<Inj<T>, Env>
{
    typedef T value;
};

template <class T>
struct Expand<Inj<T>>
{
    typedef Inj<T> result;
};

////////////////////////////////////////////////////////////////////////////////
/// Unchurchifier

struct Peano_Zero
{
    static const unsigned int interpretation = 0;
};

struct Peano_Succ;

template <class N>
struct Apply<Peano_Succ, N>
{
    typedef struct _ {
        static const unsigned int interpretation = N::interpretation + 1;
    } result;
};

typedef Lam<'n', App_i<Ref<'n'>, Inj<Peano_Succ>, Inj<Peano_Zero>>> Unchurch;

////////////////////////////////////////////////////////////////////////////////
/// Basic arithmetic and logic

typedef Lam_<Args<'a', 'b', 'f'>, App<Ref<'a'>, App_s<'b', 'f'>>> Mul;

typedef Lam_<Args<'n', 'f', 'x'>,
            App_i<
                Ref<'n'>,
                Lam_<Args<'g', 'h'>, App<Ref<'h'>, App_s<'g', 'f'>>>,
                Lam<'u', Ref<'x'>>,
                Lam<'u', Ref<'u'>> > > Pred;

typedef Lam_<Args<'a', 'b'>, App<App<Ref<'b'>, Pred>, Ref<'a'>>> Sub;

typedef Lam_<Args<'a', 'b'>, Ref<'a'>> True;
typedef Lam_<Args<'a', 'b'>, Ref<'b'>> False;

typedef Lam<'n', App_i<Ref<'n'>, Lam<'u', False>, True>> EqZero;

typedef Lam_<Args<'a', 'b'>,
            App<EqZero, App_i<Sub, Ref<'a'>, Ref<'b'>>> > Leq;

typedef Lam_<Args<'p', 'q'>, App_s<'p', 'q', 'p'>> And;

typedef Lam_<Args<'a', 'b'>,
            App_i<And, App_i<Leq, Ref<'a'>, Ref<'b'>>,
                       App_i<Leq, Ref<'b'>, Ref<'a'>>> > Eq;

////////////////////////////////////////////////////////////////////////////////
/// Standard library

typedef Bind<'=', Compute<Eq,            NullEnv>::value,
        Bind<'*', Compute<Mul,           NullEnv>::value,
        Bind<'-', Compute<Sub,           NullEnv>::value,
        Bind<'U', Compute<Unchurch,      NullEnv>::value,
        Bind<'0', Compute<MakeChurch(0), NullEnv>::value,
        Bind<'1', Compute<MakeChurch(1), NullEnv>::value,
        Bind<'2', Compute<MakeChurch(2), NullEnv>::value,
        Bind<'3', Compute<MakeChurch(3), NullEnv>::value,
        Bind<'4', Compute<MakeChurch(4), NullEnv>::value,
        Bind<'5', Compute<MakeChurch(5), NullEnv>::value,
        Bind<'6', Compute<MakeChurch(6), NullEnv>::value,
        Bind<'7', Compute<MakeChurch(7), NullEnv>::value,
        Bind<'8', Compute<MakeChurch(8), NullEnv>::value,
        Bind<'9', Compute<MakeChurch(9), NullEnv>::value,
            NullEnv>>>>>>>>>>>>>> StandardLibrary;
///
////////////////////////////////////////////////////////////////////////////////

#include <iostream>

#ifndef FACT_ARG
#define FACT_ARG 0
#endif

int main()
{
    typedef App_s<'*', '6', '7'> the_answer_to_life_the_universe_and_everything;

    std::cout <<
        Compute<App<Ref<'U'>, the_answer_to_life_the_universe_and_everything>,
                StandardLibrary>
        ::value::interpretation;

    std::cout << "\n";

    // Fact_gen = λfn.if (= n 0) 1
    //                   (* n (f (- n 1)))
    typedef Lam_<Args<'f', 'n'>,
                If<App_s<'=', 'n', '0'>,
                    Ref<'1'>,
                    App_i<Ref<'*'>, Ref<'n'>,
                        App_i<Ref<'f'>, App_s<'-', 'n', '1'>> > > > Fact_gen;

    // Z = λf.(λx.f (λy.x x y)) (λx.f (λy.x x y))
    typedef Lam<'f', App<Lam<'x', App<Ref<'f'>, Lam<'y', App_s<'x', 'x', 'y'>>>>,
                         Lam<'x', App<Ref<'f'>, Lam<'y', App_s<'x', 'x', 'y'>>>>>> Z;

    std::cout <<
        Compute<App<Ref<'U'>,
                    App_i<Z, Fact_gen, MakeChurch(FACT_ARG)>>,
                StandardLibrary>
        ::value::interpretation;

    std::cout << "\n";
}