Kotlin language specification

Type system

Glossary

$T$

Type (with unknown nullability)

$T!!$

Non-nullable type

$T?$

Nullable type

$\{T\}$

Universe of all possible types

$\{T!!\}$

Universe of non-nullable types

$\{T?\}$

Universe of nullable types

Well-formed type

A properly constructed type w.r.t. Kotlin type system

$\Gamma$

Type context

$A <: B$

A is a subtype of B

$A \mathrel{\operatorname{\cancel{<:>}}}B$

A and B are not related w.r.t. subtyping

Type constructor

An abstract type with one or more type parameters, which must be instantiated before use

Parameterized type

A concrete type, which is the result of type constructor instantiation

Type parameter

Formal type parameter of a type constructor

Type argument

Actual type argument in a parameterized type

$T\lbrack A_1, \ldots, A_n\rbrack$

The result of type constructor $T$ instantiation with type arguments $A_i$

$T\lbrack\sigma\rbrack$

The result of type constructor $T(F_1, \ldots, F_n)$ instantiation with the assumed substitution $\sigma : F_1 = A_1, \ldots, F_n = A_n$

$\sigma T$

The result of type substitution in type $T$ w.r.t. substitution $\sigma$

$K_T(F, A)$

Captured type from the type capturing of type parameter $F$ and type argument $A$ in parameterized type $T$

$T\langle K_1, \ldots, K_n\rangle$

The result of type capturing for parameterized type $T$ with captured types $K_i$

$T\langle \tau \rangle$

The result of type capturing for parameterized type $T(F_1, \ldots, F_n)$ with captured substitution $\tau : F_1 = K_1, \ldots, F_n = K_n$

$A \mathbin{\operatorname{\&}}B$

Intersection type of $A$ and $B$

$A \mathbin{\operatorname{|}}B$

Union type of $A$ and $B$

$\operatorname{\text{GLB}}$

Greatest lower bound

$\operatorname{\text{LUB}}$

Least upper bound

Introduction

• Hybrid static, gradual and flow type checking;
• Null safety;
• No unsafe implicit conversions;
• Unified top and bottom types;
• Nominal subtyping with bounded parametric polymorphism and mixed-site variance.

Type kinds

• Built-in types
• Classifier types
• Type parameters
• Function types
• Array types
• Flexible types
• Nullable types
• Intersection types
• Union types

Note: for brevity, we omit specifying that a type is concrete. All types not described as abstract are implicitly concrete.

Built-in types

kotlin.Any

Note: additional details about $\operatorname{\texttt{kotlin.Any}}$ are available here.

kotlin.Nothing

Note: additional details about $\operatorname{\texttt{kotlin.Nothing}}$ are available here.

kotlin.Function

Built-in integer types

• kotlin.Int
• kotlin.Short
• kotlin.Byte
• kotlin.Long

Note: additional details about built-in integer types are available here.

Array types

Note: unlike Java, arrays in Kotlin are declared as invariant. To use them in a co- or contravariant way, one should use use-site variance.

• DoubleArray (for $\operatorname{\texttt{kotlin.Array}}(\operatorname{\texttt{kotlin.Double}})$ )
• FloatArray (for $\operatorname{\texttt{kotlin.Array}}(\operatorname{\texttt{kotlin.Float}})$ )
• LongArray (for $\operatorname{\texttt{kotlin.Array}}(\operatorname{\texttt{kotlin.Long}})$ )
• IntArray (for $\operatorname{\texttt{kotlin.Array}}(\operatorname{\texttt{kotlin.Int}})$ )
• ShortArray (for $\operatorname{\texttt{kotlin.Array}}(\operatorname{\texttt{kotlin.Short}})$ )
• ByteArray (for $\operatorname{\texttt{kotlin.Array}}(\operatorname{\texttt{kotlin.Byte}})$ )
• CharArray (for $\operatorname{\texttt{kotlin.Array}}(\operatorname{\texttt{kotlin.Char}})$ )
• BooleanArray (for $\operatorname{\texttt{kotlin.Array}}(\operatorname{\texttt{kotlin.Boolean}})$ )

Note: the presence of such specialized types allows the compiler to perform additional array-related optimizations.

