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. 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)
Nearby terms:
typed lambda-calculus « TypedProlog « typeface «
type inference » type scheme » typo »
typographical error
|
