ML (short for “metalanguage”) was created by Robin Milner and colleagues in the early 1970s as part of the LCF project at the University of Edinburgh. Its original job was to be the language in which users wrote proof tactics for the LCF machine-assisted proof tool, which meant its type system had to make certain misuses impossible to express.
To meet that requirement Milner developed a polymorphic type discipline together with a compile-time type-checking algorithm, described in his 1978 paper “A Theory of Type Polymorphism in Programming.” The paper presents a type discipline for polymorphic procedures and a checking algorithm that enforces it, so that a program accepted by the checker cannot go wrong at run time on a type error. This was an early and influential demonstration of full type inference for a real language.
ML combined static typing with the brevity of inference: programmers rarely had to write type annotations, yet the compiler still caught type errors before the program ran. The language also brought together pattern matching and algebraic data types as everyday tools, along with a type-safe exception mechanism, as the Turing Award citation for Milner notes.
The ideas were later codified in The Definition of Standard ML, a formal specification by Milner, Tofte, Harper, and MacQueen, hosted by the SML family project. From this lineage descended Standard ML, OCaml, F#, and, more indirectly, Haskell, making ML one of the most influential roots of modern typed functional programming.