Note: specialized and non-specialized array types match modulo their iterator types, which are also specialized; Iterator<Int> is specialized to IntIterator.

• if $\operatorname{\texttt{kotlin.Array}}(T)$ has a specialized version TArray, $\operatorname{\text{ATS}}(\operatorname{\texttt{kotlin.Array}}(T)) = \texttt{TArray}$
• if $\operatorname{\texttt{kotlin.Array}}(T)$ does not have a specialized version, $\operatorname{\text{ATS}}(\operatorname{\texttt{kotlin.Array}}(T)) = \operatorname{\texttt{kotlin.Array}}(T)$

Note: additional details about built-in array types are available here.

Classifier types

Simple classifier types

• type name $T$
• (optional) list of supertypes $S_1, \ldots, S_m$

• $T$ is a valid type name
• $\forall i \in [1,m]: S_i$ must be concrete, non-nullable, well-formed type
• the transitive closure $\mathbb{S}^*(T)$ of the set of type supertypes $\mathbb{S}(T : S_1, \ldots, S_m) = \{S_1, \ldots, S_m\} \cup \mathbb{S}(S_1) \cup \ldots \cup \mathbb{S}(S_m)$ is consistent, i.e., does not contain two parameterized types with different type arguments.

Example:

// A well-formed type with no supertypes
interface Base

// A well-formed type with a single supertype Base
interface Derived : Base

// An ill-formed type,
// as nullable type cannot be a supertype
interface Invalid : Base?

Note: for the purpose of different type system examples, we assume the presence of the following well-formed concrete types:

• class String
• interface Number
• class Int $<:$ Number
• class Double $<:$ Number

Note: Number is actually a built-in abstract class; we use it as an interface for illustrative purposes.

Parameterized classifier types

• type name $T$
• type parameters $F_1, \ldots, F_n$
• (optional) list of supertypes $S_1, \ldots, S_m$

• $T$ is a valid type name
• $\forall i \in [1,n]: F_i$ must be well-formed type parameter
• $\forall j \in [1,m]: S_j$ must be concrete, non-nullable, well-formed type

• type constructor $T$
• type arguments $A_1, \ldots, A_n$

• $T$ is a well-formed type constructor with $n$ type parameters
• $\forall i \in [1,n]: A_i$ must be well-formed concrete type
• $\forall i \in [1,n]:$ variance of $A_i$ does not contradict variance of $F_i$
• $\forall i \in [1,n]: A_i <: \tau U_i$ , where $U_i$ is the upper bound for $F_i$ and captured substitution $\tau : F_1 = K_1, \ldots, F_n = K_n$ manipulates captured types.
• the transitive closure $\mathbb{S}^*(T)$ of the set of type supertypes $\mathbb{S}(T\langle \tau \rangle : \tau S_1, \ldots, \tau S_m) = \{\tau S_1, \ldots, \tau S_m\} \cup \mathbb{S}(\tau S_1) \cup \ldots \cup \mathbb{S}(\tau S_m)$ is consistent, i.e., does not contain two parameterized types with different type arguments.

Example:

// A well-formed type constructor with no supertypes
// A and B are unbounded type parameters
interface Generic<A, B>

// A well-formed type constructor
//   with a single parameterized supertype
// Int and String are well-formed concrete types
interface ConcreteDerived<P, Q> : Generic<Int, String>

// A well-formed type constructor
//   with a single parameterized supertype
// P and Q are type parameters of GenericDerived,
//   used as type arguments of Generic
interface GenericDerived<P, Q> : Generic<P, Q>

// An ill-formed type constructor,
//   as abstract type Generic
//   cannot be used as a supertype
interface Invalid<P> : Generic


// A well-formed type constructor with no supertypes
// out A is a projected type parameter
interface Out<out A>


// A well-formed type constructor with no supertypes
// S : Number is a bounded type parameter
// (S <: Number)
interface NumberWrapper<S : Number>

// A well-formed type constructor
//   with a single parameterized supertype
// NumberWrapper<Int> is well-formed,
//   as Int <: Number
interface IntWrapper : NumberWrapper<Int>

// An ill-formed type constructor,
//   as NumberWrapper<String> is an ill-formed parameterized type
//   (String not(<:>) Number)
interface InvalidWrapper : NumberWrapper<String>

