Lambda the Ultimate

... it may be worth observing that the very cool stuff being done by the Acute project uses Fresh O'Caml as its launching-off point.

I see two things here. First, there are the scope properties of the name-binders. These could be expressed with dependent types, such that only scope-consistent expressions typecheck. The resulting code would likely be significantly more verbose, though.

Second, there are the equivalance properties of values involving name binders. There are a number of possibilities for implementing this in a more general programming language. You could write a "mod-alpha-conversion" equivalance test that operates on such terms, treating this as a wider relation than equality (where some alpha-equivalant terms would be considered unequal).

Or, if your language supported finite circular terms (with recursive equality implemented internally via bisimulation), you could recognize all alpha-equivalant terms as equal. I implemented this recently and verified that it works, though I'm not sure it's a good idea. Some pointers on this topic are summarized in http://lists.seas.upenn.edu/pipermail/types-list/2004/000352.html.

Specifically, you could implement binder data types (with alpha-equivalance but not dependent typing) like this:

term:=union
   lambda:term
   application:type{func:term,parm:term}
   reference:term // A name reference, possibly circular.
   const:int
myterm:=lambda(application(reference(myterm),const(7)))

Alternatively, there is the possibility of using first-class equivalance types, though I can't see how one would implement this in a way that doesn't require programmers to constructively prove horrific things in their code.

I disagree with Tim that inbuilt provision for name binding is an "extremely special case". For example, I think it is fair to say that the main motivation behind user-defined datatype declarations in functional languages is to be able to easily represent the syntax trees of some object language. It therefore seems natural that these types ought to be equipped with the ability to represent name binding, commonplace as that is.

A similar argument applies to algorithms which manipulate such structures. In common pencil-and-paper practice we often assume the Barendregt convention, where the names of free and bound variables are kept distinct. (A good example is given on page 14 of Ariola's paper cited by Tim, where the author is talking about contexts.) When writing metaprograms which implement such algorithms, we usually cannot just assume that such conventions hold. We therefore believe that as much automatic support as possible should be provided in order that the actual `algorithmic essence' is not obscured by tedious matters to do with names.

As far as Fresh O'Caml goes, we do not claim that it is the be-all-and-end-all: there are still various issues which we need to address in the near future, and there are no doubt situations which it cannot handle. However, we do believe that once it is polished then it will provide a robust and elegant solution to this rather long-standing problem.

Feedback from users will be most welcome! There should be a release based on O'Caml 3.08 by the end of the year, which will incorporate a whole slew of bugfixes.