Types

Type                  ::=  FunType
                        |  TypeLambda
                        |  MatchType
                        |  InfixType
FunType               ::=  FunTypeArgs ‘=>’ Type
                        |  TypeLambdaParams '=>' Type
TypeLambda            ::=  TypeLambdaParams ‘=>>’ Type
MatchType             ::=  InfixType ‘match’ <<< TypeCaseClauses >>>
InfixType             ::=  RefinedType
                        |  RefinedTypeOrWildcard id [nl] RefinedTypeOrWildcard {id [nl] RefinedTypeOrWildcard}
RefinedType           ::=  AnnotType {[nl] Refinement}
AnnotType             ::=  SimpleType {Annotation}
SimpleType            ::=  SimpleLiteral
                        |  SimpleType1
SimpleType1           ::=  id
                        |  Singleton ‘.’ id
                        |  Singleton ‘.’ ‘type’
                        |  ‘(’ TypesOrWildcards ‘)’
                        |  Refinement
                        |  SimpleType1 TypeArgs
                        |  SimpleType1 ‘#’ id
Singleton             ::=  SimpleRef
                        |  SimpleLiteral
                        |  Singleton ‘.’ id
SimpleRef             ::=  id
                        |  [id ‘.’] ‘this’
                        |  [id ‘.’] ‘super’ [‘[’ id ‘]’] ‘.’ id
ParamType             ::=  [‘=>’] ParamValueType
ParamValueType        ::=  ParamValueType [‘*’]
TypeArgs              ::=  ‘[’ TypesOrWildcards ‘]’
Refinement            ::=  :<<< [RefineDef] {semi [RefineDef]} >>>

FunTypeArgs           ::=  InfixType
                        |  ‘(’ [ FunArgTypes ] ‘)’
                        |  FunParamClause
FunArgTypes           ::=  FunArgType { ‘,’ FunArgType }
FunArgType            ::=  Type
                        |  ‘=>’ Type
FunParamClause        ::=  ‘(’ TypedFunParam {‘,’ TypedFunParam } ‘)’
TypedFunParam         ::=  id ‘:’ Type

TypeLambdaParams      ::=  ‘[’ TypeLambdaParam {‘,’ TypeLambdaParam} ‘]’
TypeLambdaParam       ::=  {Annotation} (id | ‘_’) [TypeParamClause] TypeBounds
TypeParamClause       ::=  ‘[’ VariantTypeParam {‘,’ VariantTypeParam} ‘]’
VariantTypeParam      ::=  {Annotation} [‘+’ | ‘-’] (id | ‘_’) [TypeParamClause] TypeBounds

TypeCaseClauses       ::=  TypeCaseClause { TypeCaseClause }
TypeCaseClause        ::=  ‘case’ (InfixType | ‘_’) ‘=>’ Type [semi]

RefineDef             ::=  ‘val’ ValDef
                        |  ‘def’ DefDef
                        |  ‘type’ {nl} TypeDef

TypeBounds            ::=  [‘>:’ Type] [‘<:’ Type]

TypesOrWildcards      ::=  TypeOrWildcard {‘,’ TypeOrWildcard}
TypeOrWildcard        ::=  Type
                        |  WildcardType
RefinedTypeOrWildcard ::=  RefinedType
                        |  WildcardType
WildcardType          ::=  (‘?‘ | ‘_‘) TypeBounds

The above grammer describes the concrete syntax of types that can be written in user code. Semantic operations on types in the Scala type system are better defined in terms of internal types, which are desugared from the concrete type syntax.

Internal Types

The following abstract grammar defines the shape of internal types. In this specification, unless otherwise noted, "types" refer to internal types. Internal types abstract away irrelevant details such as precedence and grouping, and contain shapes of types that cannot be directly expressed using the concrete syntax. They also contain simplified, decomposed shapes for complex concrete syntax types, such as refined types.

Type              ::=  ‘AnyKind‘
                    |  ‘Nothing‘
                    |  TypeLambda
                    |  DesignatorType
                    |  ParameterizedType
                    |  ThisType
                    |  SuperType
                    |  LiteralType
                    |  ByNameType
                    |  AnnotatedType
                    |  RefinedType
                    |  RecursiveType
                    |  RecursiveThis
                    |  UnionType
                    |  IntersectionType
                    |  MatchType
                    |  SkolemType

TypeLambda        ::=  ‘[‘ TypeParams ‘]‘ ‘=>>‘ Type
TypeParams        ::=  TypeParam {‘,‘ TypeParam}
TypeParam         ::=  ParamVariance id TypeBounds
ParamVariance     ::=  ε | ‘+‘ | ‘-‘

DesignatorType    ::=  Prefix ‘.‘ id
Prefix            ::=  Type
                    |  PackageRef
                    |  ε
PackageRef        ::=  id {‘.‘ id}

ParameterizedType ::=  Type ‘[‘ TypeArgs ‘]‘
TypeArgs          ::=  TypeArg {‘,‘ TypeArg}
TypeArg           ::=  Type
                    |  WilcardTypeArg
WildcardTypeArg   ::=  ‘?‘ TypeBounds

ThisType          ::=  classid ‘.‘ ‘this‘
SuperType         ::=  classid ‘.‘ ‘super‘ ‘[‘ classid ‘]‘
LiteralType       ::=  SimpleLiteral
ByNameType        ::=  ‘=>‘ Type
AnnotatedType     ::=  Type Annotation

RefinedType       ::=  Type ‘{‘ Refinement ‘}‘
Refinement        ::=  ‘type‘ id TypeAliasOrBounds
                    |  ‘def‘ id ‘:‘ TypeOrMethodic
                    |  ‘val‘ id ‘:‘ Type

RecursiveType     ::=  ‘{‘ recid ‘=>‘ Type ‘}‘
RecursiveThis     ::=  recid ‘.‘ ‘this‘

UnionType         ::=  Type ‘|‘ Type
IntersectionType  ::=  Type ‘&‘ Type