Type parameters

• Bounded type parameter with regular bounds:
  • $F$ is a type parameter of type constructor $T$
  • $\forall i \in [1,n]: B_i$ must be concrete, non-type-parameter, well-formed type
  • No more than one of $B_i$ may be a class type

Note: the last condition is a nod to the single inheritance nature of Kotlin: any type may be a subtype of no more than one class type. For any two class types, either these types are in a subtyping relation (and you should use the more specific type in the bounded type parameter), or they are unrelated (and the bounded type parameter is empty).

Actual support for multiple class type bounds would be needed only in very rare cases, such as the following example.

interface Foo
interface Bar

open class A<T>
class B<T> : A<T>

class C<T> where T : A<out Foo>, T : B<out Bar>
// A convoluted way of saying T <: B<out Foo & Bar>,
// which contains a non-denotable intersection type

• Bounded type parameter with type parameter bound:
  • $F$ is a type parameter of type constructor $T$
  • $i = 1$ (i.e., there is a single upper bound)
  • $B_1$ must be well-formed type parameter

Function type parameters

Note: one may view such parameterized functions as a kind of function type constructors.

Mixed-site variance

Info: variance is a way of describing how subtyping works for variant parameterized types. With declaration-site variance, for two non-equivalent types $A <: B$ , subtyping between T<A> and T<B> depends on the variance of type parameter $F$ for some type constructor $T$ .

• if $F$ is covariant ($\operatorname{\texttt{out\,}}F$ ), T<A> $<:$ T<B>
• if $F$ is contravariant($\operatorname{\texttt{in\,}}F$ ), T<A> $:>$ T<B>
• if $F$ is invariant (default), T<A> $\mathrel{\operatorname{\cancel{<:>}}}$ T<B>

Use-site variance allows the user to change the type variance of an invariant type parameter by specifying it on the corresponding type argument. $\operatorname{\texttt{out\,}}A$ means covariant type argument, $\operatorname{\texttt{in\,}}A$ means contravariant type argument; for two non-equivalent types $A <: B$ and an invariant type parameter $F$ of some type constructor $T$ , subtyping for use-site variance has the following rules.

• T<out A> $<:$ T<out B>
• T<in A> $:>$ T<in B>
• T<A> $<:$ T<out A>
• T<A> $<:$ T<in A>

Important: by the transitivity of the subtyping operator these rules imply that the following also holds:

• T<A> $<:$ T<out B>
• T<in A> $:>$ T<B>

Note: Kotlin does not support specifying both co- and contravariance at the same time, i.e., it is impossible to have T<out A in B> neither on declaration- nor on use-site.

Note: informally, covariant type parameter $\operatorname{\texttt{out\,}}A$ of type constructor $T$ means “$T$ is a producer of $A$ s and gets them out”; contravariant type parameter $\operatorname{\texttt{in\,}}A$ of type constructor $T$ means “$T$ is a consumer of $A$ s and takes them in”.

Declaration-site variance

Important: declaration-site variance can be used only when declaring types, e.g., function type parameters cannot be variant.

Example:

// A type constructor with an invariant type parameter
interface Invariant<A>
// A type constructor with a covariant type parameter
interface Out<out A>
// A type constructor with a contravariant type parameter
interface In<in A>

fun testInvariant() {
    var invInt: Invariant<Int> = ...
    var invNumber: Invariant<Number> = ...
    
    if (random) invInt = invNumber // ERROR
    else invNumber = invInt // ERROR
    
    // Invariant type parameters do not create subtyping
}

fun testOut() {
    var outInt: Out<Int> = ...
    var outNumber: Out<Number> = ...
    
    if (random) outInt = outNumber // ERROR
    else outNumber = outInt // OK
    
    // Covariant type parameters create "same-way" subtyping
    //   Int <: Number => Out<Int> <: Out<Number>
    // (more specific type Out<Int> can be assigned
    //  to a less specific type Out<Number>)
}

fun testIn() {
    var inInt: In<Int> = ...
    var inNumber: In<Number> = ...
    
    if (random) inInt = inNumber // OK
    else inNumber = inInt // ERROR
    
    // Contravariant type parameters create "opposite-way" subtyping
    //   Int <: Number => In<Int> :> In<Number>
    // (more specific type In<Number> can be assigned
    //  to a less specific type In<Int>)
}

Use-site variance

Important: use-site variance cannot be used when declaring a supertype top-level type argument.

• It is a compile-time error to use a covariant type argument in a contravariant type parameter
• It is a compile-time error to use a contravariant type argument in a covariant type parameter

Note: informally, $T[\star]$ means “I can give out something very generic ($\operatorname{\texttt{kotlin.Any?}}$ ) and cannot take in anything”.

Example:

// A type constructor with an invariant type parameter
interface Inv<A>

fun test() {
    var invInt: Inv<Int> = ...
    var invNumber: Inv<Number> = ...
    var outInt: Inv<out Int> = ...
    var outNumber: Inv<out Number> = ...
    var inInt: Inv<in Int> = ...
    var inNumber: Inv<in Number> = ...
    
    when (random) {
        1 -> {
            inInt = invInt    // OK
            // T<in Int> :> T<Int>
            
            inInt = invNumber // OK
            // T<in Int> :> T<in Number> :> T<Number>
        }
        2 -> {
            outNumber = invInt    // OK
            // T<out Number> :> T<out Int> :> T<Int>
            
            outNumber = invNumber // OK
            // T<out Number> :> T<Number>
        }
        3 -> {
            invInt = inInt  // ERROR
            invInt = outInt // ERROR
            // It is invalid to assign less specific type
            // to a more specific one
            //   T<Int> <: T<in Int>
            //   T<Int> <: T<out Int>
        }
        4 -> {
            inInt = outInt    // ERROR
            inInt = outNumber // ERROR
            // types with co- and contravariant type parameters
            // are not connected by subtyping
            //   T<in Int> not(<:>) T<out Int>
        }
    }
}

Type capturing

Important: type capturing is not recursive.

Note: All applicable rules are used to create the resulting constraint set.

• For a covariant type parameter $\operatorname{\texttt{out\,}}F_i$ , if $A_i$ is an ill-formed type or a contravariant type argument, $K_i$ is an ill-formed type. Otherwise, $K_i <: A_i$ .

• For a contravariant type parameter $\operatorname{\texttt{in\,}}F_i$ , if $A_i$ is an ill-formed type or a covariant type argument, $K_i$ is an ill-formed type. Otherwise, $K_i :> A_i$ .

• For a bounded type parameter $F_i <: U_i \equiv B_1 \mathbin{\operatorname{\&}}\ldots \mathbin{\operatorname{\&}}B_m$ , if $\neg (A_i <: \tau U_i)$ , $K_i$ is an ill-formed type. Otherwise, $K_i <: \tau U_i$ .

  Note: captured substitution $\tau : F_1 = K_1, \ldots, F_n = K_n$ manipulates captured types.

• For a covariant type argument $\operatorname{\texttt{out\,}}A_i$ , if $F_i$ is a contravariant type parameter, $K_i$ is an ill-formed type. Otherwise, $K_i <: A_i$ .

• For a contravariant type argument $\operatorname{\texttt{in\,}}A_i$ , if $F_i$ is a covariant type parameter, $K_i$ is an ill-formed type. Otherwise, $K_i :> A_i$ .

• For a bivariant type argument $\star$ , $\operatorname{\texttt{kotlin.Nothing}}<: K_i <: \operatorname{\texttt{kotlin.Any?}}$ .

• Otherwise, $K_i \equiv A_i$ .

Note: for implementation reasons the compiler may approximate $L$ and/or $U$ ; for example, in the current implementation $L$ is always approximated to be a single type.

Note: as every captured type corresponds to a fresh type variable, two different captured types $K_i$ and $K_j$ which describe the same set of possible types (i.e., their constraint sets are equal) are not considered equal. However, in some cases type inference may approximate a captured type $K$ to a concrete type $K^{\approx}$ ; in our case, it would be that $K_i^{\approx} \equiv K_j^{\approx}$ .

Examples: also show the use of type containment to establish subtyping.

interface Inv<T>
interface Out<out T>
interface In<in T>

interface Root<T>

interface A
interface B : A
interface C : B

fun <T> mk(): T = TODO()

interface Bounded<T : A> : Root<T>

fun test01() {

    val bounded: Bounded<in B> = mk()

    // Bounded<in B> <: Bounded<KB> where B <: KB <: A
    //   (from type capturing)
    // Bounded<KB> <: Root<KB>
    //   (from supertype relation)

    val test: Root<in C> = bounded

    // ?- Bounded<in B> <: Root<in C>
    //
    // Root<KB> <: Root<in C> where B <: KB <: A
    //   (from above facts)
    // KB ⪯ in C
    //   (from subtyping for parameterized types)
    // KB ⪯ in KC where C <: KC <: C
    //   (from type containment rules)
    // KB :> KC
    //   (from type containment rules)
    // (A :> KB :> B) :> (C :> KC :> C)
    //   (from subtyping for captured types)
    // B :> C
    //   (from supertype relation)
    // True

}

interface Foo<T> : Root<Out<T>>

fun test02() {

    val foo: Foo<out B> = mk()

    // Foo<out B> <: Foo<KB> where KB <: B
    //   (from type capturing)
    // Foo<KB> <: Root<Out<KB>>
    //   (from supertype relation)

    val test: Root<out Out<B>> = foo

    // ?- Foo<out B> <: Root<out Out<B>>
    //
    // Root<Out<KB>> <: Root<out Out<B>> where KB <: B
    //   (from above facts)
    // Out<KB> ⪯ out Out<B>
    //   (from subtyping for parameterized types)
    // Out<KB> <: Out<B>
    //   (from type containment rules)
    // Out<out KB> <: Out<out B>
    //   (from declaration-site variance)
    // out KB ⪯ out B
    //   (from subtyping for parameterized types)
    // out KB ⪯ out KB' where B <: KB' <: B
    //   (from type containment rules)
    // KB <: KB'
    //   (from type containment rules)
    // (KB :< B) <: (B <: KB' <: B)
    //   (from subtyping for captured types)
    // B <: B
    //   (from subtyping definition)
    // True

}

interface Bar<T> : Root<Inv<T>>

fun test03() {

    val bar: Bar<out B> = mk()

    // Bar<out B> <: Bar<KB> where KB <: B
    //   (from type capturing)
    // Bar<KB> <: Root<Inv<KB>>
    //   (from supertype relation)

    val test: Root<out Inv<B>> = bar

    // ?- Bar<out B> <: Root<out Inv<B>>
    //
    // Root<Inv<KB>> <: Root<out Inv<B>> where KB <: B
    //   (from above facts)
    // Inv<KB> ⪯ out Inv<B>
    //   (from subtyping for parameterized types)
    // Inv<KB> <: Inv<B>
    //   (from type containment rules)
    // KB ⪯ B
    //   (from subtyping for parameterized types)
    // KB ⪯ KB' where B <: KB' <: B
    //   (from type containment rules)
    // KB ⊆ KB'
    //   (from type containment rules)
    // (Nothing <: KB :< B) ⊆ (B <: KB' <: B)
    //
    // False

}

interface Recursive<T : Recursive<T>>

fun <T : Recursive<T>> probe(e: Recursive<T>): T = mk()

fun test04() {
    val rec: Recursive<*> = mk()

    // Recursive<*> <: Recursive<KS> where KS <: Recursive<KS>
    //   (from type capturing)
    // Recursive<KS> <: Root<KS>
    //   (from supertype relation)

    val root: Root<*> = rec

    // ?- Recursive<*> <: Root<*>
    //
    // Root<KS> <: Root<KT>
    //     where Nothing <: KS <: Recursive<KS>
    //           Nothing <: KT <: Any?
    //   (from above facts and type capturing)
    // KS ⪯ KT
    //   (from subtyping for parameterized types)
    // KS ⊆ KT
    //   (from type containment rules)
    // (Nothing <: KS <: Recursive<KS>) ⊆ (Nothing <: KT <: Any?)
    //
    // True

    val rootRec: Root<Recursive<*>> = rec

    // ?- Recursive<*> <: Root<Recursive<*>>
    //
    // Root<KS> <: Root<Recursive<*>>
    //     where Nothing <: KS <: Recursive<KS>
    //   (from above facts)
    // KS ⪯ Recursive<*>
    //   (from subtyping for parameterized types)
    // KS ⪯ KT where Recursive<*> <: KT <: Recursive<*>
    //   (from type containment rules)
    // KS ⊆ KT
    //   (from type containment rules)
    // (Nothing <: KS <: Recursive<KS) ⊆ (Recursive<*> <: KT <: Recursive<*>)
    //
    // False
    
}

