ML started life around 1973 at the University of Edinburgh, not as a general-purpose language but as the command language of a theorem prover. Robin Milner's ML language for the LCF prover was meant to let mathematicians write proof tactics safely, and the solution Milner found, a static type system the compiler could infer on its own, turned out to be one of the most influential ideas in programming language design. The name stands for Meta Language.
Robin Milner's ML language for the LCF prover
LCF stands for Logic for Computable Functions, a logic proposed by Dana Scott. Milner had worked on an earlier LCF system at Stanford. At Edinburgh he led a team, including Malcolm Newey, Lockwood Morris, Michael Gordon and Christopher Wadsworth, that built Edinburgh LCF in the mid-1970s. Users needed a way to program proof strategies without ever being able to forge a theorem.
The trick was the type system. Theorems were values of an abstract type thm, and the only functions that could create a thm were the inference rules of the logic. Any tactic, however clever, could only build theorems through those rules. To make this practical, ML had to be strongly typed but not tedious, so Milner developed an algorithm that infers the most general type of an expression. He published it in 1978 in "A Theory of Type Polymorphism in Programming". J. Roger Hindley had found a similar result for combinatory logic in 1969, so the system is now called Hindley-Milner.
Key features of ML
- Type inference: you rarely write types, yet every expression has one, checked at compile time.
- Parametric polymorphism: a function like
lengthworks on lists of any element type. - Algebraic data types and pattern matching, added and refined in successors such as Hope and Standard ML.
- Exceptions and mutable references, so ML is functional by default but not pure.
- A module system with structures, signatures and functors in Standard ML, designed largely by David MacQueen.
fun length [] = 0
| length (_ :: xs) = 1 + length xs;
(* val length = fn : 'a list -> int *)
fun map f [] = []
| map f (x :: xs) = f x :: map f xs;
(* val map = fn : ('a -> 'b) -> 'a list -> 'b list *)No type annotations appear in that code, yet the compiler reports that map takes a function from 'a to 'b and a list of 'a, and returns a list of 'b.
From LCF ML to Standard ML, Caml and OCaml
Once ML escaped the prover, several dialects appeared. Work on a common Standard ML began in 1983, led by Milner with contributions from MacQueen, Mads Tofte, Robert Harper and others. Its formal definition, published in 1990 and revised in 1997, specified the whole language mathematically.
| Year | Milestone |
|---|---|
| around 1973 | ML created for Edinburgh LCF |
| 1983 | Standard ML design effort begins |
| 1985 | Caml developed at INRIA in France |
| 1990 | The Definition of Standard ML published |
| 1996 | Objective Caml (OCaml) released |
| 1997 | Revised Definition (SML '97) |
In France, INRIA built Caml, then Caml Light, and in 1996 OCaml, which added objects and a fast native-code compiler. Microsoft Research's F#, first released around 2005, brought the OCaml core to .NET.
Where ML-family languages are used
Theorem proving never left the family: HOL and Isabelle are written in Standard ML, and Coq (now Rocq) is written in OCaml. OCaml runs trading systems at Jane Street, powers the Tezos blockchain, and was used to build Facebook's Hack and Flow type checkers. Rust's first compiler was written in OCaml before Rust became self-hosting. Standard ML compilers such as SML/NJ, MLton and Poly/ML are still maintained.
Influence and legacy
Milner received the Turing Award in 1991, partly for ML. Type inference, algebraic data types and pattern matching spread from ML into Miranda and Haskell, then into mainstream languages: Scala, Swift, Kotlin, Rust and TypeScript all show the influence in some form.
Is ML still used today?
The original LCF ML is historical, but its descendants are healthy. OCaml has an active compiler team and added multicore support in version 5.0 in 2022, F# ships with .NET, and Standard ML remains a teaching and research language. Robin Milner's ML language for the LCF prover solved a narrow problem, keeping proofs honest, and in doing so set the template for how modern statically typed languages feel to write.
Frequently asked questions
What does ML stand for in the ML programming language?
ML stands for Meta Language. It was the language used to write proof procedures that manipulated the object logic of the LCF theorem prover. It has nothing to do with machine learning, a common source of confusion in searches today.
What is the difference between Standard ML and OCaml?
Both descend from the original Edinburgh ML. Standard ML has a formal definition and a powerful module system and changes very little. OCaml, developed at INRIA, added objects, polymorphic variants and a strong native compiler, and it evolves actively with a larger industrial user base.
Why did Milner need type inference for the LCF prover?
He wanted users to write their own proof tactics without being able to create false theorems. A strong static type system guaranteed that, but requiring annotations everywhere would have made tactic writing painful. Inference gave safety without the clutter.
