/dev/code

I've been working my way through Types and Programming Languages (TAPL). Chapter 5 discusses the untyped lambda calculus, which is a theoretical representation of computation that predates computers.

There are a number of lambda calculus tutorials out on the web, including this one (PDF). Basically, lambda calculus lets you define functions like this:

λx.x
This is a function that takes a single argument x and returns x. A function can only take a single argument, but you can nest functions to handle multiple arguments, like this:

λx.λy.x*y
In this case, the outermost function's return value is a function that multiplies its argument by x.So (λx.λy.x*y) 5 3 becomes (λy.5*y) 3 which becomes 15. This method of converting multiple arguments into nested functions is called currying.

The thing I find really interesting is that it is very easy to translate basic lambda calculus expressions into OCAML and try them out. For example, I'll start with Church Booleans.

A Church Boolean is a method of defining true and false as functions. Both functions take two arguments (using the nested notation). True returns its first argument, while false returns its second:

true = λt.λf.t
false = λt.λf.f

This translates very easily into OCAML (I am using an older form of function declaration because it matches more closely with the lambda calculus form):

let tru = fun t f -> t;;
let fls = fun t f -> f;;

Now, tru and fls are not static values, but functions. This function prints Church booleans as "true" or "false":

let print_cbool = fun b -> print_string (b "true" "false");;

You can define boolean and in lambda calculus as:

and = λa.λb.a b fls
Each argument to this function is a boolean function like tru or fls. If a is tru, then it returns its first argument, which is b, otherwise it returns fls. If b is tru, then the result of a and b is tru, otherwise it is fls.
In a similar manner, you can define or and not as:
or = λa.λb.a tru b
not = λa.a fls tru

In OCAML, these can be defined as:

let andx = fun a b -> a b tru;;
let orx = fun a b -> a tru b;;
let notx = fun a -> a fls tru;;

You can then play around with various expressions like:

print_cbool (andx tru tru);;
print_cbool (andx tru fls);;
print_cbool (andx (notx fls) tru);;

Booleans are fun, but it gets much more interesting when you get into numbers. Church numerals are formed by a combination of two functions s and z. The s function is the "successor" function and z is the zero function. The first few church numerals are defined as:
C(0) = λs.λz.z
C(1) = λs.λz.s z
C(2) = λs.λz.s (s z)
C(3) = λs.λz.s (s (s z))

If you think of s as "1+" and z as 0, then C(0) = 0, C(1) = 1+ 0, C(2) = 1+ (1+ 0), etc.
I defined a function p1 as shorthand for adding 1, and created a print_church function to display an integer version of a Church numeral:

let p1 = (+) 1;;
let print_church = fun c -> print_int (c p1 0);;

In this case, p1 is a partial function, the (+) operator takes two arguments, but since I only supplied 1, p1 actually returns a function that adds 1 to its argument.

Now, since I don't want to manually define each Church numeral, I defined a simple function that generates Church numerals:

let rec church = fun n s z->
  if n = 0 then z
  else s (church (n-1) s z);;

If you call print_church (church 55) you'll see 55.

It is also possible to define the addition operation. Since a Church numeral is essentially defined by adding 1 over and over starting from 0, addition can just be defined as adding 1 over and over starting from another number, like this:
plus=λa.λb.λs.λz.a s (b s z)
That is, instead of the usual z function, let a's z function be the evaluation of b (instead of counting from 0, a is calculated by starting from b). In OCAML, this can be defined as:

let plus = fun a b s z -> a s (b s z)

If you call print_church (plus (church 12) (church 34)) you should see a result of 46.
Multiplication can be defined in a similar way. Instead of adding 1 every time, you add b, like this:
mult=λa.λb.λs.λz.a (b s) z
In OCAML, this is:

let mult = fun a b s z -> a (b s) z;

Again, using print_church, you can test the mult function. If you call print_church (mult (church 12) (church 34)) you should see 408.

You can get a little closer to the lambda calculus notation by using only single arguments in function definitions:

let tru = fun t -> fun f -> t;;
let fls = fun t -> fun f -> f;;