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