When I find something interesting and new, I post it here - that's mostly programming, of course, not everything.

Thursday, April 28, 2011

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))

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.


Subscribe To My Podcast