The Hindley-Milner type system is the type discipline that makes full type inference practical for functional languages. Robin Milner set it out in his 1978 paper “A Theory of Type Polymorphism in Programming,” which gives a type discipline for polymorphic procedures together with a compile-time type-checking algorithm that enforces it.
Its defining feature is that it can infer the most general type of an expression: rather than committing to one concrete type, the system finds a polymorphic type that captures every way the expression can legitimately be used. The paper’s checking algorithm, often called Algorithm W, computes these types from the structure of the program alone, so the programmer can omit type annotations entirely while still getting full static checking.
A key ingredient is let-polymorphism, the rule that a value bound by a let definition can be used at several different types within its scope. This is what lets a single generic function, such as one that reverses a list, be applied to lists of any element type without rewriting it.
The Turing Award citation for Milner describes ML as the first language with polymorphic type inference and calls the inference algorithm applied to a full language a major theoretical advance. The same system, with extensions, became the typing core of ML, OCaml, and Haskell, making Hindley-Milner one of the foundations of modern typed functional programming.