An Extension to ML to Handle Bound Variables in Data Structures: Preliminary Report

Most conventional programming languages have direct methods for representing first-order terms (say, via concrete datatypes in ML). If it is necessary to represent structures containing bound variables, such as λ-terms, formulas, types, or proofs, these must first be mapped into first-order terms, and then a significant number of auxiliary procedures must be implemented to manage bound variable names, check for free occurrences, do substitution, test for equality modulo alpha conversion, etc. We shall show how the applicative core of the ML programming language can be enhanced so that λ-terms can be represented more directly and so that the enhanced language, called MLλ, provides a more elegant method of manipulating bound variables within data structures. In fact, the names of bound variables will not be accessible to the MLλ programmer. This extension to ML involves the following: introduction of the new type constructor 'a => 'b for the type of λ-terms formed by abstracting a parameter of type 'a out of a term of type 'b; a very restricted and simple form of higher-order pattern matching; a method for extending a given data structure with a new constructor; and, a method for extending function definitions to handle such new constructors. We present several examples of MLλ programs.