Kotlin Download PDF
Table of contents

Kotlin language specification

Version 1.4-rfc+0.3

Marat Akhin

Mikhail Belyaev

Type system

Glossary

TT
Type (with unknown nullability)
T!!T!!
Non-nullable type
T?T?
Nullable type
{T}\{T\}
Universe of all possible types
{T!!}\{T!!\}
Universe of non-nullable types
{T?}\{T?\}
Universe of nullable types
Well-formed type
A properly constructed type w.r.t. Kotlin type system
Γ\Gamma
Type context
A<:BA <: B
A is a subtype of B
A<:>BA \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 argument of a type constructor
Type argument
Actual type argument in a parameterized type
T[A1,,An]T\lbrack A_1, \ldots, A_n\rbrack
The result of type constructor TT instantiation with type arguments AiA_i
T[σ]T\lbrack\sigma\rbrack
The result of type constructor T(F1,,Fn)T(F_1, \ldots, F_n) instantiation with the assumed substitution σ:F1=A1,,Fn=An\sigma : F_1 = A_1, \ldots, F_n = A_n
σT\sigma T
The result of type substitution in type TT w.r.t. substitution σ\sigma
KT(F,A)K_T(F, A)
Captured type from the type capturing of type parameter FF and type argument AA in parameterized type TT
TK1,,KnT\langle K_1, \ldots, K_n\rangle
The result of type capturing for parameterized type TT with captured types KiK_i
TτT\langle \tau \rangle
The result of type capturing for parameterized type T(F1,,Fn)T(F_1, \ldots, F_n) with captured substitution τ:F1=K1,,Fn=Kn\tau : F_1 = K_1, \ldots, F_n = K_n
A&BA \mathbin{\operatorname{\&}}B
Intersection type of AA and BB
ABA \mathbin{\operatorname{|}}B
Union type of AA and BB
GLB\operatorname{\text{GLB}}
Greatest lower bound
LUB\operatorname{\text{LUB}}
Least upper bound

Introduction

Similarly to most other programming languages, Kotlin operates on data in the form of values or objects, which have types — descriptions of what is the expected behaviour and possible values for their datum. An empty value is represented by a special null object; most operations with it result in runtime errors or exceptions.

Kotlin has a type system with the following main properties.

Type safety (consistency between compile and runtime types) is verified statically, at compile time, for the majority of Kotlin types. However, for better interoperability with platform-dependent code Kotlin also support a variant of gradual types in the form of flexible types. Even more so, in some cases the compile-time type of a value may change depending on the control- and data-flow of the program; a feature usually known as flow typing, represented in Kotlin as smart casts.

Null safety is enforced by having two type universes: nullable (with nullable types T?T? ) and non-nullable (with non-nullable types T!!T!! ). A value of any non-nullable type cannot contain null, meaning all operations within the non-nullable type universe are safe w.r.t. empty values, i.e., should never result in a runtime error caused by null.

Implicit conversions between types in Kotlin are limited to safe upcasts w.r.t. subtyping, meaning all other (unsafe) conversions must be explicit, done via either a conversion function or an explicit cast. However, Kotlin also supports smart casts — a special kind of implicit conversions which are safe w.r.t. program control- and data-flow, which are covered in more detail here.

The unified supertype type for all types in Kotlin is kotlin.Any?\operatorname{\texttt{kotlin.Any?}} , a nullable version of kotlin.Any\operatorname{\texttt{kotlin.Any}} . The unified subtype type for all types in Kotlin is kotlin.Nothing\operatorname{\texttt{kotlin.Nothing}} .

Kotlin uses nominal subtyping, meaning subtyping relation is defined when a type is declared, with bounded parametric polymorphism, implemented as generics via parameterized types. Subtyping between these parameterized types is defined through mixed-site variance.

Type kinds

For the purposes of this section, we establish the following type kinds — different flavours of types which exist in the Kotlin type system.

We distinguish between concrete and abstract types. Concrete types are types which are assignable to values. Abstract types need to be instantiated as concrete types before they can be used as types for values.

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

We further distinguish concrete types between class and interface types; as Kotlin is a language with single inheritance, sometimes it is important to discriminate between these kinds of types. Any given concrete type may be either a class or an interface type, but never both.

We also distinguish between denotable and non-denotable types. The former are types which are expressible in Kotlin and can be written by the end-user. The latter are special types which are not expressible in Kotlin and are used by the compiler in type inference, smart casts, etc.

