[1] : The Free On-line Dictionary of Computing (27 SEP 03)

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 variables 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
     
     
see also:
algorithm latex infix unification type variable partial application 
generic type variable principal type 

Inference >> I Words
Inference, definition of term: Inference
inference_pag1.html

Blood Type >> B Words
Blood Type, definition of term: Blood Type
blood+type_pag1.html