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)