type inference

(programming)type inference - 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.
type 1 diabetes
Type 2 diabetes
type A
type AB
type assignment
type B
type class
type family
Type founder
Type foundry
type genus
type I allergic reaction
type I diabetes
type II diabetes
-- type inference --
type IV allergic reaction
type metal
type O
type of architecture
type scheme
type species
type specimen
Type wheel
type-ahead search
typed lambda-calculus
Definitions Index: # A B C D E F G H I J K L M N O P Q R S T U V W X Y Z

About this site and copyright information - Online Dictionary Home - Privacy Policy