When do we need complex type inference?

Question

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.

Answer 1

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
• [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<A>, 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.

Answer 2

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<Person, Pet, Person, string> (
    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.

Answer 3

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.

Answer 4

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 5

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<t> { None, Some(t) } or Result<s,e> { 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 <condition> {
      None
  } else {
      Some(34)
  }
  

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