MatchType               ::=  Type ‘match‘ ‘<:‘ Type ‘{‘ {TypeCaseClause} ‘}‘
TypeCaseClause          ::=  ‘case‘ TypeCasePattern ‘=>‘ Type
TypeCasePattern         ::=  TypeCapture
                          |  TypeCaseAppliedPattern
                          |  Type
TypeCaseAppliedPattern  ::=  Type ‘[‘ TypeCasePattern { ‘,‘ TypeCasePattern } ‘]‘
TypeCapture             ::=  (id | ‘_‘) TypeBounds

SkolemType        ::=  ‘∃‘ skolemid ‘:‘ Type

TypeOrMethodic    ::=  Type
                    |  MethodicType
MethodicType      ::=  MethodType
                    |  PolyType

MethodType        ::=  ‘(‘ MethodTypeParams ‘)‘ TypeOrMethodic
MethodTypeParams  ::=  ε
                    |  MethodTypeParam {‘,‘ MethodTypeParam}
MethodTypeParam   ::=  id ‘:‘ Type

PolyType          ::=  ‘[‘ PolyTypeParams ‘]‘ TypeOrMethodic
PolyTypeParams    ::=  PolyTypeParam {‘,‘ PolyTypeParam}
PolyTypeParam     ::=  id TypeBounds

TypeAliasOrBounds ::=  TypeAlias
                    |  TypeBounds
TypeAlias         ::=  ‘=‘ Type
TypeBounds        ::=  ‘<:‘ Type ‘>:‘ Type

Translation of Concrete Types into Internal Types

Concrete types are recursively translated, or desugared, into internal types. Most shapes of concrete types have a one-to-one translation to shapes of internal types. We elaborate hereafter on the translation of the other ones.

Infix Types

InfixType     ::=  CompoundType {id [nl] CompoundType}

A concrete infix type T1T_1 op T2T_2 consists of an infix operator op which gets applied to two type operands T1T_1 and T2T_2. The type is translated to the internal type application op[T1,T2][T_1, T_2]. The infix operator op may be an arbitrary identifier.

Type operators follow the same precedence and associativity as term operators. For example, A + B * C parses as A + (B * C) and A | B & C parses as A | (B & C). Type operators ending in a colon ‘:’ are right-associative; all other operators are left-associative.

In a sequence of consecutive type infix operations t0&ThinSpace;op&ThinSpace;t1&ThinSpace;op2&ThinSpace;...&ThinSpace;opn&ThinSpace;tnt_0 \, \mathit{op} \, t_1 \, \mathit{op_2} \, ... \, \mathit{op_n} \, t_n, all operators op1,...,opn\mathit{op}_1, ..., \mathit{op}_n must have the same associativity. If they are all left-associative, the sequence is interpreted as (...(t0op1t1)op2...)opntn(... (t_0 \mathit{op_1} t_1) \mathit{op_2} ...) \mathit{op_n} t_n, otherwise it is interpreted as t0op1(t1op2(...opntn)...)t_0 \mathit{op_1} (t_1 \mathit{op_2} ( ... \mathit{op_n} t_n) ...).

Under -source:future, if the type name is alphanumeric and the target type is not marked infix, a deprecation warning is emitted.

The type operators | and & are not really special. Nevertheless, unless shadowed, they resolve to the fundamental type aliases scala.| and scala.&, which represent union and intersection types, respectively.

Function Types

Type              ::=  FunTypeArgs ‘=>’ Type
FunTypeArgs       ::=  InfixType
                    |  ‘(’ [ FunArgTypes ] ‘)’
                    |  FunParamClause
FunArgTypes       ::=  FunArgType { ‘,’ FunArgType }
FunArgType        ::=  Type
                    |  ‘=>’ Type
FunParamClause    ::=  ‘(’ TypedFunParam {‘,’ TypedFunParam } ‘)’
TypedFunParam     ::=  id ‘:’ Type

The concrete function type (T1,...,Tn)R(T_1, ..., T_n) \Rightarrow R represents the set of function values that take arguments of types T1,...,TnT_1, ..., Tn and yield results of type RR. The case of exactly one argument type TRT \Rightarrow R is a shorthand for (T)R(T) \Rightarrow R. An argument type of the form T\Rightarrow T represents a call-by-name parameter of type TT.

Function types associate to the right, e.g. STRS \Rightarrow T \Rightarrow R is the same as S(TR)S \Rightarrow (T \Rightarrow R).

Function types are covariant in their result type and contravariant in their argument types.

Function types translate into internal class types that define an apply method. Specifically, the nn-ary function type (T1,...,Tn)R(T_1, ..., T_n) \Rightarrow R translates to the internal class type scala.Functionn_n[T1T_1, ..., TnT_n, RR]. In particular ()R() \Rightarrow R is a shorthand for class type scala.Function0_0[RR].

Such class types behave as if they were instances of the following trait:

trait Functionn_n[-T1T_1, ..., -TnT_n, +RR]:
  def apply(x1x_1: T1T_1, ..., xnx_n: TnT_n): RR

Their exact supertype and implementation can be consulted in the function classes section of the standard library page in this document.

Dependent function types are function types whose parameters are named and can referred to in result types. In the concrete type (x1:T1,...,xn:Tn)R(x_1: T_1, ..., x_n: T_n) \Rightarrow R, RR can refer to the parameters xix_i, notably to form path-dependent types. It translates to the internal refined type

scala.Functionn_n[T1T_1, ..., TnT_n, SS] {
  def apply(x1x_1: T1T_1, ..., xnx_n: TnT_n): RR
}

where SS is the least super type of RR that does not mention any of the xix_i.

Polymorphic function types are function types that take type arguments. Their result type must be a function type. In the concrete type [a1&gt;:L1&lt;:H1,...,an&gt;:L1&lt;:H1]=&gt;(T1,...,Tm)=&gt;R[a_1 &gt;: L_1 &lt;: H_1, ..., a_n &gt;: L_1 &lt;: H_1] =&gt; (T_1, ..., T_m) =&gt; R, the types TjT_j and RR can refer to the type parameters aia_i. It translates to the internal refined type

