Type system

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 data type without universally quantified type variables. During Hindley-Milner type inference, every use of a lambda-bound parameter shares one type, even if that type initially contains unknowns to be unified. In contrast, suitable let-bound definitions may admit let polymorphism.

A classification of program values together with the operations permitted on them. An algebraic data type describes values by data constructors; a function type describes acceptable arguments and produced results.

A data type with exactly one value. In Haskell, both the data type and its sole value are written (); it is often the result of a computation whose purpose is an effect.

An operation checking that a value has a requested runtime extension type and exposing the fields of that type. In Oberon, a pointer guard such as p(RealTail) permits a pointer to a base record to access the real-valued field of an appropriate record extension. Failure of the dynamic type check is a runtime error, so a representation invariant should establish that guarded values have the requested extension before the operation is used.

A classification of type-level expressions. In the traditional Haskell notation, ordinary types have kind *, while a unary type constructor such as Tree has kind * -> *. Applying it to a suitable type argument produces an ordinary type. This distinguishes the type-level application from applying a value with a function type.

A type-level constructor accepting the number and kinds of type arguments specified by its kind of a type. For example, Tree accepts one ordinary type and produces Tree a; it has kind * -> *. A data constructor such as One operates at the value level instead. The two levels can use separate namespaces in a programming language.

A type whose values are described by named data constructors with specified fields. For example, data Tree a = One a | Two (Tree a) (Tree a) describes a leaf-labelled binary tree. Its two alternatives are distinguished by pattern matching; the recursive fields give a recursive type.

A data type whose values belong to one of several alternatives, with a logical tag distinguishing the chosen alternative. If Number n and Operator op are its constructors, pattern matching can distinguish the variants even if their payloads use similar representations. The tag need not occupy a separate physical memory field in every implementation.

A named way to construct one alternative of an algebraic data type. In data Tree a = One a | Two (Tree a) (Tree a), One has type signature a -> Tree a and Two has type signature Tree a -> Tree a -> Tree a. They construct values; the type constructor Tree instead constructs types from a type argument.

Using an interface or definition across multiple types. Subtype polymorphism dispatches through a common supertype; parametric polymorphism uses a type parameter uniformly; method overloading selects among signatures by static types in languages such as Scala. These mechanisms should be distinguished from genetic or materials-science polymorphism.

Ad hoc polymorphism provides distinct implementations for selected types behind a common operation name. Method overloading is a common instance, where parameter signatures and static argument types determine the selected operation. It differs from a uniform type-parameterized definition and from dynamic dispatch on the receiver after an instance-method signature has been selected.

A Boolean data type has two truth values. A binary probabilistic query returns such a value; rejection or failure must be represented separately if false outcomes are valid observations of the query.

A class specifies overloaded methods and a constraint supplies the applicable instance operations for a type. This programming-language concept is distinct from an information-theoretic type class. A method signature does not enforce algebraic laws such as a lawful total order.

The Haskell type class providing the overloaded operations == and /=. A signature Eq a => [a] -> [a] -> Bool requires the corresponding operations for the element type. Correctness arguments treating them as mathematical equality additionally assume that the instance supplies the intended equality relation.

The Haskell class providing ordering operations, including compare. A comparison-based sorting algorithm requires the associated constraint to inspect the order of arbitrary keys. Its correctness additionally assumes that the supplied operations obey the intended ordering laws.

To check a parameter's variance, start in a positive position, reverse the sign when entering a function or method input, and preserve it through covariant outputs and covariant containers. Contravariant containers reverse the sign; invariant positions prohibit variation. Thus an immutable list of pairs exposes both pair types covariantly; a relatives-enumeration method consumes its first type and produces its second; a two-argument predicate consumes both. This derives the safe variance of three common representations of a binary relation from the roles of their inputs and outputs.

A type selected through a stable object path, allowing an object's nested type to retain its association with that instance. In Scala, editor.Snapshot can differ from otherEditor.Snapshot even when both objects have the same outer class. This is useful for originator-specific mementos and other values that must not be mixed across owners.^[ref]

The concrete type of a value or allocated object during execution. For ordinary instance methods in object-oriented programming, dynamic dispatch uses the receiver's runtime type after a signature has been selected. The runtime type of an argument does not in general restart compile-time method overloading.

The type assigned to a program expression during type checking. It controls which members and overloads are available at that expression. A reference with a broad static type can designate an object with a narrower runtime type; that does not expose additional overloads through the broad reference.

A relationship in which values of one type can be used wherever values of a broader type are required, subject to the language's compatibility rules. In nominal object-oriented programming, extending a class or implementing a trait establishes relevant subtype relationships. Type variance describes how these relationships lift through parameterized types.

A lower bound requires an admissible type argument to be a supertype of a specified type. In Scala, [V >: U] means $U<:V$. For an immutable software class covariant in U, a method accepting a new output value cannot consume U directly in a contravariant method-parameter position. Instead, add[V >: U](x: V) accepts a possibly wider value and returns a fresh instance parameterized by V. The original narrower instance remains unchanged. The variance-position rule and subtyping justify this widening; a bound alone does not authorize mutating an existing instance through a widened reference.^[ref]

