It’s a short note about type inference and programming languages in general, not an update about Kotlin :)

Every programming language with some form of generics and type inference has intersection types. They can be denotable (meaning you can write them explicitly in programs) or exist only under the hood as part of type inference, but they’re still there.

This is quite a simple and "obvious" observation, but I still remember being fascinated when I realized it many years ago. And today, I just wanted to share it.

Let’s dive in.

How type inference works

On the surface (only on the surface, unfortunately), type inference is straightforward: you need to solve constraint systems with two kinds of constraints: lower and upper bounds.

When do they appear?

Lower constraints

Let’s consider a function like listOf:

fun <T> listOf(a: T, b: T): List<T>

fun foo(s: String, c: CharSequence) {
    listOf(s, c) // List<CharSequence>
}

Here, it’s obvious that we get a List<CharSequence>. To infer this, the compiler internally builds a constraint system for the type parameter T:

<: means "subtype of"

String <: T         (1st argument)
CharSequence <: T   (2nd argument)

Now, to solve it, we have to find a type of which both String and CharSequence are subtypes. The most precise type would be a union type: String | CharSequence. However, there’s also a convenient and practical approximation: the common supertype. Here, it’s simply CharSequence.

So, whenever we have N lower-bound constraints on a type variable, the compiler computes their common supertype. The algorithm is similar to finding a common ancestor in a tree.

Upper constraints

Upper-bound constraints can come from declared upper bounds (fun <T : UpperConstraint>), contravariant types (such as function types), or be introduced internally by the constraint system solver. Let’s consider the following case:

interface A { fun memberOfA() }
interface B { fun memberOfB() }

fun <T : A> foo(f: (T) -> Unit): T = TODO()

fun test(f: (B) -> Unit) {
    foo(f).memberOfA()
    foo(f).memberOfB()
}

Here, the resulting type of foo(f) is the intersection type A & B. You can check that the code compiles and that you can invoke members from both interfaces.

What happens here? Similar to before, we have two constraints, but this time in the opposite direction:

<: means "subtype of"

T <: A                       (declared upper bound)
(B) -> Unit <: (T) -> Unit   (argument)

- functional types are contravariant in their input position! ~>

T <: A  (declared upper bound)
T <: B  (argument)

So, to solve this constraint system, we need to find a type that is a subtype of both A and B.

The problem is that, unlike in the previous case, there’s simply no good approximation (except for a bottom type like Nothing). We have an infinite set of possible types, and there’s no way to pick a single precise and unambiguous one.

This is a common situation in languages with constraint-based type inference. The only practical solution is to introduce intersection types and say that the solution to the constraint system is A & B, which is the greatest lower bound for A and B.

Languages like Java, Kotlin or Dart with constraint-based type inference and subtyping naturally need intersection types.

It’s worth noting that we can run into intersection types without upper constraints as well. Consider the following:

interface A
interface B

class Foo : A, B
class Bar : A, B

listOf(Foo(), Bar()) // It's List<A & B>

Here, we have lower-bound constraints and need to compute the common supertype of Foo and Bar. The only reasonable type here is A & B.

Lower & Upper constraints

Just a quick follow-up on what happens when we have both lower and upper constraints in our system:

L_1 <: T
...
L_N <: T

T <: U_1
...
T <: U_N

Then we solve the lower and upper constraints separately, check that the results are consistent, and typically pick the more precise one, which is the result of the lower constraints:

CommonSupertype(L_1, ... L_N) <: T <: U_1 & ... & U_N

We verify this subtyping relationship, and if it holds, we pick the left-hand side. Since the left-hand side is a subtype of the right-hand side, it is the more precise type.

That’s it! That’s the basic idea behind type inference in constraint-based systems. Of course, in reality, there are hundreds of additional cases and tricky situations. Sometimes we even have to deal with types for which subtyping isn’t transitive (platform types in Kotlin, I’m looking at you), while still computing the transitive closure in between…​

We get intersections but not unions, why?

A valid question is: if we have intersection types, why don’t we introduce unions as well?

First, we’re actually trying to hide intersection types too. We have them simply because there’s no practical alternative.

But what can be wrong with unions. Consider a type parameter T. With unions, we may get something like:

T — type  parameter

T <: Int | String
...
(other constraints)

Unfortunately, such a constraint creates a "forking" (or "branching") point: T can be either Int or String, so we now have to solve two systems independently and then pick the best solution:

T — type  parameter

T <: Int
...
(other constraints)

OR

T <: String
...
(other constraints)

And when something doubles, exponential complexity is just around the corner. In practice, this happens surprisingly quickly because lower constraints are so common, especially with functions and constructs like listOf, if, and so on.

That’s also why languages that still go for union types often restrict where they can appear, for example, only to cases where the user explicitly specifies them (and never infer them internally), and add special rules to tame the constraint solver.

Any other way outs for union types?

An interesting observation is that verifying whether a set of constraints is valid is polynomial. So, if we avoid the actual search, that is, solving the constraint system, we don’t run into exponential complexity.

We can even build a proper member scope to determine what operations are available on the potential result. Essentially, we can say: “Yes, this code is valid or not valid” without ever computing the actual types.

This idea is actually quite old, and, as with everything good but old, we’re now looking into it under the codename outference ;)

See the paper and talk by Ross Tate for more on this: