Type inference

If you write a function, you should not have to write its type twice — once in your head, once in the editor. ML proved in 1973 that a compiler can derive the type from the definition, and that the derivation can be checked rather than trusted.

The algorithm behind it, Hindley–Milner, decides the type by unification: it assumes a type, meets the definition, and revises the assumption until everything fits. It is why a single `id` function serves every type in a program, why Haskell lists type errors so precisely, and why Rust can move a value into a function and know exactly what comes back out.

The trade-off

• Inference is only as good as its rules: monomorphic Hindley–Milner cannot type the higher-rank functions that real programs need, so OCaml and Haskell grew escape hatches.
• Inferred types can surprise you — a value that looks like an int can be inferred as a float, and the error surfaces a hundred lines away.

Where it came from

ML, 1973, built for proof tactics in the LCF system — types had to be checked before a proof was run, not after.