Type containment

Important: type parameters $F_i <: U_i$ are handled as if they have been converted to well-formed captured types $K_i : \operatorname{\texttt{kotlin.Nothing}}<: K_i <: U_i$ .

• $A \preceq B$ if $A \equiv B$

• $A \preceq \operatorname{\texttt{out\,}}B$ if $A <: B$

• $A \preceq \operatorname{\texttt{in\,}}B$ if $A :> B$

• $\operatorname{\texttt{out\,}}A \preceq \operatorname{\texttt{out\,}}B$ if $A <: B$

• $\operatorname{\texttt{in\,}}A \preceq \operatorname{\texttt{in\,}}B$ if $A :> B$

• $K_A \preceq K_B$ if $K_A \subseteq K_B$

• $K_A \preceq \operatorname{\texttt{out\,}}K_B$ if $K_A <: K_B$

• $K_A \preceq \operatorname{\texttt{in\,}}K_B$ if $K_A :> K_B$

• $\operatorname{\texttt{out\,}}K_A \preceq \operatorname{\texttt{out\,}}K_B$ if $K_A <: K_B$

• $\operatorname{\texttt{in\,}}K_A \preceq \operatorname{\texttt{in\,}}K_B$ if $K_A :> K_B$

Function types

• argument types $A_i$
• return type $R$

• receiver type $\operatorname{\text{RT}}$
• argument types $A_i$
• return type $R$

Note: this means that, for example, these two types are equivalent w.r.t. type system

• Int.(Int) -> String
• (Int, Int) -> String

However, these two types are not equivalent w.r.t. overload resolution, as it distinguishes between functions with and without receiver.

Note: a compiler implementation may consider a function type $\operatorname{\text{FunctionN}}$ to have additional supertypes, if it is necessary.

Example:

// A function of type Function1<Number, Number>
//   or (Number) -> Number
fun foo(i: Number): Number = ...

// A valid assignment w.r.t. function type variance
// Function1<in Int, out Any> :> Function1<in Number, out Number>
val fooRef: (Int) -> Any = ::foo

// A function with receiver of type Function1<Number, Number>
//   or Number.() -> Number
fun Number.bar(): Number = ...

// A valid assignment w.r.t. function type variance
// Receiver is just yet another function argument
// Function1<in Int, out Any> :> Function1<in Number, out Number>
val barRef: (Int) -> Any = Number::bar

Suspending function types

Example:

fun foo(i: Int): String = TODO()

fun bar() {
    val fooRef: (Int) -> String = ::foo
    val fooLambda: (Int) -> String = { it.toString() }
    val suspendFooLambda: suspend (Int) -> String = { it.toString() }

    // Error: as suspending and non-suspending
    //   function types are unrelated
    // val error: suspend (Int) -> String = ::foo
    // val error: suspend (Int) -> String = fooLambda
    // val error: (Int) -> String = suspendFooLambda
}

Flexible types

• $L$ and $U$ are well-formed concrete types
• $L <: U$
• $L$ and $U$ are not flexible types (but may contain other flexible types as some of their type arguments)

Dynamic type

Platform types

Important: platform types should not be confused with multi-platform projects — another Kotlin feature targeted at supporting platform interop.

Nullable types

Note: informally, question mark means “$T?$ may hold values of type $T$ or value null”

• $T$ is a well-formed concrete type

Note: if an operation is safe regardless of absence or presence of null, e.g., assignment of one nullable value to another, it can be used as-is for nullable types. For operations on $T?$ which may violate null safety, e.g., access to a property, one has the following null-safe options:

1. Use safe operations
   • safe call
2. Downcast from $T?$ to $T!!$
   • unsafe cast
   • type check combined with smart casts
   • null check combined with smart casts
   • not-null assertion operator
3. Supply a default value to use if null is present
   • elvis operator

Nullability lozenge

