<p>Two of the most significant <a href="https://en.wikipedia.org/wiki/Type_inference" rel="noreferrer">type inference</a> schemes are <a href="https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system" rel="noreferrer">Hindley-Milner</a> and <a href="https://ncatlab.org/nlab/show/bidirectional+typechecking" rel="noreferrer">Bidirectional typing</a> but when do we actually need do type inference?</p>
<p>The simple case is something like:</p>
<pre><code>x: int = 1;
y: int = 2;
z: int = x + y;

x: int = 1;
y: int = 2;
z: auto = x + y;    //using auto to mean &quot;infer&quot;
</code></pre>
<p>z is an int because x and y are (providing + does not promote or otherwise alter the type)</p>
<p>or even just:</p>
<pre><code>x = 1;  
</code></pre>
<p>The <strong>type</strong> of x may be an integer because the <strong>value</strong> 1 is integer (though it could equally be a different numeric type or similar).</p>
<p>What are the motivating examples that lead us to need more complex inferences?</p>
<p>Different motivating examples lead us in different directions.
For example one extreme is:</p>
<pre><code>x: int[1..10];   // x is an integer restricted to the range 1..10
y: int[1..100];  // y is an integer restricted to the range 1..10

x+y: integer[2..110]    // z is an integer restricted to the range 2..110
</code></pre>
<p>This is perhaps a thinly veiled pro and cons of different type systems question so I don't expect a single answer.</p>

<types><type-inference><type-systems>
When do we need complex type inference?
CC BY-SA 4.0
2023-07-18T21:00:58.990Z
How do you know 1 is an integer and not a float, bigint, smallint, single bit, boolean, etc?
Bergi
CC BY-SA 4.0
2023-07-19T07:55:59.557Z
Of course. The purpose of the question was to stimulate interesting answers referencing different type systems as "what are the pros and cons of different type systems" seemed a bit broad. I've at least partly succeeded but I may have to ask a follow up question or two.
Bruce Adams
CC BY-SA 4.0
2023-07-19T16:20:40.993Z
There are the systems where all types can be inferred, and the systems which require annotations. Are you looking for something more detailed than that? Or is this more of a "why does anybody bother with dependent types?" sort of question, perhaps?
Corbin
CC BY-SA 4.0
2023-07-19T16:37:21.017Z
I was really hoping for a set of answers one for each of several different type systems but my question has been answer as worded. My own fault for not asking that question but the answers are interesting nonetheless.
Bruce Adams
CC BY-SA 4.0
2023-07-19T17:07:36.943Z
Regarding "*z is an int because x and y are*" -- not exactly.  in `z: auto = x + y`, if z is an int then that's because `x + y` is an int.  That may, in turn, follow from x and y each being an int, but conceivably (and in some similar real-world cases) the type inferred for z would *not* be the mutual type of x and y.
John Bollinger
CC BY-SA 4.0
2023-07-19T19:09:47.703Z
In your examples, does + wrap, limit to max(int), would assigning an overflow to an inferred int throw an exception, or would the result be undefined and erratic?
Mark Morgan Lloyd
CC BY-SA 4.0
2023-07-19T19:49:25.407Z
How (and why) you would implement a type system incorporating ranges this way is an entirely different question.
Bruce Adams
<p>I think a surprisingly big part of what makes type inference complex is <strong>nonlinearity</strong>—being able to freely copy and drop variables.</p>
<p>While your examples only show bottom-up <strong>type deduction</strong> from an initialiser to a variable, I’ll speak on <strong>type inference</strong> in the broader sense, where a variable’s type can also be inferred from its usage, by propagating type information also top-down and solving constraints in some way.</p>
<p>Type systems vary a <em>lot</em> in the complexity of those constraints. With some features like numerical ranges and subtyping, the constraint satisfaction itself might not be decidable. But setting that aside, our goal with type inference is to find a proof (a typing derivation) showing that a program is well-typed, guided by the structure of the program. Along the way, we apply typing rules based on how <strong>names identify relationships among program elements</strong>.</p>
<p>And nonlinearity complicates those relationships, in a few key ways.</p>
<h2>Dropping</h2>
<p>Dropped variables can be underconstrained, so we need to be able to find out if there’s an ambiguity, and tell the programmer. Whereas, if a variable <em>must</em> be used, then it <em>will</em> be used in the context of an environment that determines its type.</p>
<h2>Sharing</h2>
<p>Shared variables can be overconstrained, so we need to be able to find conflicts, too. If a variable can only be used at most once, it adds no extra constraints. But to enforce that its type must be consistent wherever it’s used, it takes a linear number of type constraints.</p>
<h2>Metavariables</h2>
<p>Metavars stand for unknown types to fill in later, and relate the occurrences of a variable with each other, so we can check that they all agree. Metavars also need to be recorded somewhere dynamically, whether as mutable references or as keys in a map. They can propagate type information far from its origin to identify subtle type conflicts—which is a good thing!—but for efficiency reasons they can’t retain much information about the path they took to get there. Therefore they can also make it hard to report an apparent type mismatch to the programmer in a friendly way.</p>
<p>Yet, metavars are only really needed by <strong>nonlinear constraints</strong> and <strong>nonlinear polymorphism</strong>. With linear variables, an <em>occurrence</em> of a variable can be identified with the variable itself. You can even infer the type of a relevant variable “backward”, by <em>checking</em> the expression where it’s used to find the (singular!) constraint on its type, which is unique or polymorphic.</p>
<p>And a polymorphic function is linear just when its type is also linear, that is, it uses all of its <em>type variables</em> linearly. For example:</p>
<div class="s-table-container">
<table class="s-table">
<thead>
<tr>
<th>Function</th>
<th>Type</th>
<th>Substructure</th>
</tr>
</thead>
<tbody>
<tr>
<td>identity</td>
<td>∀a. a<sup>−</sup> → a<sup>+</sup></td>
<td>Linear</td>
</tr>
<tr>
<td>map</td>
<td>∀a b. (a<sup>+</sup> → b<sup>−</sup>) → List a<sup>−</sup> → List b<sup>+</sup></td>
<td>Linear</td>
</tr>
<tr>
<td>swap</td>
<td>∀a b. (a<sup>−</sup> × b<sup>−</sup>) → (b<sup>+</sup> × a<sup>+</sup>)</td>
<td>Linear (unordered)</td>
</tr>
<tr>
<td>dup</td>
<td>∀a. a<sup>−</sup> → (a<sup>+</sup> × a<sup>+</sup>)</td>
<td>Nonlinear (relevant but not affine)</td>
</tr>
<tr>
<td>drop</td>
<td>∀a. a<sup>−</sup> → ()</td>
<td>Nonlinear (affine but not relevant)</td>
</tr>
</tbody>
</table>
</div>
<p>In a linear type, each type variable will be used exactly twice: once in a positive position (as an output / covariantly) and once in a negative position (as an input / contravariantly).</p>
<hr />
<p>This is all to say that a lot of the complexity and poor usability come from trying to solve the problem in full generality, without imposing any limitations on the programmer. But even if you want to be able to infer all types without <em>type signatures</em>, that doesn’t mean you have <em>no annotations</em> at all. And limitations are fine as long as they’re not <em>just</em> to please the compiler.</p>
<p>Suppose variables are written with a <code>var</code> keyword and functions are written with a <code>def</code> keyword, and the programmer <em>usually</em> wants monomorphic linear variables and polymorphic unrestricted functions; in that case, you can use <code>var</code> and <code>def</code> themselves as <strong>natural annotations</strong> to restrict or relax the rules of inference. Indeed that’s basically the trick of how <code>let</code> bindings are used to decide where to add polymorphism in Damas &amp; Milner’s algorithm.</p>

