Kotlin Download PDF
Table of contents

Kotlin language specification

Version 1.9-rfc+0.1

Marat Akhin

Mikhail Belyaev

Kotlin type constraints

Some complex tasks that need to be solved when compiling Kotlin code are formulated best using constraint systems over Kotlin types. These are solved using constraint solvers.

Type constraint definition

A type constraint in general is an inequation of the following form: T<:UT <: U where TT and UU are concrete Kotlin types. As Kotlin has parameterized types, TT and UU may be free type variables: unknown types which may be substituted by any other type in Kotlin.

Please note that, in general, not all type parameters are considered as free type variables in a constraint system. Some type variables may be fixed in a constraint system; for example, type parameters of a parameterized class inside its body are unknown types, but are not free type variables either. A fixed type variable describes an unknown, but fixed type which is not to be substituted.

We will use the notation TiT_i for a type variable and Ti~\tilde{T_i} for a fixed type variable. The main difference between fixed type variables and concrete types is that different concrete types may not be equal, but a fixed type variable may be equal to another fixed type variable or a concrete type.

Examples of valid type constraints:

Every constraint system has general implicit constraints Tj<:kotlin.Any?T_j <: \operatorname{\texttt{kotlin.Any?}} and kotlin.Nothing<:Tj\operatorname{\texttt{kotlin.Nothing}}<: T_j for every type TjT_j mentioned in the system, including type variables.

Type constraint solving

There are two tasks which a type constraint solver may perform: checking constraint system for soundness, i.e., if a solution exists, and solving constraint system, i.e., inferring a satisfying substitution of concrete types for all free type variables.

Checking a constraint system for soundness can be viewed as a much simpler case of solving that constraint system: if there is a solution, the system is sound, meaning there are only two possible outcomes. Solving a constraint system, on the other hand, may have multiple possible outcomes, as there may be multiple valid solutions.

Example: constraint systems which are sound yet no relevant solutions exist.

Checking constraint system soundness

Checking constraint system soundness is a satisfiability problem. That is, given a number of constraints in the form S<:TS <: T containing zero or more free type variables (also called inference type variables), it needs to determine if these constraints are non-contradictory, i.e., if there exists a possible instantiation of these free variables to concrete types which makes all given constraints valid.

This problem can be reduced to finding a set of lower and upper bounds for each of these variables and determining if these bounds are non-contradictory. The algorithm of finding these bounds is implementation-defined and is not guaranteed to prove the satisfiability of given constraints in all possible cases.

A sample bound inference algorithm

The algorithm given in this section is just an example of a family of algorithms that may be applied to the problem given above. A particular implementation is not guaranteed to follow this algorithm, but one may use it as a reference on how this problem may be approached.

Note: a well-informed reader may notice this algorithm to be similar to the one used by Java. This is not a coincidence: our sample inference algorithm has indeed been inspired by Java’s.

The algorithm works in two phases: reduction and incorporation which are applied to the constraint system and its current solution in turns until a fixpoint or an error is reached (aka reduction-incorporation procedure or RIP). The reduction phase is used to produce bounds for inference variables based on constraints; this phase is also responsible for eliminating the constraints which are no longer needed. The incorporation phase is used to introduce new bounds and constraints from existing bounds.

A bound is similar to a constraint in that it has the form S<:TS <: T , at least one of SS or TT is an inference variable. Thus, the current (and also the final) solution is a set of upper and lower bounds for each inference variable. A resolved type in this context is any type which does not contain inference variables.

Reduction phase: for each constraint S<:TS <: T in the constraint system the following rules are applied:

Type argument constraints for a containment relation QFQ \preceq F are constructed as follows:

Important: for the purposes of this algorithm, declaration-site variance type arguments are considered to be their equivalent use-site variance versions.

Incorporation phase: for each bound and particular bound combinations in the current solution, new constraints are produced as follows (it is safe to assume that each constraint is introduced into the system only once, so if this step produces constraints that have already been reduced, they are not added into the system):

Finding optimal constraint system solution

As any constraint system may have multiple valid solutions, finding one which is “optimal” in some sense is not possible in general, because the notion of the best solution for a task depends on the said task. To deal with this, a constraint system allows two additional types of constraints:

If a variable has no constraints of these kinds associated with it, it is assumed to have a pull-up implicit constraint. The process of instantiating the free variables of a constraint system starts by finding the bounds for each free variable (as mentioned in the previous section) and then, given these bounds, continues to pick the right type from them. Excluding other free variables, this boils down to:

If there are inference variables dependent on other inference variables (α\alpha is dependent on β\beta iff there is a bound α<:T\alpha <: T or T<:αT <: \alpha where TT contains β\beta ), this process is performed in stages.

During each stage a set of inference variables not dependent on other inference variables (but possibly dependent on each other) is selected, the solutions for these variables are found using existing bounds, and after that these variables are resolved in the current bound set by replacing all of their instances in other bounds by the solution. This may trigger a new RIP.

After that, a new independent set of inference variables is picked and this process is repeated until an inference error occurs or a solution for each inference variable is found.

The relations on types as constraints

In other sections (for example, Expressions and Statements) the relations between types may be expressed using the type operations found in the type system section of this document.

The greatest lower bound of two types is converted directly as-is, as the greatest lower bound is always an intersection type.

The least upper bound of two types is converted as follows. If type TT is defined to be the least upper bound of AA and BB , the following constraints are produced:

Important: the results of finding GLB or LUB via a constraint system may be different from the results of finding them via a normalization procedure (i.e., imprecise); however, they are sound w.r.t. bound, meaning a constraint system GLB is still a lower bound and a constraint system LUB is still an upper bound.

Example:

Let’s assume we have the following code:

val e = if (c) a else b

where a, b, c are some expressions with unknown types (having no other type constraints besides the implicit ones).

Assume the type variables generated for them are AA , BB and CC respectively, the type variable for e is EE . According to the conditional expression rules, this produces the following relations:

These, in turn, produce the following explicit constraints:

which, w.r.t. general and pull-up implicit constraints, produce the following solution: