A very useful feature of functional programming languages such as OCaml (http://caml.inria.fr/ocaml) or Haskell (http://www.haskell.org) is the facility for programmers to declare their own algebraic data types and to specify functions on that data using pattern-matching. This makes them especially useful for metaprogramming, that is, writing programs that manipulate programs, or more generally, expressions in formal languages. In this context the functional programming language is often called the meta-level language, while the language whose expressions appear as data in the functional programs is called the object-level language. We already noted at the beginning of Chapter 8 that object-level languages often involve name binding operations. In this case we may well want meta-level programs to operate not on object-level parse trees, but on their α-equivalence classes. OCaml or Haskell programmers have to deal with this issue on a case-by-case basis, according to the nature of the object-level language being implemented, using a selfimposed discipline. For example, they might work out some ‘nameless’ representation of α-equivalence classes for their object-level language, in the style of de Bruijn (1972). When designing extensions of OCaml or Haskell that deal more systematically with this issue, three desirable properties come to mind:

1. • Expressivity. Informal algorithms for manipulating syntactic data very often make explicit use of the names of bound entities; when representing α-equivalence classes of object-level expressions as meta-level data, one would still like programmers to have access to object-level bound names.

2. […]