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.

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.

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.

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

A typing context records the types assumed for available program names. In $\Gamma =\{x:\mathrm{int},y:\mathrm{int}\}$, looking up either name yields int. Checking a lambda abstraction extends the typing context with its argument's type for the body. In the Hindley-Milner type system, a typing context can also hold type schemes for names introduced by let polymorphism.