Church Numerals in Scala

As everyone knows (see http://en.wikipedia.org/wiki/Church_encoding), in pure lambda one can define natural numbers out of nothing, like this:

0 ≡ λ f λ x . x
1 ≡ λ f λ x . f x
2 ≡ λ f λ x . f (f x)
3 ≡ λ f λ x . f (f (f x))
etc.

At our BACAT meeting yesterday, there was a question, for typed lambda, how can one express natural numbers, and also how can one interpret them in a Cartesian-closed category?

The answer to this question turned out to be trivial, but we also had managed to express it in Scala:

class TypedLambda[T] {
  type TT = T => T
  type Church = TT => TT
  val cero: Church = f => x => x
  def succ(n: Church) = f => n(f) compose f
  val uno = succ(cero)
  val dos = succ(uno)
  val tres = succ(dos)
}

Looks neat, eh?

The alternative approach can be found in Jim McBeath's post.