The Hindley-Milner family of type systems combines parametric polymorphism with automatic inference of principal types.

The key distinction is between monomorphic use inside a lambda and generalization at a let-binding. Consider

let id = fun x -> x
in (id 3, id true)

The inferred type of id is generalized to

$$\forall \alpha.\ \alpha\to\alpha.$$

Each use then receives a fresh instantiation, allowing one call at Int and another at Bool.

Inference proceeds roughly by assigning fresh type variables, generating constraints from program structure, unifying them, and generalizing type variables that are not fixed by the surrounding typing environment.

The resulting principal type is the most general type from which all valid less-general typings can be obtained by substitution. For example,

fun f -> fun x -> f x

has principal type

$$(\alpha\to\beta)\to\alpha\to\beta.$$

This style of inference gives concise source code without abandoning static guarantees. Its limits are also informative: unrestricted higher-rank polymorphism, subtyping and effects complicate or destroy the simple principal-type inference story, motivating explicit annotations or richer constraint systems in more advanced languages.