Wednesday, November 14, 2007

λ-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.fn(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 notationtemplate<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.