Type inference is a feature present in some strongly statically typed programming languages. It is often characteristic of — but not limited to — functional programming languages in general. Some languages that include type inference are: Haskell, Cayenne, Clean, ML, OCaml, Epigram, Scala, Nemerle, D and Boo. This feature is planned for Fortress, C# 3.0 and C++0x.

Type inference refers to the ability to automatically either partially or fully deduce the type of the value derived from the eventual evaluation of an expression. As this process is systematically performed at compile time, the compiler is often able to infer the type of a variable or the type signature of a function, without explicit type annotations having been given. In many cases, it is possible to omit type annotations from a program completely if the type inference system is robust enough, or the program or language simple enough.

To obtain the information required to correctly infer the type of an expression lacking an explicit type annotation, the compiler either gathers this information as an aggregate and subsequent reduction of the type annotations given for its subexpressions (which may themselves be variables or functions), or through an implicit understanding of the type of various atomic values (e.g., () : Unit; true : Bool; 42 : Integer; 3.14159 : Real; etc.). It is through recognition of the eventual reduction of expressions to implicitly typed atomic values that the compiler for a type inferring language is able to compile a program completely without type annotations. In the case of highly complex forms of higher order programming and polymorphism, it is not always possible for the compiler to infer as much, however, and type annotations are occasionally necessary for disambiguation.

Example

---

For example, let us consider the Haskell function length, which may be defined as: length ^* = 0 length (first:rest) = 1 + length rest

From this, it is evident that the function handles lists as inputs, and the base case of this recursive function returns an integer (Haskell "Int"). So we can reliably construct a type signature length :: ^* -> Int

Since there are no ad-hoc polymorphic subfunctions in the function definition, we can declare the function to be parametric polymorphic.

Hindley-Milner type inference algorithm

---

The common algorithm used to perform the type inference is the one now commonly referred to as Hindley-Milner or Damas-Milner algorithm.

The origin of this algorithm is the type inference algorithm for the simply typed lambda calculus, which was devised by Haskell B. Curry and Robert Feys in 1958.

In 1969 Roger Hindley extended this work and proved that their algorithm always inferred the most general type.

In 1978 Robin Milner, independently of Hindley's work, provided an equivalent algorithm,

In 1985 Luis Damas finally proved that Milner's algorithm is complete and extended it to support systems with polymorphic references.

The Algorithm

The algorithm proceeds in two steps. First, we need to generate a number of equations to solve, then we need to solve them.

Generating the equations

The algorithm used for generating the equations is similar to a regular type checker, so let's consider first a regular type checker for the typed lambda calculus given by

$e\; \backslash ,\; ::=\; E\; \backslash mid\; v\; \backslash mid\; (\backslash lambda\; v:\backslash tau.\; e)\; \backslash mid\; (e\backslash ,\; e)$

and

$\backslash tau\; \backslash ,\; ::=\; T\; \backslash mid\; \backslash tau\; \backslash to\; \backslash tau$

where $E$ is a primitive expression (such as "3") and $T$ is a primitive type (such as "Integer").

We want to construct a function $f$ of type $\backslash epsilon\; \backslash to\; t\; \backslash to\; \backslash tau$, where $\backslash epsilon$ is a type environment and $t$ is a term. We assume that this function is already defined on primitives. The other cases are:

$f\backslash ,\; \backslash Gamma\backslash ,\; v\; =\; \backslash tau$ whenever the binding $v\backslash ,\; :\backslash ,\backslash tau$ is in $\backslash Gamma$

$f\backslash ,\; \backslash Gamma\backslash ,\; (g\backslash ,\; e)\; =\; \backslash tau$ whenever $\backslash tau\_1\; =\; \backslash tau\_2\; \backslash to\; \backslash tau$ where $\backslash tau\_1\; =\; f\backslash ,\; \backslash Gamma\backslash ,\; g$ and $\backslash tau\_2\; =\; f\backslash ,\; \backslash Gamma\backslash ,\; e$.

$f\backslash ,\; \backslash Gamma\backslash ,\; (\backslash lambda\; v:\backslash tau.\; e)\; =\; \backslash tau\; \backslash to\; \backslash tau\_e$ where $\backslash tau\_e\; =\; f\backslash ,\; \backslash Gamma\text{'}\backslash ,\; e$ and $\backslash Gamma\text{'}$ is $\backslash Gamma$ extended by the binding $v\; \backslash ,:\backslash ,\backslash tau$.

Note that so far we do not specify what to do when we fail to meet the various conditions. This is because, in the simple type *checking* algorithm, the check simply fails whenever anything goes wrong.

Now, we develop a more sophisticated algorithm that can deal with type variables and constraints on them. Therefore, we extend the set T of primitive types to include an infinite supply of variables, denoted by lowercase Greek letters $\backslash alpha,\; \backslash beta,\; ...$

This is a limited overview. For now, refer to Types and Programming Languages by Benjamin Pierce, Sections 22.1-4 .

Solving the equations

Solving the equations proceeds by unification. This is - maybe surprisingly - a rather simple algorithm. The function $u$ operates on type equations and returns a structure called a "substitution". A substitution is simply a mapping from type variables to types. Substitutions can be composed and extended in the obvious ways.

Unifying the empty set of equations is easy enough: $u\backslash ,\; \backslash emptyset\; =\; \backslash mathbf\{i\}$, where $\backslash mathbf\{i\}$ is the identity substitution.

Unifying a variable with a type goes this way: $u\backslash ,\; (=\; T\backslash cup\; C)\; =\; u\backslash ,\; (C\text{'})\; \backslash cdot\; (\backslash alpha\; \backslash mapsto\; T)$, where $\backslash cdot$ is the substitution composition operator, and $C\text{'}$ is the set of remaining constraints $C$ with the new substitution $\backslash alpha\; \backslash mapsto\; T$ applied to it.

Of course, $u\backslash ,\; (=\; \backslash alpha\backslash cup\; C)\; =\; u\; (=\; T\backslash cup\; C)$.

The interesting case remains as $u\backslash ,\; (\backslash to\; S\text{'}\; =\; T\; \backslash to\; T\text{'}\backslash cup\; C)\; =\; u\; \backslash ,\; (\backslash \{=\; T,=\; T\text{'}\backslash \}\backslash cup\; C)$.

References

---

External link

---

• Archived e-mail message by Roger Hindley explaining the history of type inference

Type theory

Typinferenz | Inferencia de tipos | Inférence de types | 型推論 | Модель типизации Хиндли-Милнера