/dev/code

There has been some discussion on Lambda the Ultimate about a new language that Guy Steele (of Scheme fame, among other things) has been working on at Sun Labs. It is called Fortress and is targeted towards the same application domain as Fortran. This is *not* Fortran, however. Take a look at this list of features (shamelessly cut&pasted from LtU):

an advanced component and linking architecture

objects and traits (which look similar to Moby and Scala)

multiple dispatch

type inference

parameterized types

extensible syntax

first-class functions

proper tail calls

labelled jumps, exceptions

contracts

some interesting parallelism features (including futures, parallel loops, atomicity primitives, transactions)

matrices

comprehensions

bignums, fixnums (signed and unsigned), floating-point, imaginary and complex numbers

dimensions

It is nice to see type inference popping up again, as well as proper tail calls, parameterized types and contracts (kinda sounds like Nice except for the tail calls). I have only glanced at the spec but one of the interesting things that popped out is that do-loops are assumed to execute in parallel by default. It will be interesting to see what happens with this language.

Well, I was doing pretty well with the lambda-calculus-in-ocaml thing until I tried to define XOR for Church booleans. I defined it as:
λa.λb.a (not b) b

I worked this out on paper and it seems to be correct. It fails when I define it in OCAML as:
let xorx = fun a b -> a (notx b) b;;

When I say it fails, I mean that I get a type error when I try something like this:
(xorx fls tru) "true" "false"
(or if I just call my print_cbool function). It works if I define xorx as:
let xorx = fun a b -> a (notx b) (b tru fls);;
Since b is supposed to be a boolean, (b tru fls) should be redundant.

A patient gentleman on the #ocaml channel tried to explain to me why OCAML wasn't good for doing Church booleans, but when I started hearing terms like "predicative polymorphism" and "prenex normal form" I realized that I wasn't going to understand the explanation. I hope I will understand some of these terms better by the time I finish Types and Programming Languages.

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

I kept getting this message from OCAML saying:
This expression has type map_path but is here used with type 'a
The type constructor map_path would escape its scope.

The error was occurring when I was trying to add a record to a Hashtbl. Here is a shorter piece of code that will generate the same error:

let ht=Hashtbl.create 100;;
type footype={foo1:int;foo2:int};;
Hashtbl.add ht "foo" {foo1=5;foo2=10};;

You'll get an error that the constructor footype would escape its scope. The thing that seems odd to me is that this error occurs because the hash table was created before the type was known, even though the hash table hasn't really been bound to a specific type yet. If you just reverse the order of the first two statements, everything works:

type footype={foo1:int;foo2:int};;
let ht=Hashtbl.create 100;;
Hashtbl.add ht "foo" {foo1=5;foo2=10};;

Although the error message is a bit confusing, the error itself makes sense when you think about it. The reason it is an error is that if you had to explicitly declare the type of the hash table when you created it, you wouldn't be able to because footype hasn't been declared yet. Once you realize that, even the error message makes sense. The type is declared after the hash table, so it was not "in scope" when the table was created. This makes more sense if you think of the statements as really being nested inside successive lets, although this isn't valid OCAML syntax:

let ht=Hashtbl.create 100 in
   let type footype={foo1:int;foo2:int} in
      Hashtbl.add ht "foo" {foo1=5; foo2=10};
      ht;;

Written like this, you see that the scope of footype would really be within the scope of "let ht=".. and you shouldn't be able to see footype outside of the let. Since the let returns the table, though, you would be violating the scoping rules. Again, that's not exactly how OCAML does it, but it makes sense when you think of it this way.