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.