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]

Let polymorphism gives an eligible let-bound name a type scheme, allowing fresh instantiation at each use. In the pure Hindley-Milner type system, generalize the inferred type's type variables that are free in that type and not free in the current typing context. The identity function example under type variable meets this condition. A lambda abstraction's parameter receives one monomorphic type shared by its uses. Languages with mutation, such as Standard ML with ML reference types, need additional restrictions on generalization.

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.

In the examples here, a simple type is a finite expression built from the base types int and bool using function types:For example, $\mathrm{int}\to \mathrm{bool}$ describes a function accepting an integer and producing a Boolean value. During type inference, the grammar is extended with type variables such as $\alpha$ for types not yet determined. A type scheme additionally binds such type variables; it is distinct from the individual simple type used at one call.

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$.

A type scheme binds type variables that may be instantiated independently at different uses. The identity function has type scheme $\forall \alpha .\alpha \to \alpha$: choose one type per use, then use that same choice on both sides of its function type. A free type variable shared with the typing context is not automatically such an independently selectable parameter.

A type substitution replaces type variables by type expressions consistently. For example, $S=\{\alpha \mapsto \mathrm{int}\}$ gives $S(\alpha \to \alpha )=\mathrm{int}\to \mathrm{int}$. Applying a type substitution to a type scheme must respect its bound type variables; separate instantiation first replaces those bound placeholders by fresh ones.

A type system assigns types to program expressions and supplies rules governing their use. A type constrains permitted operations: in our teaching programming language, int admits integer addition, bool supplies true and false for conditions, and a function type specifies an argument type and a result type. Storage as bits alone does not explain these distinctions; the type system determines whether an expression can serve as an argument, a condition or an operand.

A typing judgment $\Gamma ⊢e:\tau$ says that expression $e$ has type $\tau$ under the assumptions in the typing context $\Gamma$. For example,The assumptions give each operand type int; the addition rule then gives the sum type int. Changing $y$ to type bool prevents this derivation. Our teaching programming language has distinct int and bool types and no implicit conversions between them.

The conditional rule requires a Boolean condition and the same type for both branches:Thus if true then 1 else 2 has type int, while if true then 1 else false is rejected: its branches would require $\tau =\mathrm{int}$ and $\tau =\mathrm{bool}$ simultaneously. Even a branch that will not execute is checked by this rule. This is a rule of this particular type system; a different programming language can choose different rules. ^[ref]

The useful feature is compositional reasoning: after checking the parts, a rule explains how to check the whole. The function type diagram shows this for a call. Type inference can discover the required types automatically, and type variables let one express relationships that recur across many concrete types. The result is both a practical early error detector and a small, readable derivation explaining why an expression fits its intended use.

The guarantee depends on the rules and execution model. Type safety can exclude specified failures such as adding a Boolean or calling an integer as a function. It does not by itself establish every desired runtime property or guarantee that execution terminates. A type system that permits unrestricted recursion can accept a computation that runs forever; exception handling also needs its own account of permitted outcomes.

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

A type variable is a placeholder for a type. In a function type $\alpha \to \alpha$, the repeated type variable requires the argument and result types to agree; $\alpha \to \beta$ does not impose that agreement. A type substitution replacing $\alpha$ by int changes $\alpha \to \alpha$ to $\mathrm{int}\to \mathrm{int}$ everywhere within that instance.

For the identity function written as the lambda abstraction $\lambda x.x$, assume $x:\alpha$ in the body. Looking up $x$ gives result type $\alpha$, so the abstraction rule gives $\lambda x.x:\alpha \to \alpha$. In the pure Hindley-Milner type system, let identity = λx.x in ... gives identity the type scheme $\forall \alpha .\alpha \to \alpha$ by let polymorphism. Each use receives fresh type variables: identity 3 chooses int for its instance, and identity true chooses bool for a separate instance. These choices do not change the original type scheme.

For example, let identity = λx.x in let a = identity 3 in identity true is valid and has type bool. By contrast, (λf. let a = f 3 in f true) (λx.x) is rejected by the Hindley-Milner type system: the lambda abstraction binds f to one monomorphic function type. The first call requires its argument type to be int, and the second requires that same type to be bool. Naming the first result with let a does not generalize f. The distinction makes reusable code possible while keeping the assumptions about a supplied argument consistent.

// Target: computer-science.bigb