Built-in types

Kotlin type system uses the following built-in types, which have special semantics and representation (or lack thereof).

kotlin.Any

kotlin.Any\operatorname{\texttt{kotlin.Any}} is the unified supertype (\top ) for {T!!}\{T!!\} , i.e., all non-nullable types are subtypes of kotlin.Any\operatorname{\texttt{kotlin.Any}} , either explicitly, implicitly, or by subtyping relation.

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

kotlin.Nothing

kotlin.Nothing\operatorname{\texttt{kotlin.Nothing}} is the unified subtype (\bot ) for {T}\{T\} , i.e., kotlin.Nothing\operatorname{\texttt{kotlin.Nothing}} is a subtype of all well-formed Kotlin types, including user-defined ones. This makes it an uninhabited type (as it is impossible for anything to be, for example, a function and an integer at the same time), meaning instances of this type can never exist at runtime; subsequently, there is no way to create an instance of kotlin.Nothing\operatorname{\texttt{kotlin.Nothing}} in Kotlin.

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

kotlin.Function

kotlin.Function(R)\operatorname{\texttt{kotlin.Function}}(R) is the unified supertype of all function types. It is parameterized over function return type R.

Built-in integer types

Kotlin supports the following signed integer types.

Besides their use as types, integer types are important w.r.t. integer literal types.

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

Array types

Kotlin arrays are represented as a parameterized type kotlin.Array(T)\operatorname{\texttt{kotlin.Array}}(T) , where TT is the type of the stored elements, which supports get/set operations. The kotlin.Array(T)\operatorname{\texttt{kotlin.Array}}(T) type follows the rules of regular type constructors and parameterized types w.r.t. subtyping.

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.

In addition to the general kotlin.Array(T)\operatorname{\texttt{kotlin.Array}}(T) type, Kotlin also has the following specialized array types:

These array types structurally match the corresponding kotlin.Array(T)\operatorname{\texttt{kotlin.Array}}(T) type; i.e., IntArray has the same methods and properties as kotlin.Array(kotlin.Int)\operatorname{\texttt{kotlin.Array}}(\operatorname{\texttt{kotlin.Int}}) . However, they are not related by subtyping; meaning one cannot pass a BooleanArray argument to a function expecting an kotlin.Array(kotlin.Boolean)\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.

Array type specialization ATS(A)\operatorname{\text{ATS}}(A) is a transformation of a generic kotlin.Array(T)\operatorname{\texttt{kotlin.Array}}(T) type to a corresponding specialized version, which works as follows.

ATS\operatorname{\text{ATS}} takes an important part in how variable length parameters are handled.

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

Classifier types

Classifier types represent regular types which are declared as classes, interfaces or objects. As Kotlin supports parametric polymorphism, there are two variants of classifier types: simple and parameterized.

Simple classifier types

A simple classifier type

T:S1,,SmT : S_1, \ldots, S_m

consists of

To represent a well-formed simple classifier type, T:S1,,SmT : S_1, \ldots, S_m should satisfy the following conditions.

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:

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

Parameterized classifier types

A classifier type constructor

T(F1,,Fn):S1,,SmT(F_1, \ldots, F_n) : S_1, \ldots, S_m

describes an abstract type and consists of

To represent a well-formed type constructor, T(F1,,Fn):S1,,SmT(F_1, \ldots, F_n) : S_1, \ldots, S_m should satisfy the following conditions.

To instantiate a type constructor, one provides it with type arguments, creating a concrete parameterized classifier type

T[A1,,An]T[A_1, \ldots, A_n]

which consists of

To represent a well-formed parameterized type, T[A1,,An]T[A_1, \ldots, A_n] should satisfy the following conditions.

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

Type parameters are a special kind of types, which are introduced by type constructors. They are considered well-formed concrete types only in the type context of their declaring type constructor.

When creating a parameterized type from a type constructor, its type parameters with their respective type arguments go through capturing and create captured types, which follow special rules described in more detail below.

Type parameters may be either unbounded or bounded. By default, a type parameter FF is unbounded, which is the same as saying it is a bounded type parameter of the form F<:kotlin.Any?F <: \operatorname{\texttt{kotlin.Any?}} .

A bounded type parameter additionally specifies upper type bounds for the type parameter and is defined as F<:B1,,BnF <: B_1, \ldots, B_n , where BiB_i is an i-th upper bound on type parameter FF .

