schematic type variable ==>
generic type variable
<programming> (Also known as a "schematic type variable"). Different
occurrences of a generic type variable in a type expression may be instantiated
to different types. Thus, in the 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 the two
uses of id, a is instantiated to Bool and Int.
Compare this with
let id x = x in
let f g = (g True, g 1) in
f 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
have the same result type whereas they do not. The
type variables a and b in the above are implicitly
quantified at the top level:
f :: for all a: for all b: (a -> b) -> (b, b)
so instantiating them (removing the quantifiers) can only be done once, at
the top level. To correctly describe the type of 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 be instantiated
differently. f's actual argument must have a type 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 the top level and, now that
g's result type is a generic type variable, any
types chosen for c and d are guaranteed to be
instances of it.
This type for f does not express the fact that b only needs to be at least as
general as the types c and d. For example, if c 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 not match the above type for f.
Nearby terms:
Generic Routing Encapsulation « Generic Security
Service Application Programming Interface « generic
thunk «
generic type variable » Genesia » genetic
algorithm » genetic algorithms
|
