A language experiment from Cambridge · 2003–2005

Names and binders, made explicit.

Fresh Objective Caml extended OCaml with types of names, abstraction expressions, and pattern matching over binders—tools designed for programs that manipulate programming languages.

Download recovered source Read the examples

binding.fml

type var = t name;;

type term =
  Var of var
| Lam of <<var>>term
| App of term * term;;

let identity =
  Lam(<<x>>(Var x));;

abstraction type

The central problem

Programs about programs have to represent binding.

Compilers, proof assistants, interpreters, and metaprogramming tools all manipulate syntax containing bound names. Conventional abstract syntax leaves alpha-equivalence, capture avoidance, and fresh-name generation to the programmer. Fresh OCaml moved those concerns into the type system and runtime representation.

One change in notation

A binder becomes a value you can type and match.

Conventional representation

type term =
  Var of string
| Lam of string * term

The relationship between the string and the term is only a convention. Renaming and capture avoidance are manual.

Fresh OCaml representation

type var = t name;;

type term =
  Var of var
| Lam of <<var>>term

The abstraction is explicit. Fresh-name generation, comparison, and pattern matching can respect binding structure.

name

Name types

Typed object-language names instead of unstructured strings.

<<x>>e

Abstraction values

A direct representation of a name binding in an expression.

fresh

Fresh generation

Create a name guaranteed to be fresh for the current computation.

match

Binder-aware patterns

Deconstruct abstraction values with ordinary functional style.

Seven recovered programs

The idea is clearest in code.

The surviving examples cover lambda calculi, Hindley–Milner type inference, MetaML, normalization by evaluation, and the Pi-calculus.

Explore source files

Recovered release

3.08.2+414 January 2005 · 2.6 MB source archive

Preserved for study, not modern deployment.

This release was based on OCaml 3.08.2 and was reported to build on Linux and Mac OS X systems of its era. Contemporary toolchains, operating systems, and OCaml packages have changed substantially.

tar fxz fresh-ocaml-3.08.2+4.tar.gz
cd fresh-ocaml-3.08.2+4
./configure
make world

Download the recovered archive