Lambda calculus with type inference in C++ template

lambda.cpp

namespace lambda {

////////////////////////////////////////////////
// Lambda term

namespace term {

template<char c> struct var {};
template<typename N, typename M> struct app {};
template<char v, typename M> struct abs {};

} // term


namespace debruijn {

////////////////////////////////////////////////
// De Bruijn indexed term

template<int i, char c> struct var {};
template<typename N, typename M> struct app {};
template<char v, typename M> struct abs {};

////////////////////////////////////////////////
// Beta-reduction (leftmost strategy)

// increment binding level of free variables
template<typename T, int s, int l> struct inc {};
template<int i, char v, int s, int l>
struct inc<var<i,v>,s,l> {
  typedef var<(i>l) ? i+s : i, v> r;
};
template<typename N, typename M, int s, int l>
struct inc<app<N,M>,s,l> {
  typedef app<typename inc<N,s,l>::r, typename inc<M,s,l>::r> r;
};
template<char v, typename M, int s, int l>
struct inc<abs<v,M>,s,l> {
  typedef abs<v, typename inc<M,s,l+1>::r> r;
};

// substitution with decrementing/incrementing binding levels
template<typename S, typename T, int l> struct subst { typedef S r; };
template<int i, char v, typename T>
struct subst<var<i,v>, T, i> {
  typedef typename inc<T,i-1,0>::r r; // substitute and increment
};
template<int i, char v, typename T, int l>
struct subst<var<i,v>, T, l> {
  typedef var<(i>l) ? i-1 : i, v> r;  // do not substitute but decrement
};
template<typename N, typename M, typename T, int l>
struct subst<app<N,M>, T, l> {
  typedef app<typename subst<N,T,l>::r, typename subst<M,T,l>::r> r;
};
template<char v, typename M, typename T, int l>
struct subst<abs<v,M>, T, l> {
  typedef abs<v, typename subst<M, T, l+1>::r> r;
};

// single step beta-reduction
template<typename T>
struct beta {
  static const bool reduced = false;
  typedef T r;
};
template<bool b, typename T>
struct may_beta {
  static const bool reduced = false;
  typedef T r;
};
template<typename T>
struct may_beta<true, T> {
  typedef beta<T> t;
  static const bool reduced = t::reduced;
  typedef typename t::r r;
};
template<char v, typename M, typename N>
struct beta< app<abs<v,M>,N> > { // beta-redex
  static const bool reduced = true;
  typedef typename beta<typename subst<M,N,1>::r>::r r;
};
template<typename N, typename M>
struct beta< app<N,M> > {
  typedef beta<N> left;
  typedef may_beta<!left::reduced, M> right;
  static const bool reduced = left::reduced || right::reduced;
  typedef app<typename left::r, typename right::r > r;
};
template<char v, typename M>
struct beta< abs<v,M> > {
  typedef beta<M> body;
  static const bool reduced = body::reduced;
  typedef abs<v, typename body::r> r;
};

// multi step beta-reduction
template<typename T, bool rec=true> struct mbeta { typedef T r; };
template<typename T>
struct mbeta<T, true> {
  typedef beta<T> step;
  typedef typename mbeta<typename step::r, step::reduced>::r r;
};

////////////////////////////////////////////////
// Conversion to/from lambda terms

// list
struct nil {};
template<typename X, typename Y> struct cons {};
template<typename T, typename L> struct search {};
template<typename T> struct search<T, nil> {
  typedef nil type;
  static const int index = 0;
};
template<typename T, typename L> struct search<T, cons<T,L> > {
  typedef T type;
  static const int index = 1;
};
template<typename T, typename S, typename L> struct search<T, cons<S,L> > {
  typedef search<T,L> r;
  typedef typename r::type type;
  static const int index = r::index + (r::index != 0 ? 1 : 0);
};

// converter
template<typename T> struct conv {};

// convert to lambda term
template<int i, char c>
struct conv<var<i,c> > {
  typedef term::var<c> term;
};
template<typename N, typename M>
struct conv<app<N,M> > {
  typedef conv<N> left;
  typedef conv<M> right;
  typedef typename term::app<typename left::term, typename right::term> term;
};
template<char v, typename M>
struct conv<abs<v,M> > {
  typedef conv<M> body;
  typedef typename term::abs<v, typename body::term> term;
};

// convert from lambda term
template<typename T, typename index> struct from_term {};
template<char c, typename index>
struct from_term<term::var<c>, index> {
  typedef var<search<term::var<c>,index>::index, c> val;
};
template<typename N, typename M, typename index>
struct from_term<term::app<N,M>, index> {
  typedef from_term<N,index> left;
  typedef from_term<M,index> right;
  typedef app<typename left::val, typename right::val> val;
};
template<char v, typename M, typename index>
struct from_term<term::abs<v,M>, index> {
  typedef from_term<M,cons<term::var<v>,index> > body;
  typedef abs<v, typename body::val> val;
};
template<char c>
struct conv< term::var<c> > {
  typedef typename from_term<term::var<c>,nil>::val debruijn;
};
template<typename N, typename M>
struct conv< term::app<N,M> > {
  typedef typename from_term<term::app<N,M>,nil>::val debruijn;
};
template<char v, typename M>
struct conv< term::abs<v,M> > {
  typedef typename from_term<term::abs<v,M>,nil>::val debruijn;
};

} // debruijn


////////////////////////////////////////////////
// Beta normal form of lambda term

template<typename T>
struct beta {
  template<typename T1>
  struct internal {
    typedef typename debruijn::conv<T1>::debruijn T2;
    typedef typename debruijn::mbeta<T2>::r T3;
    typedef typename debruijn::conv<T3>::term r;
  };
  typedef typename internal<T>::r nf;
};


////////////////////////////////////////////////
// Type inference

namespace typing {

// types
template<int v> struct var {};
template<typename S, typename T> struct fun {};

// type environment
template<char v, typename T> struct ty {};
struct nil {};
template<typename X, typename Y> struct cons {};
template<typename a, typename b> struct concat { typedef b r; };
template<typename a, typename b, typename c>
struct concat<cons<a,b>, c> {
  typedef cons<a, typename concat<b,c>::r> r;
};
template<char v, typename E>
struct lookup {
  static const bool found = false;
  typedef nil type;
};
template<char v, typename T, typename E>
struct lookup< v, cons<ty<v,T>,E> > {
  static const bool found = true;
  typedef T type;
};
template<char v, typename T, typename E>
struct lookup< v, cons<T,E> > {
  typedef lookup<v, E> rec;
  static const bool found = rec::found;
  typedef typename rec::type type;
};

// type substitution
template<typename Subst, typename T> struct tysubst { typedef T type; };
template<int v, typename S, typename R>
struct tysubst< cons<cons<var<v>,S>,R>, var<v> > {
  typedef typename tysubst<R,S>::type type;
};
template<int v, typename S, typename R>
struct tysubst< cons<S,R>, var<v> > {
  typedef typename tysubst< R, var<v> >::type type;
};
template<typename Subst, typename S, typename T>
struct tysubst< Subst, fun<S,T> > {
  typedef typename tysubst<Subst,S>::type domty;
  typedef typename tysubst<Subst,T>::type ranty;
  typedef fun<domty, ranty> type;
};
template<typename Subst, typename S, typename T>
struct tysubst< Subst, cons<S,T> > {
  typedef typename tysubst<Subst,S>::type car;
  typedef typename tysubst<Subst,T>::type cdr;
  typedef cons<car,cdr> type;
};

// unification
template<int v, typename T> struct notin { static const bool r = true; };
template<int v> struct notin< v,var<v> > { static const bool r = false; };
template<int v, typename S, typename T>
struct notin< v,fun<S,T> > {
  static const bool r = notin<v,S>::r && notin<v,T>::r;
};
template<typename E>
struct unify {
  static const bool ok = false;
  typedef nil subst;
};
template<>
struct unify<nil> {
  static const bool ok = true;
  typedef nil subst;
};
template<int v, typename R>
struct unify< cons<cons< var<v>,var<v> >,R> > {
  typedef unify<R> uni;
  static const bool ok = uni::ok;
  typedef typename uni::subst subst;
};
template<typename S, typename T, typename R>
struct unify< cons<cons< fun<S,T>,fun<S,T> >,R> > {
  typedef unify<R> uni;
  static const bool ok = uni::ok;
  typedef typename uni::subst subst;
};
template<int v, typename T, typename R>
struct unify< cons<cons< var<v>,T >,R> > {
  typedef cons<cons<var<v>,T>,nil> s;
  typedef unify<typename tysubst<s,R>::type> uni;
  static const bool ok = uni::ok && notin<v,T>::r;
  typedef cons<cons<var<v>,T>, typename uni::subst> subst;
};
template<int v, typename S, typename T, typename R>
struct unify< cons<cons< fun<S,T>,var<v> >,R> > {
  typedef unify< cons<cons< var<v>,fun<S,T> >,R> > uni;
  static const bool ok = uni::ok;
  typedef typename uni::subst subst;
};
template<typename S, typename T, typename U, typename V, typename R>
struct unify< cons<cons< fun<S,T>,fun<U,V> >,R> > {
  typedef unify< cons< cons<S,U>,cons<cons<T,V>,R> > > uni;
  static const bool ok = uni::ok;
  typedef typename uni::subst subst;
};

// type check
template<typename Term>
struct check {
  template<typename env, typename T, int f>
  struct internal {
    static const bool typed = false;
    typedef nil subst;
    static const int fresh = f;
    typedef nil type;
  };
  template<typename env, char c, int f>
  struct internal<env, term::var<c>, f> {
    typedef lookup<c, env> t;

