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