type inference
type inference
(programming)f :: A -> B, x :: A--------------------- (App)f x :: B
This rule, called "App" for application, says that ifexpression f has type A -> B and expression x has type A thenwe can deduce that expression (f x) has type B. Theexpressions above the line are the premises and below, theconclusion. An alternative notation often used is:
G |- x : A
where "|-" is the turnstile symbol (LaTeX \\vdash) and G is atype assignment for the free variables of expression x. Theabove can be read "under assumptions G, expression x has typeA". (As in Haskell, we use a double "::" for typedeclarations 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 typevariables 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 thepartial application of plus to its first argument againstthe App rule, yielding a type (Int -> Int) and a substitutionX = Int. Re-using App for the application to the secondargument gives an overall type Int and no furthersubstitutions. Similarly, matching App against theapplication (head l) we get Y = [X]. We already know X = Intso therefore Y = [Int].
This process is used both to infer types for expressions andto check that any types given by the user are consistent.
See also generic type variable, principal type.