Version 1.9-rfc+0.1
Kotlin took inspiration from many programming languages, including (but not limited to) Java, Scala, C# and Groovy. One of the main ideas behind Kotlin is being pragmatic, i.e., being a programming language useful for day-to-day development, which helps the users get the job done via its features and its tools. Thus, a lot of design decisions were and still are influenced by how beneficial these decisions are for Kotlin users.
Kotlin is a multiplatform, statically typed, general-purpose programming language. Currently, as of version , it supports compilation to the following platforms.
Furthermore, it supports transparent interoperability between different platforms via its Kotlin Multiplatform Project (Kotlin MPP) feature.
The type system of Kotlin distinguishes at compile time between nullable and non-nullable types, achieving null-safety, i.e., guaranteeing the absence of runtime errors caused by the absence of value (i.e., null
value). Kotlin also extends its static type system with elements of gradual and flow typing, for better interoperability with other languages and ease of development.
Kotlin is an object-oriented language which also has a lot of functional programming elements. From the object-oriented side, it supports nominal subtyping with bounded parametric polymorphism (akin to generics) and mixed-site variance. From the functional programming side, it has first-class support for higher-order functions and lambda literals.
This specification covers Kotlin/Core, i.e., fundamental parts of Kotlin which should function mostly the same way irregardless of the underlying platform. These parts include such important things as language expressions, declarations, type system and overload resolution.
Important: due to the complexities of platform-specific implementations, platforms may extend, reduce or change the way some aspects of Kotlin/Core function. We mark these platform-dependent Kotlin/Core fragments in the specification to the best of our abilities.
Platform-specific parts of Kotlin and its multiplatform capabilities will be covered in their respective sub-specifications, i.e., Kotlin/JVM, Kotlin/JS and Kotlin/Native.
Kotlin Language Specification is still in progress and has experimental stability level, meaning no compatibility should be expected between even incremental releases of the specification, any parts can be added, removed or changed without warning.
Important: while the specification has experimental stability level, the Kotlin language itself and its compiler have different stability levels for different components, which are described in more detail here.
In several cases this specification discusses experimental Kotlin features, i.e., features which are still in active development and which may be changed in the future. When so, the specification talks about the current state of said features, with no guarantees of their future stability (or even existence in the language).
The experimental features are marked as such in the specification to the best of our abilities.
We would like to thank the following people for their invaluable help and feedback during the writing of this specification.
Note: the format is “First name Last name”, ordered by last name
We would also like to thank Pandoc, its authors and community, as this specification would be much harder to implement without Pandoc’s versatility and support.
If you have any feedback for this document, feel free to create an issue at our GitHub. In case you prefer to use email, you can use marat.akhin@jetbrains.com and mikhail.belyaev@jetbrains.com.
If one needs to reference this specification, they may use the following:
Marat Akhin, Mikhail Belyaev et al. “Kotlin language specification: Kotlin/Core”, JetBrains / JetBrains Research, 2020
This section uses a BNF-based notation similar to EBNF with the following conventions:
Rule names starting with capital letters denote lexical rules, while rule names starting with lowercase letters denote syntactic rules.
Note: this notation is similar to ISO EBNF as per standard ISO/IEC 14977, but does not employ any special symbols for concatenation or termination and does not use some of the additional notation symbols
'#!'
{<any character excluding CR and LF >}
'/*'
{ DelimitedComment | <any character> } '*/'
'//'
{<any character excluding CR and LF >}
'...'
'.'
','
'('
')'
'['
']'
'{'
'}'
'*'
'%'
'/'
'+'
'-'
'++'
'--'
'&&'
'||'
'!'
Hidden
'!'
':'
';'
'='
'+='
'-='
'*='
'/='
'%='
'->'
'=>'
'..'
'::'
';;'
'#'
'@'
'?'
Hidden
'?'
'<'
'>'
'<='
'>='
'!='
'!=='
'as?'
'=='
'==='
'\''
'return@'
Identifier
'continue@'
Identifier
'break@'
Identifier
'this@'
Identifier
'super@'
Identifier
'file'
'field'
'property'
'get'
'set'
'receiver'
'param'
'setparam'
'delegate'
'package'
'import'
'class'
'interface'
'fun'
'object'
'val'
'var'
'typealias'
'constructor'
'by'
'companion'
'init'
'this'
'super'
'typeof'
'where'
'if'
'else'
'when'
'try'
'catch'
'finally'
'for'
'do'
'while'
'throw'
'return'
'continue'
'break'
'as'
'is'
'in'
'out'
'dynamic'
'public'
'private'
'protected'
'internal'
'enum'
'sealed'
'annotation'
'data'
'inner'
'tailrec'
'operator'
'inline'
'infix'
'external'
'suspend'
'override'
'abstract'
'final'
'open'
'const'
'lateinit'
'vararg'
'noinline'
'crossinline'
'reified'
'expect'
'actual'
'1'
| '2'
| '3'
| '4'
| '5'
| '6'
| '7'
| '8'
| '9'
'0'
| '1'
| '2'
| '3'
| '4'
| '5'
| '6'
| '7'
| '8'
| '9'
'_'
'e'
| 'E'
) [('+'
| '-'
)] DecDigits
'f'
| 'F'
)'f'
| 'F'
)
'.'
DecDigits [DoubleExponent]'A'
| 'B'
| 'C'
| 'D'
| 'E'
| 'F'
'a'
| 'b'
| 'c'
| 'd'
| 'e'
| 'f'
'_'
'0'
('x'
| 'X'
) HexDigit {HexDigitOrSeparator} HexDigit'0'
('x'
| 'X'
) HexDigit
'0'
| '1'
'_'
'0'
('b'
| 'B'
) BinDigit {BinDigitOrSeparator} BinDigit'0'
('b'
| 'B'
) BinDigit
'u'
| 'U'
) ['L'
]
'L'
'true'
| 'false'
'null'
'''
(EscapeSeq | <any character excluding CR, LF, '''
or '\'
>) '''
'\'
('t'
| 'b'
| 'r'
| 'n'
| '''
| '"'
| '\'
| '$'
)
'`'
>
'_'
) {Letter | '_'
| UnicodeDigit}'`'
QuotedSymbol {QuotedSymbol} '`'
Kotlin supports escaping identifiers by enclosing any sequence of characters into backtick (`
) characters, allowing to use any name as an identifier. This allows not only using non-alphanumeric characters (like @
or #
) in names, but also using keywords like if
or when
as identifiers. Actual set of characters that is allowed to be escaped may, however, be a subject to platform restrictions. Consult particular platform sections for details.
Note: for example, the following characters are not allowed in identifiers used as declaration names on the JVM platform even when escaped due to JVM restrictions:
.
,;
,[
,]
,/
,<
,>
,:
,\\
.
Escaped identifiers are treated the same as corresponding non-escaped identifier if it is allowed. For example, an escaped identifier `foo`
and non-escaped identifier foo
may be used interchangeably and refer to the same program entity.
Some of the keywords used in Kotlin are allowed to be used as identifiers even when not escaped. Such keywords are called soft keywords. You can see the complete list of soft keyword in the rule above. All other keywords are considered hard keywords and may only be used as identifiers if escaped.
Note: for example, this is a valid property declaration in Kotlin:
val field = 2
even though
field
is a keyword
'"'
'"""'
'$'
IdentifierOrSoftKey
Opening a double quote (QUOTE_OPEN) rule puts the lexical grammar into the special “line string” mode with the following rules. Closing double quote (QUOTE_CLOSE) rule exits this mode.
'"'
'\'
, '"'
or '$'
>} | '$'
'${'
Opening a triple double quote (TRIPLE_QUOTE_OPEN) rule puts the lexical grammar into the special “multiline string” mode with the following rules. Closing triple double quote (TRIPLE_QUOTE_CLOSE) rule exits this mode.
'"""'
'"""'
{'"'
}
'"'
or '$'
>} | '$'
'${'
These are all the valid tokens in one rule. Note that syntax grammar ignores tokens DelimitedComment, LineComment and WS.
The grammar below replaces some lexical grammar rules with explicit literals (where such replacement in trivial and always correct, for example, for keywords) for better readability.
'file'
':'
'['
(unescapedAnnotation {unescapedAnnotation}) ']'
) | unescapedAnnotation)'package'
identifier [semi]]
'import'
identifier [('.'
'*'
) | importAlias] [semi]
'as'
simpleIdentifier
'typealias'
'='
'class'
| (['fun'
{NL}] 'interface'
))':'
{NL} delegationSpecifiers]'constructor'
{NL}] classParameters
'{'
'}'
'('
','
{NL} classParameter} [{NL} ','
]]')'
'val'
| 'var'
]':'
'='
{NL} expression]
','
{NL} annotatedDelegationSpecifier}
'suspend'
{NL} functionType)
'by'
'<'
','
{NL} typeParameter}','
]'>'
':'
{NL} type]
'where'
{NL} typeConstraint {{NL} ','
{NL} typeConstraint}
':'
'companion'
'data'
]'object'
':'
{NL} delegationSpecifiers]'('
','
{NL} functionValueParameter} [{NL} ','
]]')'
'='
{NL} expression]
'fun'
'.'
]':'
{NL} type]'='
{NL} expression)
':'
{NL} type]
'('
','
{NL} variableDeclaration}','
]')'
'val'
| 'var'
)'.'
]'='
{NL} expression) | propertyDelegate)]';'
]'by'
{NL} expression
'('
','
{NL} functionValueParameterWithOptionalType} [{NL} ','
]]')'
'='
{NL} expression]
':'
{NL} type]
':'
'object'
':'
{NL} delegationSpecifiers]'constructor'
':'
{NL} constructorDelegationCall]'this'
| 'super'
) {NL} valueArguments
'{'
';'
{NL} classMemberDeclarations]'}'
'dynamic'
'.'
{NL} simpleUserType}
'*'
'.'
{NL}]'->'
'('
')'
'&'
'{'
'}'
'for'
'('
'in'
')'
'while'
'('
')'
';'
)
'do'
'while'
'('
')'
'='
) | (assignableExpression assignmentAndOperator)) {NL} expression
'||'
{NL} conjunction}
':'
'..'
| '..<'
) {NL} additiveExpression}
'('
')'
'('
')'
'['
','
{NL} expression}','
]']'
'<'
','
{NL} typeProjection}','
]'>'
'('
{NL} [valueArgument {{NL} ','
{NL} valueArgument} [{NL} ','
] {NL}] ')'
'='
{NL}]'*'
]'('
')'
'['
{NL} [expression {{NL} ','
{NL} expression} [{NL} ','
] {NL}] ']'
'null'
'"'
{lineStringContent | lineStringExpression} '"'
'"""'
{multiLineStringContent | multiLineStringExpression | '"'
} TRIPLE_QUOTE_CLOSE
'${'
'}'
'"'
'${'
'}'
'{'
'->'
{NL}]'}'
','
{NL} lambdaParameter} [{NL} ','
]
':'
{NL} type])
'suspend'
]'fun'
'.'
]':'
{NL} type]'this'
'if'
'('
')'
';'
] {NL} 'else'
{NL} (controlStructureBody | ';'
)) | ';'
)
'('
[{annotation} {NL} 'val'
{NL} variableDeclaration {NL} '='
{NL}] expression ')'
','
{NL} whenCondition} [{NL} ','
] {NL} '->'
{NL} controlStructureBody [semi])'else'
{NL} '->'
{NL} controlStructureBody [semi])
'try'
{NL} block ((({NL} catchBlock {{NL} catchBlock}) [{NL} finallyBlock]) | ({NL} finallyBlock))
'catch'
'('
':'
','
]')'
'throw'
{NL} expression)'return'
| RETURN_AT) [expression])'continue'
'break'
'::'
{NL} (simpleIdentifier | 'class'
)
'+='
'-='
'*='
'/='
'%='
'!='
'!=='
'=='
'==='
'<'
'>'
'<='
'>='
'in'
'is'
'+'
'-'
'*'
'/'
'%'
'as'
'as?'
'++'
'--'
'-'
'+'
'++'
'--'
'!'
excl)
'!'
'suspend'
{NL})
'enum'
'sealed'
'annotation'
'data'
'inner'
'value'
'override'
'lateinit'
'public'
'private'
'internal'
'protected'
'in'
'out'
'tailrec'
'operator'
'infix'
'inline'
'external'
'suspend'
'const'
'abstract'
'final'
'open'
'vararg'
'noinline'
'crossinline'
'reified'
'expect'
'actual'
'['
(unescapedAnnotation {unescapedAnnotation}) ']'
'abstract'
'annotation'
'by'
'catch'
'companion'
'constructor'
'crossinline'
'data'
'dynamic'
'enum'
'external'
'final'
'finally'
'get'
'import'
'infix'
'init'
'inline'
'inner'
'internal'
'lateinit'
'noinline'
'open'
'operator'
'out'
'override'
'private'
'protected'
'public'
'reified'
'sealed'
'tailrec'
'set'
'vararg'
'where'
'field'
'property'
'receiver'
'param'
'setparam'
'delegate'
'file'
'expect'
'actual'
'const'
'suspend'
'value'
'.'
simpleIdentifier}
Kotlin supports special comment syntax for code documentation purposes, called KDoc. The syntax is based on Markdown and Javadoc. Documentation comments start with /**
and end with */
and allows external tools to generate documentation based on the comment contents.
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
) and non-nullable (with non-nullable types
). 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 , a nullable version of . The unified subtype type for all types in Kotlin is .
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.
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.
Kotlin type system uses the following built-in types, which have special semantics and representation (or lack thereof).
kotlin.Any
is the unified supertype ( ) for , i.e., all non-nullable types are subtypes of , either explicitly, implicitly, or by subtyping relation.
Note: additional details about are available here.
kotlin.Nothing
is the unified subtype ( ) for , i.e., 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 in Kotlin.
Note: additional details about are available here.
kotlin.Function
is the unified supertype of all function types. It is parameterized over function return type R
.
Kotlin supports the following signed integer types.
kotlin.Int
kotlin.Short
kotlin.Byte
kotlin.Long
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.
Kotlin arrays are represented as a parameterized type
, where
is the type of the stored elements, which supports get
/set
operations. The
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 type, Kotlin also has the following specialized array types:
DoubleArray
(for
)FloatArray
(for
)LongArray
(for
)IntArray
(for
)ShortArray
(for
)ByteArray
(for
)CharArray
(for
)BooleanArray
(for
)These array types structurally match the corresponding
type; i.e., IntArray
has the same methods and properties as
. However, they are not related by subtyping; meaning one cannot pass a BooleanArray
argument to a function expecting an
.
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 toIntIterator
.
Array type specialization is a transformation of a generic type to a corresponding specialized version, which works as follows.
TArray
,
takes an important part in how variable length parameters are handled.
Note: additional details about built-in array types are available here.
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.
A simple classifier type
consists of
To represent a well-formed simple classifier type, 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:
- 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.
A classifier type constructor
describes an abstract type and consists of
To represent a well-formed type constructor, should satisfy the following conditions.
To instantiate a type constructor, one provides it with type arguments, creating a concrete parameterized classifier type
which consists of
To represent a well-formed parameterized type, 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 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 is unbounded, which is the same as saying it is a bounded type parameter of the form .
A bounded type parameter additionally specifies upper type bounds for the type parameter and is defined as , where is an i-th upper bound on type parameter .
To represent a well-formed bounded type parameter of type constructor , 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 can be represented as where (aka intersection type).
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.
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 , subtyping between
T<A>
andT<B>
depends on the variance of type parameter for some type constructor .
- if is covariant ( ),
T<A>
T<B>
- if is contravariant( ),
T<A>
T<B>
- if is invariant (default),
T<A>
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. means covariant type argument, means contravariant type argument; for two non-equivalent types and an invariant type parameter of some type constructor , 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 of type constructor means “ is a producer of s and gets them out”; contravariant type parameter of type constructor means “ is a consumer of s and takes them in”.
For further discussion about mixed-site variance and its practical applications, we readdress you to subtyping.
A type parameter may be invariant, covariant or contravariant.
By default, all type parameters are invariant.
To specify a covariant type parameter, it is marked as . To specify a contravariant type parameter, it is marked as .
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>) }
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 . To specify a contravariant type argument, it is marked as .
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 , which is roughly equivalent to a combination of and (for further details, see subtyping).
Note: informally, means “I can give out something very generic ( ) 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 -> { // OK inInt = invInt // T<in Int> :> T<Int> // OK inInt = invNumber // T<in Int> :> T<in Number> :> T<Number> } 2 -> { // OK outNumber = invInt // T<out Number> :> T<out Int> :> T<Int> // OK outNumber = invNumber // T<out Number> :> T<Number> } 3 -> { // ERROR invInt = inInt // ERROR invInt = outInt // It is invalid to assign less specific type // to a more specific one // T<Int> <: T<in Int> // T<Int> <: T<out Int> } 4 -> { // ERROR inInt = outInt // ERROR inInt = outNumber // types with co- and contravariant type parameters // are not connected by subtyping // T<in Int> not(<:>) T<out Int> } } }
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:
. 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 , its instance uses the following rules to create captured type from the type parameter and type argument , 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 .
Important: type capturing is not recursive.
Note: All applicable rules are used to create the resulting constraint set.
For a covariant type parameter , if is an ill-formed type or a contravariant type argument, is an ill-formed type. Otherwise, .
For a contravariant type parameter , if is an ill-formed type or a covariant type argument, is an ill-formed type. Otherwise, .
For a bounded type parameter , if , is an ill-formed type. Otherwise, .
Note: captured substitution manipulates captured types.
For a covariant type argument , if is a contravariant type parameter, is an ill-formed type. Otherwise, .
For a contravariant type argument , if is a covariant type parameter, is an ill-formed type. Otherwise, .
For a bivariant type argument , .
Otherwise, .
By construction, every captured type has the following form:
which can be represented as
where and .
Note: for implementation reasons the compiler may approximate and/or ; for example, in the current implementation is always approximated to be a single type.
Note: as every captured type corresponds to a fresh type variable, two different captured types and 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 to a concrete type ; in our case, it would be that .
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 operator is used to decide, whether a type is contained in another type denoted , for the purposes of establishing type argument subtyping.
Let be concrete, well-defined non-type-parameter types, be captured types.
Important: type parameters are handled as if they have been converted to well-formed captured types .
is defined as follows.
if
if
if
if
if
Rules for captured types follow the same structure.
if
if
if
if
if
In case we need to establish type containment between regular type and captured type , is considered as if it is a captured type .
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
consists of
and may be considered the following instantiation of a special type constructor (please note the variance of type parameters)
These types follow the rules of regular type constructors and parameterized types w.r.t. subtyping.
A function type with receiver
consists of
From the type system’s point of view, it is equivalent to the following function type
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
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.
Furthermore, all function types are subtypes of a general argument-agnostic type for the purpose of unification; this subtyping relation is also used in overload resolution.
Note: a compiler implementation may consider a function type 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
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 , 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 }
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 (lower bound) and type (upper bound), written as . 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, should satisfy the following conditions.
As the name suggests, flexible types are flexible — a value of type can be used in any context, where one of the possible types between and is needed (for more details, see subtyping rules for flexible types). However, the actual runtime type will be a specific type satisfying , 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.
Kotlin includes a special dynamic
type, which in many contexts can be viewed as a flexible type
. 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.
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.
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 , one needs to use as a type. Redundant nullability specifiers are ignored: .
Note: informally, question mark means “ may hold values of type or value
null
”
To represent a well-formed nullable type, 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 which may violate null safety, e.g., access to a property, one has the following null-safe options:
- Use safe operations
- Downcast from to
- unsafe cast
- type check combined with smart casts
- null check combined with smart casts
- not-null assertion operator
- Supply a default value to use if
null
is present
Nullability lozenge represents valid possible subtyping relations between two nullable or non-nullable types in different combinations of their versions. For type , we call its non-nullable version, its nullable version.
Note: trivial subtyping relation 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 corresponds to , and corresponds to . Following the lozenge structure, for regular types and , as soon as we have established any valid subtyping between two versions of and , it implies subtyping between all other valid w.r.t. nullability lozenge combinations of versions of types and .
Type variable types (e.g., captured types or type parameters) are mapped to either nullability lozenge edges or vertices, as for them corresponds to either or , and corresponds to . Following the lozenge structure, for type variable type (i.e., either non-nullable or nullable version) we need to consider valid subtyping for both versions and w.r.t. nullability lozenge.
Example: if we have , we also have and , meaning we can establish .
Example: if we have , we also have and , however, we can establish only , as would need which is forbidden by the nullability lozenge.
As discussed here, type variable types have unknown nullability, e.g., a type parameter may correspond to either nullable version , or non-nullable version . In some cases, one might need to specifically denote a nullable/non-nullable version of .
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() }
To denote a nullable version of , one can use the nullable type syntax .
To denote a non-nullable version of , one can use the definitely non-nullable type syntax .
To represent a well-formed definitely non-nullable type, should satisfy the following conditions.
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!! }
One may notice the syntax looks like an intersection type
, and that is not a coincidence, as an intersection type with
describes exactly a type which cannot hold null
values. For the purposes of the type system, a definitely non-nullable type
is consider to be the same as an intersection type
.
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 and is denoted and is equivalent to the greatest lower bound of its components . Thus, the normalization procedure for may be used to normalize an intersection type.
Note: this means intersection types are commutative and associative (following the GLB properties); e.g., is the same type as , and is the same type as .
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. Another restricted version of intersection types are definitely non-nullable types.
An integer literal type containing types , denoted is a special non-denotable type designed for integer literals. Each type 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.
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 and is denoted and is equivalent to the least upper bound of its components . Thus, the normalization procedure for 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.
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.
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 of a parent type declaration does not include the type parameters of .
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") }
Kotlin uses the classic notion of subtyping as substitutability — if is a subtype of (denoted as ), values of type can be safely used where values of type are expected. The subtyping relation is:
Two types and are equivalent ( ), iff . 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 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.
Flexible types (being flexible) follow a simple subtyping relation with other rigid (i.e., non-flexible) types. Let be rigid types.
This captures the notion of flexible type as something which may be used in place of any type in between and . 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 be two different types, for which . The following relations hold:
However, .
Intersection types introduce several new rules for subtyping. Let be non-nullable types.
Moreover, any type with supertypes is also a subtype of .
All integer literal type are equivalent w.r.t. subtyping, meaning that for any sets and of built-in integer types:
Note: the last two rules mean can be considered as an intersection type or as a union type , depending on the context. Viewing as intersection type allows us to use integer literals where built-in integer types are expected. Making 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) {} 1377) // ILT(Short, Int, Long) <: Short foo(} fun iltAsUnion() { val a: Short = 42 1337.asIn()) select(a, // 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 two possibly nullable types and is defined via two relations, both of which must hold.
Subtyping by nullability for two possibly nullable types and uses the following rules.
Informally: these rules represent the following idea derived from the nullability lozenge.
if is definitely non-nullable and may be nullable or may be non-nullable and is definitely nullable.
Note: these rules follow the structure of the nullability lozenge and check the absence of nullability violation via underapproximating it using the supertype relation (as we cannot enumerate the subtype relation for ).
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 is used to prove .
A type is an upper bound of types and if and . A type is a lower bound of types and if and .
Note: as the type system of Kotlin is bounded by definition (the upper bound of all types is , and the lower bound of all types is ), any two types have at least one lower bound and at least one upper bound.
The least upper bound of types and is an upper bound of and such that there is no other upper bound of these types which is less by subtyping relation than .
Note: is commutative, i.e., . This property is used in the subsequent description, e.g., other properties of are defined only for a specific order of the arguments. Definitions following from commutativity of are implied.
has the following properties, which may be used to normalize it. This normalization procedure, if finite, creates a canonical representation of LUB.
Important: and are considered to be non-flexible, unless specified otherwise.
if ,
if is nullable,
if and , , where and are defined as follows:
Informally: in many cases, one may view as follows.
if and ,
if and is not flexible,
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 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 is defined as .
The greatest lower bound of types and is a lower bound of and such that there is no other lower bound of these types which is greater by subtyping relation than .
Note: is commutative, i.e., . This property is used in the subsequent description, e.g., other properties of are defined only for a specific order of the arguments. Definitions following from commutativity of are implied.
has the following properties, which may be used to normalize it. This normalization procedure, if finite, creates a canonical representation of GLB.
Important: and are considered to be non-flexible, unless specified otherwise.
if ,
if is non-nullable,
if and , , where and are defined as follows:
Informally: in many cases, one may view as follows.
Note: the function preserves type system consistency; , type is the evidence of type , which makes the type system inconsistent. To avoid this situation, we overapproximate with when needed. Further details are available in the “Mixed-site variance” paper.