Kotlin Download PDF
Table of contents

Kotlin language specification

Version 1.9-rfc+0.1

Marat Akhin

Mikhail Belyaev

Kotlin/Core

Introduction

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 1.9\textrm{1.9}{} , 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.

Compatibility

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.

Experimental features

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.

Acknowledgments

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.

Feedback

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.

Reference

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

Syntax and grammar

Notation

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

Lexical grammar

Whitespace and comments

LF:
<unicode character Line Feed U+000A>
CR:
<unicode character Carriage Return U+000D>
ShebangLine:
'#!' {<any character excluding CR and LF >}
DelimitedComment:
'/*' { DelimitedComment | <any character> } '*/'
LineComment:
'//' {<any character excluding CR and LF >}
WS:
<one of the following characters: SPACE U+0020, TAB U+0009, Form Feed U+000C>
NL:
LF | (CR [LF])
Hidden:
DelimitedComment | LineComment | WS

Keywords and operators

RESERVED:
'...'
DOT:
'.'
COMMA:
','
LPAREN:
'('
RPAREN:
')'
LSQUARE:
'['
RSQUARE:
']'
LCURL:
'{'
RCURL:
'}'
MULT:
'*'
MOD:
'%'
DIV:
'/'
ADD:
'+'
SUB:
'-'
INCR:
'++'
DECR:
'--'
CONJ:
'&&'
DISJ:
'||'
EXCL_WS:
'!' Hidden
EXCL_NO_WS:
'!'
COLON:
':'
SEMICOLON:
';'
ASSIGNMENT:
'='
ADD_ASSIGNMENT:
'+='
SUB_ASSIGNMENT:
'-='
MULT_ASSIGNMENT:
'*='
DIV_ASSIGNMENT:
'/='
MOD_ASSIGNMENT:
'%='
ARROW:
'->'
DOUBLE_ARROW:
'=>'
RANGE:
'..'
COLONCOLON:
'::'
DOUBLE_SEMICOLON:
';;'
HASH:
'#'
AT_NO_WS:
'@'
AT_POST_WS:
'@' (Hidden | NL)
AT_PRE_WS:
(Hidden | NL) '@'
AT_BOTH_WS:
(Hidden | NL) '@' (Hidden | NL)
QUEST_WS:
'?' Hidden
QUEST_NO_WS:
'?'
LANGLE:
'<'
RANGLE:
'>'
LE:
'<='
GE:
'>='
EXCL_EQ:
'!='
EXCL_EQEQ:
'!=='
AS_SAFE:
'as?'
EQEQ:
'=='
EQEQEQ:
'==='
SINGLE_QUOTE:
'\''
RETURN_AT:
'return@' Identifier
CONTINUE_AT:
'continue@' Identifier
BREAK_AT:
'break@' Identifier
THIS_AT:
'this@' Identifier
SUPER_AT:
'super@' Identifier
FILE:
'file'
FIELD:
'field'
PROPERTY:
'property'
GET:
'get'
SET:
'set'
RECEIVER:
'receiver'
PARAM:
'param'
SETPARAM:
'setparam'
DELEGATE:
'delegate'
PACKAGE:
'package'
IMPORT:
'import'
CLASS:
'class'
INTERFACE:
'interface'
FUN:
'fun'
OBJECT:
'object'
VAL:
'val'
VAR:
'var'
TYPE_ALIAS:
'typealias'
CONSTRUCTOR:
'constructor'
BY:
'by'
COMPANION:
'companion'
INIT:
'init'
THIS:
'this'
SUPER:
'super'
TYPEOF:
'typeof'
WHERE:
'where'
IF:
'if'
ELSE:
'else'
WHEN:
'when'
TRY:
'try'
CATCH:
'catch'
FINALLY:
'finally'
FOR:
'for'
DO:
'do'
WHILE:
'while'
THROW:
'throw'
RETURN:
'return'
CONTINUE:
'continue'
BREAK:
'break'
AS:
'as'
IS:
'is'
IN:
'in'
NOT_IS:
'!is' (Hidden | NL)
NOT_IN:
'!in' (Hidden | NL)
OUT:
'out'
DYNAMIC:
'dynamic'
PUBLIC:
'public'
PRIVATE:
'private'
PROTECTED:
'protected'
INTERNAL:
'internal'
ENUM:
'enum'
SEALED:
'sealed'
ANNOTATION:
'annotation'
DATA:
'data'
INNER:
'inner'
TAILREC:
'tailrec'
OPERATOR:
'operator'
INLINE:
'inline'
INFIX:
'infix'
EXTERNAL:
'external'
SUSPEND:
'suspend'
OVERRIDE:
'override'
ABSTRACT:
'abstract'
FINAL:
'final'
OPEN:
'open'
CONST:
'const'
LATEINIT:
'lateinit'
VARARG:
'vararg'
NOINLINE:
'noinline'
CROSSINLINE:
'crossinline'
REIFIED:
'reified'
EXPECT:
'expect'
ACTUAL:
'actual'

