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.