Note: trivial subtyping relation $A!! <: A?$ is not represented in the nullability lozenge.

Example: if we have $\operatorname{\texttt{kotlin.Int}}? <: T?$ , we also have $\operatorname{\texttt{kotlin.Int}}!! <: T?$ and $\operatorname{\texttt{kotlin.Int}}!! <: T!!$ , meaning we can establish $\operatorname{\texttt{kotlin.Int}}!! <: T \equiv \operatorname{\texttt{kotlin.Int}}<: T$ .

Example: if we have $T? <: \operatorname{\texttt{kotlin.Int}}?$ , we also have $T!! <: \operatorname{\texttt{kotlin.Int}}?$ and $T!! <: \operatorname{\texttt{kotlin.Int}}!!$ , however, we can establish only $T <: \operatorname{\texttt{kotlin.Int}}?$ , as $T <: \operatorname{\texttt{kotlin.Int}}$ would need $T? <: \operatorname{\texttt{kotlin.Int}}!!$ which is forbidden by the nullability lozenge.

Definitely non-nullable types

Note: for example, it is needed when overriding a Java method with a @NotNull annotated generic parameter.

Example:

public interface JBox {
    <T> void put(@NotNull T t);
}

class KBox : JBox {
    override fun <T> put(t: T/* !! */) = TODO()
}

• $T$ is a well-formed type parameter with a nullable upper bound
• $Any$ is resolved to $\operatorname{\texttt{kotlin.Any}}$

Example:

typealias MyAny = kotlin.Any

fun <T /* : Any? */, Q : Any> bar(t: T?, q: Q?, i: Int?) {
    // OK
    val a: T & Any = t!!
    // OK: MyAny is resolved to kotlin.Any
    val b: T & MyAny = t!!
    // ERROR: Int is not kotlin.Any
    val c: T & Int = t!!

    // ERROR: Q does not have a nullable upper bound
    val d: Q & Any = q!!

    // ERROR: Int? is not a type parameter
    val e: Int? & Any = i!!
}

Intersection types

Note: this means intersection types are commutative and associative (following the GLB properties); e.g., $A \mathbin{\operatorname{\&}}B$ is the same type as $B \mathbin{\operatorname{\&}}A$ , and $A \mathbin{\operatorname{\&}}(B \mathbin{\operatorname{\&}}C)$ is the same type as $A \mathbin{\operatorname{\&}}B \mathbin{\operatorname{\&}}C$ .

Note: for presentation purposes, we will henceforth order intersection type operands lexicographically based on their notation.

Integer literal types

Union types

Important: Kotlin does not have union types in its type system. However, they make reasoning about several type system features easier. Therefore, we decided to include a brief intro to the union types here.

Type contexts and scopes

Inner and nested type contexts

Note: nested type declarations cannot capture parent type parameters, as they simply create a regular type available under a nested path.

Example:

class Parent<T> {
    class Nested(val i: Int)

    // Can use type parameter T as a type
    // in an inner class
    inner class Inner(val t: T)

    // Cannot use type parameter T as a type
    // in a nested class
    class Error(val t: T)
}

fun main() {
    val nested = Parent.Nested(42)

    val inner = Parent<String>().Inner("42")
}

Subtyping

• reflexive ($A <: A$ )
• rigidly transitive ($A <: B \land B <: C \Rightarrow A <: C$ for non-flexible types $A$ , $B$ and $C$ )

Subtyping rules

• $\forall T : \operatorname{\texttt{kotlin.Nothing}}<: T <: \operatorname{\texttt{kotlin.Any}}$
• For any simple classifier type $T : S_1, \ldots, S_m$ it is true that $\forall i \in [1,m]: T <: S_i$
• For any parameterized type $\widehat{T} = T\langle \tau \rangle: S_1, \ldots, S_m$ it is true that $\forall i \in [1,m]: \widehat{T} <: \tau S_i$
• For any two parameterized types $\widehat{T} = T\langle \tau \rangle$ and $\widehat{T^\prime} = T\langle \tau^\prime \rangle$ with captured type arguments $K_i$ and $K_i^\prime$ it is true that $\widehat{T} <: \widehat{T^\prime}$ if $\forall i \in [1,n]: K_i \preceq K_i^\prime$