scala.PolyFunction {
  def apply[a1&gt;:L1&lt;:H1,...,an&gt;:L1&lt;:H1a_1 &gt;: L_1 &lt;: H_1, ..., a_n &gt;: L_1 &lt;: H_1](x1x_1: T1T_1, ..., xnx_n: TnT_n): RR
}

Tuple Types

SimpleType1           ::=  ...
                        |  ‘(’ TypesOrWildcards ‘)’

A tuple type (T1,...,Tn)(T_1, ..., T_n) where n2n \geq 2 is sugar for the type T1T_1 *: ... *: TnT_n *: scala.EmptyTuple, which is itself a series of nested infix types which are sugar for *:[T1T_1, *:[T2T_2, ... *:[TnT_n, scala.EmptyTuple]]]. The TiT_i can be wildcard type arguments.

Notes:

Concrete Refined Types

RefinedType           ::=  AnnotType {[nl] Refinement}
SimpleType1           ::=  ...
                        |  Refinement
Refinement            ::=  :<<< [RefineDef] {semi [RefineDef]} >>>

RefineDef             ::=  ‘val’ ValDef
                        |  ‘def’ DefDef
                        |  ‘type’ {nl} TypeDef

In the concrete syntax of types, refinements can contain several refined definitions. They must all be abstract. Moreover, the refined definitions can refer to each other as well as to members of the parent type, i.e., they have access to this.

In the internal types, each refinement defines exactly one refined definition, and references to this must be made explicit in a recursive type.

The conversion from the concrete syntax to the abstract syntax works as follows:

  1. Create a fresh recursive this name α\alpha.
  2. Replace every implicit or explicit reference to this in the refinement definitions by α\alpha.
  3. Create nested refined types, one for every refined definition.
  4. Unless α\alpha was never actually used, wrap the result in a recursive type { α\alpha => ...... }.

Concrete Match Types

MatchType             ::=  InfixType ‘match’ <<< TypeCaseClauses >>>
TypeCaseClauses       ::=  TypeCaseClause { TypeCaseClause }
TypeCaseClause        ::=  ‘case’ (InfixType | ‘_’) ‘=>’ Type [semi]

In the concrete syntax of match types, patterns are arbitrary InfixTypes, and there is no explicit notion of type capture. In the abstract syntax, however, captures are made explicit and can only appear as arguments to TypeCaseAppliedPatterns.

If the concrete pattern is _, its conversion is the internal type scala.Any. If it is a concrete InfixType, it is first converted to an internal type PP. If PP is not a ParameterizedType, then use PP as the internal pattern. Otherwise, PP is recursively converted into a TypeCasePattern as follows:

  1. If PP is a WildcardTypeArg of the form ? >: LL <: HH, return a TypeCapture of the form _ >: LL <: HH.
  2. If PP is a direct type designator tt whose name starts with a lowercase and was not written using backticks, return a TypeCapture tt >: LL <: HH where >: LL <: HH is the declared type definition of tt.
  3. If PP is a ParameterizedType of the form TT[T1T_1, ..., TnT_n]:
    1. Recursively convert each TiT_i into a pattern PiP_i.
    2. If PiP_i is a Type for all ii, return PP.
    3. Otherwise, return the TypeCaseAppliedPattern TT[P1P_1, ..., PnP_n].
  4. Otherwise, return PP.

This conversion ensures that every TypeCaseAppliedPattern recursively contains at least one TypeCapture. Moreover, at the top level, the pattern is never a TypeCapture: all TypeCaptures are nested within a TypeCaseAppliedPattern.

The bound of the internal MatchType is always <: scala.Any by default. It can be overridden in a type member definition.

Concrete Type Lambdas

TypeLambda            ::= TypeLambdaParams ‘=>>’ Type
TypeLambdaParams      ::=  ‘[’ TypeLambdaParam {‘,’ TypeLambdaParam} ‘]’
TypeLambdaParam       ::=  {Annotation} (id | ‘_’) [TypeParamClause] TypeBounds
TypeParamClause       ::=  ‘[’ VariantTypeParam {‘,’ VariantTypeParam} ‘]’
VariantTypeParam      ::=  {Annotation} [‘+’ | ‘-’] (id | ‘_’) [TypeParamClause] TypeBounds

At the top level of concrete type lambda parameters, variance annotations are not allowed. However, in internal types, all type lambda parameters have explicit variance annotations.

When translating a concrete type lambda into an internal one, the variance of each type parameter is inferred from its usages in the body of the type lambda.

Definitions

From here onwards, we refer to internal types by default.

Kinds

The Scala type system is fundamentally higher-kinded. Types are either proper types, type constructors or poly-kinded types.

All types live in a single lattice with respect to a conformance relationship &lt;:&lt;:. The top type is AnyKind and the bottom type is Nothing: all types conform to AnyKind, and Nothing conforms to all types. They can be referred to with the fundamental type aliases scala.AnyKind and scala.Nothing, respectively.

Types can be concrete or abstract. An abstract type TT always has lower and upper bounds LL and HH such that L&gt;:TL &gt;: T and T&lt;:HT &lt;: H. A concrete type TT is considered to have itself as both lower and upper bound.

The kind of a type is indicated by its (transitive) upper bound:

As a consequece, AnyKind itself is poly-kinded. Nothing is universally-kinded: it has all kinds at the same time, since it conforms to all types.

With this representation, it is rarely necessary to explicitly talk about the kinds of types. Usually, the kinds of types are implicit through their bounds.

Another way to look at it is that type bounds are kinds. They represent sets of types: &gt;:L&lt;:H&gt;: L &lt;: H denotes the set of types TT such that L&lt;:TL &lt;: T and T&lt;:HT &lt;: H. A set of types can be seen as a type of types, i.e., as a kind.

Conventions

Type bounds are formally always of the form &gt;:L&lt;:H&gt;: L &lt;: H. By convention, we can omit either of both bounds in writing.

These conventions correspond to the defaults in the concrete syntax.

Proper Types

Proper types are also called value types, as they represent sets of values.

Stable types are value types that contain exactly one non-null value. Stable types can be used as prefixes in named designator types. The stable types are

