## Fresh O'Caml

Fresh O'Caml aims to provide the features of the Objective Caml language (with the exception of native-code compilation) together with:

• a type of names for representing object-level bindable names;
• abstraction expressions for representing object-level binding;
• pattern-matching for deconstructing abstraction values;

Fresh O'Caml is Mark Shinwell's sucessor to Andrew Pitts's last summer's blockbuster FreshML. It's experimental, but Tom tells me it's very cool, and I trust him. This work comes out of... no, not INRIA, enclave of O'Caml High Acolytes, but rather the University of Cambridge Computer Laboratory Theory and Semantics Group. Here are the obligatory tasty paper morsels:

More papers than you can shake a stick at on Fresh O'Caml's dad, FreshML, are also available.
Finally, there's a mailing list you can join for information, updates, and discussion about FreshML and Fresh O'Caml

## Comment viewing options

### On a Related Note...

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

### Acute

Neat! Thanks for the pointer Paul! I'll definitely add this to my running list of Cool Projects To Check Out.

### Generalization?

This seems like an extremely special-case feature to add to a programming language. When presented with something like this, it's useful to consider what would be needed to be able to write this sort of code in a more general language without special-case support.

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

Zena Ariola, in http://www.cs.uoregon.edu/~ariola/cycles.ps, describes this representation of name references as the "Bourbaki" style, refering to mathematical texts where graphs of lambda terms were drawn with lines between lambda terms instead of using traditional names for variables.

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.

### Not really a special case...

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.