type inference


Also found in: Wikipedia.

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.
References in periodicals archive ?
Type inclusion constraints and type inference. In Proceedings of the International Conference on Functional Programming Languages and Computer Architecture.
- Inline variable declaration, type inference, and more for the Delphi language.
Local-variable type inference: enhances the Java language to extend type inference to declarations of local variables with initializers.
After the raw data capturing process five modules, session reconstruction, message reassembling, HsMM, message segmentation, and message type inference, follow.
The fuzzy proportional derivative plus integral inference is based on Mamdani type inference, the controller output u(k),is based on the centroid defuzzification technique and the input variables are the error between reference and output, [e.sub.fuzz](k), and the error variation, [DELTA][e.sub.fuzz] (k).
The results of message type inference are important for constructing protocol state machine which will be discussed in our future work.
proposed two types of modification procedures--expansion type inference and reduction type inference [4], and B' may be computed by any one of the following form:
In addition, new Java SE 7 features such as try-with-resources, strings in switch, type inference with the diamond operator, NIO.2, and the Fork/Join Framework are also discussed in detail.
A set of small language changes intended to simplify common, day-to-day programming tasks: Strings in switch statements, try-with-resources statements, improved type inference for generic instance creation ("diamond"), simplified varargs method invocation, better integral literals, and improved exception handling (multi-catch)
Among the topics are the mathematics of mathematical handwriting recognition, a knowledge acquisition and processing system for Romanian historical documents, type inference for regular expression pattern matching, personality filter in mobile networks with communications constraints.
Type elaboration is a technique for type inference on verifiable Java bytecode.
This approach has several advantages with respect to the Modula-3/Java approach: it blends better with ML type inference; it does not change the language and supports the static debugging of "legacy" applications; it allows the use of complex approximations of exception sets, as those need not be written by the programmer (within reason--the results of the analysis must still be understandable to the programmer).