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
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.
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.
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.
Articles by others on the same topic
In programming, a **type variable** is a placeholder for a type that can be specified later. Type variables are often used in generic programming to allow functions, classes, or interfaces to operate on types that are not specified until the code is invoked or instantiated. This allows for greater flexibility and reusability of code. ### Key Concepts: 1. **Generics**: Type variables are commonly used in languages that support generics (e.g., Java, C#, TypeScript, etc.).