    static const bool typed = t::found;
    typedef nil subst;
    static const int fresh = f;
    typedef typename t::type type;
  };
  template<typename env, typename N, typename M, int f>
  struct internal<env, term::app<N,M>, f> {
    typedef var<f> ranty;
    typedef internal<env, N, f+1> left;
    typedef internal<env, M, left::fresh> right;
    typedef fun<typename right::type, ranty> funty;
    typedef typename left::subst eq1;
    typedef typename right::subst eq2;
    typedef cons<cons<typename left::type, funty>, nil> eq3;
    typedef typename concat<eq2, eq3>::r eq4;
    typedef typename concat<eq1, eq4>::r eq5;
    typedef unify<eq5> uni;

    static const bool typed = left::typed && right::typed && uni::ok;
    typedef typename uni::subst subst;
    static const int fresh = right::fresh;
    typedef typename tysubst<subst, ranty>::type type;
  };
  template<typename env, char v, typename M, int f>
  struct internal<env, term::abs<v,M>, f> {
    typedef internal<cons<ty< v,var<f> >,env>, M, f+1> body;
    typedef tysubst<typename body::subst, var<f> > domty;

    static const bool typed = body::typed;
    typedef typename body::subst subst;
    static const int fresh = body::fresh;
    typedef fun<typename domty::type, typename body::type> type;
  };

