Word:

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.
Browse
Typal
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
type-ahead search
typecast
typed
typed lambda-calculus
TypedProlog
typeface
typescript
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