资料来源 : Free On-Line Dictionary of Computing

generic type variable
     
         (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 {quantifier}s) 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.