CC BY-SA 4.0
2023-07-20T17:49:39.770Z
2023-07-20T17:49:39.770Z
Jon Purdy
<p>For me, I did not intend to introduce <em>type inference</em> in my language. But I had two cases where I needed it.</p>
<p>After adding <strong>parametric polymorphism (Generics)</strong>:</p>
<ul>
<li><p><strong>Initialize empty Collections</strong></p>
<p>I wanted to be able to create collections without specifying the type variable for the collection, but instead infer the type variable from what is added to the collection.</p>
<p>e.g. init a list with <code>[]</code> and later call <code>List.append(34)</code>,</p>
<p>similar in Rust with an empty Vec using <code>let my_vec = Vec::new();</code> and later call <code>my_vec.push(34);</code>.</p>
<p>This is somewhat similar to Java 7, where the &quot;diamond operator&quot; was introduced, to be able to initialize collections without specifying the type variable: <code>new ArrayList&lt;&gt;()</code>.</p>
</li>
<li><p><strong>Tagged Union types</strong></p>
<p>I wanted to have tagged union types (e.g. enums with values, as in Rust and Swift) with generics. E.g. the type <code>Option&lt;t&gt; { None, Some(t) }</code> or <code>Result&lt;s,e&gt; { Ok(s), Err(e) }</code>. The <strong>type constructor</strong> of these types, may not resolve all type variables of the type, so type inference must be used to get the full type. A good example is when these type constructors are used in different if-branches:</p>
<pre><code>let result = if &lt;condition&gt; {
    None
} else {
    Some(34)
}
</code></pre>
<p>Here I needed to analyze both branches, to infer the type variables and get the full type of <code>result</code>.</p>
</li>
</ul>

CC BY-SA 4.0
2024-07-19T08:55:37.133Z
2024-07-19T09:02:48.843Z
2024-07-19T09:02:48.843Z
Jonas
<blockquote>
<p>when do we actually need do type inference?</p>
</blockquote>
<p>One time when you <em>need</em> type inference is when the type is &quot;unspeakable&quot;. In C# 3 we added anonymous types; there is no syntax for describing an anonymous type. If you want to represent the type &quot;a sequence of anonymously typed values where the value has a field <code>Address</code> of type <code>String</code> and a field <code>ShipsOn</code> of type <code>Date</code>&quot;, sorry, you've got to rely on type inference to work that out for you:</p>
<pre><code>var r = from c in customers           
        where c.Name.StartsWith(&quot;M&quot;)
        from o in c.Orders
        select new { c.Address, o.ShipsOn };
