Search in: Word
Vietnamese keyboard: Off
Virtual keyboard: Show
Computing (FOLDOC) dictionary
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].