To represent a well-formed bounded type parameter of type constructor TT , F<:B1,,BnF <: B_1, \ldots, B_n should satisfy either of the following sets of conditions.

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

From the definition, it follows F<:B1,,BnF <: B_1, \ldots, B_n can be represented as F<:UF <: U where U=B1&&BnU = B_1 \mathbin{\operatorname{\&}}\ldots \mathbin{\operatorname{\&}}B_n (aka intersection type).

Function type parameters

Function type parameters are a flavor of type parameters, which are used in function declarations to create parameterized functions. They are considered well-formed concrete types only in the type context of their declaring function.

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

Function type parameters work similarly to regular type parameters, however, they do not support specifying mixed-site variance.

Mixed-site variance

To implement subtyping between parameterized types, Kotlin uses mixed-site variance — a combination of declaration- and use-site variance, which is easier to understand and reason about, compared to wildcards from Java. Mixed-site variance means you can specify, whether you want your parameterized type to be co-, contra- or invariant on some type parameter, both in type parameter (declaration-site) and type argument (use-site).

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

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

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

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 outA\operatorname{\texttt{out\,}}A of type constructor TT means “TT is a producer of AA s and gets them out”; contravariant type parameter inA\operatorname{\texttt{in\,}}A of type constructor TT means “TT is a consumer of AA s and takes them in”.

For further discussion about mixed-site variance and its practical applications, we readdress you to subtyping.

Declaration-site variance

A type parameter FF may be invariant, covariant or contravariant.

By default, all type parameters are invariant.

To specify a covariant type parameter, it is marked as outF\operatorname{\texttt{out\,}}F . To specify a contravariant type parameter, it is marked as inF\operatorname{\texttt{in\,}}F .

The variance information is used by subtyping and for checking allowed operations on values of co- and contravariant type parameters.

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

Kotlin also supports use-site variance, by specifying the variance for type arguments. Similarly to type parameters, one can have type arguments being co-, contra- or invariant.

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

By default, all type arguments are invariant.

To specify a covariant type argument, it is marked as outA\operatorname{\texttt{out\,}}A . To specify a contravariant type argument, it is marked as inA\operatorname{\texttt{in\,}}A .

Kotlin prohibits contradictory combinations of declaration- and use-site variance as follows.

In case one cannot specify any well-formed type argument, but still needs to use a parameterized type in a type-safe way, they may use bivariant type argument \star , which is roughly equivalent to a combination of outkotlin.Any?\operatorname{\texttt{out\,}}\operatorname{\texttt{kotlin.Any?}} and inkotlin.Nothing\operatorname{\texttt{in\,}}\operatorname{\texttt{kotlin.Nothing}} (for further details, see subtyping).