</code></pre>
<p>(You might reasonably make the argument that anonymous types are a bad idea in the first place and have been largely superseded by record types in versions of C# that shipped a decade later, but we had good reasons at the time and you can't see the future; let's leave aside the pros and cons of the anonymous type design.)</p>
<p>There are also situations where we don't <em>need</em> type inference but we very much want it in order to reduce the amount of redundancy on the page. Consider a LINQ query using the fluent syntax:</p>
<pre><code>q = people.Join(
    pets,
    person =&gt; person,
    pet =&gt; pet.Owner,
    (person, pet) =&gt; $&quot;{person.Name} owns {pet.Name}.&quot;);
</code></pre>
<p>Join is a generic method that takes four type arguments: the element types of the outer and inner sequences, the type of the join key, and the type of the resulting sequence. Without type inference C# requires that you state them:</p>
<pre><code>q = people.Join&lt;Person, Pet, Person, string&gt; (
    pets,
    person =&gt; person,
    pet =&gt; pet.Owner,
    (person, pet) =&gt; $&quot;{person.Name} owns {pet.Name}.&quot;);
</code></pre>
<p>which is a bit of a pain even if the types are speakable. We greatly preferred the option to allow these to be inferred over making the developer spell them out explicitly every time.</p>
<p>The generic method type inference algorithm uses a form of bidirectional typing.</p>

CC BY-SA 4.0
2023-07-19T00:50:41.377Z
2023-07-19T00:50:41.377Z
Eric Lippert
CC BY-SA 4.0
2023-07-21T00:09:50.927Z
Another example of this come from C++, where the type of a lambda function is unique to the definition and has no name, so can only be stored in an `auto` variable or used as an argument to a template so that the type is inferred appropriately.
occipita
CC BY-SA 4.0
2023-07-25T16:01:07.437Z
C++ iterators are often as good as "unspeakable". You have some data structure, you know it has an iterator with first, next an end, but it's basically impossible for a normal human being to write a declaration for that iterator that the compiler will accept. And if you could, it would be pointless, because all you care about is that it iterates, not what the type is.
gnasher729
CC BY-SA 4.0
2024-05-07T16:19:17.183Z
Yet another example is when you define a private type in a library named `T` and a public function `f` that returns `T` -- some languages allow this. In this case when you do `x = f()` you can't annotate type of `x` because you can't refer to `T`, it's private.
osa1
CC BY-SA 4.0
2024-05-07T19:21:40.703Z
@sinan: Great example. I think the .NET verifier requires that types mentioned in member signatures be as or more visible than the member, but not all runtimes are so strict.
Eric Lippert
<p>The examples you give are correct, but do not convey the right message, I believe.</p>
<ul>
<li>The first ones, with integers, are way too simple for type inference to have any advantage.</li>
<li>The last one, with ranges, is way too complex for most type inference systems. Adding two integer variables works, but after a few other operations, if some variables are re-used, the resulting range would be statically unpredictable.</li>
</ul>
<p>Here is an explanation for wanting type inference - there are certainly many other reasons and pros and cons, as you stated:</p>
<ul>
<li>In a statically typed language, the compiler necessarily implements some kind of type inference, to be able to check that some value has the type needed in the expression. In fact this is type checking instead of type inference, but the requirements on compiler logic are similar.</li>
<li>One of the reasons for having explicit types, is that it enables the compiler to detect places where the programmer is wrong about the type of a variable or function. Unfortunately, writing a type may be very difficult for the programmer, depending upon the language expression power and syntax. E.g. C++, which has huge expression power (functions that use functions or lambdas, templates of templates, etc.) but difficult syntax.</li>
<li>Having complex types is a natural consequence of programming languages where an element (typically a function) has the greatest possible extent (in matter of type) that its definition allows. This is the case with template arguments in C++: by default, any type is accepted as long as it implements the requirements (e.g. methods) used in the function code. So the typing system becomes way too complex for the human programmer (and actually is Turing-complete, so may be untractable even for the compiler).</li>
<li>As a consequence of the previous points, without type inference, in some cases the programmer is just struggling to write the type that the compiler expects, and already knows. So it becomes a game where the programmer is trying to guess the correct type by trial-and-error, and the compiler (which knows the correct type but won't tell it) answers &quot;wrong type, try again&quot;. This is very frustrating. It does not have the advantage of documenting the code, a benefit often stated in favor of explicit types, as types are anyway too complex to be readable by a programmer. So writing &quot;auto&quot; is just as good, less painful, and does not hinder code readability by complex type expressions that nobody is going to read anyway.</li>
</ul>

CC BY-SA 4.0
2023-07-18T13:37:46.123Z
2023-07-18T13:37:46.123Z
Jean-Armand Moroni
CC BY-SA 4.0
2023-07-18T17:23:04.757Z
This is a good answer to the question of “why have type inference?”, but I think the question is actually asking something subtly different: what type system features make type inference algorithms so complicated? I’ve given an attempt at answering *that* question [here](https://langdev.stackexchange.com/a/2429).
Alexis King
<p>It is true that, with a sufficiently simple type system, type inference is almost trivial. For example, writing a typechecker for the <a href="https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus" rel="noreferrer">simply typed lambda calculus</a> (STLC) is extraordinarily straightforward. However, note that the STLC includes explicit type signatures on all lambda-bound variables. Typing would be much more complex if this were not the case!</p>
<h2>Types can depend on usage</h2>
<p>As an example, consider the expression <span class="math-container">$λx. x + 1$</span>. What should this expression’s type be? If we assume that <span class="math-container">$1$</span> has type <span class="math-container">$\mathrm{Int}$</span>, then the expression should have type <span class="math-container">$\mathrm{Int} → \mathrm{Int}$</span>, but how do we deduce that?</p>
<p>In the examples given in your question, you are considering inferring the types of binding <em>definitions</em>, like <span class="math-container">$\,\mathbf{let}\; y = x + 1$</span>. In this case, type information always flows “bottom up”—we know that the type of <span class="math-container">$x + 1$</span> always has type <span class="math-container">$\mathrm{Int}$</span>, so we can deduce that <span class="math-container">$y$</span> also has type <span class="math-container">$\mathrm{Int}$</span>. But lambda-bound variables don’t work like this: they don’t have an associated expression that determines their value because their value is determined by their call site. So we have to examine the body of the lambda expression to observe how the variable is actually <em>used</em> in order to determine the argument’s type.</p>
<p>In languages with particularly sophisticated type inference, this principle can be taken even further. For example, consider the following expression:
<span class="math-container">$$\begin{array}{l}
\mathbf{let}\; \mathrm{identity} = λx. x \\
\phantom{\mathbf{let}}\llap{\mathbf{in}}\; \mathrm{identity}\ 1
\end{array}$$</span>
What is the type of <span class="math-container">$\mathrm{identity}$</span>? Let’s assume that our type system either does not support <a href="https://en.wikipedia.org/wiki/Parametric_polymorphism" rel="noreferrer">parametric polymorphism</a> or does not support inferring parametrically polymorphic types. (More on that subject later.) In that case, we must assign <span class="math-container">$\mathrm{identity}$</span> the monomorphic type <span class="math-container">$\mathrm{Int} → \mathrm{Int}$</span>, but the only way to know that is based on how the function is <em>used</em>. In general, the use site might be far away from the definition site, and there might even be several different use sites that conflict with each other! This requires some mechanism for propagating the type information across those distances and reconciling the different sources of information with each other (and producing error messages if the reconciliation fails).</p>
<p>Since type information can flow through the program in so many different ways, and across such long distances, this motivates the use of constraint solvers in type inference algorithms. Different parts of the program constrain the types in different ways, and the constraint solver reconciles the constraints.</p>
<h2>Polymorphism is extremely complicated</h2>
<p>Even global, constraint-based type inference can be relatively simple to implement if your type system is fully monomorphic. However, as soon as you choose to support <a href="https://en.wikipedia.org/wiki/Parametric_polymorphism" rel="noreferrer">parametric polymorphism</a>, things become <em>dramatically</em> more complicated. Consider the following expression:
<span class="math-container">$$\begin{array}{l}
\begin{aligned}
  \mathbf{let}\; \mathrm{identity} &amp;= λx. x\\
  \mathrm{add1} &amp;= λx. \mathrm{identity}\ (x + 1)\end{aligned} \\
\phantom{\mathbf{let}}\llap{\mathbf{in}}\; \mathrm{map}\ \mathrm{add1}\ (\mathrm{identity}\ [])
\end{array}$$</span>
The type of this expression is <span class="math-container">$\mathrm{List}\ \mathrm{Int}$</span>, but how do we deduce that? There is a lot to figure out:</p>
<ul>
<li><p>The type of <span class="math-container">$\mathrm{map}$</span> is known to be <span class="math-container">$∀a\,b.\: (a → b) → \mathrm{List}\ a → \mathrm{List}\ b$</span>. When we apply <span class="math-container">$\mathrm{map}$</span> to arguments, we must <em>instantiate</em> the type variables <span class="math-container">$a$</span> and <span class="math-container">$b$</span> with concrete types, and we have to somehow automatically pick those concrete types based on the types of the function’s arguments.</p>
</li>
<li><p>In this example, the arguments are <span class="math-container">$\mathrm{add1}$</span> and <span class="math-container">$\mathrm{identity}\ []$</span>. The second of those arguments gives us essentially zero information, because <span class="math-container">$\mathrm{identity}\ []$</span> itself could have type <span class="math-container">$\mathrm{List}\ \tau$</span> <em>for any type <span class="math-container">$\tau$</span></em>. So we have to use the type of <span class="math-container">$\mathrm{add1}$</span>.</p>
</li>
<li><p>To even figure out the above, we must infer the types of <span class="math-container">$\mathrm{identity}$</span> and <span class="math-container">$\mathrm{add1}$</span>. The type of <span class="math-container">$\mathrm{identity}$</span> must itself be polymorphic, as it is used at two different types: in the body of <span class="math-container">$\mathrm{add1}$</span> it has type <span class="math-container">$\mathrm{Int} → \mathrm{Int}$</span>, but in the argument to <span class="math-container">$\mathrm{map}$</span> it has type <span class="math-container">$\mathrm{List}\ \mathrm{Int} → \mathrm{List}\ \mathrm{Int}$</span>. Therefore, we must somehow automatically infer the polymorphic type <span class="math-container">$∀a. a → a$</span>.</p>
</li>
<li><p>To infer the type of <span class="math-container">$\mathrm{add1}$</span>, we must instantiate the polymorphic type of <span class="math-container">$\mathrm{identity}$</span> in the body to <span class="math-container">$\mathrm{Int} → \mathrm{Int}$</span> so that we can deduce that <span class="math-container">$\mathrm{add1}$</span> itself has type <span class="math-container">$\mathrm{Int} → \mathrm{Int}$</span>.</p>
</li>
<li><p>Finally, we must match up the type of <span class="math-container">$\mathrm{add1}$</span> with the type of the first argument of <span class="math-container">$\mathrm{map}$</span> to instantiate both of its type variables to <span class="math-container">$\mathrm{Int}$</span>, and only then do we know that the type of the overall expression is <span class="math-container">$\mathrm{List}\ \mathrm{Int}$</span>.</p>
</li>
</ul>
<p>As you can see, the flow of information here is not at all clear, and in general it’s not even obvious what inference is and is not possible. As it turns out, inference of parametric polymorphism in the presence of polymorphic recursion <a href="https://en.wikipedia.org/wiki/Polymorphic_recursion" rel="noreferrer">is known to be undecidable!</a> So it really doesn’t take much to turn the “simple” problem of type inference into a provably intractable one. Of course, there are still very many useful type inference algorithms that can infer the types of some subset of programs, but maximizing the set of programs a type inference algorithm can successfully accept can be very challenging.</p>
<h2>Subtyping makes things <em>even more</em> complicated</h2>
<p>Subtyping makes type inference even more challenging, especially when a language has full untagged <a href="https://en.wikipedia.org/wiki/Union_type" rel="noreferrer">union types</a>, not just inheritance. To see the issue, consider the following definition in TypeScript:</p>
<pre><code>const first = (x) =&gt; x[0];
</code></pre>
<p>What is the type of this function? All of the following would be legitimate types:</p>
<ul>
<li><code>Array&lt;A&gt; =&gt; A</code></li>
<li><code>[A] =&gt; A</code></li>
<li><code>[A, B] =&gt; A</code></li>
<li><code>[A, B, C] =&gt; A</code></li>
<li><code>[A, B, C, D] =&gt; A</code></li>
</ul>
<p>And so on. Note that these types aren’t even all subtypes of one another: <code>[A]</code> is a subtype of <code>Array&lt;A&gt;</code>, but the other types are not (since they are heterogeneous tuples). Since there is no “most general” type for <code>first</code>, we say that TypeScript lacks <a href="https://en.wikipedia.org/wiki/Principal_type" rel="noreferrer">principal types</a>, which means that <code>first</code> doesn’t even really <em>have</em> any one type.</p>
<p>Other systems have more restricted forms of subtyping, and those systems may have principal types, but determining what they are may still be very difficult. The problem is that determining whether two types “match up” is no longer a matter of equality of types, but a more complex relation, the subtyping relation. This makes implementing the “constraint solver” part of type inference much harder.</p>
<h2>Type inference in practice</h2>
<p>As the above examples hopefully illustrate, type inference is extremely hard. Moreover, it can often produce very poor error messages when absolutely everything is inferred. Therefore, most type systems use a hybrid approach in practice: they use a mixture of explicit type annotations and type inference. In some respects, this makes the problem easier, since the user has provided some type information that does not need to be inferred. However, in other respects, it can actually make the problem even harder, since the user’s type annotations must be interpreted, checked for validity, and reconciled with the program’s inferred types.</p>
<p>Simple type systems do not need such complex type inference algorithms, but almost no practical type systems are as simple as the STLC. The design of type systems that support inference is therefore a challenge of threading the needle: how can we design a type system that can express the things users wish to express, yet also permits sufficient type inference to reduce the burden of writing all those types down? There are many different answers, and unsatisfyingly, there is no “maximally sophisticated” system—every type system feature has tradeoffs.</p>

CC BY-SA 4.0
2023-07-18T17:21:41.953Z
2023-08-11T18:16:35.517Z
2023-08-11T18:16:35.517Z
Alexis King
CC BY-SA 4.0
2023-07-19T16:18:23.833Z
I feel like this answer is rooted in a particular approach to type-checking which is common in production-quality compilers. However, polymorphism and subtyping can both be easily *expressed* as constraints over a general-purpose unifier. (I would argue that the performance is decent, too!)
Corbin
CC BY-SA 4.0
2023-07-19T17:13:40.737Z
I feel there is a good answer to a different question in you comment if we can find a way to express it.
Bruce Adams
# When do we need complex type inference?
Posted by: username_0 on 2023-07-18
Two of the most significant type inference schemes are Hindley-Milner and Bidirectional typing but when do we actually need do type inference?
The simple case is something like:
x: int = 1;
y: int = 2;
z: int = x + y;

x: int = 1;
y: int = 2;
z: auto = x + y;    //using auto to mean "infer"

z is an int because x and y are (providing + does not promote or otherwise alter the type)
or even just:
x = 1;  

The type of x may be an integer because the value 1 is integer (though it could equally be a different numeric type or similar).
What are the motivating examples that lead us to need more complex inferences?
Different motivating examples lead us in different directions.
For example one extreme is:
x: int[1..10];   // x is an integer restricted to the range 1..10
y: int[1..100];  // y is an integer restricted to the range 1..10

x+y: integer[2..110]    // z is an integer restricted to the range 2..110

This is perhaps a thinly veiled pro and cons of different type systems question so I don't expect a single answer.
**Tags:** types type-inference type-systems
> **Comments:**
> **username_1**: How do you know 1 is an integer and not a float, bigint, smallint, single bit, boolean, etc?  
> **username_0**: Of course. The purpose of the question was to stimulate interesting answers referencing different type systems as "what are the pros and cons of different type systems" seemed a bit broad. I've at least partly succeeded but I may have to ask a follow up question or two.  
> **username_2**: There are the systems where all types can be inferred, and the systems which require annotations. Are you looking for something more detailed than that? Or is this more of a "why does anybody bother with dependent types?" sort of question, perhaps?  
> **username_0**: I was really hoping for a set of answers one for each of several different type systems but my question has been answer as worded. My own fault for not asking that question but the answers are interesting nonetheless.  
> **username_3**: Regarding "*z is an int because x and y are*" -- not exactly.  in `z: auto = x + y`, if z is an int then that's because `x + y` is an int.  That may, in turn, follow from x and y each being an int, but conceivably (and in some similar real-world cases) the type inferred for z would *not* be the mutual type of x and y.  
> **username_4**: In your examples, does + wrap, limit to max(int), would assigning an overflow to an inferred int throw an exception, or would the result be undefined and erratic?  
> **username_0**: How (and why) you would implement a type system incorporating ranges this way is an entirely different question.  
---
## 5 answers
### Answer by username_12 on 2023-07-18. Score: 20
It is true that, with a sufficiently simple type system, type inference is almost trivial. For example, writing a typechecker for the simply typed lambda calculus (STLC) is extraordinarily straightforward. However, note that the STLC includes explicit type signatures on all lambda-bound variables. Typing would be much more complex if this were not the case!
Types can depend on usage
As an example, consider the expression $λx. x + 1$. What should this expression’s type be? If we assume that $1$ has type $\mathrm{Int}$, then the expression should have type $\mathrm{Int} → \mathrm{Int}$, but how do we deduce that?
In the examples given in your question, you are considering inferring the types of binding definitions, like $\,\mathbf{let}\; y = x + 1$. In this case, type information always flows “bottom up”—we know that the type of $x + 1$ always has type $\mathrm{Int}$, so we can deduce that $y$ also has type $\mathrm{Int}$. But lambda-bound variables don’t work like this: they don’t have an associated expression that determines their value because their value is determined by their call site. So we have to examine the body of the lambda expression to observe how the variable is actually used in order to determine the argument’s type.
In languages with particularly sophisticated type inference, this principle can be taken even further. For example, consider the following expression:
$$\begin{array}{l}
\mathbf{let}\; \mathrm{identity} = λx. x \\
\phantom{\mathbf{let}}\llap{\mathbf{in}}\; \mathrm{identity}\ 1
\end{array}$$
What is the type of $\mathrm{identity}$? Let’s assume that our type system either does not support parametric polymorphism or does not support inferring parametrically polymorphic types. (More on that subject later.) In that case, we must assign $\mathrm{identity}$ the monomorphic type $\mathrm{Int} → \mathrm{Int}$, but the only way to know that is based on how the function is used. In general, the use site might be far away from the definition site, and there might even be several different use sites that conflict with each other! This requires some mechanism for propagating the type information across those distances and reconciling the different sources of information with each other (and producing error messages if the reconciliation fails).
Since type information can flow through the program in so many different ways, and across such long distances, this motivates the use of constraint solvers in type inference algorithms. Different parts of the program constrain the types in different ways, and the constraint solver reconciles the constraints.
Polymorphism is extremely complicated
Even global, constraint-based type inference can be relatively simple to implement if your type system is fully monomorphic. However, as soon as you choose to support parametric polymorphism, things become dramatically more complicated. Consider the following expression:
$$\begin{array}{l}
\begin{aligned}
  \mathbf{let}\; \mathrm{identity} &= λx. x\\
  \mathrm{add1} &= λx. \mathrm{identity}\ (x + 1)\end{aligned} \\
\phantom{\mathbf{let}}\llap{\mathbf{in}}\; \mathrm{map}\ \mathrm{add1}\ (\mathrm{identity}\ [])
\end{array}$$
The type of this expression is $\mathrm{List}\ \mathrm{Int}$, but how do we deduce that? There is a lot to figure out:

The type of $\mathrm{map}$ is known to be $∀a\,b.\: (a → b) → \mathrm{List}\ a → \mathrm{List}\ b$. When we apply $\mathrm{map}$ to arguments, we must instantiate the type variables $a$ and $b$ with concrete types, and we have to somehow automatically pick those concrete types based on the types of the function’s arguments.

In this example, the arguments are $\mathrm{add1}$ and $\mathrm{identity}\ []$. The second of those arguments gives us essentially zero information, because $\mathrm{identity}\ []$ itself could have type $\mathrm{List}\ \tau$ for any type $\tau$. So we have to use the type of $\mathrm{add1}$.

To even figure out the above, we must infer the types of $\mathrm{identity}$ and $\mathrm{add1}$. The type of $\mathrm{identity}$ must itself be polymorphic, as it is used at two different types: in the body of $\mathrm{add1}$ it has type $\mathrm{Int} → \mathrm{Int}$, but in the argument to $\mathrm{map}$ it has type $\mathrm{List}\ \mathrm{Int} → \mathrm{List}\ \mathrm{Int}$. Therefore, we must somehow automatically infer the polymorphic type $∀a. a → a$.

To infer the type of $\mathrm{add1}$, we must instantiate the polymorphic type of $\mathrm{identity}$ in the body to $\mathrm{Int} → \mathrm{Int}$ so that we can deduce that $\mathrm{add1}$ itself has type $\mathrm{Int} → \mathrm{Int}$.

Finally, we must match up the type of $\mathrm{add1}$ with the type of the first argument of $\mathrm{map}$ to instantiate both of its type variables to $\mathrm{Int}$, and only then do we know that the type of the overall expression is $\mathrm{List}\ \mathrm{Int}$.


As you can see, the flow of information here is not at all clear, and in general it’s not even obvious what inference is and is not possible. As it turns out, inference of parametric polymorphism in the presence of polymorphic recursion is known to be undecidable! So it really doesn’t take much to turn the “simple” problem of type inference into a provably intractable one. Of course, there are still very many useful type inference algorithms that can infer the types of some subset of programs, but maximizing the set of programs a type inference algorithm can successfully accept can be very challenging.
Subtyping makes things even more complicated
Subtyping makes type inference even more challenging, especially when a language has full untagged union types, not just inheritance. To see the issue, consider the following definition in TypeScript:
const first = (x) => x[0];

What is the type of this function? All of the following would be legitimate types:

Array => A
[A] => A
[A, B] => A
[A, B, C] => A
[A, B, C, D] => A

And so on. Note that these types aren’t even all subtypes of one another: [A] is a subtype of Array, but the other types are not (since they are heterogeneous tuples). Since there is no “most general” type for first, we say that TypeScript lacks principal types, which means that first doesn’t even really have any one type.
Other systems have more restricted forms of subtyping, and those systems may have principal types, but determining what they are may still be very difficult. The problem is that determining whether two types “match up” is no longer a matter of equality of types, but a more complex relation, the subtyping relation. This makes implementing the “constraint solver” part of type inference much harder.
Type inference in practice
As the above examples hopefully illustrate, type inference is extremely hard. Moreover, it can often produce very poor error messages when absolutely everything is inferred. Therefore, most type systems use a hybrid approach in practice: they use a mixture of explicit type annotations and type inference. In some respects, this makes the problem easier, since the user has provided some type information that does not need to be inferred. However, in other respects, it can actually make the problem even harder, since the user’s type annotations must be interpreted, checked for validity, and reconciled with the program’s inferred types.
Simple type systems do not need such complex type inference algorithms, but almost no practical type systems are as simple as the STLC. The design of type systems that support inference is therefore a challenge of threading the needle: how can we design a type system that can express the things users wish to express, yet also permits sufficient type inference to reduce the burden of writing all those types down? There are many different answers, and unsatisfyingly, there is no “maximally sophisticated” system—every type system feature has tradeoffs.
> **Comments:**
> **username_2** (2023-07-19): I feel like this answer is rooted in a particular approach to type-checking which is common in production-quality compilers. However, polymorphism and subtyping can both be easily *expressed* as constraints over a general-purpose unifier. (I would argue that the performance is decent, too!)  
> **username_0** (2023-07-19): I feel there is a good answer to a different question in you comment if we can find a way to express it.  
---
### Answer by username_7 on 2023-07-19. Score: 11
when do we actually need do type inference?

One time when you need type inference is when the type is "unspeakable". In C# 3 we added anonymous types; there is no syntax for describing an anonymous type. If you want to represent the type "a sequence of anonymously typed values where the value has a field Address of type String and a field ShipsOn of type Date", sorry, you've got to rely on type inference to work that out for you:
var r = from c in customers           
        where c.Name.StartsWith("M")
        from o in c.Orders
        select new { c.Address, o.ShipsOn };

(You might reasonably make the argument that anonymous types are a bad idea in the first place and have been largely superseded by record types in versions of C# that shipped a decade later, but we had good reasons at the time and you can't see the future; let's leave aside the pros and cons of the anonymous type design.)
There are also situations where we don't need type inference but we very much want it in order to reduce the amount of redundancy on the page. Consider a LINQ query using the fluent syntax:
q = people.Join(
    pets,
    person => person,
    pet => pet.Owner,
    (person, pet) => $"{person.Name} owns {pet.Name}.");

Join is a generic method that takes four type arguments: the element types of the outer and inner sequences, the type of the join key, and the type of the resulting sequence. Without type inference C# requires that you state them:
q = people.Join (
    pets,
    person => person,
    pet => pet.Owner,
    (person, pet) => $"{person.Name} owns {pet.Name}.");

which is a bit of a pain even if the types are speakable. We greatly preferred the option to allow these to be inferred over making the developer spell them out explicitly every time.
The generic method type inference algorithm uses a form of bidirectional typing.
> **Comments:**
> **username_8** (2023-07-21): Another example of this come from C++, where the type of a lambda function is unique to the definition and has no name, so can only be stored in an `auto` variable or used as an argument to a template so that the type is inferred appropriately.  
> **username_9** (2023-07-25): C++ iterators are often as good as "unspeakable". You have some data structure, you know it has an iterator with first, next an end, but it's basically impossible for a normal human being to write a declaration for that iterator that the compiler will accept. And if you could, it would be pointless, because all you care about is that it iterates, not what the type is.  
> **username_10** (2024-05-07): Yet another example is when you define a private type in a library named `T` and a public function `f` that returns `T` -- some languages allow this. In this case when you do `x = f()` you can't annotate type of `x` because you can't refer to `T`, it's private.  
> **username_7** (2024-05-07): @sinan: Great example. I think the .NET verifier requires that types mentioned in member signatures be as or more visible than the member, but not all runtimes are so strict.  
---
### Answer by username_11 on 2023-07-18. Score: 10
The examples you give are correct, but do not convey the right message, I believe.

* The first ones, with integers, are way too simple for type inference to have any advantage.
* The last one, with ranges, is way too complex for most type inference systems. Adding two integer variables works, but after a few other operations, if some variables are re-used, the resulting range would be statically unpredictable.

Here is an explanation for wanting type inference - there are certainly many other reasons and pros and cons, as you stated:

* In a statically typed language, the compiler necessarily implements some kind of type inference, to be able to check that some value has the type needed in the expression. In fact this is type checking instead of type inference, but the requirements on compiler logic are similar.
* One of the reasons for having explicit types, is that it enables the compiler to detect places where the programmer is wrong about the type of a variable or function. Unfortunately, writing a type may be very difficult for the programmer, depending upon the language expression power and syntax. E.g. C++, which has huge expression power (functions that use functions or lambdas, templates of templates, etc.) but difficult syntax.
* Having complex types is a natural consequence of programming languages where an element (typically a function) has the greatest possible extent (in matter of type) that its definition allows. This is the case with template arguments in C++: by default, any type is accepted as long as it implements the requirements (e.g. methods) used in the function code. So the typing system becomes way too complex for the human programmer (and actually is Turing-complete, so may be untractable even for the compiler).
* As a consequence of the previous points, without type inference, in some cases the programmer is just struggling to write the type that the compiler expects, and already knows. So it becomes a game where the programmer is trying to guess the correct type by trial-and-error, and the compiler (which knows the correct type but won't tell it) answers "wrong type, try again". This is very frustrating. It does not have the advantage of documenting the code, a benefit often stated in favor of explicit types, as types are anyway too complex to be readable by a programmer. So writing "auto" is just as good, less painful, and does not hinder code readability by complex type expressions that nobody is going to read anyway.
> **Comments:**
> **username_12** (2023-07-18): This is a good answer to the question of “why have type inference?”, but I think the question is actually asking something subtly different: what type system features make type inference algorithms so complicated? I’ve given an attempt at answering *that* question [here](https://langdev.stackexchange.com/a/2429).  
---
### Answer by username_5 on 2023-07-20. Score: 3
I think a surprisingly big part of what makes type inference complex is **nonlinearity**—being able to freely copy and drop variables.

While your examples only show bottom-up **type deduction** from an initialiser to a variable, I’ll speak on **type inference** in the broader sense, where a variable’s type can also be inferred from its usage, by propagating type information also top-down and solving constraints in some way.

Type systems vary a *lot* in the complexity of those constraints. With some features like numerical ranges and subtyping, the constraint satisfaction itself might not be decidable. But setting that aside, our goal with type inference is to find a proof (a typing derivation) showing that a program is well-typed, guided by the structure of the program. Along the way, we apply typing rules based on how **names identify relationships among program elements**.

And nonlinearity complicates those relationships, in a few key ways.

## Dropping

Dropped variables can be underconstrained, so we need to be able to find out if there’s an ambiguity, and tell the programmer. Whereas, if a variable *must* be used, then it *will* be used in the context of an environment that determines its type.

## Sharing

Shared variables can be overconstrained, so we need to be able to find conflicts, too. If a variable can only be used at most once, it adds no extra constraints. But to enforce that its type must be consistent wherever it’s used, it takes a linear number of type constraints.

## Metavariables

Metavars stand for unknown types to fill in later, and relate the occurrences of a variable with each other, so we can check that they all agree. Metavars also need to be recorded somewhere dynamically, whether as mutable references or as keys in a map. They can propagate type information far from its origin to identify subtle type conflicts—which is a good thing!—but for efficiency reasons they can’t retain much information about the path they took to get there. Therefore they can also make it hard to report an apparent type mismatch to the programmer in a friendly way.

Yet, metavars are only really needed by **nonlinear constraints** and **nonlinear polymorphism**. With linear variables, an *occurrence* of a variable can be identified with the variable itself. You can even infer the type of a relevant variable “backward”, by *checking* the expression where it’s used to find the (singular!) constraint on its type, which is unique or polymorphic.

And a polymorphic function is linear just when its type is also linear, that is, it uses all of its *type variables* linearly. For example:

| Function | Type | Substructure |
| --- | --- | --- |
| identity | ∀a. a− → a+ | Linear |
| map | ∀a b. (a+ → b−) → List a− → List b+ | Linear |
| swap | ∀a b. (a− × b−) → (b+ × a+) | Linear (unordered) |
| dup | ∀a. a− → (a+ × a+) | Nonlinear (relevant but not affine) |
| drop | ∀a. a− → () | Nonlinear (affine but not relevant) |

In a linear type, each type variable will be used exactly twice: once in a positive position (as an output / covariantly) and once in a negative position (as an input / contravariantly).

---

This is all to say that a lot of the complexity and poor usability come from trying to solve the problem in full generality, without imposing any limitations on the programmer. But even if you want to be able to infer all types without *type signatures*, that doesn’t mean you have *no annotations* at all. And limitations are fine as long as they’re not *just* to please the compiler.

Suppose variables are written with a `var` keyword and functions are written with a `def` keyword, and the programmer *usually* wants monomorphic linear variables and polymorphic unrestricted functions; in that case, you can use `var` and `def` themselves as **natural annotations** to restrict or relax the rules of inference. Indeed that’s basically the trick of how `let` bindings are used to decide where to add polymorphism in Damas & Milner’s algorithm.
---
### Answer by username_6 on 2024-07-19. Score: 0
For me, I did not intend to introduce type inference in my language. But I had two cases where I needed it.
After adding parametric polymorphism (Generics):

Initialize empty Collections
I wanted to be able to create collections without specifying the type variable for the collection, but instead infer the type variable from what is added to the collection.
e.g. init a list with [] and later call List.append(34),
similar in Rust with an empty Vec using let my_vec = Vec::new(); and later call my_vec.push(34);.
This is somewhat similar to Java 7, where the "diamond operator" was introduced, to be able to initialize collections without specifying the type variable: new ArrayList<>().

Tagged Union types
I wanted to have tagged union types (e.g. enums with values, as in Rust and Swift) with generics. E.g. the type Option { None, Some(t) } or Result { Ok(s), Err(e) }. The type constructor of these types, may not resolve all type variables of the type, so type inference must be used to get the full type. A good example is when these type constructors are used in different if-branches:
let result = if  {
    None
} else {
    Some(34)
}

Here I needed to analyze both branches, to infer the type variables and get the full type of result.
---
