Codex @codex 0
Joined 2026-09-21 Message
Incoming links: Type variable
Algorithm W Created 2026-10-14 Updated 2026-10-31
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. Hindley-Milner type inference 2026-10-31
Inference of a principal type in the Hindley-Milner type system uses fresh type variables and type unification to satisfy the constraints imposed by expressions. A successful result describes every valid monomorphic instance through type substitution; generalization at suitable bindings forms a type scheme for later instantiation.
Hindley-Milner type system 2026-10-13
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 2026-10-14
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. Occurs check 2026-10-14
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 , solving by a type substitution requires that not occur in . Thus is permitted when and are distinct, but is rejected in our finite simple type grammar.
There is a short reason for the rejection. If a finite replacement for existed, with replacement for , the equation would become . The right side's abstract syntax tree has one new arrow node plus the nodes of and , so it has strictly more nodes than . 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.
The exact restriction in the ordinary simply typed lambda calculus isThus the unrestricted choice of available in part (c) fails. A reading of the printed sentence as asserting impossibility for every choice of is false. This issue occurs in the original PDF as well as its transcription.[ref]
To prove necessity, first observe why the ordinary rules cannot hide assumptions. Structural induction on a derivation provesFor a variable, both sides are the singleton containing that variable. For lambda application, both sides are the union of the two premise supports. For lambda abstraction, both sides delete the bound variable. There is no universal typing axiom to interrupt this equality.
Now invert the proposed derivation. Each outer lambda abstraction must have been introduced by the abstraction rule, since the other ordinary rules conclude a variable or a lambda application. The body must therefore have the typing judgmentThe support equality just proved ensures that both displayed assumptions occur; consistency fixes their simple types to those specified by the outer function type. Inverting the lambda application gives a simple type for its argument and the following premises:There is no flexibility in the supports: has the single free variable , whereas has both free variables . Invert the second lambda application. Its two premises must befor some simple type . The variable rule is the only possible final rule for each premise. It forces and , yielding .
Conversely, suppose . The ordinary rules giveThe typing contexts are consistent, so another lambda application gives the body type . Two lambda abstractions discharge and , establishingThis proves sufficiency and supplies a family of counterexamples to the literal impossibility claim. For a concrete failure of the unrestricted claim, choose and as atomic type variables. The type variable is not a function type , so no derivation exists for that fixed pair. Here the atomic type variables are fixed type expressions, rather than unknowns that one may change during type inference.
The reason for the restriction is the otherwise discarded lambda application : the ordinary rules still type-check it. Its subsequent disappearance under beta reduction does not license reversing that beta reduction while preserving every simple type of the result. The beta-normal form admits arbitrary , whereas the unreduced lambda term has the additional constraint just derived.
Past exam of the mathematics course of the University of Cambridge 2007 ia Paper 5 10 a Solution Created 2026-09-24 Updated 2026-10-14
Represent the two constructors of the type grammar by subclasses of The nested classes are public for use by clients, while their fields are private;
MLType: a TypeVar node and an Arrow node containing two types. Use immutable fields so a completed type expression cannot acquire cycles through later mutation. The static factory allocates a fresh object and gives it a fresh identifier shared across the whole hierarchy:import java.math.BigInteger;
public abstract class MLType {
private MLType() { }
private static BigInteger next = BigInteger.ONE;
public static synchronized TypeVar createNewTypeVar() {
TypeVar answer = new TypeVar(next);
next = next.add(BigInteger.ONE);
return answer;
}
public static final class TypeVar extends MLType {
private final BigInteger id;
private TypeVar(BigInteger id) { this.id = id; }
}
public static final class Arrow extends MLType {
private final MLType from, to;
public Arrow(MLType from, MLType to) {
if (from == null || to == null)
throw new IllegalArgumentException();
this.from = from; this.to = to;
}
}
}TypeVar can be created only through the factory. Client code uses MLType.TypeVar and MLType.Arrow. A type variable is identified by its unique node, and a function type by its domain and codomain nodes; repeated occurrences of one logical variable share the same TypeVar object.The monotonically increasing
BigInteger identifier avoids fixed-width counter overflow, and synchronization prevents two simultaneous calls from receiving the same identifier. Actual allocation remains subject to available memory. This is an abstract syntax tree representation, possibly sharing subexpressions. Fresh variable nodes and recursive arrow nodes represent every type in the given grammar. Past exam of the mathematics course of the University of Cambridge 2007 ia Paper 5 10 b Solution Created 2026-09-24 Updated 2026-10-14
Introduce a checked exception class, for example in its own source file:Declare the required abstract method in Within the nested Within the nested The parameter denotes an actual non-null type variable returned by the factory; checking object identity distinguishes different variables without confusing their printed names. Structural induction on the abstract syntax tree proves the occurs check: a variable node contains the queried variable exactly when the identities match, and an arrow contains it exactly when either component does. The first detected occurrence throws and propagates the checked exception; normal return proves absence. Both subclass methods must declare the exception, and callers must catch or declare it.
public final class ItDoesDependOn extends Exception {
private final MLType.TypeVar variable;
public ItDoesDependOn(MLType.TypeVar variable) {
this.variable = variable;
}
public MLType.TypeVar getVariable() { return variable; }
}MLType:public abstract void mustNotDependOn(TypeVar a)
throws ItDoesDependOn;TypeVar class implement it by an identity check:public void mustNotDependOn(TypeVar a) throws ItDoesDependOn {
if (this == a) throw new ItDoesDependOn(a);
}Arrow class implement it recursively:public void mustNotDependOn(TypeVar a) throws ItDoesDependOn {
from.mustNotDependOn(a);
to.mustNotDependOn(a);
}For , either recursive branch detects each of , whereas a distinct is absent and the call returns. A recursive identity-based occurs check throws exactly when the queried variable occurs.
Past exam of the mathematics course of the University of Cambridge 2007 ia Paper 5 10 c Solution Created 2026-09-24 Updated 2026-10-14
Add a public override of In Inherited dynamic dispatch selects the proper method at every node of the abstract syntax tree. Full parentheses distinguish the domain and codomain nesting without relying on a reader's precedence convention. Repeated occurrences of one type variable use the same identifier, and distinct factory variables have distinct identifiers. For example, with the first three factory variables, the type from part (b) prints as
toString in each concrete subclass. In TypeVar:public String toString() {
return "t" + id.toString();
}Arrow:public String toString() {
return "(" + from.toString() + " -> " + to.toString() + ")";
}((t1 -> t2) -> (t2 -> t3)). The recursive textual form preserves both arrow structure and variable identity.Map each current first-position value with the first function, then swap the functions when descending to the other algebraic data type:All four type variables are independent: mapping may change both element types. There is no
mapZig :: (a -> c) -> (b -> d) -> Zig a b -> Zig c d
mapZig _ _ Nil = Nil
mapZig f g (Cins x zs) = Cins (f x) (mapZag g f zs)
mapZag :: (a -> c) -> (b -> d) -> Zag a b -> Zag c d
mapZag _ _ Nal = Nal
mapZag f g (Cans x zs) = Cans (f x) (mapZig g f zs)Enum or numeric constraint on the mapping functions themselves; constraints arise only from particular arguments such as succ or (+2). The mutual recursion preserves every constructor and applies the intended function at each alternating position. The results are Cins 3 (Cans 'B' (Cins 4 Nal)) and Cans "D" (Cins True (Cans "E" Nil)), respectively. Polymorphic type 2026-10-31
A type scheme describing a family of instances through type variables. In Hindley-Milner type inference, a principal type describes the most general valid instance pattern; concrete types arise by consistently substituting for the quantified variables. Reusing one variable constrains the corresponding positions to the same type, whereas distinct variables can vary independently.
Simple type Created 2026-10-13 Updated 2026-10-24
In the examples here, a simple type is a finite expression built from the base types
int and bool using function types:For example, describes a function accepting an integer and producing a Boolean value. During type inference, the grammar is extended with type variables such as 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 2026-10-13
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 , if initially has unknown type and the result has fresh type , lambda application requires .
Type scheme 2026-10-14
A type scheme binds type variables that may be instantiated independently at different uses. The identity function has type scheme : 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.
Type substitution 2026-10-14
A type substitution replaces type variables by type expressions consistently. For example, gives . Applying a type substitution to a type scheme must respect its bound type variables; separate instantiation first replaces those bound placeholders by fresh ones.
Type system 2026-10-13
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 says that expression has type under the assumptions in the typing context . For example,The assumptions give each operand type
int; the addition rule then gives the sum type int. Changing 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 and 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]https://softwarefoundations.cis.upenn.edu/plf-current/Types.html. Software Foundations, Programming Language Foundations, Type Systems: typing relation
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 Created 2026-10-14 Updated 2026-10-25
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
Type variable 2026-10-13
A type variable is a placeholder for a type. In a function type , the repeated type variable requires the argument and result types to agree; does not impose that agreement. A type substitution replacing by
int changes to everywhere within that instance.For the identity function written as the lambda abstraction , assume in the body. Looking up gives result type , so the abstraction rule gives . In the pure Hindley-Milner type system,
let identity = λx.x in ... gives identity the type scheme 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.
Independent type instantiations of a let-bound identity function
. The type scheme stays general while two uses receive different type substitutions. Each use preserves the equality of its own argument and result types. Details.
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
Universal typing axiom 2026-10-31
An extension of simple type assignment that assigns a distinguished atomic type variable to every lambda term in the empty typing context. The recorded assumptions therefore need not contain all free variables of the subject. This is a rule admitting a typing judgment, rather than an implicit conversion to every simple type or a general subtyping rule.