In type theory, type inference (sometimes called type reconstruction) is the automatic detection of the type of an expression. These include programming languages and mathematical type systems, but also natural languages in some branches of computer science and linguistics. Typeability is sometimes used quasi-synonymously with type inference, however some authors make a distinction between typeability as a decision problem (that has yes/no answer) and type inference as the computation of an actual type for a term.
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 4 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 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 delay: seconds := 4 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 delay to the value 4, but the delay: seconds part also indicates that delay'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 "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 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 decidable. The situation is not as comfortable when more expressive types are allowed.
Types in programming languages
Types are a feature present in some strongly statically typed languages. It is often characteristic of functional programming languages in general. Some languages that include type inference include C (since C23), C++ (since C++11), C# (starting with version 3.0), Chapel, Clean, Crystal, D, Dart, F#, FreeBASIC, Go, Haskell, Java (starting with version 10), Julia, Kotlin, ML, Nim, OCaml, Opa, Q#, RPython, Rust, Scala, Swift, TypeScript, Vala, Zig, and Visual Basic (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 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. 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 variables ordinarily must be explicitly provided by type annotations. For example, in ANSI C:
… excerpt ends here. Continue reading the full article.