  typedef internal<nil, Term, 0> check_;
  static const bool ok = check_::typed;
  typedef typename check_::type type;
};

} // typing

} // lambda


////////////////////////////////////////////////
// Pretty printing

#include <iostream>

// terms
static const char* LAMBDA = "λ";
template<typename T>
std::ostream& print_left(std::ostream& os, T) {
  return os << T();
}
template<char v, typename M>
std::ostream& print_left(std::ostream& os, lambda::term::abs<v,M>) {
  return os << '(' << lambda::term::abs<v,M>() << ')';
}
template<char v, typename M>
std::ostream& print_left(std::ostream& os, lambda::debruijn::abs<v,M>) {
  return os << '(' << lambda::debruijn::abs<v,M>() << ')';
}
template<typename T>
std::ostream& print_right(std::ostream& os, T) {
  return os << '(' << T() << ')';
}
template<char c>
std::ostream& print_right(std::ostream& os, lambda::term::var<c>) {
  return os << lambda::term::var<c>();
}
template<int i, char c>
std::ostream& print_right(std::ostream& os, lambda::debruijn::var<i,c>) {
  return os << lambda::debruijn::var<i,c>();
}
template<typename T>
std::ostream& print_abs(std::ostream& os, T) {
  return os << '.' << T();
}
template<char v, typename N>
std::ostream& print_abs(std::ostream& os, lambda::term::abs<v,N>) {
  return print_abs(os << v, N());
}
template<char v, typename N>
std::ostream& print_abs(std::ostream& os, lambda::debruijn::abs<v,N>) {
  return print_abs(os << LAMBDA, N());
}
template<char c>
std::ostream& operator<<(std::ostream& os, lambda::term::var<c>) {
  return os << c;
}
template<char c>
std::ostream& operator<<(std::ostream& os, lambda::debruijn::var<0,c>) {
  return (os << c);
}
template<int i, char c>
std::ostream& operator<<(std::ostream& os, lambda::debruijn::var<i,c>) {
  return (os << i);
}
template<typename N, typename M>
std::ostream& operator<<(std::ostream& os, lambda::term::app<N,M>) {
  return print_right(print_left(os, N()) << ' ', M());
}
template<typename N, typename M>
std::ostream& operator<<(std::ostream& os, lambda::debruijn::app<N,M>) {
  return print_right(print_left(os, N()) << ' ', M());
}
template<char v, typename M>
std::ostream& operator<<(std::ostream& os, lambda::term::abs<v,M>) {
  return print_abs(os << LAMBDA, lambda::term::abs<v,M>());
}
template<char v, typename M>
std::ostream& operator<<(std::ostream& os, lambda::debruijn::abs<v,M>) {
  return print_abs(os, lambda::debruijn::abs<v,M>());
}