Every stable type TT is concrete and has an underlying type UU such that T&lt;:UT &lt;: U.

Type Constructors

To each type constructor corresponds an inferred type parameter clause which is computed as follows:

Type Definitions

A type definition DD represents the right-hand-side of a type member definition or the bounds of a type parameter. It is either:

All type definitions have a lower bound LL and an upper bound HH, which are types. For type aliases, L=H=UL = H = U.

The type definition of a type parameter is never a type alias.

Types

Type Lambdas

TypeLambda     ::=  ‘[‘ TypeParams ‘]‘ ‘=>>‘ Type
TypeParams     ::=  TypeParam {‘,‘ TypeParam}
TypeParam      ::=  ParamVariance id TypeBounds
ParamVariance  ::=  ε | ‘+‘ | ‘-‘

A type lambda of the form [±a1&gt;:L1&lt;:H1\pm a_1 &gt;: L_1 &lt;: H_1, ..., ±an&gt;:Ln&lt;:Hn\pm a_n &gt;: L_n &lt;: H_n] =>> UU is a direct representation of a type constructor with nn type parameters. When applied to nn type arguments that conform to the specified bounds, it produces another type UU. Type lambdas are always concrete types.

The scope of a type parameter extends over the result type UU as well as the bounds of the type parameters themselves.

All type constructors conform to some type lambda.

The type bounds of the parameters of a type lambda are in contravariant position, while its result type is in covariant position. If some type constructor T&lt;:T &lt;: [±a1&gt;:L1&lt;:H1\pm a_1 &gt;: L_1 &lt;: H_1, ..., ±an&gt;:Ln&lt;:Hn\pm a_n &gt;: L_n &lt;: H_n] =>> UU, then TT's iith type parameter bounds contain the bounds &gt;:Li&lt;:Hi&gt;: L_i &lt;: H_i, and its result type conforms to UU.

Note: the concrete syntax of type lambdas does not allow to specify variances for type parameters. Instead, variances are inferred from the body of the lambda to be as general as possible.

Example
type Lst = [T] =>> List[T] // T is inferred to be covariant with bounds >: Nothing <: Any
type Fn = [A <: Seq[?], B] =>> (A => B) // A is inferred to be contravariant, B covariant

val x: Lst[Int] = List(1) // ok, Lst[Int] expands to List[Int]
val f: Fn[List[Int], Int] = (x: List[Int]) => x.head // ok

val g: Fn[Int, Int] = (x: Int) => x // error: Int does not conform to the bound Seq[?]

def liftPair[F <: [T] =>> Any](f: F[Int]): Any = f
liftPair[Lst](List(1)) // ok, Lst <: ([T] =>> Any)

Designator Types

DesignatorType    ::=  Prefix ‘.‘ id
Prefix            ::=  Type
                    |  PackageRef
                    |  ε
PackageRef        ::=  id {‘.‘ id}

A designator type (or designator for short) is a reference to a definition. Term designators refer to term definitions, while type designators refer to type definitions.

In the abstract syntax, the id retains whether it is a term or type. In the concrete syntax, an id refers to a type designator, while id.type refers to a term designator. In that context, term designators are often called singleton types.

Designators with an empty prefix ϵ\epsilon are called direct designators. They refer to local definitions available in the scope:

The ids of direct designators are protected from accidental shadowing in the abstract syntax. They retain the identity of the exact definition they refer to, rather than relying on scope-based name resolution. 1

The ϵ\epsilon prefix cannot be written in the concrete syntax. A bare id is used instead and resolved based on scopes.

Named designators refer to member definitions of a non-empty prefix:

Term Designators

A term designator p.xp.x referring to a term definition t has an underlying type UU. If p=ϵp = \epsilon or pp is a package ref, the underlying type UU is the declared type of t and p.xp.x is a stable type if an only if t is a val or object definition. Otherwise, the underlying type UU and whether p.xp.x is a stable type are determined by memberType(pp, xx).

All term designators are concrete types. If scala.Null &lt;:U&lt;: U, the term designator denotes the set of values consisting of null and the value denoted by tt, i.e., the value vv for which t eq v. Otherwise, the designator denotes the singleton set only containing vv.

Type Designators

A type designator p.Cp.C referring to a class definition (including traits and hidden object classes) is a class type. If the class is monomorphic, the type designator is a value type denoting the set of instances of CC or any of its subclasses. Otherwise it is a type constructor with the same type parameters as the class definition. All class types are concrete, non-stable types.

If a type designator p.Tp.T is not a class type, it refers to a type definition T (a type parameter or a type member definition) and has an underlying type definition. If p=ϵp = \epsilon or pp is a package ref, the underlying type definition is the declared type definition of T. Otherwise, it is determined by memberType(pp, TT). A non-class type designator is concrete (resp. stable) if and only if its underlying type definition is an alias UU and UU is itself concrete (resp. stable).

Parameterized Types

ParameterizedType ::=  Type ‘[‘ TypeArgs ‘]‘
TypeArgs          ::=  TypeArg {‘,‘ TypeArg}
TypeArg           ::=  Type
                    |  WilcardTypeArg
WildcardTypeArg   ::=  ‘?‘ TypeBounds

A parameterized type T[T1,...,Tn]T[T_1, ..., T_n] consists of a type constructor TT and type arguments T1,...,TnT_1, ..., T_n where n1n \geq 1. The parameterized type is well-formed if

T[T1,...,Tn]T[T_1, ..., T_n] is a parameterized class type if and only if TT is a class type. All parameterized class types are value types.

In the concrete syntax of wildcard type arguments, if both bounds are omitted, the real bounds are inferred from the bounds of the corresponding type parameter in the target type constructor (which must be concrete). If only one bound is omitted, Nothing or Any is used, as usual.

Also in the concrete syntax, _ can be used instead of ? for compatibility reasons, with the same meaning. This alternative will be deprecated in the future, and is already deprecated under -source:future.

Simplification Rules

Wildcard type arguments used in covariant or contravariant positions can always be simplified to regular types.