An upper type bound $A<:B$ requires the type argument assigned to $A$ to be a subtype of $B$. Two independently bounded parameters can retain different precise component types while sharing the same upper bound. Bounds and type variance answer different questions: admissible arguments versus subtyping between instantiations.

A type parameter can be bounded using a type expression containing that same parameter. In Scala, [T <: Ordered[T]] requires each admissible T to provide comparison with another T. This gives a generic minimum scan access to x < y for two elements of type T. An arbitrary unrelated upper bound would not establish the needed argument type.

A type $S$ is a supertype of $T$ when $T$ is a subtype of $S$. A lower type bound requires an admissible type argument to lie above a specified type in this subtyping relation.

Subtype polymorphism lets a value implementing a more specific type be used through a common supertype object interface. Calls to overridable instance methods can select implementations by dynamic dispatch. Behavioral subtyping additionally requires the concrete implementation to honor the common contract, including preconditions, postconditions and state invariants; structural access to object method names alone does not establish that guarantee.

Substitution of an implementation for an interface while preserving its behavioral contracts, not just method types. Strengthening a method's precondition or weakening its postcondition can invalidate substitution. A nonnegative immutable refinement of a signed count value can inherit an exact subtraction returning the signed supertype; changing that same operation into truncated subtraction would not satisfy its parent's exact-difference postcondition.

The type-level description of a value or operation, including parameter and result types. A type signature can rule out some invalid uses, but ordinary type annotations alone do not express every precondition, postcondition or relationship to an abstract program state.

The data type of the value produced by a function or object method when it returns normally.

A name for an existing type expression, without constructing a distinct runtime datatype. In Haskell, type Seq a = a -> [Integer] names a function representation; an equality test constraint can belong to an operation on that representation without belonging to the synonym itself.

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

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.

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]

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 principal type is a most general valid type scheme: every other valid typing of the expression is obtained by substituting types for its quantified type variables, subject to any declared class constraints. For example, \s x f y -> f (s y x) has type (u -> v -> w) -> v -> (w -> r) -> u -> r; the application constraints require precisely these connections and no equality between the four type variables. A concrete typing is an instance, not evidence that the expression needs that particular type.

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

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

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.

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 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 data type describing a callable procedure's parameter types and any return type. A traversal callback taking an integer and producing no data result can be passed using an Oberon declaration such as Visit = PROCEDURE(x: INTEGER).

A procedure passed as an argument to another procedure. For a nested procedure under lexical scope, the argument must preserve both its code and its defining environment, for example as a programming closure.

If $A^{\prime }<:A$ and $B<:B^{\prime }$, a function of type $A\to B$ safely supplies a contract of type $A^{\prime }\to B^{\prime }$. Every input permitted by the new contract is already accepted, and every possible returned value meets the weakened result promise. This proves contravariance of inputs and covariance of outputs. Reversing either direction can respectively supply an unsupported input or promise a result more specific than the implementation returns. A language's generic type object constructor may nevertheless be invariant unless its declaration exposes the appropriate variance.

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

// Target: computer-science.bigb

An object method with its own type parameters, instantiated or inferred at each call. In Scala, def identity[T](x: T): T = x is a generic method. A method def accept(x: T) inside class Box[T] instead uses a class type parameter fixed by the receiver's type argument; it is not itself a generic method with a separately chosen T on every call. This distinction matters in method overloading.

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.

A type parameter is a named variable ranging over admissible types in a generic definition. Instantiation substitutes a particular type argument, allowing one declaration to retain type information across uses. An upper type bound restricts the admissible arguments; a variance annotation instead describes how instantiated types participate in subtyping.

A type substituted for a type parameter when a generic declaration is instantiated. A type argument must satisfy the declaration's upper and lower bounds. It is distinct from an ordinary run-time argument supplied to a function call.

A parameter position for which $S<:T$ implies $F[T]<:F[S]$. In Scala, it is annotated -. A consumer capable of accepting every broad-type value can safely serve a context that supplies only narrower values. Returning a value of that parameter type would generally break this guarantee.

A parameter position for which $S<:T$ implies $F[S]<:F[T]$. In Scala, it is annotated +. An immutable producer can return narrower values where broader values are expected. A method consuming that parameter directly would generally make covariance unsafe, since a widened reference could then receive unsupported inputs.

Suppose a mutable collection of narrow-type values could be viewed as a mutable collection of a wider type. Inserting a wider-only value through that alias would make a subsequent narrow-type read invalid. For example, hypothetical covariance would let one insert a string through an Any-typed alias of an integer multiset. Generic type invariance prevents that substitution; making a parameter covariant does not authorize an unsound consuming method.

How subtyping between parameter types affects subtyping between instances of a parameterized type. A covariant type parameter preserves the direction, a contravariant type parameter reverses it, and generic type invariance permits neither conversion solely from the parameter relationship. Safe variance depends on how a type is consumed, produced and stored.

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]

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.

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.