#include <map>
#include <string>
#include <sstream>

struct varmap {
  varmap():max(0),m(){}
  std::string string_of_var(int v) {
    if (m.count(v) <= 0) m[v] = max++;
    int s = m[v];
    std::ostringstream oss;
    oss << static_cast<char>('a' + s%26);
    if (s/26 > 0) oss << s/26;
    return oss.str();
  }
private:
  int max;
  std::map<int,int> m;
};

// types
std::ostream& print_var(std::ostream& os, int v, varmap& m) {
  return os << m.string_of_var(v);
}
template<typename T>
std::ostream& print_left(std::ostream& os, T, varmap& m) {
  return print_ty(os << '(', T(), m) << ')';
}
template<int v>
std::ostream& print_left(std::ostream& os, lambda::typing::var<v>, varmap& m) {
  return print_var(os, v, m);
}
template<typename T>
std::ostream& print_ty(std::ostream& os, T, varmap&) {
  return os;
}
template<int v>
std::ostream& print_ty(std::ostream& os, lambda::typing::var<v>, varmap& m) {
  return print_var(os, v, m);
}
template<typename S, typename T>
std::ostream& print_ty(std::ostream& os, lambda::typing::fun<S,T>, varmap& m) {
  return print_ty(print_left(os, S(), m) << " -> ", T(), m);
}
template<int i>
std::ostream& operator<<(std::ostream& os, lambda::typing::var<i>) {
  varmap m;
  return print_ty(os, lambda::typing::var<i>(), m);
}
template<typename S, typename T>
std::ostream& operator<<(std::ostream& os, lambda::typing::fun<S,T>) {
  varmap m;
  return print_ty(os, lambda::typing::fun<S,T>(), m);
}
std::ostream& operator<<(std::ostream& os, lambda::typing::nil) {
  varmap m;
  return print_ty(os, lambda::typing::nil(), m);
}


////////////////////////////////////////////////
// Test method

#include <string>
#include <sstream>
#include <functional>

template<typename F> struct tester {
  template<typename T, typename E>
  static bool is(T val, const E& expected, const std::string& msg="",
                 const std::string& file="", const int line=0) {
    F f = F();
    if (f(val) == expected) {
      return true;
    } else {
      if (msg != "") {
        std::cerr << msg << std::endl;
      }
      if (file != "") {
        std::cerr << "[" << file << ", "
                  << "line " << line << "]" << std::endl;
      }
      std::cerr << "  Returned: " << f(val) << std::endl;
      std::cerr << "  Expected: " << expected << std::endl;
      return false;
    }
  }
};
struct printable {
  template<typename T> std::string operator()(T val) {
    std::ostringstream oss;
    oss << val;
    return oss.str();
  }
};
struct testinfo {
  std::string file_; int line_;
  testinfo(const std::string& file, const int line)
    : file_(file), line_(line) {}
  template<typename T>
  bool is(T val, const std::string& expected, const std::string& msg="") {
    return tester<printable>::is(val, expected, msg, file_, line_);
  }
  bool ng(bool val, const std::string& msg="") {
    return tester<std::logical_not<bool> >::is(val, true, msg, file_, line_);
  }
  bool ok(bool val, const std::string& msg="") {
    return ng(!val, msg);
  }
};
#define NG testinfo(__FILE__, __LINE__).ng
#define OK testinfo(__FILE__, __LINE__).ok
#define IS testinfo(__FILE__, __LINE__).is


////////////////////////////////////////////////
// Test

namespace lambda { namespace term {

template<int i> struct s { typedef app<var<'s'>,typename s<i-1>::r> r; };
template<> struct s<0> { typedef var<'z'> r; };
template<int n> struct church {
  typedef abs<'s',abs<'z',typename s<n>::r> > term;
};

} }

