View source for Type inference

{{Short description|Automatic detection of the type of an expression in a formal language}}
{{Type systems}}
'''Type inference''', sometimes called '''type reconstruction''',<ref name="TAPL">{{cite book |author1=[[Benjamin C. Pierce]] |title=Types and Programming Languages |url=https://books.google.com/books?id=ti6zoAC9Ph8C |year=2002 |publisher=MIT Press |isbn=978-0-262-16209-8}}</ref>{{rp|pages=320}} refers to the automatic detection of the [[type (type theory)|type]] of an expression in a [[formal language]]. These include [[programming language]]s and mathematical [[type system]]s, but also [[natural languages]] in some branches of [[computer science]] and [[linguistics]].

==Nontechnical explanation==
In a typed language, a term's type determines the ways it can and cannot be used in that language. For example, consider the English language and terms that could fill in the blank in the phrase "sing _."  The term "a song" is of singable type, so it could be placed in the blank to form a meaningful phrase: "sing a song."  On the other hand, the term "a friend" does not have the singable type, so "sing a friend" is nonsense. At best it might be metaphor; bending type rules is a feature of poetic language.

A term's type can also affect the interpretation of operations involving that term. For instance, "a song" is of composable type, so we interpret it as the thing created in the phrase "write a song". On the other hand, "a friend" is of recipient type, so we interpret it as the addressee in the phrase "write a friend". In normal language, we would be surprised if "write a song" meant addressing a letter to a song or "write a friend" meant drafting a friend on paper.

Terms with different types can even refer to materially the same thing. For example, we would interpret "to hang up the clothes line" as putting it into use, but "to hang up the leash" as putting it away, even though, in context, both "clothes line" and "leash" might refer the same rope, just at different times.

Typings are often used to prevent an object from being considered too generally. For instance, if the type system treats all numbers as the same, then a programmer who accidentally writes code where <code>4</code> is supposed to mean "4 seconds" but is interpreted as "4 meters" would have no warning of their mistake until it caused problems at runtime. By incorporating [[unit of measurement|units]] into the type system, these mistakes can be detected much earlier. As another example, [[Russell's paradox]] arises when anything can be a set element and any predicate can define a set, but more careful typing gives several ways to resolve the paradox. In fact, Russell's paradox sparked early versions of type theory.

There are several ways that a term can get its type:

* The type might be provided from somewhere outside the passage. For instance, if a speaker refers to "a song" in English, they generally do not have to tell the listener that "a song" is singable and composable; that information is part of their shared background knowledge.
* The type can be declared explicitly. For example, a programmer might write a statement like <code>delay: seconds := 4</code> in their code, where the colon is the conventional mathematical symbol to mark a term with its type. That is, this statement is not only setting <code>delay</code> to the value <code>4</code>, but the <code>delay: seconds</code> part also indicates that <code>delay</code>'s type is an amount of time in seconds.
* The type can be '''inferred''' from context. For example, in the phrase "I bought it for a song", we can observe that trying to give the term "a song" types like "singable" and "composable" would lead to nonsense, whereas the type "amount of currency" works out. Therefore, without having to be told, we conclude that "song" here must mean "little to nothing", as in the English idiom "{{wt|en|for a song}}", not "a piece of music, usually with lyrics".

Especially in programming languages, there may not be much shared background knowledge available to the computer. In [[manifest typing|manifestly typed]] languages, this means that most types have to be declared explicitly. '''Type inference''' aims to alleviate this burden, freeing the author from declaring types that the computer should be able to deduce from context.

==Type-checking vs. type-inference==

In a typing, an expression E is opposed to a type T, formally written as E : T. Usually a typing only makes sense within some context, which is omitted here.

In this setting, the following questions are of particular interest:

# E : T? In this case, both an expression E and a type T are given. Now, is E really a T? This scenario is known as [[type-checking]].
# E : _? Here, only the expression is known. If there is a way to derive a type for E, then we have accomplished ''type inference''.
# _ : T? The other way round. Given only a type, is there any expression for it or does the type have no values? Is there any example of a T? This is known as [[type inhabitation]].

For the [[simply typed lambda calculus]], all three questions are [[Decidability (logic)#Decidability of a theory|decidable]]. The situation is not as comfortable when more [[Expressive power (computer science)|expressive]] types are allowed.

==Types in programming languages==
{{More citations needed section|date=November 2020}}

Types are a feature present in some [[strongly-typed programming language|strongly]] [[Type system#Static typing|statically typed]] languages. It is often characteristic of [[functional programming language]]s in general. Some languages that include type inference include [[C23 (C standard revision)|C23]],<ref>{{cite web |title=WG14-N3007 : Type inference for object definitions |url=https://www.open-std.org/jtc1/sc22/wg14/www/docs/n3007.htm |website=open-std.org |archive-url=https://web.archive.org/web/20221224105654/https://open-std.org/JTC1/SC22/WG14/www/docs/n3007.htm |archive-date=December 24, 2022 |date=2022-06-10 |url-status=live}}</ref> [[C++11]],<ref>{{Cite web|title=Placeholder type specifiers (since C++11) - cppreference.com|url=https://en.cppreference.com/w/cpp/language/auto|access-date=2021-08-15|website=en.cppreference.com}}</ref> [[C Sharp 3.0#Local variable type inference|C#]] (starting with version 3.0), [[Chapel (programming language)|Chapel]], [[Clean (programming language)|Clean]], [[Crystal (programming language)|Crystal]], [[D (programming language)|D]], [[Dart (programming language)|Dart]],<ref>{{Cite web|title=The Dart type system|url=https://dart.dev/guides/language/type-system|access-date=2020-11-21|website=dart.dev}}</ref> [[F Sharp (programming language)|F#]],<ref>{{Cite web|last=cartermp|title=Type Inference - F#|url=https://docs.microsoft.com/en-us/dotnet/fsharp/language-reference/type-inference|access-date=2020-11-21|website=docs.microsoft.com|language=en-us}}</ref> [[FreeBASIC]], [[Go (programming language)|Go]], [[Haskell (programming language)|Haskell]], [[Java (programming language)|Java]] (starting with version 10), [[Julia (programming language)|Julia]],<ref>{{Cite web|title=Inference · The Julia Language|url=https://docs.julialang.org/en/v1/devdocs/inference/|access-date=2020-11-21|website=docs.julialang.org}}</ref> [[Kotlin (programming language)|Kotlin]],<ref>{{Cite web|title=Kotlin language specification|url=https://kotlinlang.org/spec/type-inference.html|access-date=2021-06-28|website=kotlinlang.org}}</ref> [[ML (programming language)|ML]], [[Nim (programming language)|Nim]], [[OCaml]], [[Opa (programming language)|Opa]], Q#, [[RPython]], [[Rust (programming language)|Rust]],<ref>{{Cite web|title=Statements - The Rust Reference|url=https://doc.rust-lang.org/reference/statements.html?highlight=inference#let-statements|access-date=2021-06-28|website=doc.rust-lang.org}}</ref> [[Scala (programming language)|Scala]],<ref>{{Cite web|title=Type Inference|url=https://docs.scala-lang.org/tour/type-inference.html|access-date=2020-11-21|website=Scala Documentation}}</ref> [[Swift (programming language)|Swift]],<ref>{{Cite web|title=The Basics — The Swift Programming Language (Swift 5.5)|url=https://docs.swift.org/swift-book/LanguageGuide/TheBasics.html#ID322|access-date=2021-06-28|website=docs.swift.org}}</ref> [[TypeScript]],<ref>{{Cite web|title=Documentation - Type Inference|url=https://www.typescriptlang.org/docs/handbook/type-inference.html|access-date=2020-11-21|website=www.typescriptlang.org|language=en}}</ref> [[Vala (programming language)|Vala]],<ref>{{Cite web|title=Projects/Vala/Tutorial - GNOME Wiki!|url=https://wiki.gnome.org/Projects/Vala/Tutorial#Type_Inference|access-date=2021-06-28|website=wiki.gnome.org}}</ref> [[Zig (programming language)|Zig]], and [[Visual Basic .NET#2008 (VB 9.0)|Visual Basic]]<ref>{{Cite web|last=KathleenDollard|title=Local Type Inference - Visual Basic|url=https://docs.microsoft.com/en-us/dotnet/visual-basic/programming-guide/language-features/variables/local-type-inference|access-date=2021-06-28|website=docs.microsoft.com|language=en-us}}</ref> (starting with version 9.0). 
The majority of them use a simple form of type inference; the [[Hindley–Milner type system]] can provide more complete type inference. The ability to infer types automatically makes many programming tasks easier, leaving the programmer free to omit [[type signature|type annotations]] while still permitting type checking.

In some programming languages, all values have a [[data type]] explicitly declared at [[compile time]], limiting the values a particular expression can take on at [[Run time (program lifecycle phase)|run-time]]. Increasingly, [[just-in-time compilation]] blurs the distinction between run time and compile time. However, historically, if the type of a value is known only at run-time, these languages are [[dynamically typed]]. In other languages, the type of an expression is known only at [[compile time]]; these languages are [[statically typed]]. In most statically typed languages, the input and output types of functions and [[local variable]]s ordinarily must be explicitly provided by type annotations. For example, in [[ANSI C]]:
<syntaxhighlight lang="c">
int add_one(int x) {
    int result; /* declare integer result */

    result = x + 1;
    return result;
}
</syntaxhighlight>
The [[Type signature|signature]] of this function definition, <code>int add_one(int x)</code>, declares that <code>add_one</code> is a function that takes one argument, an [[integer (computer science)|integer]], and returns an integer. <code>int result;</code> declares that the local variable <code>result</code> is an integer. In a hypothetical language supporting type inference, the code might be written like this instead:
<syntaxhighlight lang="javascript">
add_one(x) {
    var result;  /* inferred-type variable result */
    var result2; /* inferred-type variable result #2 */

    result = x + 1;
    result2 = x + 1.0;  /* this line won't work (in the proposed language) */
    return result;
}</syntaxhighlight>
This is identical to how code is written in the language [[Dart (programming language)|Dart]], except that it is subject to some added constraints as described below.  It would be possible to ''infer'' the types of all the variables at compile time. In the example above, the compiler would infer that <code>result</code> and <code>x</code> have type integer since the constant <code>1</code> is type integer, and hence that <code>add_one</code> is a function <code>int -> int</code>. The variable <code>result2</code> isn't used in a legal manner, so it wouldn't have a type.

In the imaginary language in which the last example is written, the compiler would assume that, in the absence of information to the contrary, <code>+</code> takes two integers and returns one integer. (This is how it works in, for example, [[OCaml]].) From this, the type inferencer can infer that the type of <code>x + 1</code> is an integer, which means <code>result</code> is an integer and thus the return value of <code>add_one</code> is an integer. Similarly, since <code>+</code> requires both of its arguments be of the same type<!--integers-->, <code>x</code> must be an integer, and thus, <code>add_one</code> accepts one integer as an argument.

However, in the subsequent line, ''result2'' is calculated by adding a decimal <code>1.0</code> with [[floating-point arithmetic]], causing a conflict in the use of <code>x</code> for both integer and floating-point expressions. The correct type-inference algorithm for such a situation has been known [[#Hindley–Milner type inference algorithm|since 1958]] and has been known to be correct since 1982. It revisits the prior inferences and uses the most general type from the outset: in this case floating-point. This can however have detrimental implications, for instance using a floating-point from the outset can introduce precision issues that would have not been there with an integer type.

Frequently, however, degenerate type-inference algorithms are used that cannot backtrack and instead generate an error message in such a situation. This behavior may be preferable as type inference may not always be neutral algorithmically, as illustrated by the prior floating-point precision issue.

An algorithm of intermediate generality implicitly declares ''result2'' as a floating-point variable, and the addition implicitly converts <code>x</code> to a floating point. This can be correct if the calling contexts never supply a floating point argument. Such a situation shows the difference between ''type inference'', which does not involve [[type conversion]], and [[implicit type conversion]], which forces data to a different data type, often without restrictions.

Finally, a significant downside of complex type-inference algorithm is that the resulting type inference resolution is not going to be obvious to humans (notably because of the backtracking), which can be detrimental as code is primarily intended to be comprehensible to humans.

The recent emergence of [[just-in-time compilation]] allows for hybrid approaches where the type of arguments supplied by the various calling context is known at compile time, and can generate a large number of compiled versions of the same function. Each compiled version can then be optimized for a different set of types. For instance, JIT compilation allows there to be at least two compiled versions of ''add_one'':

:A version that accepts an integer input and uses implicit type conversion.
:A version that accepts a floating-point number as input and uses floating point instructions throughout.

==Technical description==
Type inference is the ability to automatically deduce, either partially or fully, the type of an expression 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 is simple enough.

To obtain the information required to infer the type of an expression, the compiler either gathers this information as an aggregate and subsequent reduction of the type annotations given for its subexpressions, or through an implicit understanding of the type of various atomic values (e.g. 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 complex forms of [[higher-order programming]] and [[polymorphism (computer science)|polymorphism]], it is not always possible for the compiler to infer as much, and type annotations are occasionally necessary for disambiguation. For instance, type inference with [[polymorphic recursion]] is known to be undecidable. Furthermore, explicit type annotations can be used to optimize code by forcing the compiler to use a more specific (faster/smaller) type than it had inferred.<ref>{{cite book |author1=Bryan O'Sullivan |author2=Don Stewart |author3=John Goerzen |year=2008 |title=Real World Haskell |chapter=Chapter 25. Profiling and optimization |publisher=O'Reilly |chapter-url=http://book.realworldhaskell.org/read/profiling-and-optimization.html}}</ref>

Some methods for type inference are based on [[constraint satisfaction problem|constraint satisfaction]]<ref>Talpin, Jean-Pierre, and Pierre Jouvelot. "[https://pdfs.semanticscholar.org/57b0/e240c36a26c05b2eb7b6ccf3fabbfd383b25.pdf Polymorphic type, region and effect inference]." Journal of functional programming 2.3 (1992): 245-271.</ref> or [[satisfiability modulo theories]].<ref>{{Cite book|chapter-url=https://link.springer.com/chapter/10.1007/978-3-319-96142-2_2|doi=10.1007/978-3-319-96142-2_2|chapter=MaxSMT-Based Type Inference for Python 3|title=Computer Aided Verification|series=Lecture Notes in Computer Science|year=2018|last1=Hassan|first1=Mostafa|last2=Urban|first2=Caterina|last3=Eilers|first3=Marco|last4=Müller|first4=Peter|volume=10982|pages=12–19|isbn=978-3-319-96141-5}}</ref>

==High-Level Example==
As an example, the [[Haskell (programming language)|Haskell]] function <syntaxhighlight lang="haskell" inline>map</syntaxhighlight> applies a function to each element of a list, and may be defined as:
<syntaxhighlight lang="haskell">
map f [] = []
map f (first:rest) = f first : map f rest
</syntaxhighlight>
(Recall that <syntaxhighlight lang="haskell" inline>:</syntaxhighlight> in Haskell denotes [[cons]], structuring a head element and a list tail into a bigger list or destructuring a nonempty list into its head element and its tail. It does not denote "of type" as in mathematics and elsewhere in this article; in Haskell that "of type" operator is written <syntaxhighlight lang="haskell" inline>::</syntaxhighlight> instead.)

Type inference on the <syntaxhighlight lang="haskell" inline>map</syntaxhighlight> function proceeds as follows. <syntaxhighlight lang="haskell" inline>map</syntaxhighlight> is a function of two arguments, so its type is constrained to be of the form <syntaxhighlight lang="haskell" inline>a -> b -> c</syntaxhighlight>. In Haskell, the patterns <syntaxhighlight lang="haskell" inline>[]</syntaxhighlight> and <syntaxhighlight lang="haskell" inline>(first:rest)</syntaxhighlight> always match lists, so the second argument must be a list type: <syntaxhighlight lang="haskell" inline>b = [d]</syntaxhighlight> for some type <syntaxhighlight lang="haskell" inline>d</syntaxhighlight>. Its first argument <syntaxhighlight lang="haskell" inline>f</syntaxhighlight> is [[function application|applied]] to the argument <syntaxhighlight lang="haskell" inline>first</syntaxhighlight>, which must have type <syntaxhighlight lang="haskell" inline>d</syntaxhighlight>, corresponding with the type in the list argument, so <syntaxhighlight lang="haskell" inline>f :: d -> e</syntaxhighlight> (<syntaxhighlight lang="haskell" inline>::</syntaxhighlight> means "is of type") for some type <syntaxhighlight lang="haskell" inline>e</syntaxhighlight>. The return value of <syntaxhighlight lang="haskell" inline>map f</syntaxhighlight>, finally, is a list of whatever <syntaxhighlight lang="haskell" inline>f</syntaxhighlight> produces, so <syntaxhighlight lang="haskell" inline>[e]</syntaxhighlight>.

Putting the parts together leads to <syntaxhighlight lang="haskell" inline>map :: (d -> e) -> [d] -> [e]</syntaxhighlight>. Nothing is special about the type variables, so it can be relabeled as
<syntaxhighlight lang="haskell" style="">
map :: (a -> b) -> [a] -> [b]
</syntaxhighlight>

It turns out that this is also the most general type, since no further constraints apply. As the inferred type of <syntaxhighlight lang="haskell" inline>map</syntaxhighlight> is [[parametric polymorphism|parametrically polymorphic]], the type of the arguments and results of <syntaxhighlight lang="haskell" inline>f</syntaxhighlight> are not inferred, but left as type variables, and so <syntaxhighlight lang="haskell" inline>map</syntaxhighlight> can be applied to functions and lists of various types, as long as the actual types match in each invocation.

==Detailed Example==
The algorithms used by programs like compilers are equivalent to the informally structured reasoning above, but a bit more verbose and methodical. The exact details depend on the inference algorithm chosen (see the following section for the best-known algorithm), but the example below gives the general idea. We again begin with the definition of <syntaxhighlight lang="haskell" inline>map</syntaxhighlight>:
<syntaxhighlight lang="haskell">
map f [] = []
map f (first:rest) = f first : map f rest
</syntaxhighlight>
(Again, remember that the <syntaxhighlight lang="haskell" inline>:</syntaxhighlight> here is the Haskell list constructor, not the "of type" operator, which Haskell instead spells <syntaxhighlight lang="haskell" inline>::</syntaxhighlight>.)

First, we make fresh type variables for each individual term:
* <code>α</code> shall denote the type of <syntaxhighlight lang="haskell" inline>map</syntaxhighlight> that we want to infer.
* <code>β</code> shall denote the type of <syntaxhighlight lang="haskell" inline>f</syntaxhighlight> in the first equation.
* <code>[γ]</code> shall denote the type of <syntaxhighlight lang="haskell" inline>[]</syntaxhighlight> on the left side of the first equation.
* <code>[δ]</code> shall denote the type of <syntaxhighlight lang="haskell" inline>[]</syntaxhighlight> on the right side of the first equation.
* <code>ε</code> shall denote the type of <syntaxhighlight lang="haskell" inline>f</syntaxhighlight> in the second equation.
* <code>ζ -> [ζ] -> [ζ]</code> shall denote the type of <syntaxhighlight lang="haskell" inline>:</syntaxhighlight> on the left side of the first equation. (This pattern is known from its definition.)
* <code>η</code> shall denote the type of <syntaxhighlight lang="haskell" inline>first</syntaxhighlight>.
* <code>θ</code> shall denote the type of <syntaxhighlight lang="haskell" inline>rest</syntaxhighlight>.
* <code>ι -> [ι] -> [ι]</code> shall denote the type of <syntaxhighlight lang="haskell" inline>:</syntaxhighlight> on the right side of the first equation.

Then we make fresh type variables for subexpressions built from these terms, constraining the type of the function being invoked accordingly:
* <code>κ</code> shall denote the type of <syntaxhighlight lang="haskell" inline>map f []</syntaxhighlight>. We conclude that <code>α ~ β -> [γ] -> κ</code> where the "similar" symbol <code>~</code> means "unifies with"; we are saying that <code>α</code>, the type of <syntaxhighlight lang="haskell" inline>map</syntaxhighlight>, must be compatible with the type of a function taking a <code>β</code> and a list of <code>γ</code>s and returning a <code>κ</code>.
* <code>λ</code> shall denote the type of <syntaxhighlight lang="haskell" inline>(first:rest)</syntaxhighlight>. We conclude that <code>ζ -> [ζ] -> [ζ] ~ η -> θ -> λ</code>.
* <code>μ</code> shall denote the type of <syntaxhighlight lang="haskell" inline>map f (first:rest)</syntaxhighlight>. We conclude that <code>α ~ ε -> λ -> μ</code>.
* <code>ν</code> shall denote the type of <syntaxhighlight lang="haskell" inline>f first</syntaxhighlight>. We conclude that <code>ε ~ η -> ν</code>.
* <code>ξ</code> shall denote the type of <syntaxhighlight lang="haskell" inline>map f rest</syntaxhighlight>. We conclude that <code>α ~ ε -> θ -> ξ</code>.
* <code>ο</code> shall denote the type of <syntaxhighlight lang="haskell" inline>f first : map f rest</syntaxhighlight>. We conclude that <code>ι -> [ι] -> [ι] ~ ν -> ξ -> ο</code>.

We also constrain the left and right sides of each equation to unify with each other: <code>κ ~ [δ]</code> and <code>μ ~ ο</code>. Altogether the system of unifications to solve is:
<pre>
α ~ β -> [γ] -> κ
ζ -> [ζ] -> [ζ] ~ η -> θ -> λ
α ~ ε -> λ -> μ
ε ~ η -> ν
α ~ ε -> θ -> ξ
ι -> [ι] -> [ι] ~ ν -> ξ -> ο
κ ~ [δ]
μ ~ ο
</pre>

Then we substitute until no further variables can be eliminated. The exact order is immaterial; if the code type-checks, any order will lead to the same final form. Let us begin by substituting <code>ο</code> for <code>μ</code> and <code>[δ]</code> for <code>κ</code>:
<pre>
α ~ β -> [γ] -> [δ]
ζ -> [ζ] -> [ζ] ~ η -> θ -> λ
α ~ ε -> λ -> ο
ε ~ η -> ν
α ~ ε -> θ -> ξ
ι -> [ι] -> [ι] ~ ν -> ξ -> ο
</pre>

Substituting <code>ζ</code> for <code>η</code>, <code>[ζ]</code> for <code>θ</code> and <code>λ</code>, <code>ι</code> for <code>ν</code>, and <code>[ι]</code> for <code>ξ</code> and <code>ο</code>, all possible because a type constructor like <syntaxhighlight lang="haskell" inline>· -> ·</syntaxhighlight> is [[Inverse function#Definitions|invertible]] in its arguments:
<pre>
α ~ β -> [γ] -> [δ]
α ~ ε -> [ζ] -> [ι]
ε ~ ζ -> ι
</pre>

Substituting <code>ζ -> ι</code> for <code>ε</code> and <code>β -> [γ] -> [δ]</code> for <code>α</code>, keeping the second constraint around so that we can recover <code>α</code> at the end:
<pre>
α ~ (ζ -> ι) -> [ζ] -> [ι]
β -> [γ] -> [δ] ~ (ζ -> ι) -> [ζ] -> [ι]
</pre>

And, finally, substituting <code>(ζ -> ι)</code> for <code>β</code> as well as <code>ζ</code> for <code>γ</code> and <code>ι</code> for <code>δ</code> because a type constructor like <syntaxhighlight lang="haskell" inline>[·]</syntaxhighlight> is [[Inverse function#Definitions|invertible]] eliminates all the variables specific to the second constraint:
<pre>
α ~ (ζ -> ι) -> [ζ] -> [ι]
</pre>

No more substitutions are possible, and relabeling gives us <syntaxhighlight lang="haskell" inline>map :: (a -> b) -> [a] -> [b]</syntaxhighlight>, the same as we found without going into these details.

=={{anchor|algorithm}}Hindley–Milner type inference algorithm==
{{Main|Hindley–Milner type system}}
The algorithm first used to perform type inference is now informally termed the Hindley–Milner algorithm, although the algorithm should properly be attributed to Damas and Milner.<ref name="Damas-and-Milner-1982">{{Citation
 |last1= Damas |first1= Luis
 |last2= Milner |first2= Robin
 |contribution= Principal type-schemes for functional programs
 |title= POPL '82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on principles of programming languages
 |publisher= ACM
 |pages= 207–212
 |year= 1982
 |url= http://groups.csail.mit.edu/pag/6.883/readings/p207-damas.pdf
 }}</ref>
It is also traditionally called ''type reconstruction''.<ref name="TAPL" />{{rp|pages=320}} If a term is well-typed in accordance with Hindley–Milner typing rules, then the rules generate a principal typing for the term. The process of discovering this principal typing is the process of "reconstruction".

The origin of this algorithm is the type inference algorithm for the [[simply typed lambda calculus]] that was devised by [[Haskell Curry]] and [[Robert Feys]] in 1958.{{Citation needed|reason=This probably refers to [Combinatory Logic Volume 1 https://www.worldcat.org/title/combinatory-logic-vol-1-haskell-b-curry-and-robert-feys-with-two-sections-by-william-craig/oclc/769219250], however this actual claim is hard to find - it's 417 pages and has no table of contents. Please add a citation with page numbers if you can confirm this is a valid source. Also update [[Hindley–Milner type system]] as this claim is present there too.|date=February 2021}}
In 1969 [[J. Roger Hindley]] extended this work and proved that their algorithm always inferred the most general type.
In 1978 [[Robin Milner]],<ref>{{Citation
 |last1= Milner |first1= Robin
 |title= A Theory of Type Polymorphism in Programming
 |journal=  Journal of Computer and System Sciences
 |pages= 348–375
 |volume= 17
 |issue= 3
 |year= 1978
 |doi=10.1016/0022-0000(78)90014-4
 |doi-access= free
 |hdl= 20.500.11820/d16745d7-f113-44f0-a7a3-687c2b709f66
 |hdl-access= free
 }}</ref> independently of Hindley's work, provided an equivalent algorithm, [[Algorithm W]].
In 1982 [[Luis Damas]]<ref name="Damas-and-Milner-1982" /> finally proved that Milner's algorithm is complete and extended it to support systems with polymorphic references.

==Side-effects of using the most general type==
By design, type inference will infer the most general type appropriate. However, many languages, especially older programming languages, have slightly unsound type systems, where using a more general types may not always be algorithmically neutral. Typical cases include:
* Floating-point types being considered as generalizations of integer types. Actually, floating-point arithmetic has different precision and wrapping issues than integers do.
* Variant/dynamic types being considered as generalizations of other types in cases where this affects the selection of operator overloads. For example, the <code>+</code> operator may add integers but may concatenate variants as strings, even if those variants hold integers.

==Type inference for natural languages==
Type inference algorithms have been used to analyze [[natural languages]] as well as programming languages.<ref>Center, Artificiał Intelligence. [https://www.sri.com/sites/default/files/uploads/publications/pdf/511.pdf Parsing and type inference for natural and computer languages] {{Webarchive|url=https://web.archive.org/web/20120704032805/https://www.sri.com/sites/default/files/uploads/publications/pdf/511.pdf |date=2012-07-04 }}. Diss. Stanford University, 1989.</ref><ref>Emele, Martin C., and Rémi Zajac. "[https://aclanthology.info/pdf/C/C90/C90-3052.pdf Typed unification grammars] {{Webarchive|url=https://web.archive.org/web/20180205072400/https://aclanthology.info/pdf/C/C90/C90-3052.pdf |date=2018-02-05 }}." Proceedings of the 13th conference on Computational linguistics-Volume 3. Association for Computational Linguistics, 1990.</ref><ref>Pareschi, Remo. "[https://www.era.lib.ed.ac.uk/bitstream/handle/1842/19215/PareschiR_1989redux.pdf?sequence=1 Type-driven natural language analysis]." (1988).</ref> Type inference algorithms are also used in some [[grammar induction]]<ref>Fisher, Kathleen, et al. "Fisher, Kathleen, et al. "[https://www.cs.princeton.edu/~dpw/papers/learningpopl08-final.pdf From dirt to shovels: fully automatic tool generation from ad hoc data]." ACM SIGPLAN Notices. Vol. 43. No. 1. ACM, 2008." ACM SIGPLAN Notices. Vol. 43. No. 1. ACM, 2008.</ref><ref>{{cite journal | last1 = Lappin | first1 = Shalom | last2 = Shieber | first2 = Stuart M. | year = 2007 | title = Machine learning theory and practice as a source of insight into universal grammar | url = https://dash.harvard.edu/bitstream/handle/1/2031673/MachineLearning.pdf?sequence=3 | journal = Journal of Linguistics | volume = 43 | issue = 2| pages = 393–427 | doi=10.1017/s0022226707004628| s2cid = 215762538 }}</ref> and [[constraint-based grammar]] systems for natural languages.<ref name="Shieber1992">{{cite book|author=Stuart M. Shieber|title=Constraint-based Grammar Formalisms: Parsing and Type Inference for Natural and Computer Languages|url=https://books.google.com/books?id=QcYl_ylrHmcC&q=%22type+inference%22|year=1992|publisher=MIT Press|isbn=978-0-262-19324-5}}</ref>

==References==
{{Reflist}}

==External links==
* [http://www.cis.upenn.edu/~bcpierce/types/archives/1988/msg00042.html Archived e-mail message] by Roger Hindley, explains history of type inference
* [https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=7775e9c89fdf64b677b091259393a0f26698d0ee Polymorphic Type Inference] by Michael Schwartzbach, gives an overview of Polymorphic type inference.
* [http://lucacardelli.name/Papers/BasicTypechecking.pdf Basic Typechecking] paper by Luca Cardelli, describes algorithm, includes implementation in [[Modula-2]]
* [http://dysphoria.net/2009/06/28/hindley-milner-type-inference-in-scala/ Implementation] of Hindley–Milner type inference in [[Scala (programming language)|Scala]], by Andrew Forrest (retrieved July 30, 2009)
* {{webarchive |url=https://web.archive.org/web/20070218103011/http://www.cs.berkeley.edu/~nikitab/courses/cs263/hm.html |date=February 18, 2007 |title=Implementation of Hindley-Milner in Perl 5, by Nikita Borisov }}
* [https://web.archive.org/web/20090101030825/http://www.codecommit.com/blog/scala/what-is-hindley-milner-and-why-is-it-cool What is Hindley-Milner? (and why is it cool?)] Explains Hindley–Milner, examples in Scala

{{DEFAULTSORT:Type Inference}}
<!--Categories-->
[[Category:Type inference| ]]
[[Category:Type systems]]
[[Category:Type theory]]
[[Category:Inference]]
[[Category:Articles with example C code]]
[[Category:Articles with example Haskell code]]
[[Category:Articles with example JavaScript code]]