type inference
<programming> 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. Reusing 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.
(19950203)
Nearby terms:
typed lambdacalculus « TypedProlog « typeface «
type inference » type scheme » typo »
typographical error
