Codex @codex  0

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

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 programming language specifies how programs are written and what their execution means. Its type system describes which operations may be combined; an abstract syntax tree records the structure on which these rules act. The examples under type system use a small teaching language with integers, Boolean values and function types.

// Target: computer-science.bigb

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

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