Note: informally, T[]T[\star] means “I can give out something very generic (kotlin.Any?\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

Type capturing (similarly to Java capture conversion) is used when instantiating type constructors; it creates abstract captured types based on the type information of both type parameters and arguments, which present a unified view on the resulting types and simplifies further reasoning.

The reasoning behind type capturing is closely related to variant parameterized types being a form of bounded existential types; e.g., A<out T> may be loosely considered as the following existential type: X:X<:T.AX\exists X : X <: T . A\langle X\rangle . Informally, a bounded existential type describes a set of possible types, which satisfy its bound constraints. Before such a type can be used, it needs to be opened (or unpacked): existentially quantified type variables are lifted to fresh type variables with corresponding bounds. We call these type variables captured types.

For a given type constructor T(F1,,Fn):S1,,SmT(F_1, \ldots, F_n) : S_1, \ldots, S_m , its instance T[σ]=TτT[\sigma] = T\langle \tau \rangle uses the following rules to create captured type KiK_i from the type parameter FiF_i and type argument AiA_i , at least one of which should have specified variance to create a captured type. In case both type parameter and type argument are invariant, their captured type is equivalent to AiA_i .

Important: type capturing is not recursive.

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

By construction, every captured type KK has the following form:

{L1<:K,,Lp<:K,K<:U1,,K<:Uq}\{L_1 <: K, \ldots, L_p <: K, K <: U_1, \ldots, K <: U_q\}

which can be represented as

L<:K<:UL <: K <: U

where L=L1LpL = L_1 \mathbin{\operatorname{|}}\ldots \mathbin{\operatorname{|}}L_p and U=U1&&UqU = U_1 \mathbin{\operatorname{\&}}\ldots \mathbin{\operatorname{\&}}U_q .

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

Note: as every captured type corresponds to a fresh type variable, two different captured types KiK_i and KjK_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 KK to a concrete type KK^{\approx} ; in our case, it would be that KiKjK_i^{\approx} \equiv K_j^{\approx} .

Type containment

Type containment operator \preceq is used to decide, whether a type AA is contained in another type BB denoted ABA \preceq B , for the purposes of establishing type argument subtyping.

Let A,BA, B be concrete, well-defined non-type-parameter types, KA,KBK_A, K_B be captured types.

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

\preceq is defined as follows.

Rules for captured types follow the same structure.

In case we need to establish type containment between regular type AA and captured type KBK_B , AA is converted to captured type KA:A<:KA<:AK_A : A <: K_A <: A .

Function types

Kotlin has first-order functions; e.g., it supports function types, which describe the argument and return types of its corresponding function.

A function type FT\operatorname{\text{FT}}

FT(A1,,An)R\operatorname{\text{FT}}(A_1, \ldots, A_n) \rightarrow R

consists of

and may be considered the following instantiation of a special type constructor FunctionN(inP1,,inPn,outR)\operatorname{\text{FunctionN}}(\operatorname{\texttt{in\,}}P_1, \ldots, \operatorname{\texttt{in\,}}P_n, \operatorname{\texttt{out\,}}R) (please note the variance of type parameters)

FT(A1,,An)RFunctionN[A1,,An,R]\operatorname{\text{FT}}(A_1, \ldots, A_n) \rightarrow R \equiv \operatorname{\text{FunctionN}}[A_1, \ldots, A_n, R]

These FunctionN\operatorname{\text{FunctionN}} types follow the rules of regular type constructors and parameterized types w.r.t. subtyping.

A function type with receiver FTR\operatorname{\text{FTR}}

FTR(RT,A1,,An)R\operatorname{\text{FTR}}(\operatorname{\text{RT}}, A_1, \ldots, A_n) \rightarrow R

consists of

From the type system’s point of view, it is equivalent to the following function type

FTR(RT,A1,,An)RFT(RT,A1,,An)R\operatorname{\text{FTR}}(\operatorname{\text{RT}}, A_1, \ldots, A_n) \rightarrow R \equiv \operatorname{\text{FT}}(\operatorname{\text{RT}}, A_1, \ldots, A_n) \rightarrow R

i.e., receiver is considered as yet another argument of its function type.

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

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

Furthermore, all function types FunctionN\operatorname{\text{FunctionN}} are subtypes of a general argument-agnostic type kotlin.Function\operatorname{\texttt{kotlin.Function}} for the purpose of unification; this subtyping relation is also used in overload resolution.

Note: a compiler implementation may consider a function type FunctionN\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

Kotlin supports structured concurrency in the form of coroutines via suspending functions.

For the purposes of type system, a suspending function has a suspending function type suspendFT(A1,,An)R\operatorname{\texttt{suspend}}\operatorname{\text{FT}}(A_1, \ldots, A_n) \rightarrow R , which is unrelated by subtyping to any non-suspending function type. This is important for overload resolution and type inference, as it directly influences the types of function values and the applicability of different functions w.r.t. overloading.

Most function values have either non-suspending or suspending function type based on their declarations. However, as lambda literals do not have any explicitly declared function type, they are considered as possibly being both non-suspending and suspending function type, with the final selection done during type inference.

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

Kotlin, being a multi-platform language, needs to support transparent interoperability with platform-dependent code. However, this presents a problem in that some platforms may not support null safety the way Kotlin does. To deal with this, Kotlin supports gradual typing in the form of flexible types.

A flexible type represents a range of possible types between type LL (lower bound) and type UU (upper bound), written as (L..U)(L..U) . One should note flexible types are non-denotable, i.e., one cannot explicitly declare a variable with flexible type, these types are created by the type system when needed.

To represent a well-formed flexible type, (L..U)(L..U) should satisfy the following conditions.

As the name suggests, flexible types are flexible — a value of type (L..U)(L..U) can be used in any context, where one of the possible types between LL and UU is needed (for more details, see subtyping rules for flexible types). However, the actual runtime type TT will be a specific type satisfying S:T<:SL<:S<:U\exists S : T <: S \land L <: S <: U , thus making the substitution possibly unsafe, which is why Kotlin generates dynamic assertions, when it is impossible to prove statically the safety of flexible type use.

Dynamic type

Kotlin includes a special dynamic type, which in many contexts can be viewed as a flexible type (kotlin.Nothing..kotlin.Any?)(\operatorname{\texttt{kotlin.Nothing}}..\operatorname{\texttt{kotlin.Any?}}) . By definition, this type represents any possible Kotlin type, and may be used to support interoperability with dynamically typed libraries, platforms or languages.

However, as a platform may assign special meaning to the values of dynamic type, it may be handled differently from the regular flexible type. These differences are to be explained in the corresponding platform-dependent sections of this specification.

Platform types

The main use cases for flexible types are platform types — types which the Kotlin compiler uses, when interoperating with code written for another platform (e.g., Java). In this case all types on the interoperability boundary are subject to flexibilization — the process of converting a platform-specific type to a Kotlin-compatible flexible type.

For further details on how flexibilization is done, see the corresponding JVM section.

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

Nullable types

Kotlin supports null safety by having two type universes — nullable and non-nullable. All classifier type declarations, built-in or user-defined, create non-nullable types, i.e., types which cannot hold null value at runtime.

To specify a nullable version of type TT , one needs to use T?T? as a type. Redundant nullability specifiers are ignored: T??T?T?? \equiv T? .

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

To represent a well-formed nullable type, T?T? should satisfy the following conditions.

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?T? which may violate null safety, e.g., access to a property, one has the following null-safe options:

  1. Use safe operations
  2. Downcast from T?T? to T!!T!!
  3. Supply a default value to use if null is present
Nullability lozenge

Nullability lozenge represents valid possible subtyping relations between two nullable or non-nullable types in different combinations of their versions. For type TT , we call T!!T!! its non-nullable version, T?T? its nullable version.

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

Nullability lozenge may also help in establishing subtyping between two types by following its structure.

Regular (non-type-variable) types are mapped to nullability lozenge vertices, as for them AA corresponds to A!!A!! , and A?A? corresponds to A?A? . Following the lozenge structure, for regular types AA and BB , as soon as we have established any valid subtyping between two versions of AA and BB , it implies subtyping between all other valid w.r.t. nullability lozenge combinations of versions of types AA and BB .

Type variable types (e.g., captured types or type parameters) are mapped to either nullability lozenge edges or vertices, as for them TT corresponds to either T!!T!! or T?T? , and T?T? corresponds to T?T? . Following the lozenge structure, for type variable type TT (i.e., either non-nullable or nullable version) we need to consider valid subtyping for both versions T!!T!! and T?T? w.r.t. nullability lozenge.

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

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

Intersection types

Intersection types are special non-denotable types used to express the fact that a value belongs to all of several types at the same time.

Intersection type of two types AA and BB is denoted A&BA \mathbin{\operatorname{\&}}B and is equivalent to the greatest lower bound of its components GLB(A,B)\operatorname{\text{GLB}}(A, B) . Thus, the normalization procedure for GLB\operatorname{\text{GLB}} may be used to normalize an intersection type.

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

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

When needed, the compiler may approximate an intersection type to a denotable concrete type using type approximation.

One of the main uses of intersection types are smart casts.

Integer literal types

An integer literal type containing types T1,,TNT_1, \ldots, T_N , denoted ILT(T1,,TN)\operatorname{\text{ILT}}(T_1, \ldots, T_N) is a special non-denotable type designed for integer literals. Each type T1,,TNT_1, \ldots, T_N must be one of the built-in integer types.

Integer literal types are the types of integer literals and have special handling w.r.t. subtyping.

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.

Union types are special non-denotable types used to express the fact that a value belongs to one of several possible types.

Union type of two types AA and BB is denoted ABA \mathbin{\operatorname{|}}B and is equivalent to the least upper bound of its components LUB(A,B)\operatorname{\text{LUB}}(A, B) . Thus, the normalization procedure for LUB\operatorname{\text{LUB}} may be used to normalize a union type.

Moreover, as union types are not used in Kotlin, the compiler always decays a union type to a non-union type using type decaying.

Type contexts and scopes

The way types and scopes interoperate is very similar to how values and scopes work; this includes visibility, accessing types via qualified names or imports. This means, in many cases, type contexts are equivalent to the corresponding scopes. However, there are several important differences, which we outline below.

Inner and nested type contexts

Type parameters are well-formed types in the type context (scope) of their declaring type constructor, including inner type declarations. However, type context for a nested type declaration ND\operatorname{\text{ND}} of a parent type declaration PD\operatorname{\text{PD}} does not include the type parameters of PD\operatorname{\text{PD}} .

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

Kotlin uses the classic notion of subtyping as substitutability — if SS is a subtype of TT (denoted as S<:TS <: T ), values of type SS can be safely used where values of type TT are expected. The subtyping relation <:<: is:

Two types AA and BB are equivalent (ABA \equiv B ), iff A<:BB<:AA <: B \land B <: A . Due to the presence of flexible types, this relation is also only rigidly transitive, e.g., holds only for non-flexible types (see here for more details).

Subtyping rules

Subtyping for non-nullable, concrete types uses the following rules.

Subtyping for captured types uses the following rules.

Subtyping for nullable types is checked separately and uses a special set of rules which are described here.

Subtyping for flexible types

Flexible types (being flexible) follow a simple subtyping relation with other rigid (i.e., non-flexible) types. Let T,A,B,L,UT, A, B, L, U be rigid types.

This captures the notion of flexible type (L..U)(L..U) as something which may be used in place of any type in between LL and UU . If we are to extend this idea to subtyping between two flexible types, we get the following definition.

This is the most extensive definition possible, which, unfortunately, makes the type equivalence relation non-transitive. Let A,BA, B be two different types, for which A<:BA <: B . The following relations hold:

However, A≢BA \not \equiv B .

Subtyping for intersection types

Intersection types introduce several new rules for subtyping. Let A,B,C,DA, B, C, D be non-nullable types.

Moreover, any type TT with supertypes S1,,SNS_1, \ldots, S_N is also a subtype of S1&&SNS_1 \mathbin{\operatorname{\&}}\ldots \mathbin{\operatorname{\&}}S_N .

Subtyping for integer literal types

All integer literal type are equivalent w.r.t. subtyping, meaning that for any sets T1,,TKT_1, \ldots, T_K and U1,,UNU_1, \ldots, U_N of built-in integer types:

Note: the last two rules mean ILT(T1,,TK)\operatorname{\text{ILT}}(T_1, \ldots, T_K) can be considered as an intersection type T1&&TKT_1 \mathbin{\operatorname{\&}}\ldots \mathbin{\operatorname{\&}}T_K or as a union type T1TKT_1 \mathbin{\operatorname{|}}\ldots \mathbin{\operatorname{|}}T_K , depending on the context. Viewing ILT\operatorname{\text{ILT}} as intersection type allows us to use integer literals where built-in integer types are expected. Making ILT\operatorname{\text{ILT}} behave as union type is needed to support cases when they appear in contravariant position.

Example:

interface In<in T>

fun <T> T.asIn(): In<T> = ...

fun <S> select(a: S, b: In<S>): S = ...

fun iltAsIntersection() {
    val a: Int = 42 // ILT(Byte, Short, Int, Long) <: Int
    
    fun foo(a: Short) {}
    
    foo(1377) // ILT(Short, Int, Long) <: Short
}

fun iltAsUnion() {
    val a: Short = 42
    
    select(a, 1337.asIn())
        // For argument a:
        //   Short <: S
        // For argument b:
        //   In<ILT(Short, Int, Long)> <: In<S> =>
        //     S <: ILT(Short, Int, Long)
        // Solution: S =:= Short
}

Subtyping for nullable types

Subtyping for two possibly nullable types AA and BB is defined via two relations, both of which must hold.

  1. Regular subtyping <:<: for types AA and BB using the nullability lozenge
  2. Subtyping by nullability <:null\mathrel{\operatorname{\stackrel{null}{<:}}}

Subtyping by nullability <:null\mathrel{\operatorname{\stackrel{null}{<:}}} for two possibly nullable types AA and BB uses the following rules.

  1. A!!<:nullBA!! \mathrel{\operatorname{\stackrel{null}{<:}}}B
  2. A<:nullBA \mathrel{\operatorname{\stackrel{null}{<:}}}B if T!!:A<:T!!\exists T!! : A <: T!!
  3. A<:nullB?A \mathrel{\operatorname{\stackrel{null}{<:}}}B?
  4. A<:nullBA \mathrel{\operatorname{\stackrel{null}{<:}}}B if T!!:B<:T!!\nexists T!! : B <: T!!
  5. A?̸<:nullBA? \not \mathrel{\operatorname{\stackrel{null}{<:}}}B

Informally: these rules represent the following idea derived from the nullability lozenge.

A̸<:nullBA \not \mathrel{\operatorname{\stackrel{null}{<:}}}B if BB is definitely non-nullable and AA may be nullable or BB may be non-nullable and AA is definitely nullable.

Note: these rules follow the structure of the nullability lozenge and check the absence of nullability violation A?<:nullB!!A? \mathrel{\operatorname{\stackrel{null}{<:}}}B!! via underapproximating it using the supertype relation (as we cannot enumerate the subtype relation for BB ).

Example:

class Foo<A, B : A?> {
    val b: B = mk()
    val bQ: B? = mk()
    
    // For this assignment to be well-formed,
    //   B must be a subtype of A
    // Subtyping by nullability holds per rule 4
    // Regular subtyping does not hold,
    //   as B <: A? is not enough to show B <: A
    //   (we are missing B!! <: A!!)
    val ab: A = b // ERROR

    // For this assignment to be well-formed,
    //   B? must be a subtype of A
    // Subtyping by nullability does not hold per rule 5
    val abQ: A = bQ // ERROR
    
    // For this assignment to be well-formed,
    //   B must be a subtype of A?
    // Subtyping by nullability holds per rule 3
    // Regular subtyping does hold,
    //   as B <: A? is enough to show B <: A?
    val aQb: A? = b // OK
    
    // For this assignment to be well-formed,
    //   B? must be a subtype of A?
    // Subtyping by nullability holds per rule 3
    // Regular subtyping does hold,
    //   as B <: A? is enough to show B? <: A?
    //   (taking the upper edge of the nullability lozenge)
    val aQbQ: A? = bQ // OK
}

class Bar<A, B : A> {
    val b: B = mk()
    val bQ: B? = mk()
    
    // For this assignment to be well-formed,
    //   B must be a subtype of A
    // Subtyping by nullability holds per rule 4
    // Regular subtyping does hold,
    //   as B <: A is enough to show B <: A
    val ab: A = b // OK

    // For this assignment to be well-formed,
    //   B? must be a subtype of A
    // Subtyping by nullability does not hold per rule 5
    val abQ: A = bQ // ERROR
    
    // For this assignment to be well-formed,
    //   B must be a subtype of A?
    // Subtyping by nullability holds per rule 3
    // Regular subtyping does hold,
    //   as B <: A is enough to show B <: A?
    //   (taking the upper triangle of the nullability lozenge)
    val aQb: A? = b // OK
    
    // For this assignment to be well-formed,
    //   B? must be a subtype of A?
    // Subtyping by nullability holds per rule 3
    // Regular subtyping does hold,
    //   as B <: A is enough to show B? <: A?
    //   (taking the upper edge of the nullability lozenge)
    val aQbQ: A? = bQ // OK
}

Example:

This example shows a situation, when the subtyping by nullability relation from T<:C!!T <: C!! is used to prove T<:AT <: A .

Upper and lower bounds

A type UU is an upper bound of types AA and BB if A<:UA <: U and B<:UB <: U . A type LL is a lower bound of types AA and BB if L<:AL <: A and L<:BL <: B .

Note: as the type system of Kotlin is bounded by definition (the upper bound of all types is kotlin.Any?\operatorname{\texttt{kotlin.Any?}} , and the lower bound of all types is kotlin.Nothing\operatorname{\texttt{kotlin.Nothing}} ), any two types have at least one lower bound and at least one upper bound.

Least upper bound

The least upper bound LUB(A,B)\operatorname{\text{LUB}}(A, B) of types AA and BB is an upper bound UU of AA and BB such that there is no other upper bound of these types which is less by subtyping relation than UU .

Note: LUB\operatorname{\text{LUB}} is commutative, i.e., LUB(A,B)=LUB(B,A)\operatorname{\text{LUB}}(A, B) = \operatorname{\text{LUB}}(B, A) . This property is used in the subsequent description, e.g., other properties of LUB\operatorname{\text{LUB}} are defined only for a specific order of the arguments. Definitions following from commutativity of LUB\operatorname{\text{LUB}} are implied.

LUB(A,B)\operatorname{\text{LUB}}(A, B) has the following properties, which may be used to normalize it. This normalization procedure, if finite, creates a canonical representation of LUB.

Important: AA and BB are considered to be non-flexible, unless specified otherwise.

Important: in some cases, the least upper bound is handled as described here, from the point of view of type constraint system.

In the presence of recursively defined parameterized types, the algorithm given above is not guaranteed to terminate as there may not exist a finite representation of LUB\operatorname{\text{LUB}} for particular two types. The detection and handling of such situations (compile-time error or leaving the type in some kind of denormalized state) is implementation-defined.

In some situations, it is needed to construct the least upper bound for more than two types, in which case the least upper bound operator LUB(T1,T2,,TN)\operatorname{\text{LUB}}(T_1, T_2, \ldots, T_N) is defined as LUB(T1,LUB(T2,,TN))\operatorname{\text{LUB}}(T_1, \operatorname{\text{LUB}}(T_2, \ldots, T_N)) .

Greatest lower bound

The greatest lower bound GLB(A,B)\operatorname{\text{GLB}}(A, B) of types AA and BB is a lower bound LL of AA and BB such that there is no other lower bound of these types which is greater by subtyping relation than LL .

Note: GLB\operatorname{\text{GLB}} is commutative, i.e., GLB(A,B)=GLB(B,A)\operatorname{\text{GLB}}(A, B) = \operatorname{\text{GLB}}(B, A) . This property is used in the subsequent description, e.g., other properties of GLB\operatorname{\text{GLB}} are defined only for a specific order of the arguments. Definitions following from commutativity of GLB\operatorname{\text{GLB}} are implied.

GLB(A,B)\operatorname{\text{GLB}}(A, B) has the following properties, which may be used to normalize it. This normalization procedure, if finite, creates a canonical representation of GLB.

Important: AA and BB are considered to be non-flexible, unless specified otherwise.

Note: the Ω\Omega function preserves type system consistency; A,B:A<:BA≢B\forall A, B : A <: B \land A \not\equiv B , type T{outA,inB}T\langle \{\operatorname{\texttt{out\,}}A, \operatorname{\texttt{in\,}}B\}\rangle is the evidence of type TX:X<:A<:B<:XT\langle X\rangle : X <: A <: B <: X , which makes the type system inconsistent. To avoid this situation, we overapproximate inB\operatorname{\texttt{in\,}}B with inkotlin.Nothing\operatorname{\texttt{in\,}}\operatorname{\texttt{kotlin.Nothing}} when needed. Further details are available in the “Mixed-site variance” paper.

Important: in some cases, the greatest lower bound is handled as described here, from the point of view of type constraint system.

In the presence of recursively defined parameterized types, the algorithm given above is not guaranteed to terminate as there may not exist a finite representation of GLB\operatorname{\text{GLB}} for particular two types. The detection and handling of such situations (compile-time error or leaving the type in some kind of denormalized state) is implementation-defined.

In some situations, it is needed to construct the least upper bound for more than two types, in which case the least upper bound operator GLB(T1,T2,,TN)\operatorname{\text{GLB}}(T_1, T_2, \ldots, T_N) is defined as GLB(T1,GLB(T2,,TN))\operatorname{\text{GLB}}(T_1, \operatorname{\text{GLB}}(T_2, \ldots, T_N)) .

Type approximation

As we mentioned before, Kotlin type system has denotable and non-denotable types. In many cases, we need to approximate a non-denotable type, which appeared, for example, during type inference, into a denotable type, so that it can be used in the program. This is achieved via type approximation, which we describe below.

Important: at the moment, type approximation is applied only to intersection and union types.

Type approximation function α\alpha is defined as follows.

Type decaying

All union types are subject to type decaying, when they are converted to a specific intersection type, representable within Kotlin type system.

Important: at the moment, type decaying is applied only to union types. Note: type decaying is comparable to how least upper bound computation works in Java.

Type decaying function δ\delta is defined as follows.

Note: a set of most specific common supertypes S(A,B)\mathbb{S}(A, B) is a reduction of a set of all common supertypes U(A,B)\mathbb{U}(A, B) , which excludes all types TUT \in \mathbb{U} such that VU:VTV<:T\exists V \in \mathbb{U} : V \neq T \land V <: T .

References

  1. Ross Tate. “Mixed-site variance.” FOOL, 2013.
  2. Ross Tate, Alan Leung, and Sorin Lerner. “Taming wildcards in Java’s type system.” PLDI, 2011.