Types

Type                  ::=  FunType
                        |  TypeLambda
                        |  InfixType
FunType               ::=  FunTypeArgs ‘=>’ Type
                        |  TypeLambdaParams '=>' Type
TypeLambda            ::=  TypeLambdaParams ‘=>>’ Type
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

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
                    |  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

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 ´T_1´ op ´T_2´ consists of an infix operator op which gets applied to two type operands ´T_1´ and ´T_2´. The type is translated to the internal type application op´[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 ´t_0 \, \mathit{op} \, t_1 \, \mathit{op_2} \, ... \, \mathit{op_n} \, t_n´, all operators ´\mathit{op}_1, ..., \mathit{op}_n´ must have the same associativity. If they are all left-associative, the sequence is interpreted as ´(... (t_0 \mathit{op_1} t_1) \mathit{op_2} ...) \mathit{op_n} t_n´, otherwise it is interpreted as ´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 ´(T_1, ..., T_n) \Rightarrow R´ represents the set of function values that take arguments of types ´T_1, ..., Tn´ and yield results of type ´R´. The case of exactly one argument type ´T \Rightarrow R´ is a shorthand for ´(T) \Rightarrow R´. An argument type of the form ´\Rightarrow T´ represents a call-by-name parameter of type ´T´.

Function types associate to the right, e.g. ´S \Rightarrow T \Rightarrow R´ is the same as ´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 ´n´-ary function type ´(T_1, ..., T_n) \Rightarrow R´ translates to the internal class type scala.Function´_n´[´T_1´, ..., ´T_n´, ´R´]. In particular ´() \Rightarrow R´ is a shorthand for class type scala.Function´_0´[´R´].

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

trait Function´_n´[-´T_1´, ..., -´T_n´, +´R´]:
  def apply(´x_1´: ´T_1´, ..., ´x_n´: ´T_n´): ´R´

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 ´(x_1: T_1, ..., x_n: T_n) \Rightarrow R´, ´R´ can refer to the parameters ´x_i´, notably to form path-dependent types. It translates to the internal refined type

scala.Function´_n´[´T_1´, ..., ´T_n´, ´S´] {
  def apply(´x_1´: ´T_1´, ..., ´x_n´: ´T_n´): ´R´
}

where ´S´ is the least super type of ´R´ that does not mention any of the ´x_i´.

Polymorphic function types are function types that take type arguments. Their result type must be a function type. In the concrete type ´[a_1 >: L_1 <: H_1, ..., a_n >: L_1 <: H_1] => (T_1, ..., T_m) => R´, the types ´T_j´ and ´R´ can refer to the type parameters ´a_i´. It translates to the internal refined type

scala.PolyFunction {
  def apply[´a_1 >: L_1 <: H_1, ..., a_n >: L_1 <: H_1´](´x_1´: ´T_1´, ..., ´x_n´: ´T_n´): ´R´
}

Tuple Types

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

A tuple type ´(T_1, ..., T_n)´ where ´n \geq 2´ is sugar for the type ´T_1´ *: ... *: ´T_n´ *: scala.EmptyTuple, which is itself a series of nested infix types which are sugar for *:[´T_1´, *:[´T_2´, ... *:[´T_n´, scala.EmptyTuple]]]. The ´T_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 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 ´<:´. 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 ´T´ always has lower and upper bounds ´L´ and ´H´ such that ´L >: T´ and ´T <: H´. A concrete type ´T´ 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: ´>: L <: H´ denotes the set of types ´T´ such that ´L <: T´ and ´T <: 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 ´>: L <: 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 ´T´ is concrete and has an underlying type ´U´ such that ´T <: U´.

Type Constructors

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

Type Definitions

A type definition ´D´ 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 ´L´ and an upper bound ´H´, which are types. For type aliases, ´L = 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 [´\pm a_1 >: L_1 <: H_1´, ..., ´\pm a_n >: L_n <: H_n´] =>> ´U´ is a direct representation of a type constructor with ´n´ type parameters. When applied to ´n´ type arguments that conform to the specified bounds, it produces another type ´U´. Type lambdas are always concrete types.

The scope of a type parameter extends over the result type ´U´ 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 <:´ [´\pm a_1 >: L_1 <: H_1´, ..., ´\pm a_n >: L_n <: H_n´] =>> ´U´, then ´T´'s ´i´th type parameter bounds contain the bounds ´>: L_i <: H_i´, and its result type conforms to ´U´.

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.x´ referring to a term definition t has an underlying type ´U´. If ´p = \epsilon´ or ´p´ is a package ref, the underlying type ´U´ is the declared type of t and ´p.x´ is a stable type if an only if t is a val or object definition. Otherwise, the underlying type ´U´ and whether ´p.x´ is a stable type are determined by memberType(´p´, ´x´).

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

Type Designators

A type designator ´p.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 ´C´ 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.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 = \epsilon´ or ´p´ is a package ref, the underlying type definition is the declared type definition of T. Otherwise, it is determined by memberType(´p´, ´T´). A non-class type designator is concrete (resp. stable) if and only if its underlying type definition is an alias ´U´ and ´U´ is itself concrete (resp. stable).

Parameterized Types

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

A parameterized type ´T[T_1, ..., T_n]´ consists of a type constructor ´T´ and type arguments ´T_1, ..., T_n´ where ´n \geq 1´. The parameterized type is well-formed if

´T[T_1, ..., T_n]´ is a parameterized class type if and only if ´T´ 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[T_1, ..., T_n]´ be a parameterized type for a concrete type constructor. Then, applying a wildcard type argument ´? >: L <: H´ at the ´i´'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 ´C´.this denotes the this value of class ´C´ within ´C´.

This types often appear implicitly as the prefix of designator types referring to members of ´C´. 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 ´C´.this is the self type of ´C´.

Super Types

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

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

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 ´=> 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 ´T a´ attaches the annotation ´a´ to the type ´T´.

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 ´T { R }´ denotes the set of values that belong to ´T´ and also have a member conforming to the refinement ´R´.

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

As an exception to the last rule, a polymorphic method type refinement is allowed if ´T <:´ scala.PolyFunction and ´id´ is the name apply.

If the refinement ´R´ overrides no member of ´T´ 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 ´T´ 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´ => ´T´ } represents the same values as ´T´, while offering ´T´ 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´ => ´T´ { 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 ´<:´ { ´\alpha´ => ´T´ { def foo: ´\alpha´.X } }. We first unfold the recursive type, substituting ´z´ for ´\alpha´, resulting in z ´<:´ T { def foo: z.X }. Since the underlying type of ´z´ is ´Z´, we can resolve z.X to mean Option[Int], and then validate that z ´<:´ 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, ´S ｜ T´ and ´S ＆ 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 ´A´, ´B´ and ´C´, all of the following relationships hold:

If ´C´ is a co- or contravariant type constructor, ´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 ´T_1 ｜ ... ｜ T_n´ as the smallest intersection type of base class instances of ´T_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 ´A ｜ B´ is ´C[A ｜ B] ＆ D´

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 ´∃ \alpha : T´ represents a stable reference to unknown value of type ´T´. 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 ´(\mathit{Ps})U´, where ´(\mathit{Ps})´ is a sequence of parameter names and types ´(p_1:T_1, ..., p_n:T_n)´ for some ´n \geq 0´ and ´U´ is a (value or method) type. This type represents named methods that take arguments named ´p_1, ..., p_n´ of types ´T_1, ..., T_n´ and that return a result of type ´U´.

Method types associate to the right: ´(\mathit{Ps}_1)(\mathit{Ps}_2)U´ is treated as ´(\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 [´\mathit{tps}\,´]´T´ where [´\mathit{tps}\,´] is a type parameter section [´a_1´ >: ´L_1´ <: ´U_1, ..., a_n´ >: ´L_n´ <: ´U_n´] for some ´n \geq 0´ and ´T´ is a (value or method) type. This type represents named methods that take type arguments ´S_1, ..., S_n´ which conform to the lower bounds ´L_1, ..., L_n´ and the upper bounds ´U_1, ..., U_n´ and that yield results of type ´T´.

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(´T´, ´C´), where ´T´ is a proper type and ´C´ is a class identifier, computes the smallest type ´U´ of the form ´p.C´ or ´p.C´[´U_1, ..., U_n´] such that ´T <: 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(´T´, ´C´) as follows. For brevity, we write ´p.X´[´U_1, ..., U_n´] instead of ´p.X´ with ´n = 0´.

The definition above uses the following helper functions.

superType(´T´) computes the "next upper bound" of ´T´, 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[T_1, ..., T_n]´, ´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(´T_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(´T´, ´C´, ´p´), where ´T´ is a type or methodic type visible inside the class ´C´ and ´p´ is a stable type, rebases the type ´T´ "as seen from" the prefix ´p´. Essentially, it substitutes this-types and class type parameters in ´T´ to appropriate types visible from outside. Since T is visible inside ´C´, it can contain this-types and class type parameters of ´C´ itself as well as of all its enclosing classes. This-types of enclosing classes must be mapped to appropriate subprefixes of ´p´, while class type parameters must be mapped to appropriate concrete type arguments.

asSeenFrom(´T´, ´C´, ´p´) only makes sense if ´p´ has a base type for ´C´, i.e., if baseType(´p´, ´C´) is defined.

We define asSeenFrom(´T´, ´C´, ´p´) where baseType(´p´, ´C´) = ´q.C[U_1, ..., U_n]´ as follows:

For convenience, we generalize asSeenFrom to type definitions ´D´.

Member Type

The meta-function memberType(´T´, ´id´, ´p´), where ´T´ is a proper type, ´id´ is a term or type identifier, and ´p´ 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 ´p´. 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 ´M´ of a memberType is one of:

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

We define memberType(´T´, ´id´, ´p´) as follows:

We define the helper function mergeMemberType(´M_1´, ´M_2´) as:

Relations between types

We define the following relations between types.

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

Conformance

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

We define isSubPrefix(´p´, ´q´) where ´p´ and ´q´ are prefixes as:

We define matches(´S´, ´T´) where ´S´ and ´T´ are types or methodic types as:

Note that conformance in Scala is not transitive. Given two abstract types ´A´ and ´B´, and one abstract type ´C >: A <: B´ available on prefix ´p´, we have ´A <: p.C´ and ´C <: p.B´ but not necessarily ´A <: B´.

Least upper bounds and greatest lower bounds

The ´(<:)´ 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 =:= T´ if and only if both ´S <: T´ and ´T <: S´.

Weak Conformance

In some situations Scala uses a more general conformance relation. A type ´S´ weakly conforms to a type ´T´, written ´S <:_w T´, if ´S <: T´ or both ´S´ and ´T´ are primitive number types and ´S´ precedes ´T´ in the following ordering.

Byte  ´<:_w´ Short
Short ´<:_w´ Int
Char  ´<:_w´ Int
Int   ´<:_w´ Long
Long  ´<:_w´ Float
Float ´<:_w´ Double

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

Compatibility

A type ´T´ is compatible to a type ´U´ if ´T´ (or its corresponding function type) weakly conforms to ´U´ after applying eta-expansion. If ´T´ 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 ´T´ is realizable if and only if it is inhabited by non-null values. It is defined as:

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

Note: it is possible for baseType(´T´, ´C´) 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|´ for the erasure of type ´T´. 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)´ 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. ↩