Let T[T1,...,Tn]T[T_1, ..., T_n] be a parameterized type for a concrete type constructor. Then, applying a wildcard type argument ?&gt;:L&lt;:H? &gt;: L &lt;: H at the ii'th position obeys the following equivalences:

Example Parameterized Types

Given the partial type definitions:

class TreeMap[A <: Comparable[A], B] { ... }
class List[+A] { ... }
class I extends Comparable[I] { ... }

class F[M[A], X] { ... } // M[A] desugars to M <: [A] =>> Any
class S[K <: String] { ... }
class G[M[Z <: I], I] { ... } // M[Z <: I] desugars to M <: [Z <: I] =>> Any

the following parameterized types are well-formed:

TreeMap[I, String]
List[I]
List[List[Boolean]]

F[List, Int]
F[[X] =>> List[X], Int]
G[S, String]

List[?] // ? inferred as List[_ >: Nothing <: Any], equivalent to List[Any]
List[? <: String] // equivalent to List[String]
S[? <: String]
F[?, Boolean] // ? inferred as ? >: Nothing <: [A] =>> Any

and the following types are ill-formed:

TreeMap[I]            // illegal: wrong number of parameters
TreeMap[List[I], Int] // illegal: type parameter not within bound
List[[X] => List[X]]

F[Int, Boolean]       // illegal: Int is not a type constructor
F[TreeMap, Int]       // illegal: TreeMap takes two parameters,
                      //   F expects a constructor taking one
F[[X, Y] => (X, Y)]
G[S, Int]             // illegal: S constrains its parameter to
                      //   conform to String,
                      // G expects type constructor with a parameter
                      //   that conforms to Int

The following code also contains an ill-formed type:

trait H[F[A]]:  // F[A] desugars to F <: [A] =>> Any, which is abstract
  def f: F[_]   // illegal : an abstract type constructor
                // cannot be applied to wildcard arguments.

This Types

ThisType  ::=  classid ‘.‘ ‘this‘

A this type CC.this denotes the this value of class CC within CC.

This types often appear implicitly as the prefix of designator types referring to members of CC. They play a particular role in the type system, since they are affected by the as seen from operation on types.

This types are stable types. The underlying type of CC.this is the self type of CC.

Super Types

SuperType  ::=  classid ‘.‘ ‘super‘ ‘[‘ classid ‘]‘

A super type CC.super[DD] denotes the this value of class C within C, but "widened" to only see members coming from a parent class or trait DD.

Super types exist for compatibility with Scala 2, which allows shadowing of inner classes. In a Scala 3-only context, a super type can always be replaced by the corresponding this type. Therefore, we omit further discussion of super types in this specification.

Literal Types

LiteralType  ::=  SimpleLiteral

A literal type lit denotes the single literal value lit. Thus, the type ascription 1: 1 gives the most precise type to the literal value 1: the literal type 1.

At run time, an expression e is considered to have literal type lit if e == lit. Concretely, the result of e.isInstanceOf[lit] and e match { case _ : lit => } is determined by evaluating e == lit.

Literal types are available for all primitive types, as well as for String. However, only literal types for Int, Long, Float, Double, Boolean, Char and String can be expressed in the concrete syntax.

Literal types are stable types. Their underlying type is the primitive type containing their value.

Example
val x: 1 = 1
val y: false = false
val z: false = y
val int: Int = x

val badX: 1 = int       // error: Int is not a subtype of 1
val badY: false = true  // error: true is not a subtype of false

By-Name Types

ByNameType  ::=  ‘=>‘ Type

A by-name type =&gt;T=&gt; T denotes the declared type of a by-name term parameter. By-name types can only appear as the types of parameters in method types, and as type arguments in parameterized types.

Annotated Types

AnnotatedType  ::=  Type Annotation

An annotated type TaT a attaches the annotation aa to the type TT.

Example

The following type adds the @suspendable annotation to the type String:

String @suspendable

Refined Types

RefinedType  ::=  Type ‘{‘ Refinement ‘}‘
Refinement   ::=  ‘type‘ id TypeAliasOrBounds
               |  ‘def‘ id ‘:‘ TypeOrMethodic
               |  ‘val‘ id ‘:‘ Type

A refined type TRT { R } denotes the set of values that belong to TT and also have a member conforming to the refinement RR.

The refined type TRT { R } is well-formed if:

As an exception to the last rule, a polymorphic method type refinement is allowed if T&lt;:T &lt;: scala.PolyFunction and idid is the name apply.

If the refinement RR overrides no member of TT and is not an occurrence of the scala.PolyFunction exception, the refinement is said to be “structural” 2.

Note: since a refinement does not define a class, it is not possible to use a this type to reference term and type members of the parent type TT within the refinement. When the surface syntax of refined types makes such references, a recursive type wraps the refined type, given access to members of self through a recursive-this type.

Example

Given the following class definitions:

trait T:
  type X <: Option[Any]
  def foo: Any
  def fooPoly[A](x: A): Any

trait U extends T:
  override def foo: Int
  override def fooPoly[A](x: A): A

trait V extends T
  type X = Some[Int]
  def bar: Int
  def barPoly[A](x: A): A

We get the following conformance relationships:

The following refined types are not well-formed:

Recursive Types

RecursiveType  ::=  ‘{‘ recid ‘=>‘ Type ‘}‘
RecursiveThis  ::=  recid ‘.‘ ‘this‘

A recursive type of the form { α\alpha => TT } represents the same values as TT, while offering TT access to its recursive this type α\alpha.

Recursive types cannot directly be expressed in the concrete syntax. They are created as needed when a refined type in the concrete syntax contains a refinement that needs access to the this value. Each recursive type defines a unique self-reference α\alpha, distinct from any other recursive type in the system.

Recursive types can be unfolded during subtyping as needed, replacing references to its α\alpha by a stable reference to the other side of the conformance relationship.

Example

Given the class definitions in the refined types section, we can write the following refined type in the source syntax:

T { def foo: X }
// equivalent to
T { def foo: this.X }