int main(void) {
  using namespace std;
  using namespace lambda;

  { using namespace debruijn;
    IS(var<0,'a'>(), "a");
    IS(app<var<0,'a'>,var<0,'b'> >(), "a b");
    IS(abs<'x',var<1,'x'> >(), "λ.1");
  }

  { using namespace term;
    using debruijn::conv;

    typedef abs<'x',abs<'y',abs<'z',
      app<app<var<'x'>,var<'z'> >,app<var<'y'>,var<'z'> > > > > > s;
    typedef abs<'x',abs<'y',var<'x'> > > k;

    typedef app<s,k> sk;
    typedef app<k,s> ks;
    typedef app<sk,k> skk;
    typedef app<app<s,app<app<s,ks>,k> >,skk> sskski;

    typedef church<0>::term _0;
    typedef church<1>::term _1;
    typedef church<2>::term _2;
    typedef church<3>::term _3;
    typedef church<4>::term _4;
    typedef k t;
    typedef abs<'x',abs<'y',var<'y'> > > f;
    typedef abs<'n',app<app<var<'n'>,abs<'x',f> >,t> > if0;
    typedef abs<'m',abs<'n',abs<'s',abs<'z',
      app<app<var<'n'>,app<var<'m'>,var<'s'> > >, var<'z'> > > > > > mul;
    typedef abs<'n',abs<'s',abs<'z',
      app<app<app<var<'n'>,
                  abs<'f',abs<'g',app<var<'g'>,app<var<'f'>,var<'s'> > > > > >,
              abs<'x',var<'z'> > >,abs<'x',var<'x'> > > > > > pred;

    typedef abs<'a',app<var<'a'>,var<'a'> > > o; // infinite loop
    typedef abs<'x',app<var<'f'>,app<var<'x'>,var<'x'> > > > yy;
    typedef abs<'f',app<yy,yy> > y;

    typedef abs<'r',abs<'n',
      app<app<app<if0,var<'n'> >,_1>,
          app<app<mul,var<'n'> >,
              app<var<'r'>,app<pred,var<'n'> > > > > > > fact;

    // syntax

    IS(var<'a'>(), "a");
    IS(app<var<'a'>,var<'b'> >(), "a b");
    IS(abs<'x',var<'x'> >(), "λx.x");

    IS(k(), "λxy.x");
    IS(conv<k>::debruijn(), "λλ.2");
    IS(conv<conv<k>::debruijn>::term(), "λxy.x");

    IS(s(), "λxyz.x z (y z)");
    IS(conv<s>::debruijn(), "λλλ.3 1 (2 1)");
    IS(conv<conv<s>::debruijn>::term(), "λxyz.x z (y z)");

    IS(church<0>::term(), "λsz.z");
    IS(church<1>::term(), "λsz.s z");
    IS(church<2>::term(), "λsz.s (s z)");
    IS(church<3>::term(), "λsz.s (s (s z))");

    // reduction

    IS(beta<skk>::nf(), "λz.z");
    IS(beta<sskski>::nf(), "λzz.z (z z)",
       "we have no alpha-conversion");
    IS(beta<app<app<sskski,var<'a'> >,var<'b'> > >::nf(), "a (a b)");

    // IS(beta<app<o,o> >::nf(), "this yields compile error");
    IS(beta<app<app<k,var<'c'> >,app<o,o> > >::nf(), "c",
       "leftmost strategy is normalizing");

    IS(beta<app<app<app<if0,_0>,var<'a'> >,var<'b'> > >::nf(), "a");
    IS(beta<app<app<app<if0,_1>,var<'a'> >,var<'b'> > >::nf(), "b");
    IS(beta<app<app<mul,_2>,_2> >::nf(), "λsz.s (s (s (s z)))");
    IS(beta<app<app<y,fact>,_3> >::nf(), "λsz.s (s (s (s (s (s z)))))");

    // typing

    NG(typing::check<o>::ok,
      "infinite loop is not typeable");
    NG(typing::check<y>::ok,
      "recursive function is not typeable");

    OK(typing::check<k>::ok);
    IS(typing::check<k>::type(), "a -> b -> a");
    OK(typing::check<s>::ok);
    IS(typing::check<s>::type(), "(a -> b -> c) -> (a -> b) -> a -> c");
    OK(typing::check<skk>::ok);
    IS(typing::check<skk>::type(), "a -> a");
    OK(typing::check<_1>::ok);
    IS(typing::check<_1>::type(), "(a -> b) -> a -> b");
    OK(typing::check<_2>::ok);
    IS(typing::check<_2>::type(), "(a -> a) -> a -> a");
    OK(typing::check<_3>::ok);
    IS(typing::check<_3>::type(), "(a -> a) -> a -> a");
    OK(typing::check<_4>::ok);
    IS(typing::check<_4>::type(), "(a -> a) -> a -> a");
  }

  return 0;
}