λ-fun in metaC++: Church numerals

The classical way to represent natural numbers in λ-calculus was invented by Church:

0 = λfx.x
1 = λfx.fx
2 = λfx.f(fx)
...
N = λfx.fⁿ(x)

This translates to our C++ embedding as follows:

struct ZERO;
template<typename F,typename X>
struct apply<apply<ZERO,F>,X>{typedef X type;};

struct ONE;
template<typename F,typename X>
struct apply<apply<ONE,F>,X>:apply<F,X>{};

struct TWO;
template<typename F,typename X>
struct apply<apply<TWO,F>,X>:apply<F,typename apply<F,X>::type>{};
...

The corresponding basic arithmetic operations are easy to define:

SUCC = λnfx.f(nfx) (successor function)
PLUS = λmnfx.nf(mfx)
MULT = λmn.m(PLUS n) 0

and to translate to C++:

// syntax sugar to abbreviate notation
template<typename F,typename G,typename H>
struct apply2{
  typedef typename apply<typename apply<F,G>::type,H>::type type;
};

struct SUCC;
template<typename N,typename F,typename X>
struct apply<apply<apply<SUCC,N>,F>,X>:
  apply<F,typename apply2<N,F,X>::type>{};

struct PLUS;
template<typename M,typename N,typename F,typename X>
struct apply<apply<apply<apply<PLUS,M>,N>,F>,X>:
  apply2<N,F,typename apply2<M,F,X>::type>{};

struct MULT;
template<typename M,typename N>
struct apply<apply<MULT,M>,N>:
  apply2<M,typename apply<PLUS,N>::type,ZERO>{};

I've written a little C++ program exercising these ideas (you'll need Boost to compile it). How to test our constructs? That is, how to verify for instance that the type NINE defined as:

typedef apply<apply<MULT,THREE>::type,THREE>::type NINE;

actually corresponds to λfx.f(f(f(f(f(f(f(f(fx)))))))))? Well, if we define

template <int N>struct int_{};
struct succ;
template<int N> struct apply<succ,int_<N> >{
  typedef int_<N+1> type;
};

then we have that

apply<apply<N,succ>::type,int_<0> >::type

is the same type as

int_<n>

as long as N stands for the Church numeral N. This verification can be easily done with some metaprogramming machinery. Note that succ is not a proper λ-term even though we have used it inside our apply machinery: this hints at a general technique called λ-calculus extension.