This type is not directly expressible as a refined type alone, as the refinement cannot access the this value. Instead, in the abstract syntax of types, it is translated to { α\alpha => TT { def foo: α\alpha.X } }.

Given the following definitions:

trait Z extends T:
  type X = Option[Int]
  def foo: Option[Int] = Some(5)

val z: Z

we can check that z &lt;:&lt;: { α\alpha => TT { def foo: α\alpha.X } }. We first unfold the recursive type, substituting zz for α\alpha, resulting in z &lt;:&lt;: T { def foo: z.X }. Since the underlying type of zz is ZZ, we can resolve z.X to mean Option[Int], and then validate that z &lt;:&lt;: T and that z has a member def foo: Option[Int].

Union and Intersection Types

UnionType         ::=  Type ‘|‘ Type
IntersectionType  ::=  Type ‘&‘ Type

Syntactically, the types S | T and S & T are infix types, where the infix operators are | and &, respectively (see infix types).

However, in this specification, STS | T and STS & T refer to the underlying core concepts of union and intersection types, respectively.

From the conformance rules rules on union and intersection types, we can show that and are commutative and associative. Moreover, is distributive over . For any type AA, BB and CC, all of the following relationships hold:

If CC is a co- or contravariant type constructor, C[A]C[B]C[A] & C[B] can be simplified using the following rules:

The right-to-left validity of the above two rules can be derived from the definition of covariance and contravariance and the conformance rules of union and intersection types:

Join of a union type

In some situations, a union type might need to be widened to a non-union type. For this purpose, we define the join of a union type T1...TnT_1 | ... | T_n as the smallest intersection type of base class instances of T1,...,TnT_1, ..., T_n. Note that union types might still appear as type arguments in the resulting type, this guarantees that the join is always finite.

For example, given

trait C[+T]
trait D
trait E
class A extends C[A] with D
class B extends C[B] with D with E

The join of ABA | B is C[AB]DC[A | B] & D

Match Types

MatchType               ::=  Type ‘match‘ ‘<:‘ Type ‘{‘ {TypeCaseClause} ‘}‘
TypeCaseClause          ::=  ‘case‘ TypeCasePattern ‘=>‘ Type
TypeCasePattern         ::=  TypeCapture
                          |  TypeCaseAppliedPattern
                          |  Type
TypeCaseAppliedPattern  ::=  Type ‘[‘ TypeCasePattern { ‘,‘ TypeCasePattern } ‘]‘
TypeCapture             ::=  (id | ‘_‘) TypeBounds

A match type contains a scrutinee, a list of case clauses, and an upper bound. The scrutinee and the upper bound must both be proper types. A match type can be reduced to the body of a case clause if the scrutinee matches its pattern, and if it is provably disjoint from every earlier pattern.

A TypeCasePattern is a legal pattern if and only if one of the following is true:

A type PP is a "pattern-legal type constructor" if one of the following is true:

Given the following definitions:

class Inv[A]
class Cov[+A]
class Contra[-A]

class Base {
  type Y
}

type YExtractor[t] = Base { type Y = t }
type ZExtractor[t] = Base { type Z = t }

type IsSeq[t <: Seq[Any]] = t

Here are examples of legal patterns:

// TypeWithoutCapture's
case Any => // also the desugaring of `case _ =>` when the _ is at the top-level
case Int =>
case List[Int] =>
case Array[String] =>

// Class type constructors with direct captures
case scala.collection.immutable.List[t] => // not Predef.List; it is a type alias
case Array[t] =>
case Contra[t] =>
case Either[s, t] =>
case Either[s, Contra[Int]] =>
case h *: t =>
case Int *: t =>

// The S type constructor
case S[n] =>

// An abstract type constructor
// given a [F[_]] or `type F[_] >: L <: H` in scope
case F[t] =>

// Nested captures in covariant position
case Cov[Inv[t]] =>
case Cov[Cov[t]] =>
case Cov[Contra[t]] =>
case Array[h] *: t => // sugar for *:[Array[h], t]
case g *: h *: EmptyTuple =>

// Type aliases
case List[t] => // which is Predef.List, itself defined as `type List[+A] = scala.collection.immutable.List[A]`

// Refinements (through a type alias)
case YExtractor[t] =>

The following patterns are not legal:

// Type capture nested two levels below a non-covariant type constructor
case Inv[Cov[t]] =>
case Inv[Inv[t]] =>
case Contra[Cov[t]] =>

// Type constructor with bounds that do not contain all possible instantiations
case IsSeq[t] =>

// Type refinement where the refined type member is not a member of the parent
case ZExtractor[t] =>

Matching

