18
$\begingroup$

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.

$\endgroup$
7
  • 4
    $\begingroup$ How do you know 1 is an integer and not a float, bigint, smallint, single bit, boolean, etc? $\endgroup$
    – Bergi
    Jul 18, 2023 at 21:00
  • $\begingroup$ 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. $\endgroup$ Jul 19, 2023 at 7:55
  • $\begingroup$ 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? $\endgroup$
    – Corbin
    Jul 19, 2023 at 16:20
  • $\begingroup$ 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. $\endgroup$ Jul 19, 2023 at 16:37
  • $\begingroup$ 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. $\endgroup$ Jul 19, 2023 at 17:07

4 Answers 4

19
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ 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!) $\endgroup$
    – Corbin
    Jul 19, 2023 at 16:18
  • $\begingroup$ I feel there is a good answer to a different question in you comment if we can find a way to express it. $\endgroup$ Jul 19, 2023 at 17:13
11
$\begingroup$

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.

$\endgroup$
2
  • 1
    $\begingroup$ 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. $\endgroup$
    – occipita
    Jul 21, 2023 at 0:09
  • 1
    $\begingroup$ 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. $\endgroup$
    – gnasher729
    Jul 25, 2023 at 16:01
10
$\begingroup$

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.
$\endgroup$
1
  • 3
    $\begingroup$ 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. $\endgroup$
    – Alexis King
    Jul 18, 2023 at 17:23
3
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .