Type Inference

Type inference is the automatic deduction of the types of expressions in a programming language without requiring the programmer to annotate every expression with an explicit type declaration. The canonical algorithm, Hindley-Milner type inference (independently discovered by Roger Hindley in 1969 and Robin Milner in 1978, with efficient implementation by Luis Damas in 1982), determines the most general type of any expression in the simply-typed lambda calculus in polynomial time. The algorithm works by generating a system of type constraints from the structure of the program, then solving those constraints by unification — the same unification used in logic programming and automated theorem proving. Type inference is one of the most practically significant results of Programming Language Theory: it allows programmers to write code that is statically verified for type safety without the annotation overhead that makes fully explicit type systems laborious. The tradeoff is that error messages from failed type inference are notoriously difficult to interpret — the algorithm reports failure at the point where the constraint system becomes unsolvable, which is often far from the logical site of the error. This mismatch between the mathematical elegance of the algorithm and the practical experience of debugging type errors is one of the most consequential gaps in language design that the field has not yet closed. See also: Formal Systems, Lambda Calculus.