ML: From a Proof Metalanguage to Polymorphic Programming

The name ML comes from “metalanguage.” It initially allowed users to write proof strategies and interact with a proof system. From 1973, Robin Milner and his colleagues at the University of Edinburgh developed the Logic for Computable Functions system, LCF, separating the language used to program proof procedures from the logical expressions being proved. Early team members included Malcolm Newey and Lockwood Morris; Michael Gordon and Christopher Wadsworth subsequently joined.

The researchers needed flexibility and trustworthiness. Users had to combine proof steps and write repeatable strategies, while an erroneous strategy program should not be able to turn an arbitrary proposition into a theorem. ML therefore combined functions, type checking and controlled construction of data. It gradually extended beyond a single proof system and became a starting point for general-purpose language development.

References: [1] [5]

In LCF, theorems were represented by the abstract type thm. Users obtained values of this type through operations representing valid inference rules, while its internal representation remained hidden. Strategies assembled from these operations could be complex, but could not directly manufacture a theorem value without a derivation. The trusted boundary lay in the kernel implementing the inference rules and its type interface.

Proof search frequently reached dead ends, so early ML included a mechanism for reporting and catching failures: when one strategy failed, a program could try another. Functions could also be passed as ordinary data, allowing smaller strategies to form larger ones. Alongside its functional core, the language included mutable variables and loops, supporting expression-based computation and operations requiring state.

References: [1] [5]

Milner’s 1978 paper systematically described parametric polymorphism and type inference. The function map applies a function to each element of a list. If f adds one to an integer, applying map to f and [1,2,3] gives [2,3,4]. If f instead turns an integer into a true-or-false test, the output is a Boolean list. The traversal stays the same while element and result types change.

The compiler derives types from constraints connecting operations such as taking a list’s head, constructing a list and calling a function. Users need not repeat declarations at every position. Input-list elements must match f’s argument type, and output elements must match its result type. The paper presents a type-checking algorithm and a soundness argument ruling out type confusion such as treating an integer as a function.

References: [2]

The ML used in early LCF ran in a DEC-10 environment through translation into Lisp code. From 1980, Luca Cardelli developed a VAX implementation whose compiler and runtime were written in Pascal and generated machine code. This moved ML from an implementation tied to the proof system toward an independently distributed tool for a wider range of programs.

The surviving Edinburgh ML distribution instructions from March 1982 specifically target VAX-VMS. Users copied files from floppy disks, ran a linking command to build the system and entered the ML environment through a command file. The instructions list array and lambda-calculus example programs and discuss the ML heap, garbage-collection space and the Pascal heap used during compilation. Distribution involved a concrete installation package, an entry point and storage-management requirements.

References: [1] [3]

Extensions accumulated by different implementations also produced differences. In his June 1983 second-draft manuscript, Milner recalled that some parts of the early DEC-10 version were incomplete and others redundant. Cardelli’s VAX version corrected several problems, while the HOPE language offered additional design ideas. In April 1983, encouraged by Bernard Sufrin, Milner put forward a preliminary proposal to bring ML together.

Subsequent discussion incorporated views from Rod Burstall, Cardelli, David MacQueen, Gordon and other researchers. Standardization aimed to organize syntax, types, state and program structure while retaining the language’s basic character. These discussions moved ML from separately extended implementations toward a jointly designed standard language.

References: [4]

The Definition of Standard ML, published in 1990, provided a formal account of the standard language. Its 1997 revision was authored by Milner, Mads Tofte, Robert Harper and MacQueen. It separates the core language from the module language, using static semantics to specify types and name binding and dynamic semantics to describe execution. Implementers gained a common reference extending beyond the behavior of any one compiler.

ML’s legacy includes static type inference with relatively few explicit declarations, reusable polymorphic functions, abstract types and modular organization. Standard ML is the standardized branch of this development, while other ML-family languages followed their own paths. Early proof tools, the spread of implementations in the 1980s and later formal definitions together trace its movement from a specialized metalanguage to general-purpose programming.

References: [5]