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