Literals

DecDigitNoZero:
'1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9'
DecDigit:
'0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9'
DecDigitOrSeparator:
DecDigit | '_'
DecDigits:
DecDigit {DecDigitOrSeparator} DecDigit
| DecDigit
DoubleExponent:
('e' | 'E') [('+' | '-')] DecDigits
RealLiteral:
FloatLiteral | DoubleLiteral
FloatLiteral:
DoubleLiteral ('f' | 'F')
| DecDigits ('f' | 'F')
DoubleLiteral:
[DecDigits] '.' DecDigits [DoubleExponent]
| DecDigits DoubleExponent
IntegerLiteral:
DecDigitNoZero {DecDigitOrSeparator} DecDigit
| DecDigit
HexDigit:
DecDigit
| 'A' | 'B' | 'C' | 'D' | 'E' | 'F'
| 'a' | 'b' | 'c' | 'd' | 'e' | 'f'
HexDigitOrSeparator:
HexDigit | '_'
HexLiteral
'0' ('x' | 'X') HexDigit {HexDigitOrSeparator} HexDigit
| '0' ('x' | 'X') HexDigit
BinDigit
'0' | '1'
BinDigitOrSeparator
BinDigit | '_'
BinLiteral
'0' ('b' | 'B') BinDigit {BinDigitOrSeparator} BinDigit
| '0' ('b' | 'B') BinDigit
UnsignedLiteral
(IntegerLiteral | HexLiteral | BinLiteral) ('u' | 'U') ['L']
LongLiteral
(IntegerLiteral | HexLiteral | BinLiteral) 'L'
BooleanLiteral
'true' | 'false'
NullLiteral
'null'
CharacterLiteral
''' (EscapeSeq | <any character excluding CR, LF, ''' or '\'>) '''
UniCharacterLiteral
'\' 'u' HexDigit HexDigit HexDigit HexDigit
EscapedIdentifier
'\' ('t' | 'b' | 'r' | 'n' | ''' | '"' | '\' | '$')
EscapeSeq
UniCharacterLiteral | EscapedIdentifier

Identifiers

