Интерпретатор бестипового лямбда-исчисления на шаблонах С++

lc.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;
};

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

template <class T> struct Inj;

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

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

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

struct Succ;

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

///                                                                          ///
////////////////////////////////////////////////////////////////////////////////

#include <iostream>

int main()
{
    // 1 = λfx.f x
    typedef Lam<'f', Lam<'x', App<Ref<'f'>, Ref<'x'>>>> One;

    // 2 = λfx.f (f x)
    typedef Lam<'f', Lam<'x', App<Ref<'f'>, App<Ref<'f'>, Ref<'x'>>>>> Two;

    // + = λab.λfx.a f (b f x)
    typedef Lam<'a', Lam<'b', Lam<'f', Lam<'x',
                App<App<Ref<'a'>, Ref<'f'>>,
                    App<App<Ref<'b'>, Ref<'f'>>, Ref<'x'>>>
        >>>> Plus;

    // Sum = (+ 1 2)
    typedef App<App<Plus, One>, Two> Sum;

    // Result := (Sum +1 =0)
    typedef App<App<Sum, Inj<Succ>>, Inj<Zero>> Output;

    typedef Eval<Output, NullEnv>::value Result;

    std::cout << Result::interpretation;
}