Symptom

You write this in OCaml or Haskell and annotate nothing:

let rec map f = function
  | [] -> []
  | x :: xs -> f x :: map f xs

The compiler reports ('a -> 'b) -> 'a list -> 'b list. It found the most general possible type, on its own, with no hints, and it will reject any call that does not fit.

In Java the same function requires you to write <T, R> List<R> map(Function<T, R> f, List<T> xs), spelling out what the compiler could have worked out. In Python you get nothing, and you find out at runtime. In C++ templates you get inference of a sort and an error message four hundred lines long when it fails.

So the question is what makes full inference possible in one language and not another, and what it costs. Because it does cost something: ML-family languages lack a feature almost every mainstream language has, and the absence is not an oversight.

Statement

Principal types. In the Hindley–Milner system, every typable term has a principal type: a type from which all its other types are obtained by substitution. Algorithm W computes it, and it is complete: if a term is typable at all, W finds its principal type.

Let types be $\tau ::= \alpha \mid \tau \to \tau \mid T\ \overline{\tau}$ and type schemes $\sigma ::= \tau \mid \forall \alpha. \sigma$, with quantifiers only at the outermost position (prenex, rank-1 polymorphism). If $\Gamma \vdash e : \tau$ for some $\tau$, then there is a $\sigma_p$ with $\Gamma \vdash e : \sigma_p$ such that every derivable type for $e$ is an instance of $\sigma_p$. Algorithm W computes $\sigma_p$, and its worst-case complexity is DEXPTIME-complete, though it is effectively linear on programs people write.

The restriction that makes it work is rank-1: $\forall$ appears only at the top. forall a. a -> a is fine. (forall a. a -> a) -> Int is not, because the quantifier is nested inside an argument. That single restriction is what buys decidable, complete inference, and it is exactly what you give up when you want higher-rank types.

Argument

Algorithm W is unification plus generalization. Walk the syntax tree, inventing a fresh type variable wherever the type is unknown, and collect equations that must hold. Then solve the equations by unification.

For \f -> \x -> f (f x):

  1. Assign $f : \alpha$, $x : \beta$.
  2. f x requires $\alpha = \beta \to \gamma$ for a fresh $\gamma$.
  3. f (f x) applies $f$ to something of type $\gamma$, so $\alpha = \gamma \to \delta$.
  4. Unify the two constraints on $\alpha$: $\beta \to \gamma = \gamma \to \delta$, forcing $\beta = \gamma$ and $\gamma = \delta$.
  5. Everything collapses to one variable: $f : \beta \to \beta$, $x : \beta$, result $\beta$.
  6. Generalize the variables not free in the environment: $\forall \beta.\ (\beta \to \beta) \to \beta \to \beta$.

Nothing was guessed. Unification finds the most general unifier, and most-general-at-every-step composes into most-general-overall, which is the proof of principality in outline.

Generalization at let is the whole polymorphism story. In let id = \x -> x in (id 1, id True), id gets type $\alpha \to \alpha$, and at the let the compiler generalizes to $\forall \alpha.\ \alpha \to \alpha$. Each use then instantiates with a fresh variable, so one use takes Int and the other Bool with no conflict.

Lambda-bound variables are not generalized, and this is the essential asymmetry. \id -> (id 1, id True) is rejected: $id$ has a monomorphic type inside the body and cannot be both. To accept it you would need id’s argument type to be $\forall \alpha.\alpha \to \alpha$, which is rank-2, and inference for rank-2 and above is undecidable in general. The feature is missing because including it would make the algorithm not exist.

The occurs check is where infinite types are caught. Unifying $\alpha$ with $\alpha \to \beta$ would need a type satisfying $\tau = \tau \to \beta$. The occurs check rejects it, and this is why \x -> x x does not typecheck, and therefore why the Y combinator (T041) is not expressible without a fix primitive. The untypability of self-application is not an accident of the system; it is the same fact as strong normalization.

Why the exponential worst case never bites. Chained lets can double the type size each level:

let p1 = (id, id) in
let p2 = (p1, p1) in
let p3 = (p2, p2) in ...

Each level squares the type, so $n$ levels give a type of size $2^n$ — at 20 levels, over a million type nodes, and at 30 levels over a billion. This is Kfoury, Tiuryn, and Urzyczyn’s DEXPTIME-completeness result made concrete. It requires deliberately nested let-bound tuples of polymorphic values, and no human writes it, which is why an inference engine that is exponential in theory is unnoticeable in practice.

Where subtyping breaks it, and why this matters for mainstream languages. Unification asks whether two types are equal. Subtyping asks whether one is below another, replacing equations with inequalities, so a constraint set becomes a lattice problem rather than a substitution. Principal types in the HM sense stop existing: a term can have many incomparable minimal types, and the best you can offer is a principal typing scheme carrying the whole constraint set, which is large and unreadable in error messages.

That is why Java, C#, Scala, and TypeScript all have local or bidirectional inference rather than global inference. They chose subtyping, which their object models require, and paid for it with annotations at every declaration boundary. The annotations in Java are not a failure of ambition; they are the price of a feature ML does not have.

The value restriction, and the bug that forced it. Naive generalization plus mutable references is unsound:

let r = ref [] in      (* would get forall 'a. 'a list ref *)
r := [1];              (* instantiate at int *)
List.map (fun s -> s ^ "!") !r   (* instantiate at string *)

This typechecks under naive HM and segfaults. Standard ML shipped it, the hole was found, and the fix, restricting generalization to syntactic values, is what every ML dialect now implements. It is a rare case of a type-system bug that reached production languages before being caught.

Forbids

Type inference for unrestricted polymorphism. Rank-2 inference is decidable but impractical; rank-3 and above is undecidable (Wells, 1999). Higher-rank types are available in GHC via RankNTypes only because you supply the annotation.

Typing self-application. \x -> x x is untypable, and so is Y.

Global inference with subtyping. Not as a matter of engineering effort. The principal-type property fails.

Full inference with dependent types. Higher-order unification is undecidable (Huet), which is why Agda, Idris, and Lean have elaboration with holes rather than inference, and why their error messages are about unsolved metavariables.

Does not forbid

It does not mean annotations are useless in ML. They serve as documentation, they localize errors dramatically, and they enable extensions. Idiomatic Haskell annotates every top-level binding even though nothing requires it, because inferred types drift silently when a definition changes and a signature turns that into a local error.

It does not mean HM is obsolete. OCaml, Standard ML, Elm, PureScript, and Rust’s local inference all use it, and GHC’s constraint-based system is HM extended, with the core unification engine intact underneath type classes and GADTs.

It does not mean inference and subtyping are permanently incompatible. TypeScript, Flow, and Scala 3 do a great deal of inference with subtyping; they simply do it locally and bidirectionally rather than globally, propagating expected types inward. MLsub and Algebraic Subtyping (Dolan, 2017) recover principal types with subtyping by moving to a lattice of types with unions and intersections, which is a genuine result rather than a workaround.

It does not require the exponential case to be avoided by luck. The blowup needs nested let-bound polymorphic pairs; ordinary programs have shallow sharing and inference is effectively linear in practice.

It does not say type classes break principality. They complicate it. With open type classes, an inferred type may be ambiguous, which is why Haskell has the monomorphism restriction and defaulting rules, and why show (read "1") is rejected as ambiguous rather than accepted.

Boundary

  • Rank-1 only. Prenex quantification. Anything else needs annotation.
  • No subtyping. Adding it forfeits principal types in this form.
  • Value restriction. Required for soundness with mutable references, and it costs real expressiveness: some perfectly safe programs are rejected.
  • Type classes and GADTs push it further. Each addition needs careful design to preserve what remains of principality, and GHC’s -XScopedTypeVariables and friends exist because some of them require the programmer to supply what inference no longer can.

The trade to carry: full inference is not free, it is bought with rank-1 restriction and no subtyping, and the languages that annotate more are not less advanced but differently priced.