ML

ML (short for Meta Language) is one of the most consequential programming languages in computing history. Created by Robin Milner and colleagues at the University of Edinburgh starting in 1973, ML began life not as a general-purpose language but as the metalanguage of a theorem prover. From that narrow origin it introduced ideas - most famously sound, automatic type inference - that reshaped how programming languages are designed. Today ML survives less as a single language than as the head of a large family: Standard ML, Caml, OCaml, and F# are all its direct descendants, and its fingerprints are visible in Haskell, Rust, Scala, and many others.

History & Origins

ML was born from the practical needs of automated reasoning. When Robin Milner arrived at the University of Edinburgh in 1973, he set out to build a successor to Stanford LCF (Logic for Computable Functions), an interactive proof-checking system. The challenge was that users needed a way to write proof tactics - programs that manipulate and combine proofs - in a language that was both expressive and safe. Milner’s answer was ML, a small functional language that served as both the metalanguage and the command (REPL) language of the new Edinburgh LCF system.

Milner was assisted by research associates Lockwood Morris and Malcolm Newey, both postdocs who had come from Stanford, and later by Michael Gordon and Christopher Wadsworth. The language and the LCF system were described together in the 1979 book Edinburgh LCF.

The Type Soundness Problem

A central requirement of LCF was that theorems be represented as an abstract data type whose only constructors were valid inference rules. For this guarantee to hold, the language had to ensure that programs could not subvert the type system - you should never be able to fabricate a “theorem” by misusing types. This requirement drove Milner toward a strong, static type system, and to the realization that types could be inferred rather than written out by the programmer.

Milner’s 1978 paper, A Theory of Type Polymorphism in Programming, presented the algorithm (building on earlier work by J. Roger Hindley) that the world now calls Hindley-Milner type inference. It was both practical and provably sound, captured in Milner’s famous slogan that “well-typed programs cannot go wrong.”

From Proof Tool to Programming Language

As ML proved useful, it began to escape the confines of LCF. Around 1980, graduate student Luca Cardelli built a standalone ML compiler - initially called “ML under VMS,” or VAX ML - written in Pascal and targeting VAX machine code via a functional abstract machine (FAM). This let people use ML without the theorem prover. Meanwhile, the related Hope language (Rod Burstall, David MacQueen, and Don Sannella, around 1980) introduced algebraic datatypes, pattern matching, and clausal function definitions - features that would soon be absorbed into the ML lineage.

By the early 1980s several incompatible ML dialects existed. A 1982 meeting on “ML, LCF, and Hope” set out to reconcile them, and in 1983 Milner began the design of Standard ML, which culminated in the formally specified Definition of Standard ML (1990, revised 1997).

Design Philosophy

ML was shaped by a handful of ideas that were radical for their time and are now mainstream:

• Types you don’t have to write. The compiler reconstructs the most general type of every expression, so programs are statically and strongly typed without the annotation burden of languages like Pascal or C.
• Parametric polymorphism. Functions can operate uniformly over any type, expressed with type variables, so a single length function works on a list of anything.
• Safety as a guarantee, not a hope. The type system was designed so that well-typed programs cannot violate the abstractions they are built on - the very property LCF needed to trust its proofs.
• Functions as first-class values. ML treats functions as ordinary data that can be passed, returned, and stored, embracing the higher-order style.
• A blend of pragmatism and theory. Unlike purely theoretical calculi, ML included mutable references, exceptions, and eager evaluation, making it usable for real systems while remaining grounded in formal semantics.

Key Features

Hindley-Milner Type Inference

ML’s signature contribution. The programmer writes little or no type information, and the compiler infers the most general type:

(* Inferred as: int -> int -> int *)
fun add x y = x + y

(* Inferred as polymorphic: 'a list -> int *)
fun length [] = 0
  | length (_ :: xs) = 1 + length xs

Algebraic Data Types and Pattern Matching

Adopted from the Hope tradition, these let programmers model structured data and deconstruct it clause by clause - a style that has since spread far beyond functional languages:

datatype 'a tree = Leaf
                 | Node of 'a tree * 'a * 'a tree

fun size Leaf = 0
  | size (Node (l, _, r)) = 1 + size l + size r

Exceptions

ML introduced a structured exception mechanism for handling errors and non-local control flow, a feature later widely copied:

exception NotFound

fun find p [] = raise NotFound
  | find p (x :: xs) = if p x then x else find p xs

Mutable References

Although functional in spirit, ML was never purely so. It provides explicit mutable cells, keeping side effects visible and controlled:

val counter = ref 0
val () = counter := !counter + 1

Interactive Use

From the start ML was an interactive system - the metalanguage of LCF was typed at a prompt. This REPL-driven, “type a definition and immediately use it” workflow became a hallmark of the ML family.

Evolution

ML did not so much evolve as radiate. The original Edinburgh ML branched into several enduring lineages:

Each branch kept ML’s core - type inference, pattern matching, and an emphasis on safety - while adapting to new goals. Standard ML pursued a rigorous formal definition and a powerful module system; the Caml branch chased performance and practicality, leading to OCaml; and F# carried the tradition into industrial .NET development.

Current Relevance

The original Edinburgh ML is now a historical artifact, no longer maintained as a distinct product. Its relevance today is enormous but indirect: it is the ancestor that every modern ML-family language traces back to. Standard ML remains a staple of programming-language courses and compiler research; OCaml powers production systems in finance, formal verification, and tooling; and F# is a first-class language on .NET. More broadly, the type inference, pattern matching, exhaustiveness checking, and algebraic data types that ML pioneered are now considered table stakes in modern language design, appearing in Rust, Swift, Scala, Kotlin, TypeScript, and beyond.

Why It Matters

ML’s importance is hard to overstate. It demonstrated that a language could be strongly and statically typed and convenient, dissolving a tradeoff that earlier languages took for granted. Its Hindley-Milner type system is one of the most studied and reused ideas in computer science. Robin Milner’s contributions to ML - alongside his later work on concurrency - earned him the 1991 ACM Turing Award. And as the progenitor of an entire language family, ML stands as a rare case of a research tool, built to check mathematical proofs, that quietly reshaped the everyday practice of programming.

Learning More

Because the original ML is best understood through its living descendants, readers can explore:

• Standard ML - the formally defined, classroom-favorite dialect
• OCaml - the practical, high-performance branch
• F# - ML for the .NET ecosystem

Together these languages keep Robin Milner’s 1973 invention very much alive.