| Type systems |
|---|
| General concepts |
| Major categories |
| Minor categories |
Type inference, sometimes calledtype reconstruction,[1]: 320 refers to the automatic detection of thetype of an expression in aformal language. These includeprogramming languages and mathematicaltype systems, but alsonatural languages in some branches ofcomputer science andlinguistics.
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 where4 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 incorporatingunits 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:
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 settingdelay to the value4, but thedelay: seconds part also indicates thatdelay's type is an amount of time in seconds.Especially in programming languages, there may not be much shared background knowledge available to the computer. Inmanifestly 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.
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:
For thesimply typed lambda calculus, all three questions aredecidable. The situation is not as comfortable when moreexpressive types are allowed.
 | This sectionneeds additional citations forverification. Please helpimprove this article byadding citations to reliable sources in this section. Unsourced material may be challenged and removed.(November 2020) (Learn how and when to remove this message) |
Types are a feature present in somestronglystatically typed languages. It is often characteristic offunctional programming languages in general. Some languages that include type inference includeC23,[2]C++11,[3]C# (starting with version 3.0),Chapel,Clean,Crystal,D,F#,[4]FreeBASIC,Go,Haskell,Java (starting with version 10),Julia,[5]Kotlin,[6]ML,Nim,OCaml,Opa, Q#,RPython,Rust,[7]Scala,[8]Swift,[9]TypeScript,[10]Vala,[11]Dart,[12] andVisual Basic[13] (starting with version 9.0). The majority of them use a simple form of type inference; theHindley–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 omittype annotations while still permitting type checking.
In some programming languages, all values have adata type explicitly declared atcompile time, limiting the values a particular expression can take on atrun-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 aredynamically typed. In other languages, the type of an expression is known only atcompile time; these languages arestatically typed. In most statically typed languages, the input and output types of functions andlocal variables ordinarily must be explicitly provided by type annotations. For example, inANSI C:
intadd_one(intx){intresult;/* declare integer result */result=x+1;returnresult;}
Thesignature of this function definition,int add_one(int x), declares thatadd_one is a function that takes one argument, aninteger, and returns an integer.int result; declares that the local variableresult is an integer. In a hypothetical language supporting type inference, the code might be written like this instead:
add_one(x){varresult;/* inferred-type variable result */varresult2;/* inferred-type variable result #2 */result=x+1;result2=x+1.0;/* this line won't work (in the proposed language) */returnresult;}
This is identical to how code is written in the languageDart, except that it is subject to some added constraints as described below. It would be possible toinfer the types of all the variables at compile time. In the example above, the compiler would infer thatresult andx have type integer since the constant1 is type integer, and hence thatadd_one is a functionint -> int. The variableresult2 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,+ 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 ofx + 1 is an integer, which meansresult is an integer and thus the return value ofadd_one is an integer. Similarly, since+ requires both of its arguments be of the same type,x must be an integer, and thus,add_one accepts one integer as an argument.
However, in the subsequent line,result2 is calculated by adding a decimal1.0 withfloating-point arithmetic, causing a conflict in the use ofx for both integer and floating-point expressions. The correct type-inference algorithm for such a situation has been knownsince 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 declaresresult2 as a floating-point variable, and the addition implicitly convertsx to a floating point. This can be correct if the calling contexts never supply a floating point argument. Such a situation shows the difference betweentype inference, which does not involvetype conversion, andimplicit 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 ofjust-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 ofadd_one:
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 thetype 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 ofhigher-order programming andpolymorphism, it is not always possible for the compiler to infer as much, and type annotations are occasionally necessary for disambiguation. For instance, type inference withpolymorphic 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.[14]
Some methods for type inference are based onconstraint satisfaction[15] orsatisfiability modulo theories.[16]
As an example, theHaskell functionmap applies a function to each element of a list, and may be defined as:
mapf[]=[]mapf(first:rest)=ffirst:mapfrest
(Recall that: in Haskell denotescons, 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:: instead.)
Type inference on themap function proceeds as follows.map is a function of two arguments, so its type is constrained to be of the forma->b->c. In Haskell, the patterns[] and(first:rest) always match lists, so the second argument must be a list type:b=[d] for some typed. Its first argumentf isapplied to the argumentfirst, which must have typed, corresponding with the type in the list argument, sof::d->e (:: means "is of type") for some typee. The return value ofmapf, finally, is a list of whateverf produces, so[e].
Putting the parts together leads tomap::(d->e)->[d]->[e]. Nothing is special about the type variables, so it can be relabeled as
map::(a->b)->[a]->[b]
It turns out that this is also the most general type, since no further constraints apply. As the inferred type ofmap isparametrically polymorphic, the type of the arguments and results off are not inferred, but left as type variables, and somap can be applied to functions and lists of various types, as long as the actual types match in each invocation.
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 ofmap:
mapf[]=[]mapf(first:rest)=ffirst:mapfrest
(Again, remember that the: here is the Haskell list constructor, not the "of type" operator, which Haskell instead spells::.)
First, we make fresh type variables for each individual term:
α shall denote the type ofmap that we want to infer.β shall denote the type off in the first equation.[γ] shall denote the type of[] on the left side of the first equation.[δ] shall denote the type of[] on the right side of the first equation.ε shall denote the type off in the second equation.ζ -> [ζ] -> [ζ] shall denote the type of: on the left side of the first equation. (This pattern is known from its definition.)η shall denote the type offirst.θ shall denote the type ofrest.ι -> [ι] -> [ι] shall denote the type of: 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:
κ shall denote the type ofmapf[]. We conclude thatα ~ β -> [γ] -> κ where the "similar" symbol~ means "unifies with"; we are saying thatα, the type ofmap, must be compatible with the type of a function taking aβ and a list ofγs and returning aκ.λ shall denote the type of(first:rest). We conclude thatζ -> [ζ] -> [ζ] ~ η -> θ -> λ.μ shall denote the type ofmapf(first:rest). We conclude thatα ~ ε -> λ -> μ.ν shall denote the type offfirst. We conclude thatε ~ η -> ν.ξ shall denote the type ofmapfrest. We conclude thatα ~ ε -> θ -> ξ.ο shall denote the type offfirst:mapfrest. We conclude thatι -> [ι] -> [ι] ~ ν -> ξ -> ο.We also constrain the left and right sides of each equation to unify with each other:κ ~ [δ] andμ ~ ο. Altogether the system of unifications to solve is:
α ~ β -> [γ] -> κζ -> [ζ] -> [ζ] ~ η -> θ -> λα ~ ε -> λ -> με ~ η -> να ~ ε -> θ -> ξι -> [ι] -> [ι] ~ ν -> ξ -> οκ ~ [δ]μ ~ ο
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ο forμ and[δ] forκ:
α ~ β -> [γ] -> [δ]ζ -> [ζ] -> [ζ] ~ η -> θ -> λα ~ ε -> λ -> οε ~ η -> να ~ ε -> θ -> ξι -> [ι] -> [ι] ~ ν -> ξ -> ο
Substitutingζ forη,[ζ] forθ andλ,ι forν, and[ι] forξ andο, all possible because a type constructor like·->· isinvertible in its arguments:
α ~ β -> [γ] -> [δ]α ~ ε -> [ζ] -> [ι]ε ~ ζ -> ι
Substitutingζ -> ι forε andβ -> [γ] -> [δ] forα, keeping the second constraint around so that we can recoverα at the end:
α ~ (ζ -> ι) -> [ζ] -> [ι]β -> [γ] -> [δ] ~ (ζ -> ι) -> [ζ] -> [ι]
And, finally, substituting(ζ -> ι) forβ as well asζ forγ andι forδ because a type constructor like[·] isinvertible eliminates all the variables specific to the second constraint:
α ~ (ζ -> ι) -> [ζ] -> [ι]
No more substitutions are possible, and relabeling gives usmap::(a->b)->[a]->[b], the same as we found without going into these details.
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.[17]It is also traditionally calledtype reconstruction.[1]: 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 thesimply typed lambda calculus that was devised byHaskell Curry andRobert Feys in 1958.[citation needed]In 1969J. Roger Hindley extended this work and proved that their algorithm always inferred the most general type.In 1978Robin Milner,[18] independently of Hindley's work, provided an equivalent algorithm,Algorithm W.In 1982Luis Damas[17] finally proved that Milner's algorithm is complete and extended it to support systems with polymorphic references.
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:
+ operator may add integers but may concatenate variants as strings, even if those variants hold integers.Type inference algorithms have been used to analyzenatural languages as well as programming languages.[19][20][21] Type inference algorithms are also used in somegrammar induction[22][23] andconstraint-based grammar systems for natural languages.[24]