Given a scrutinee X and a match type case case P => R with type captures ts, matching proceeds in three steps:

  1. Compute instantiations for the type captures ts', and check that they are specific enough.
  2. If successful, check that X <:< [ts := ts']P.
  3. If successful, reduce to [ts := ts']R.

The instantiations are computed by the recursive function matchPattern(X, P, variance, scrutIsWidenedAbstract). At the top level, variance = 1 and scrutIsWidenedAbstract = false.

matchPattern behaves according to what kind is P:

Disjointness

A scrutinee XX is provably disjoint from a pattern PP iff it is provably disjoint from the type PP&#x27; obtained by replacing every type capture in PP by a wildcard type argument with the same bounds.

We note XYX ⋔ Y to say that XX and YY are provably disjoint. Intuitively, that notion is based on the following properties of the Scala language:

However, a precise definition of provably-disjoint is complicated and requires some helpers. We start with the notion of "simple types", which are a minimal subset of Scala internal types that capture the concepts mentioned above.

A "simple type" is one of:

We define X⌈X⌉ a function from a full Scala type to a simple type. Intuitively, it returns the "smallest" simple type that is a supertype of X. It is defined as follows:

The following properties hold about X⌈X⌉ (we have paper proofs for those):

The "lower-bound rule" states that S&lt;:TS &lt;: T if T=q.XT = q.X and q.Xq.X is a non-class type designator and S&lt;:LS &lt;: L where LL is the lower bound of the underlying type definition of q.Xq.X". That rule is known to break transitivy of subtyping in Scala already.

Second, we define the relation on classes (including traits, hidden classes of objects, and enum terms) as:

We can now define for types.

For arbitrary types XX and YY, we define XYX ⋔ Y as XY⌈X⌉ ⋔ ⌈Y⌉.

Two simple types SS and TT are provably disjoint if there is a finite derivation tree for STS ⋔ T using the following rules. Most rules go by pair, which makes the whole relation symmetric:

It is worth noting that this definition disregards prefixes entirely. p.Cp.C and q.Cq.C are never provably disjoint, even if pp could be proven disjoint from qq. It also disregards type members.

We have a proof sketch of the following property for :

This is a very desirable property. It means that if we make the scrutinee of a match type more precise (a subtype) through substitution, and the match type previously reduced, then the match type will still reduce to the same case.

Note: if were a "true" disjointness relationship, and not a provably-disjoint relationship, that property would trivially hold based on elementary set theoretic properties. It would amount to proving that if STS ⊆ T and TU=T ⋂ U = ∅, then SU=S ⋂ U = ∅.

Reduction

The result of reducing XX match { case P1P_1 => R1;...;R_1; ...; case PnP_n => RnR_n } can be a type, undefined, or a compile error.

For n1n \geq 1, it is specified as:

The reduction of an "empty" match type XX match { } (which cannot be written in user programs) is a compile error.

Skolem Types

SkolemType  ::=  ‘∃‘ skolemid ‘:‘ Type

Skolem types cannot directly be written in the concrete syntax. Moreover, although they are proper types, they can never be inferred to be part of the types of term definitions (vals, vars and defs). They are exclusively used temporarily during subtyping derivations.

Skolem types are stable types. A skolem type of the form α:T∃ \alpha : T represents a stable reference to unknown value of type TT. The identifier α\alpha is chosen uniquely every time a skolem type is created. However, as a skolem type is stable, it can be substituted in several occurrences in other types. When "copied" through substitution, all the copies retain the same α\alpha, and are therefore equivalent.

Methodic Types

TypeOrMethodic    ::=  Type
                    |  MethodicType
MethodicType      ::=  MethodType
                    |  PolyType

Methodic types are not real types. They are not part of the type lattice.

However, they share some meta-properties with types. In particular, when contained within other types that undertake some substitution, the substitution carries to the types within methodic types. It is therefore often convenient to think about them as types themselves.

Methodic types are used as the "declared type" of def definitions that have at least one term or type parameter list.

Method Types

MethodType        ::=  ‘(‘ MethodTypeParams ‘)‘ TypeOrMethodic
MethodTypeParams  ::=  ε
                    |  MethodTypeParam {‘,‘ MethodTypeParam}
MethodTypeParam   ::=  id ‘:‘ Type

A method type is denoted internally as (Ps)U(\mathit{Ps})U, where (Ps)(\mathit{Ps}) is a sequence of parameter names and types (p1:T1,...,pn:Tn)(p_1:T_1, ..., p_n:T_n) for some n0n \geq 0 and UU is a (value or method) type. This type represents named methods that take arguments named p1,...,pnp_1, ..., p_n of types T1,...,TnT_1, ..., T_n and that return a result of type UU.

Method types associate to the right: (Ps1)(Ps2)U(\mathit{Ps}_1)(\mathit{Ps}_2)U is treated as (Ps1)((Ps2)U)(\mathit{Ps}_1)((\mathit{Ps}_2)U).

Method types do not exist as types of values. If a method name is used as a value, its type is implicitly converted to a corresponding function type.

Example

The definitions

def a: Int
def b (x: Int): Boolean
def c (x: Int) (y: String, z: String): String

produce the typings

a: Int
b: (Int) Boolean
c: (Int) (String, String) String

Polymorphic Method Types

PolyType          ::=  ‘[‘ PolyTypeParams ‘]‘ TypeOrMethodic
PolyTypeParams    ::=  PolyTypeParam {‘,‘ PolyTypeParam}
PolyTypeParam     ::=  ‘id‘ TypeBounds

A polymorphic method type, or poly type for short, is denoted internally as [tps&ThinSpace;\mathit{tps}\,]TT where [tps&ThinSpace;\mathit{tps}\,] is a type parameter section [a1a_1 >: L1L_1 <: U1,...,anU_1, ..., a_n >: LnL_n <: UnU_n] for some n0n \geq 0 and TT is a (value or method) type. This type represents named methods that take type arguments S1,...,SnS_1, ..., S_n which conform to the lower bounds L1,...,LnL_1, ..., L_n and the upper bounds U1,...,UnU_1, ..., U_n and that yield results of type TT.

Example

The definitions

def empty[A]: List[A]
def union[A <: Comparable[A]] (x: Set[A], xs: Set[A]): Set[A]

produce the typings

empty : [A >: Nothing <: Any] List[A]
union : [A >: Nothing <: Comparable[A]] (x: Set[A], xs: Set[A]) Set[A]

Operations on Types

This section defines a few meta-functions on types and methodic types.

These meta-functions are mutually recursive.

Base Type

The meta-function baseType(TT, CC), where TT is a proper type and CC is a class identifier, computes the smallest type UU of the form p.Cp.C or p.Cp.C[U1,...,UnU_1, ..., U_n] such that T&lt;:UT &lt;: U. If no such type exists, the function is not defined. The main purpose of baseType is to substitute prefixes and class type parameters along the inheritance chain.

We define baseType(TT, CC) as follows. For brevity, we write p.Xp.X[U1,...,UnU_1, ..., U_n] instead of p.Xp.X with n=0n = 0.

The definition above uses the following helper functions.

superType(TT) computes the "next upper bound" of TT, if it exists:

Note that the cases of superType do not overlap with each other nor with any baseType case other than the superType-based one. The cases of baseType therefore do not overlap with each other either. That makes baseType an algorithmic partial function.

meet(p.C[T1,...,Tn]p.C[T_1, ..., T_n], q.C[U1,...,Un]q.C[U_1, ..., U_n]) computes an intersection of two (parameterized) class types for the same class, and join computes a union:

We generalize meet(T1,...,TnT_1, ..., T_n) for a sequence as:

Examples

Given the following definitions:

trait Iterable[+A]
trait List[+A] extends Iterable[A]
trait Map[K, +V] extends Iterable[(K, V)]
trait Foo

we have the following baseType results:

As Seen From

The meta-function asSeenFrom(TT, CC, pp), where TT is a type or methodic type visible inside the class CC and pp is a stable type, rebases the type TT "as seen from" the prefix pp. Essentially, it substitutes this-types and class type parameters in TT to appropriate types visible from outside. Since T is visible inside CC, it can contain this-types and class type parameters of CC itself as well as of all its enclosing classes. This-types of enclosing classes must be mapped to appropriate subprefixes of pp, while class type parameters must be mapped to appropriate concrete type arguments.

asSeenFrom(TT, CC, pp) only makes sense if pp has a base type for CC, i.e., if baseType(pp, CC) is defined.

We define asSeenFrom(TT, CC, pp) where baseType(pp, CC) = q.C[U1,...,Un]q.C[U_1, ..., U_n] as follows:

For convenience, we generalize asSeenFrom to type definitions DD.

Member Type

The meta-function memberType(TT, idid, pp), where TT is a proper type, idid is a term or type identifier, and pp is a stable type, finds a member of a type (T.id) and computes its underlying type (for a term) or type definition (for a type) as seen from the prefix pp. For a term, it also computes whether the term is stable. memberType is the fundamental operation that computes the underlying type or underlying type definition of a named designator type.

The result MM of a memberType is one of:

As short-hand, we define memberType(TT, idid) to be the same as memberType(TT, idid, TT) when TT is a stable type.

We define memberType(TT, idid, pp) as follows:

We define the helper function mergeMemberType(M1M_1, M2M_2) as:

Relations between types

We define the following relations between types.

Name Symbolically Interpretation
Conformance T&lt;:UT &lt;: U Type TT conforms to ("is a subtype of") type UU.
Equivalence T=:=UT =:= U TT and UU conform to each other.
Weak Conformance T&lt;:wUT &lt;:_w U Augments conformance for primitive numeric types.
Compatibility Type TT conforms to type UU after conversions.

Conformance

The conformance relation (&lt;:)(&lt;:) is the smallest relation such that S&lt;:TS &lt;: T is true if any of the following conditions hold. Note that the conditions are not all mutually exclusive.

We define isSubPrefix(pp, qq) where pp and qq are prefixes as:

We define matches(SS, TT) where SS and TT are types or methodic types as:

Note that conformance in Scala is not transitive. Given two abstract types AA and BB, and one abstract type C&gt;:A&lt;:BC &gt;: A &lt;: B available on prefix pp, we have A&lt;:p.CA &lt;: p.C and C&lt;:p.BC &lt;: p.B but not necessarily A&lt;:BA &lt;: B.

Least upper bounds and greatest lower bounds

The (&lt;:)(&lt;:) relation forms pre-order between types, i.e. it is transitive and reflexive. This allows us to define least upper bounds and greatest lower bounds of a set of types in terms of that order.

By construction, for all types A and B, the least upper bound of A and B is A | B, and their greatest lower bound is A & B.

Equivalence

Equivalence is defined as mutual conformance.

S=:=TS =:= T if and only if both S&lt;:TS &lt;: T and T&lt;:ST &lt;: S.

Weak Conformance

In some situations Scala uses a more general conformance relation. A type SS weakly conforms to a type TT, written S&lt;:wTS &lt;:_w T, if S&lt;:TS &lt;: T or both SS and TT are primitive number types and SS precedes TT in the following ordering.

Byte  &lt;:w&lt;:_w Short
Short &lt;:w&lt;:_w Int
Char  &lt;:w&lt;:_w Int
Int   &lt;:w&lt;:_w Long
Long  &lt;:w&lt;:_w Float
Float &lt;:w&lt;:_w Double

A weak least upper bound is a least upper bound with respect to weak conformance.

Compatibility

A type TT is compatible to a type UU if TT (or its corresponding function type) weakly conforms to UU after applying eta-expansion. If TT is a method type, it's converted to the corresponding function type. If the types do not weakly conform, the following alternatives are checked in order:

Examples

Function compatibility via SAM conversion

Given the definitions

def foo(x: Int => String): Unit
def foo(x: ToString): Unit

trait ToString { def convert(x: Int): String }

The application foo((x: Int) => x.toString) resolves to the first overload, as it's more specific:

Realizability

A type TT is realizable if and only if it is inhabited by non-null values. It is defined as:

A concrete type TT has good bounds if all of the following apply:

Note: it is possible for baseType(TT, CC) not to be defined because of the meet computation, which may fail to merge prefixes and/or invariant type arguments.

Type Erasure

A type is called generic if it contains type arguments or type variables. Type erasure is a mapping from (possibly generic) types to non-generic types. We write T|T| for the erasure of type TT. The erasure mapping is defined as follows. Internal computations are performed in a transparent mode, which has an effect on how memberType behaves for opaque type aliases.

The erased LUB is computed as follows:

The rules for eglb(A,B)eglb(A, B) are given below in pseudocode:

eglb(scala.Array[A], JArray[B]) = scala.Array[eglb(A, B)]
eglb(scala.Array[T], _)         = scala.Array[T]
eglb(_, scala.Array[T])         = scala.Array[T]
eglb(A, B)                      = A                     if A extends B
eglb(A, B)                      = B                     if B extends A
eglb(A, _)                      = A                     if A is not a trait
eglb(_, B)                      = B                     if B is not a trait
eglb(A, _)                      = A                     // use first

  1. In the literature, this is often achieved through De Bruijn indices or through alpha-renaming when needed. In a concrete implementation, this is often achieved through retaining symbolic references in a symbol table. 

  2. A reference to a structurally defined member (method call or access to a value or variable) may generate binary code that is significantly slower than an equivalent code to a non-structural member. 

  3. In these cases, if T_i and/or U_i are wildcard type arguments, the simplification rules for parameterized types allow to reduce them to real types.