Friday, August 05, 2005

alphaCaml

I've written my first Cαml program: a little lambda-calculus term manipulation language and interpreter. Since it's a language for manipulating terms, there's an object language (the lambda calculus) and a meta-language (the term manipulation language). Expressions in the meta-language evaluate to lambda calculus terms; for example, cps e evaluates the expression e to get a term and then converts the term to continuation-passing style.

Here's the data definition and binding specification of the object language datatype:
sort var

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

type lambda binds var = atom var * inner term
The declaration sort var declares a disjoint universe of atoms that will be used as lambda calculus variables. The type lambda is a binding datatype: it binds atoms of sort var, which are then in scope in the right-hand conjunct of the product type (the keyword inner indicates that all the bindings in lambda are in scope in the term). This binding specification actually automatically generates a bunch of Ocaml datatype and library definitions, including:
type term =
| Var of var
| Lam of opaque_lambda
| App of term * term
and var = Var.Atom.t
and lambda = var * expression
and opaque_lambda

val create_lambda : lambda → opaque_lambda
val open_lambda : opaque_lambda → lambda
By making the contents of the Lam constructor opaque, it forces programmers to use open_lambda whenever they need to get at its contents, which has the side effect of freshening all of its bound names. This alleviates the programmer from having to avoid capture explicitly, since bound names are kept unique.

Now here's a term manipulation function written in Cαml. (In fact, this is really just an Ocaml program, since the only extension to Ocaml is the binding specification language. Beyond that, Cαml is just a library.)
let make_lambda : var → term → term = fun v body →
Lam (create_lambda (v, body))

let rec beta : term → var → term → term = fun t x arg →
match t with
| Var x' when Var.Atom.equal x x' → arg
| Var _ → t
| App (l, r) → App (beta l x arg, beta r x arg)
| Lam lam → let (x', body) = open_lambda lam in
make_lambda x' (beta body x arg)

let rec reduce : term → term = function
| App ((Lam lam), rand) when isValue rand →
let (x, body) = open_lambda lam in
beta body x rand
| App(rator, rand) when (isValue rator) && (isValue rand) →
raise No_redex
| App(rator, rand) when (isValue rator) →
App(rator, reduce rand)
| App(rator, rand) →
App(reduce rator, rand)
| _ → raise No_redex
There's no need to implement capture-avoiding substitution, because every time an abstraction is opened, its bound variable is automatically freshened by open_lambda.