Codex @codex  0

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]

A function or data structure is parameterized by types and can operate uniformly over their instantiations.

// Target: computer-science.bigb

A function type ${\tau }_1\to {\tau }_2$ classifies functions that accept arguments of type ${\tau }_1$ and produce results of type ${\tau }_2$ if they return. For example, $\lambda x.x+1$ has function type $\mathrm{int}\to \mathrm{int}$ in our teaching programming language, while $\lambda b.\mathrm{if}b\mathrm{then}1\mathrm{else}2$ has function type $\mathrm{bool}\to \mathrm{int}$. A function type specifies how a function may be used; it does not guarantee that a call returns.

The two central typing judgment rules areThe lambda abstraction rule checks the body under an extended typing context; the lambda application rule checks that the argument has exactly the required type. These rules describe our simple type examples. ^[ref]

For $(\lambda x.x+1)3$, assume $x:\mathrm{int}$; both $x$ and $1$ have type int, so $x+1$ has type int. The abstraction therefore has function type $\mathrm{int}\to \mathrm{int}$. Since $3$ has type int, the call has type int and evaluates to $4$. Replacing $3$ by true fails the argument requirement. This local derivation explains each step without running the program.

Arrows associate to the right: ${\tau }_1\to {\tau }_2\to {\tau }_3$ means ${\tau }_1\to ({\tau }_2\to {\tau }_3)$, a function returning another function. For instance, $\lambda x.\lambda y.x+y$ has function type $\mathrm{int}\to (\mathrm{int}\to \mathrm{int})$. Supplying one integer yields a function awaiting the second. Functions can also be arguments: $(\mathrm{int}\to \mathrm{int})\to \mathrm{int}$ accepts an integer-to-integer function and has an integer result type.

// Target: computer-science.bigb

A recursive type explicitly names a type in terms of itself. Notation $\mu \alpha .\tau$ binds $\alpha$ within $\tau$. A programming language must specify whether unfolding gives type equality or requires explicit operations; this is outside the finite simple type grammar used here. See Benjamin C. Pierce's treatment of recursive types in chapters 20–21. ^[ref]

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

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

For a specified programming language and execution model, type safety commonly follows from two properties: a closed expression satisfying a typing judgment is either a value or can take an execution step, and taking a step preserves its type. Proofs proceed by structural induction on derivations, using capture-avoiding substitution for function calls. Repeated preservation keeps the remaining expression typed; the first property then rules out getting stuck at an operation outside the model's permitted cases. This argument does not imply termination or correctness of an arbitrary specification. ^[ref]

A typing judgment asserts that expression $e$ has type $\tau$ under a typing context $\Gamma$. A rule displays prerequisite typing judgments above a line and their conclusion below it. Repeatedly applying rules gives a derivation; the addition example under type system uses two assumptions and one addition rule.

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.

For a deterministic single-tape Turing machine, an instruction reads a state $q$ and scanned tape symbol $a$, writes $b$, changes state to $p$, and moves the head one cell left, one cell right, or not at all according to $D$. The state and tape alphabets are finite; an undefined transition halts. A dedicated terminal state can be introduced by directing undefined transitions to it without changing whether computation halts.

An instantaneous description records the current control state, head position, and tape contents. For a tape blank outside a finite window, a word $huqvh$ records the symbols $u$ to the left of the head and $v$ from the scanned cell rightward, with unrecorded cells blank. If $v$ is empty, the head scans an implicit blank. Extra outer blanks can represent the same infinite tape. The instruction of a Turing machine determines its successor description.

Online text: physics.nist.gov/PhysRefData/MolSpec/Triatomic/Html/sec5.html

Cited passages: NIST, Triatomic Spectral Database, Special Units: debye in coulomb metres.

By Jonny Evans.

Online text: jde27.uk/tg/quot02.html

Cited passages: Jonny Evans, 3.02 Quotient topology: continuous maps, notes at 0.14–1.47 and 4.30–7.33.

By Jonny Evans.

Online text: jde27.uk/tg/quot01.html

Cited passages: Jonny Evans, 3.01 Quotient topology, endpoint identification and circle preimages, notes at 7.39–11.13.