Meta-Programming with Scala Part I: Addition

This is the code for the blog entry Meta-Programming with Scala Part I: Addition

package michid;

object Metaaddition {
  // Church encoding of natural numbers
  type _0[s[_], z] = z
  type _1[s[_], z] = s[z]
  type _2[s[_], z] = s[s[z]]
  type _3[s[_], z] = s[s[s[z]]]

  // Addition for this encoding
  type plus[m[s[_], z], n[s[_], z], s[_], z] = n[s, m[s, z]]

  abstract class Zero
  abstract class Succ[T]

  // Use of infix notation for more convinient syntax
  type +[m[s[_], z], n[s[_], z]] = plus[m, n, Succ, Zero]

  // See http://michid.wordpress.com/2008/03/12/puzzle-the-depth-of-a-type-solution/
  def nullval[T] = null.asInstanceOf[T];

  trait Rep[T] {
      def eval: int
  }

  implicit def toRep0(n: Zero) = new Rep[Zero] {
    def eval = 0
  }

  implicit def toRepN[T](n: Succ[T])(implicit f: T => Rep[T]) = new Rep[Succ[T]] {
    def eval = f(nullval[T]).eval + 1
  }

  def depth[T <% Rep[T]](n: T) = n.eval

  def main(args: Array[String]) {
    type two = _2[Succ, Zero]
    println(depth(nullval[two]))  // prints 2

    println(depth(nullval[_2 + _2])) // prints 4
    println(depth(nullval[_2 + _3])) // prints 5
  }

}