Letter
<any unicode character of categories Lu, Ll, Lt, Lm or Lo>
QuotedSymbol
<any character excluding CR, LF and '`'>
UnicodeDigit
<any unicode character of category Nd>
Identifier
(Letter | '_') {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.

IdentifierOrSoftKey
Identifier
| ABSTRACT
| ANNOTATION
| BY
| CATCH
| COMPANION
| CONSTRUCTOR
| CROSSINLINE
| DATA
| DYNAMIC
| ENUM
| EXTERNAL
| FINAL
| FINALLY
| IMPORT
| INFIX
| INIT
| INLINE
| INNER
| INTERNAL
| LATEINIT
| NOINLINE
| OPEN
| OPERATOR
| OUT
| OVERRIDE
| PRIVATE
| PROTECTED
| PUBLIC
| REIFIED
| SEALED
| TAILREC
| VARARG
| WHERE
| GET
| SET
| FIELD
| PROPERTY
| RECEIVER
| PARAM
| SETPARAM
| DELEGATE
| FILE
| EXPECT
| ACTUAL
| CONST
| SUSPEND

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

String mode grammar

QUOTE_OPEN
'"'
TRIPLE_QUOTE_OPEN
'"""'
FieldIdentifier
'$' 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.

QUOTE_CLOSE
'"'
LineStrRef
FieldIdentifier
LineStrText
{<any character except '\', '"' or '$'>} | '$'
LineStrEscapedChar
EscapedIdentifier | UniCharacterLiteral
LineStrExprStart
'${'

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.

TRIPLE_QUOTE_CLOSE
[MultilineStringQuote] '"""'
MultilineStringQuote
'"""' {'"'}
MultiLineStrRef
FieldIdentifier
MultiLineStrText
{<any character except '"' or '$'>} | '$'
MultiLineStrExprStart
'${'

Tokens

These are all the valid tokens in one rule. Note that syntax grammar ignores tokens DelimitedComment, LineComment and WS.

KotlinToken
ShebangLine
| DelimitedComment
| LineComment
| WS
| NL
| RESERVED
| DOT
| COMMA
| LPAREN
| RPAREN
| LSQUARE
| RSQUARE
| LCURL
| RCURL
| MULT
| MOD
| DIV
| ADD
| SUB
| INCR
| DECR
| CONJ
| DISJ
| EXCL_WS
| EXCL_NO_WS
| COLON
| SEMICOLON
| ASSIGNMENT
| ADD_ASSIGNMENT
| SUB_ASSIGNMENT
| MULT_ASSIGNMENT
| DIV_ASSIGNMENT
| MOD_ASSIGNMENT
| ARROW
| DOUBLE_ARROW
| RANGE
| COLONCOLON
| DOUBLE_SEMICOLON
| HASH
| AT_NO_WS
| AT_POST_WS
| AT_PRE_WS
| AT_BOTH_WS
| QUEST_WS
| QUEST_NO_WS
| LANGLE
| RANGLE
| LE
| GE
| EXCL_EQ
| EXCL_EQEQ
| AS_SAFE
| EQEQ
| EQEQEQ
| SINGLE_QUOTE
| RETURN_AT
| CONTINUE_AT
| BREAK_AT
| THIS_AT
| SUPER_AT
| FILE
| FIELD
| PROPERTY
| GET
| SET
| RECEIVER
| PARAM
| SETPARAM
| DELEGATE
| PACKAGE
| IMPORT
| CLASS
| INTERFACE
| FUN
| OBJECT
| VAL
| VAR
| TYPE_ALIAS
| CONSTRUCTOR
| BY
| COMPANION
| INIT
| THIS
| SUPER
| TYPEOF
| WHERE
| IF
| ELSE
| WHEN
| TRY
| CATCH
| FINALLY
| FOR
| DO
| WHILE
| THROW
| RETURN
| CONTINUE
| BREAK
| AS
| IS
| IN
| NOT_IS
| NOT_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
| Identifier
| RealLiteral
| IntegerLiteral
| HexLiteral
| BinLiteral
| LongLiteral
| BooleanLiteral
| NullLiteral
| CharacterLiteral
| QUOTE_OPEN
| QUOTE_CLOSE
| TRIPLE_QUOTE_OPEN
| TRIPLE_QUOTE_CLOSE
| LineStrRef
| LineStrText
| LineStrEscapedChar
| LineStrExprStart
| MultilineStringQuote
| MultiLineStrRef
| MultiLineStrText
| MultiLineStrExprStart
EOF
<end of input>

Syntax grammar

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.

kotlinFile:
[shebangLine]
{NL}
{fileAnnotation}
packageHeader
importList
{topLevelObject}
EOF
script:
[shebangLine]
{NL}
{fileAnnotation}
packageHeader
importList
{statement semi}
EOF
shebangLine:
ShebangLine (NL {NL})
fileAnnotation:
(AT_NO_WS | AT_PRE_WS)
'file'
{NL}
':'
{NL}
(('[' (unescapedAnnotation {unescapedAnnotation}) ']') | unescapedAnnotation)
{NL}
packageHeader:
['package' identifier [semi]]
importList:
{importHeader}
importHeader:
'import' identifier [('.' '*') | importAlias] [semi]
importAlias:
'as' simpleIdentifier
topLevelObject:
declaration [semis]
typeAlias:
[modifiers]
'typealias'
{NL}
simpleIdentifier
[{NL} typeParameters]
{NL}
'='
{NL}
type
declaration:
classDeclaration
| objectDeclaration
| functionDeclaration
| propertyDeclaration
| typeAlias
classDeclaration:
[modifiers]
('class' | (['fun' {NL}] 'interface'))
{NL}
simpleIdentifier
[{NL} typeParameters]
[{NL} primaryConstructor]
[{NL} ':' {NL} delegationSpecifiers]
[{NL} typeConstraints]
[({NL} classBody) | ({NL} enumClassBody)]
primaryConstructor:
[[modifiers] 'constructor' {NL}] classParameters
classBody:
'{'
{NL}
classMemberDeclarations
{NL}
'}'
classParameters:
'('
{NL}
[classParameter {{NL} ',' {NL} classParameter} [{NL} ',']]
{NL}
')'
classParameter:
[modifiers]
['val' | 'var']
{NL}
simpleIdentifier
':'
{NL}
type
[{NL} '=' {NL} expression]
delegationSpecifiers:
annotatedDelegationSpecifier {{NL} ',' {NL} annotatedDelegationSpecifier}
delegationSpecifier:
constructorInvocation
| explicitDelegation
| userType
| functionType
| ('suspend' {NL} functionType)
constructorInvocation:
userType {NL} valueArguments
annotatedDelegationSpecifier:
{annotation} {NL} delegationSpecifier
explicitDelegation:
(userType | functionType)
{NL}
'by'
{NL}
expression
typeParameters:
'<'
{NL}
typeParameter
{{NL} ',' {NL} typeParameter}
[{NL} ',']
{NL}
'>'
typeParameter:
[typeParameterModifiers] {NL} simpleIdentifier [{NL} ':' {NL} type]
typeConstraints:
'where' {NL} typeConstraint {{NL} ',' {NL} typeConstraint}
typeConstraint:
{annotation}
simpleIdentifier
{NL}
':'
{NL}
type
classMemberDeclarations:
{classMemberDeclaration [semis]}
classMemberDeclaration:
declaration
| companionObject
| anonymousInitializer
| secondaryConstructor
anonymousInitializer:
'init' {NL} block
companionObject:
[modifiers]
'companion'
{NL}
['data']
{NL}
'object'
[{NL} simpleIdentifier]
[{NL} ':' {NL} delegationSpecifiers]
[{NL} classBody]
functionValueParameters:
'('
{NL}
[functionValueParameter {{NL} ',' {NL} functionValueParameter} [{NL} ',']]
{NL}
')'
functionValueParameter:
[parameterModifiers] parameter [{NL} '=' {NL} expression]
functionDeclaration:
[modifiers]
'fun'
[{NL} typeParameters]
[{NL} receiverType {NL} '.']
{NL}
simpleIdentifier
{NL}
functionValueParameters
[{NL} ':' {NL} type]
[{NL} typeConstraints]
[{NL} functionBody]
functionBody:
block
| ('=' {NL} expression)
variableDeclaration:
{annotation} {NL} simpleIdentifier [{NL} ':' {NL} type]
multiVariableDeclaration:
'('
{NL}
variableDeclaration
{{NL} ',' {NL} variableDeclaration}
[{NL} ',']
{NL}
')'
propertyDeclaration:
[modifiers]
('val' | 'var')
[{NL} typeParameters]
[{NL} receiverType {NL} '.']
({NL} (multiVariableDeclaration | variableDeclaration))
[{NL} typeConstraints]
[{NL} (('=' {NL} expression) | propertyDelegate)]
[{NL} ';']
{NL}
(([getter] [{NL} [semi] setter]) | ([setter] [{NL} [semi] getter]))
propertyDelegate:
'by' {NL} expression
getter:
[modifiers] 'get' [{NL} '(' {NL} ')' [{NL} ':' {NL} type] {NL} functionBody]
setter:
[modifiers] 'set' [{NL} '(' {NL} functionValueParameterWithOptionalType [{NL} ','] {NL} ')' [{NL} ':' {NL} type] {NL} functionBody]
parametersWithOptionalType:
'('
{NL}
[functionValueParameterWithOptionalType {{NL} ',' {NL} functionValueParameterWithOptionalType} [{NL} ',']]
{NL}
')'
functionValueParameterWithOptionalType:
[parameterModifiers] parameterWithOptionalType [{NL} '=' {NL} expression]
parameterWithOptionalType:
simpleIdentifier {NL} [':' {NL} type]
parameter:
simpleIdentifier
{NL}
':'
{NL}
type
objectDeclaration:
[modifiers]
'object'
{NL}
simpleIdentifier
[{NL} ':' {NL} delegationSpecifiers]
[{NL} classBody]
secondaryConstructor:
[modifiers]
'constructor'
{NL}
functionValueParameters
[{NL} ':' {NL} constructorDelegationCall]
{NL}
[block]
constructorDelegationCall:
('this' | 'super') {NL} valueArguments
enumClassBody:
'{'
{NL}
[enumEntries]
[{NL} ';' {NL} classMemberDeclarations]
{NL}
'}'
enumEntries:
enumEntry {{NL} ',' {NL} enumEntry} {NL} [',']
enumEntry:
[modifiers {NL}] simpleIdentifier [{NL} valueArguments] [{NL} classBody]
type:
[typeModifiers] (functionType | parenthesizedType | nullableType | typeReference | definitelyNonNullableType)
typeReference:
userType
| 'dynamic'
nullableType:
(typeReference | parenthesizedType) {NL} (quest {quest})
quest:
QUEST_NO_WS
| QUEST_WS
userType:
simpleUserType {{NL} '.' {NL} simpleUserType}
simpleUserType:
simpleIdentifier [{NL} typeArguments]
typeProjection:
([typeProjectionModifiers] type)
| '*'
typeProjectionModifiers:
typeProjectionModifier {typeProjectionModifier}
typeProjectionModifier:
(varianceModifier {NL})
| annotation
functionType:
[receiverType {NL} '.' {NL}]
functionTypeParameters
{NL}
'->'
{NL}
type
functionTypeParameters:
'('
{NL}
[parameter | type]
{{NL} ',' {NL} (parameter | type)}
[{NL} ',']
{NL}
')'
parenthesizedType:
'('
{NL}
type
{NL}
')'
receiverType:
[typeModifiers] (parenthesizedType | nullableType | typeReference)
parenthesizedUserType:
'('
{NL}
(userType | parenthesizedUserType)
{NL}
')'
definitelyNonNullableType:
[typeModifiers]
(userType | parenthesizedUserType)
{NL}
'&'
{NL}
[typeModifiers]
(userType | parenthesizedUserType)
statements:
[statement {semis statement}] [semis]
statement:
{label | annotation} (declaration | assignment | loopStatement | expression)
label:
simpleIdentifier (AT_NO_WS | AT_POST_WS) {NL}
controlStructureBody:
block
| statement
block:
'{'
{NL}
statements
{NL}
'}'
loopStatement:
forStatement
| whileStatement
| doWhileStatement
forStatement:
'for'
{NL}
'('
{annotation}
(variableDeclaration | multiVariableDeclaration)
'in'
expression
')'
{NL}
[controlStructureBody]
whileStatement:
'while'
{NL}
'('
expression
')'
{NL}
(controlStructureBody | ';')
doWhileStatement:
'do'
{NL}
[controlStructureBody]
{NL}
'while'
{NL}
'('
expression
')'
assignment:
((directlyAssignableExpression '=') | (assignableExpression assignmentAndOperator)) {NL} expression
semi:
(';' | NL) {NL}
semis:
';' | NL {';' | NL}
expression:
disjunction
disjunction:
conjunction {{NL} '||' {NL} conjunction}
conjunction:
equality {{NL} '&&' {NL} equality}
equality:
comparison {equalityOperator {NL} comparison}
comparison:
genericCallLikeComparison {comparisonOperator {NL} genericCallLikeComparison}
genericCallLikeComparison:
infixOperation {callSuffix}
infixOperation:
elvisExpression {(inOperator {NL} elvisExpression) | (isOperator {NL} type)}
elvisExpression:
infixFunctionCall {{NL} elvis {NL} infixFunctionCall}
elvis:
QUEST_NO_WS ':'
infixFunctionCall:
rangeExpression {simpleIdentifier {NL} rangeExpression}
rangeExpression:
additiveExpression {('..' | '..<') {NL} additiveExpression}
additiveExpression:
multiplicativeExpression {additiveOperator {NL} multiplicativeExpression}
multiplicativeExpression:
asExpression {multiplicativeOperator {NL} asExpression}
asExpression:
prefixUnaryExpression {{NL} asOperator {NL} type}
prefixUnaryExpression:
{unaryPrefix} postfixUnaryExpression
unaryPrefix:
annotation
| label
| (prefixUnaryOperator {NL})
postfixUnaryExpression:
primaryExpression {postfixUnarySuffix}
postfixUnarySuffix:
postfixUnaryOperator
| typeArguments
| callSuffix
| indexingSuffix
| navigationSuffix
directlyAssignableExpression:
(postfixUnaryExpression assignableSuffix)
| simpleIdentifier
| parenthesizedDirectlyAssignableExpression
parenthesizedDirectlyAssignableExpression:
'('
{NL}
directlyAssignableExpression
{NL}
')'
assignableExpression:
prefixUnaryExpression
| parenthesizedAssignableExpression
parenthesizedAssignableExpression:
'('
{NL}
assignableExpression
{NL}
')'
assignableSuffix:
typeArguments
| indexingSuffix
| navigationSuffix
indexingSuffix:
'['
{NL}
expression
{{NL} ',' {NL} expression}
[{NL} ',']
{NL}
']'
navigationSuffix:
memberAccessOperator {NL} (simpleIdentifier | parenthesizedExpression | 'class')
callSuffix:
[typeArguments] (([valueArguments] annotatedLambda) | valueArguments)
annotatedLambda:
{annotation} [label] {NL} lambdaLiteral
typeArguments:
'<'
{NL}
typeProjection
{{NL} ',' {NL} typeProjection}
[{NL} ',']
{NL}
'>'
valueArguments:
'(' {NL} [valueArgument {{NL} ',' {NL} valueArgument} [{NL} ','] {NL}] ')'
valueArgument:
[annotation]
{NL}
[simpleIdentifier {NL} '=' {NL}]
['*']
{NL}
expression
primaryExpression:
parenthesizedExpression
| simpleIdentifier
| literalConstant
| stringLiteral
| callableReference
| functionLiteral
| objectLiteral
| collectionLiteral
| thisExpression
| superExpression
| ifExpression
| whenExpression
| tryExpression
| jumpExpression
parenthesizedExpression:
'('
{NL}
expression
{NL}
')'
collectionLiteral:
'[' {NL} [expression {{NL} ',' {NL} expression} [{NL} ','] {NL}] ']'
literalConstant:
BooleanLiteral
| IntegerLiteral
| HexLiteral
| BinLiteral
| CharacterLiteral
| RealLiteral
| 'null'
| LongLiteral
| UnsignedLiteral
stringLiteral:
lineStringLiteral
| multiLineStringLiteral
lineStringLiteral:
'"' {lineStringContent | lineStringExpression} '"'
multiLineStringLiteral:
'"""' {multiLineStringContent | multiLineStringExpression | '"'} TRIPLE_QUOTE_CLOSE
lineStringContent:
LineStrText
| LineStrEscapedChar
| LineStrRef
lineStringExpression:
'${'
{NL}
expression
{NL}
'}'
multiLineStringContent:
MultiLineStrText
| '"'
| MultiLineStrRef
multiLineStringExpression:
'${'
{NL}
expression
{NL}
'}'
lambdaLiteral:
'{'
{NL}
[[lambdaParameters] {NL} '->' {NL}]
statements
{NL}
'}'
lambdaParameters:
lambdaParameter {{NL} ',' {NL} lambdaParameter} [{NL} ',']
lambdaParameter:
variableDeclaration
| (multiVariableDeclaration [{NL} ':' {NL} type])
anonymousFunction:
['suspend']
{NL}
'fun'
[{NL} type {NL} '.']
{NL}
parametersWithOptionalType
[{NL} ':' {NL} type]
[{NL} typeConstraints]
[{NL} functionBody]
functionLiteral:
lambdaLiteral
| anonymousFunction
objectLiteral:
['data']
{NL}
'object'
[{NL} ':' {NL} delegationSpecifiers {NL}]
[{NL} classBody]
thisExpression:
'this'
| THIS_AT
superExpression:
('super' ['<' {NL} type {NL} '>'] [AT_NO_WS simpleIdentifier])
| SUPER_AT
ifExpression:
'if'
{NL}
'('
{NL}
expression
{NL}
')'
{NL}
(controlStructureBody | ([controlStructureBody] {NL} [';'] {NL} 'else' {NL} (controlStructureBody | ';')) | ';')
whenSubject:
'(' [{annotation} {NL} 'val' {NL} variableDeclaration {NL} '=' {NL}] expression ')'
whenExpression:
'when'
{NL}
[whenSubject]
{NL}
'{'
{NL}
{whenEntry {NL}}
{NL}
'}'
whenEntry:
(whenCondition {{NL} ',' {NL} whenCondition} [{NL} ','] {NL} '->' {NL} controlStructureBody [semi])
| ('else' {NL} '->' {NL} controlStructureBody [semi])
whenCondition:
expression
| rangeTest
| typeTest
rangeTest:
inOperator {NL} expression
typeTest:
isOperator {NL} type
tryExpression:
'try' {NL} block ((({NL} catchBlock {{NL} catchBlock}) [{NL} finallyBlock]) | ({NL} finallyBlock))
catchBlock:
'catch'
{NL}
'('
{annotation}
simpleIdentifier
':'
type
[{NL} ',']
')'
{NL}
block
finallyBlock:
'finally' {NL} block
jumpExpression:
('throw' {NL} expression)
| (('return' | RETURN_AT) [expression])
| 'continue'
| CONTINUE_AT
| 'break'
| BREAK_AT
callableReference:
[receiverType] '::' {NL} (simpleIdentifier | 'class')
assignmentAndOperator:
'+='
| '-='
| '*='
| '/='
| '%='
equalityOperator:
'!='
| '!=='
| '=='
| '==='
comparisonOperator:
'<'
| '>'
| '<='
| '>='
inOperator:
'in'
| NOT_IN
isOperator:
'is'
| NOT_IS
additiveOperator:
'+'
| '-'
multiplicativeOperator:
'*'
| '/'
| '%'
asOperator:
'as'
| 'as?'
prefixUnaryOperator:
'++'
| '--'
| '-'
| '+'
| excl
postfixUnaryOperator:
'++'
| '--'
| ('!' excl)
excl:
'!'
| EXCL_WS
memberAccessOperator:
({NL} '.')
| ({NL} safeNav)
| '::'
safeNav:
QUEST_NO_WS '.'
modifiers:
annotation | modifier {annotation | modifier}
parameterModifiers:
annotation | parameterModifier {annotation | parameterModifier}
modifier:
(classModifier | memberModifier | visibilityModifier | functionModifier | propertyModifier | inheritanceModifier | parameterModifier | platformModifier) {NL}
typeModifiers:
typeModifier {typeModifier}
typeModifier:
annotation
| ('suspend' {NL})
classModifier:
'enum'
| 'sealed'
| 'annotation'
| 'data'
| 'inner'
| 'value'
memberModifier:
'override'
| 'lateinit'
visibilityModifier:
'public'
| 'private'
| 'internal'
| 'protected'
varianceModifier:
'in'
| 'out'
typeParameterModifiers:
typeParameterModifier {typeParameterModifier}
typeParameterModifier:
(reificationModifier {NL})
| (varianceModifier {NL})
| annotation
functionModifier:
'tailrec'
| 'operator'
| 'infix'
| 'inline'
| 'external'
| 'suspend'
propertyModifier:
'const'
inheritanceModifier:
'abstract'
| 'final'
| 'open'
parameterModifier:
'vararg'
| 'noinline'
| 'crossinline'
reificationModifier:
'reified'
platformModifier:
'expect'
| 'actual'
annotation:
(singleAnnotation | multiAnnotation) {NL}
singleAnnotation:
((annotationUseSiteTarget {NL}) | AT_NO_WS | AT_PRE_WS) unescapedAnnotation
multiAnnotation:
((annotationUseSiteTarget {NL}) | AT_NO_WS | AT_PRE_WS) '[' (unescapedAnnotation {unescapedAnnotation}) ']'
annotationUseSiteTarget:
(AT_NO_WS | AT_PRE_WS) ('field' | 'property' | 'get' | 'set' | 'receiver' | 'param' | 'setparam' | 'delegate') {NL} ':'
unescapedAnnotation:
constructorInvocation
| userType
simpleIdentifier:
Identifier
| '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'
identifier:
simpleIdentifier {{NL} '.' simpleIdentifier}

Documentation comments

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.

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 parameter 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} .

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

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 considered as if it is a 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.

Definitely non-nullable types

As discussed here, type variable types have unknown nullability, e.g., a type parameter TT may correspond to either nullable version T?T? , or non-nullable version T!!T!! . In some cases, one might need to specifically denote a nullable/non-nullable version of TT .

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 TT , one can use the nullable type syntax T?T? .

To denote a non-nullable version of TT , one can use the definitely non-nullable type syntax T&AnyT \mathbin{\operatorname{\&}}Any .

To represent a well-formed definitely non-nullable type, T&AnyT \mathbin{\operatorname{\&}}Any 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 T&AnyT \mathbin{\operatorname{\&}}Any , and that is not a coincidence, as an intersection type with AnyAny describes exactly a type which cannot hold null values. For the purposes of the type system, a definitely non-nullable type T&AnyT \mathbin{\operatorname{\&}}Any is consider to be the same as an intersection type T&AnyT \mathbin{\operatorname{\&}}Any .

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. Another restricted version of intersection types are definitely non-nullable types.

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.