generic type variable

generic type variable

(programming)(Also known as a "schematic type variable").Different occurrences of a generic type variable in a typeexpression may be instantiated to different types. Thus, inthe expression

let id x = x in(id True, id 1)

id's type is (for all a: a -> a). The universal quantifier"for all a:" means that a is a generic type variable. For thetwo uses of id, a is instantiated to Bool and Int. Comparethis with

let id x = x inlet f g = (g True, g 1) inf id

This looks similar but f has no legal Hindley-Milner type.If we say

f :: (a -> b) -> (b, b)

this would permit g's type to be any instance of (a -> b)rather than requiring it to be at least as general as (a ->b). Furthermore, it constrains both instances of g to havethe same result type whereas they do not. The type variablesa and b in the above are implicitly quantified at the toplevel:

f :: for all a: for all b: (a -> b) -> (b, b)

so instantiating them (removing the quantifiers) can only bedone once, at the top level. To correctly describe the typeof f requires that they be locally quantified:

f :: ((for all a: a) -> (for all b: b)) -> (c, d)

which means that each time g is applied, a and b may beinstantiated differently. f's actual argument must have atype at least as general as ((for all a: a) -> (for all b:b)), and may not be some less general instance of this type.Type variables c and d are still implicitly quantified at thetop level and, now that g's result type is a generic typevariable, any types chosen for c and d are guaranteed to beinstances of it.

This type for f does not express the fact that b only needs tobe at least as general as the types c and d. For example, ifc and d were both Bool then any function of type (for all a: a-> Bool) would be a suitable argument to f but it would notmatch the above type for f.