Kotlin language specification

Kotlin type constraints

Type constraint definition

Examples of valid type constraints:

• $\texttt{List<}\widetilde{X}\texttt{>} <: Y$
• $\texttt{List<}\widetilde{X}\texttt> <: \texttt{List<}\texttt{List<}\texttt{Int}\texttt>\texttt>$
• $\widetilde{X} <: Y$

Type constraint solving

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

• $X <: Y$
• $\texttt{List<}X\texttt> <: \texttt{Collection}\texttt<X\texttt>$

Checking constraint system soundness

A sample bound inference algorithm

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.

• If $S$ and $T$ are resolved types and:
  • If $S <: T$ , this constraint is eliminated;
  • Otherwise, this is an inference error;
• Otherwise, if $S$ is an inference variable $\alpha$ , a new bound $\alpha <: T$ is added to current solution;
• Otherwise, if $T$ is an inference variable $\beta$ , a new bound $S <: \beta$ is added to current solution;
• Otherwise, if $S$ is a flexible type of the form $(\alpha..\alpha?)$ where $\alpha$ is an inference variable, a new bound $\alpha <: (T..T?)$ is added to current solution;
• Otherwise, if $T$ is a flexible type of the form $(\alpha..\alpha?)$ where $\alpha$ is an inference variable, a new bound $(S..S?) <: \alpha$ is added to current solution;
• Otherwise, if $S$ is a nullable type of the form $A?$ and:
  • If $T$ is a known non-nullable type (a classifier type, a nullability-asserted type $B!!$ , a type variable with a known non-nullable lower bound, or an intersection type containing a known non-nullable type), this is an inference error;
  • Otherwise, the constraint is reduced to $A <: T$ . Also, if $T$ is also a nullable type of the form $B?$ , an additional constraint $A!! <: B$ is introduced;
• Otherwise, if $S$ is a flexible type of the form $(B..A?)$ and:
  • If $T$ is a nullable type of form $C?$ , the constraint is reduced to $(B..A) <: C$ , or to $A <: C$ if $A \equiv B$ ;
  • Otherwise, the constraint is reduced to $(B..A) <: T$ , or to $A <: T$ if $A \equiv B$ ;
• Otherwise, if $T$ is a parameterized type $G[A_1, \ldots, A_N]$ , among all supertypes of $S$ the one of the form $G[B_1, \ldots, B_N]$ is chosen.
  • If no such supertype exists, this is an inference error;
  • Otherwise, for each $M \in [1,N]$ , a type argument constraint for containment $A_M \preceq B_M$ is introduced (see below);
• Otherwise, if $T$ is any other classifier type and $T$ is among supertypes for $S$ , the constraint is eliminated; otherwise, this is an inference error;
• Otherwise, if $T$ is a type variable and:
  • If $S$ is an intersection type containing $T$ , this constraint is eliminated;
  • Otherwise, if $T$ has a lower bound $B$ , the constraint is reduced to $S <: B$ ;
  • Otherwise, this is an inference error;
• Otherwise, if $T$ is an intersection type $A_1 \mathbin{\operatorname{\&}}\ldots \mathbin{\operatorname{\&}}A_N$ , the constraint is reduced to $N$ constraints $S <: A_M$ for each $M \in [1, N]$ ;
• Otherwise, if $T$ is a nullable type of the form $B?$ and:
  • If $S$ is a known non-nullable type (a classifier type, a nullability-asserted type $A!!$ , a type variable with a known non-nullable lower bound, or an intersection type containing a known non-nullable type), the constraint is reduced to $S <: B$ ;
  • Otherwise, this is an inference error.

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

• If either $Q$ or $F$ is a special bivariant type argument $\star$ , no constraints are produced;
• If $F$ has the form $F'$ (is invariant):
  • If $Q$ is also invariant and of the form $Q'$ , two constraints are produced: $F' <: Q'$ and $Q' <: F'$ ;
  • If $Q$ has any other variance, this is an inference error;
• If $F$ has the form $\operatorname{\texttt{out\,}}F'$ (is covariant):
  • If $Q$ has the form $\operatorname{\texttt{out\,}}Q'$ or $Q'$ , the following constraint is produced: $Q' <: F'$ ;
  • If $Q$ has the form $\operatorname{\texttt{in\,}}Q'$ , the following constraint is produced: $\operatorname{\texttt{kotlin.Any?}}<: F'$ ;
• If $F$ has the form $\operatorname{\texttt{in\,}}F'$ (is contravariant):
  • If $Q$ has the form $\operatorname{\texttt{in\,}}Q'$ or $Q'$ , the following constraint is produced: $F' <: Q'$ ;
  • If $Q$ has the form $\operatorname{\texttt{out\,}}Q'$ , the following constraint is produced: $F' <: \operatorname{\texttt{kotlin.Nothing}}$ .

• For each inference variable $\alpha$ , for each pair of bounds $S <: \alpha$ and $\alpha <: T$ , a new constraint is produced: $S <: T$ ;
• For each inference variable $\alpha$ , if there is a pair of bounds $S <: \alpha$ and $\alpha <: S$ (i.e., $\alpha$ is equivalent to $S$ ), for each bound $Q <: P$ where $Q$ or $P$ contains $\alpha$ , a new constraint is produced: $Q[\alpha := S] <: P[\alpha := S]$ ;
• For each inference variable $\alpha$ , for each pair of bounds $\alpha <: S$ and $\alpha <: T$ where $S$ has a supertype of the form $G[A_1,\ldots,A_N]$ and $T$ has a matching supertype of the form $G[B_1,\ldots,B_N]$ , for each matching supertype $G$ and each $M \in [1,N]$ , if both $A_M$ and $B_M$ are invariant and have forms $A'_M$ and $B'_M$ respectively, the following new constraints are produced: $A'_M <: B'_M$ and $B'_M <: A'_M$ .

Finding optimal constraint system solution

• A pull-up constraint for type variable $T$ , denoted $\uparrow T$ , signifying that when finding a substitution for this variable, the optimal solution is the largest one according to subtyping relation;
• A push-down constraint for type variable $T$ , denoted $\downarrow T$ , signifying that when finding a substitution for this variable, the optimal solution is the smallest one according to subtyping relation.

• For a variable with a push-down constraint, the solution is the greatest lower bound of all upper bounds for this variable, excluding other free variables;
• For a variable with a pull-up constraint, the solution is the least upper bound of all lower bounds for this variable, excluding other free variables;
• For a variable with both or none, the solution is also the least upper bound of all lower bounds for this variable, excluding other free variables.

The relations on types as constraints

• $A <: T$
• $B <: T$
• $\downarrow T$
• $\uparrow A$
• $\uparrow B$

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 $A$ , $B$ and $C$ respectively, the type variable for e is $E$ . According to the conditional expression rules, this produces the following relations:

• $C <: \texttt{kotlin.Boolean}$
• $E = \operatorname{\text{LUB}}(A, B)$

These, in turn, produce the following explicit constraints:

• $C <: \texttt{kotlin.Boolean}$
• $A <: E$
• $B <: E$
• $\downarrow E$
• $\uparrow A$
• $\uparrow B$

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

• $C \rightarrow \texttt{kotlin.Boolean}$
• $A \rightarrow \operatorname{\texttt{kotlin.Any?}}$
• $B \rightarrow \operatorname{\texttt{kotlin.Any?}}$
• $E \rightarrow \operatorname{\texttt{kotlin.Any?}}$