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

type inference
     
         An {algorithm} for ascribing types to
        expressions in some language, based on the types of the
        constants of the language and a set of type inference rules
        such as
     
        	f :: A -> B,  x :: A
        	---------------------  (App)
        	      f x :: B
     
        This rule, called "App" for application, says that if
        expression f has type A -> B and expression x has type A then
        we can deduce that expression (f x) has type B.  The
        expressions above the line are the premises and below, the
        conclusion.  An alternative notation often used is:
     
        	G |- x : A
     
        where "|-" is the turnstile symbol ({LaTeX} \vdash) and G is a
        type assignment for the free variables of expression x.  The
        above can be read "under assumptions G, expression x has type
        A".  (As in Haskell, we use a double "::" for type
        declarations and a single ":" for the {infix} list constructor,
        cons).
     
        Given an expression
     
        	plus (head l) 1
     
        we can label each subexpression with a type, using type
        variables X, Y, etc. for unknown types:
     
        	(plus :: Int -> Int -> Int)
        		(((head :: [a] -> a) (l :: Y)) :: X)
        		(1 :: Int)
     
        We then use {unification} on {type variable}s to match the
        {partial application} of plus to its first argument against
        the App rule, yielding a type (Int -> Int) and a substitution
        X = Int.  Re-using App for the application to the second
        argument gives an overall type Int and no further
        substitutions.  Similarly, matching App against the
        application (head l) we get Y = [X].  We already know X = Int
        so therefore Y = [Int].
     
        This process is used both to infer types for expressions and
        to check that any types given by the user are consistent.
     
        See also {generic type variable}, {principal type}.
     
        (1995-02-03)