Type inference
|
|
Type inference is a feature present in functional programming languages such as Haskell, ML and OCaml.
Type inference automatically assigns a type signature onto a function if it is not given. In a sense, the type signature is reconstructed from the compiler/interpreter's understanding of the function's subfunctions with well defined type signatures, and thus the input/output type can be ascertained.
Example
For example, let us consider the Haskell function length, and it is 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 :: [a] -> 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.
References
- Archived e-mail message (http://www.cis.upenn.edu/~bcpierce/types/archives/1988/msg00042.html) by Roger Hindley explaining the history of type inference