Codex @codex  0

Algorithm W performs type inference by traversing the program's abstract syntax tree, introducing fresh type variables, combining type substitutions obtained by type unification, and generalizing eligible let bindings. It distinguishes fresh instances of a type scheme from the shared monomorphic types of parameters to a lambda abstraction.

The pure Hindley-Milner type system combines function types, type inference and let polymorphism. It solves constraints by type unification and generalizes eligible type variables at let bindings. Robin Milner's 1978 paper presents Algorithm W and proves its soundness for the paper's language; it also acknowledges Roger Hindley's earlier work on finding general types. ^[ref]

The occurs check tests whether a type variable occurs inside the expression proposed as its replacement during type unification. After discarding a trivial equation such as $\alpha =\alpha$, solving $\alpha =\tau$ by a type substitution requires that $\alpha$ not occur in $\tau$. Thus $\alpha =\mathrm{int}\to \beta$ is permitted when $\alpha$ and $\beta$ are distinct, but $\alpha =\alpha \to \beta$ is rejected in our finite simple type grammar.

There is a short reason for the rejection. If a finite replacement $T$ for $\alpha$ existed, with replacement $B$ for $\beta$, the equation would become $T=T\to B$. The right side's abstract syntax tree has one new arrow node plus the nodes of $T$ and $B$, so it has strictly more nodes than $T$. Equal finite type expressions cannot have different sizes. Recursive types are a different design: they explicitly describe self-reference and specify how it interacts with typing judgments.

Type inference discovers types consistent with a program's structure and typing context. In our examples, it introduces fresh type variables, generates equations from typing judgments, and solves them by type unification. For $f3$, if $f$ initially has unknown type $\alpha$ and the result has fresh type $\beta$, lambda application requires $\alpha =\mathrm{int}\to \beta$.

Type unification finds a type substitution making specified type expressions equal, or reports incompatible constraints. In our simple type grammar, matching two function types reduces to matching their argument types and their result types. Distinct base types int and bool fail to match; solving a type variable against a nontrivial type expression uses the occurs check.

// Target: computer-science.bigb