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 op
consists of an infix operator op
which gets applied to two type operands and .
The type is translated to the internal type application op
.
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 , all operators must have the same associativity. If they are all left-associative, the sequence is interpreted as , otherwise it is interpreted as .
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 represents the set of function values that take arguments of types and yield results of type . The case of exactly one argument type is a shorthand for . An argument type of the form represents a call-by-name parameter of type .
Function types associate to the right, e.g. is the same as .
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 -ary function type translates to the internal class type scala.Function[, ..., , ]
.
In particular is a shorthand for class type scala.Function[]
.
Such class types behave as if they were instances of the following trait:
trait Function_n[-T_1, ..., -T_n, +R]:
def apply(: T_1, ..., : 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 , can refer to the parameters , notably to form path-dependent types. It translates to the internal refined type
scala.Function_n[T_1, ..., T_n, S] {
def apply(: T_1, ..., : T_n): R
}
where is the least super type of that does not mention any of the .
Polymorphic function types are function types that take type arguments. Their result type must be a function type. In the concrete type , the types and can refer to the type parameters . It translates to the internal refined type
scala.PolyFunction {
def apply[a_1 >: L_1 <: H_1, ..., a_n >: L_1 <: H_1](: T_1, ..., : T_n): R
}
Tuple Types
SimpleType1 ::= ...
| ‘(’ TypesOrWildcards ‘)’
A tuple type where is sugar for the type *: ... *: *: scala.EmptyTuple
, which is itself a series of nested infix types which are sugar for *:[, *:[, ... *:[, scala.EmptyTuple]]]
.
The can be wildcard type arguments.
Notes:
()
is the type , and not*: scala.EmptyTuple
( cannot be a wildcard type argument in that case).()
is not a valid type (i.e. it is not desugared toscala.EmptyTuple
).
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:
- Create a fresh recursive this name .
- Replace every implicit or explicit reference to
this
in the refinement definitions by . - Create nested refined types, one for every refined definition.
- Unless was never actually used, wrap the result in a recursive type
{ => }
.
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 InfixType
s, 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 TypeCaseAppliedPattern
s.
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 .
If is not a ParameterizedType
, then use as the internal pattern.
Otherwise, is recursively converted into a TypeCasePattern
as follows:
- If is a
WildcardTypeArg
of the form? >: <:
, return aTypeCapture
of the form_ >: <:
. - If is a direct type designator
whose name starts with a lowercase and was not written using backticks, return a
TypeCapture
>: <:
where>: <:
is the declared type definition of.
- If is a
ParameterizedType
of the form[, ..., ]
:- Recursively convert each into a pattern .
- If is a
Type
for all , return . - Otherwise, return the
TypeCaseAppliedPattern
[, ..., ]
.
- Otherwise, return .
This conversion ensures that every TypeCaseAppliedPattern
recursively contains at least one TypeCapture
.
Moreover, at the top level, the pattern is never a TypeCapture
: all TypeCapture
s 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.
- Proper types are the types of terms.
- Type constructors are type-level functions from types to types.
- Poly-kinded types can take various kinds.
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 always has lower and upper bounds and such that and . A concrete type is considered to have itself as both lower and upper bound.
The kind of a type is indicated by its (transitive) upper bound:
- A type
scala.Any
is a proper type. - A type
where is a type lambda (of the form
[, ..., ] =>>
) is a type constructor. - Other types are poly-kinded; they are neither proper types nor type constructors.
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: denotes the set of types such that and . 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 .
By convention, we can omit either of both bounds in writing.
- When omitted, the lower bound is
Nothing
. - When omitted, the higher bound is
Any
(notAnyKind
).
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
- designator types referencing a stable term,
- this types,
- super types,
- literal types,
- recursive this types, and
- skolem types.
Every stable type is concrete and has an underlying type such that .
Type Constructors
To each type constructor corresponds an inferred type parameter clause which is computed as follows:
- For a type lambda, its type parameter clause (including variance annotations).
- For a polymorphic class type, the type parameter clause of the referenced class definition.
- For a non-class type designator, the inferred clause of its upper bound.
Type Definitions
A type definition represents the right-hand-side of a type
member definition or the bounds of a type parameter.
It is either:
- a type alias of the form , or
- an abstract type definition with bounds .
All type definitions have a lower bound and an upper bound , which are types. For type aliases, .
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 [, ..., ] =>>
is a direct representation of a type constructor with type parameters.
When applied to type arguments that conform to the specified bounds, it produces another type .
Type lambdas are always concrete types.
The scope of a type parameter extends over the result type 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 [, ..., ] =>>
, then 's th type parameter bounds contain the bounds , and its result type conforms to .
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 are called direct designators. They refer to local definitions available in the scope:
- Local
type
,object
,val
,lazy val
,var
ordef
definitions - Term or type parameters
The id
s 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 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:
- Top-level definitions, including top-level classes, have a package ref prefix
- Class member definitions and refinements have a type prefix
Term Designators
A term designator referring to a term definition t
has an underlying type .
If or is a package ref, the underlying type is the declared type of t
and is a stable type if an only if t
is a val
or object
definition.
Otherwise, the underlying type and whether is a stable type are determined by memberType
(, )
.
All term designators are concrete types.
If scala.Null
, the term designator denotes the set of values consisting of null
and the value denoted by , i.e., the value for which t eq v
.
Otherwise, the designator denotes the singleton set only containing .
Type Designators
A type designator 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 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 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 or is a package ref, the underlying type definition is the declared type definition of T
.
Otherwise, it is determined by memberType
(, )
.
A non-class type designator is concrete (resp. stable) if and only if its underlying type definition is an alias and is itself concrete (resp. stable).
Parameterized Types
ParameterizedType ::= Type ‘[‘ TypeArgs ‘]‘
TypeArgs ::= TypeArg {‘,‘ TypeArg}
TypeArg ::= Type
| WilcardTypeArg
WildcardTypeArg ::= ‘?‘ TypeBounds
A parameterized type consists of a type constructor and type arguments where . The parameterized type is well-formed if
- is a type constructor which takes type parameters , i.e., it must conform to a type lambda of the form , and
- if is an abstract type constructor, none of the type arguments is a wildcard type argument, and
- each type argument conforms to its bounds, i.e., given the substitution , for each type :
- if is a type and , or
- is a wildcard type argument and and .
is a parameterized class type if and only if 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 be a parameterized type for a concrete type constructor. Then, applying a wildcard type argument at the 'th position obeys the following equivalences:
- If the type parameter is declared covariant, then .
- If the type parameter is declared contravariant, then .
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 .this
denotes the this
value of class within .
This types often appear implicitly as the prefix of designator types referring to members of . 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 .this
is the self type of .
Super Types
SuperType ::= classid ‘.‘ ‘super‘ ‘[‘ classid ‘]‘
A super type .super[]
denotes the this
value of class C
within C
, but "widened" to only see members coming from a parent class or trait .
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 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 attaches the annotation to the type .
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 denotes the set of values that belong to and also have a member conforming to the refinement .
The refined type is well-formed if:
- is a proper type, and
- if is a term (
def
orval
) refinement, the refined type is a proper type, and - if overrides a member of , the usual rules for overriding apply, and
- if is a
def
refinement with a polymorphic method type, then overrides a member definition of .
As an exception to the last rule, a polymorphic method type refinement is allowed if scala.PolyFunction
and is the name apply
.
If the refinement overrides no member of 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 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:
U <: T { def foo: Int }
U <: T { def fooPoly[A](x: A): A }
U <: (T { def foo: Int }) { def fooPoly[A](x: A): A }
(we can chain refined types to refine multiple members)V <: T { type X <: Some[Any] }
V <: T { type X >: Some[Nothing] }
V <: T { type X = Some[Int] }
V <: T { def bar: Any }
(a structural refinement)
The following refined types are not well-formed:
T { def barPoly[A](x: A): A }
(structural refinement for a polymorphic method type)T { type X <: List[Any] }
(does not satisfy overriding rules)List { def head: Int }
(the parent typeList
is not a proper type)T { def foo: List }
(the refined typeList
is not a proper type)T { def foo: T.this.X }
(T.this
is not allowed outside the body ofT
)
Recursive Types
RecursiveType ::= ‘{‘ recid ‘=>‘ Type ‘}‘
RecursiveThis ::= recid ‘.‘ ‘this‘
A recursive type of the form { => }
represents the same values as , while offering access to its recursive this type .
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 , distinct from any other recursive type in the system.
Recursive types can be unfolded during subtyping as needed, replacing references to its 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 { => { def foo: .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 { => { def foo: .X } }
.
We first unfold the recursive type, substituting for , resulting in z T { def foo: z.X }
.
Since the underlying type of is , 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, and refer to the underlying core concepts of union and intersection types, respectively.
- The type represents the set of values that are represented by either or .
- The type represents the set of values that are represented by both and .
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 , and , all of the following relationships hold:
- ,
- ,
- ,
- , and
- .
If is a co- or contravariant type constructor, can be simplified using the following rules:
- If is covariant,
- If is contravariant,
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:
- When is covariant, we can derive .
- When is contravariant, we can derive .
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 as the smallest intersection type of base class instances of . 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 is
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.
Legal patterns
A TypeCasePattern
is a legal pattern if and only if one of the following is true:
- It is a
Type
, or - It is a
TypeCaseAppliedPattern
of the form[, ..., ]
where is a "pattern-legal type constructor" and for each , either:- is a
TypeCapture
, or - is a
Type
, or - is a
TypeCaseAppliedPattern
, the type constructor is covariant in its th type parameter, and is recursively a legal pattern.
- is a
A type is a "pattern-legal type constructor" if one of the following is true:
- It is a class type constructor, or
- It is the
scala.compiletime.ops.int.S
type constructor, or - It is an abstract type constructor, or
- It is a type lambda with a refined result type of the form
[ >: <: ] =>> { type = }
where:- contains no occurrence of ,
- there exists a type member in , and
- the bounds
>: <:
are not any more restrictive than those of in , i.e.,<: <:
.
- It is a type lambda of the form
[, ..., ] =>>
such that:- Its bounds contain all possible values of its arguments, and
- When applied to the type arguments, it beta-reduces to a new legal
MatchTypeAppliedPattern
that contains exactly one instance of every type capture present in the type arguments.
- It is a concrete type designator with underlying type definition
=
and is recursively a "pattern-legal type constructor".
Examples of legal patterns
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:
- Compute instantiations for the type captures
ts'
, and check that they are specific enough. - If successful, check that
X <:< [ts := ts']P
. - 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
:
- If
P
is aTypeWithoutCapture
:- Do nothing (always succeed).
- If
P
is aWildcardCapture
ti = _
:- If
X
is of the form_ >: L <: H
, instantiateti := H
(anything betweenL
andH
would work here), - Otherwise, instantiate
ti := X
.
- If
- If
P
is aTypeCapture
ti
:- If
X
is of the form_ >: L <: H
,- If
scrutIsWidenedAbstract
istrue
, fail as not specific. - Otherwise, if
variance = 1
, instantiateti := H
. - Otherwise, if
variance = -1
, instantiateti := L
. - Otherwise, fail as not specific.
- If
- Otherwise, if
variance = 0
orscrutIsWidenedAbstract
isfalse
, instantiateti := X
. - Otherwise, fail as not specific.
- If
- If
P
is aMatchTypeAppliedPattern
of the formT[Qs]
:- Assert:
variance = 1
(from the definition of legal patterns). - If
T
is a class type constructor of the formp.C
:- If
baseType(X, C)
is not defined, fail as not matching. - Otherwise, it is of the form
q.C[Us]
. - If
p =:= q
is false, fail as not matching. - Let
innerScrutIsWidenedAbstract
be true if eitherscrutIsWidenedAbstract
orX
is not a concrete type. - For each pair of
(Ui, Qi)
, computematchPattern(Ui, Qi, vi, innerScrutIsWidenedAbstract)
wherevi
is the variance of thei
th type parameter ofT
.
- If
- If
T
isscala.compiletime.ops.int.S
:- If
n = natValue(X)
is undefined orn <= 0
, fail as not matching. - Otherwise, compute
matchPattern(n - 1, Q1, 1, scrutIsWidenedAbstract)
.
- If
- If
T
is an abstract type constructor:- If
X
is not of the formF[Us]
orF =:= T
is false, fail as not matching. - Otherwise, for each pair of
(Ui, Qi)
, computematchPattern(Ui, Qi, vi, scrutIsWidenedAbstract)
wherevi
is the variance of thei
th type parameter ofT
.
- If
- If
T
is a refined type of the formBase { type Y = ti }
:- Let
q
beX
ifX
is a stable type, or the skolem type∃α:X
otherwise. - If
q
does not have a type memberY
, fail as not matching (that implies thatX <:< Base
is false, becauseBase
must have a type memberY
for the pattern to be legal). - If
q
is not a skolem type:- Compute
matchPattern(ti, q.Y, 0, scrutIsWidenedAbstract)
.
- Compute
- Otherwise, if
q.Y
is a type alias with underlying type definition= U
:- Let
U'
be the result of perform type avoidance onU
to remove references toq
. - If successful, compute
matchPattern(ti, U', 0, scrutIsWidenedAbstract)
. - Otherwise, fail as not specific.
- Let
- Let
- If
T
is a concrete type alias to a type lambda:- Let
P'
be the beta-reduction ofP
. - Compute
matchPattern(P', X, variance, scrutIsWidenedAbstract)
.
- Let
- Assert:
Disjointness
A scrutinee is provably disjoint from a pattern iff it is provably disjoint from the type obtained by replacing every type capture in by a wildcard type argument with the same bounds.
We note to say that and are provably disjoint. Intuitively, that notion is based on the following properties of the Scala language:
- Single inheritance of classes
- Final classes cannot be extended
- Sealed traits have a known set of direct children
- Constant types with distinct values are nonintersecting
- Singleton paths to distinct
enum
case values are nonintersecting
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:
Nothing
AnyKind
- a possibly parameterized class type, where and are arbitrary types (not just simple types)
- a literal type
- where
C
is anenum
class andx
is one of its valuecase
s - where and are both simple types
- where and are both simple types
=>>
where is a simple type
We define 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:
- if is a simple type
- if is a stable type but not a simple type and its underlying type is
- if is a non-class type designator with upper bound
- if is a polymorphic class type designator, where is its eta-expansion
- if is a match type that reduces to
- if is a match type that does not reduce and is its upper bound
- where
Y
is the beta-reduction of if is a type lambda - if is neither a type lambda nor a class type designator
{ }
{ => }
=>> =>>
The following properties hold about (we have paper proofs for those):
- for all type .
- If , and the subtyping derivation does not use the "lower-bound rule" of anywhere, then .
The "lower-bound rule" states that if and is a non-class type designator and where is the lower bound of the underlying type definition of ". 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:
- if
baseClasses
and isfinal
- if
baseClasses
and isfinal
- if there exists
class
esbaseClasses
andbaseClasses
such thatbaseClasses
andbaseClasses
. - if is
sealed
without anonymous child and for all direct children of - if is
sealed
without anonymous child and for all direct children of
We can now define for types.
For arbitrary types and , we define as .
Two simple types and are provably disjoint if there is a finite derivation tree for using the following rules. Most rules go by pair, which makes the whole relation symmetric:
Nothing
is disjoint from everything (including itself):Nothing
Nothing
- A union type is disjoint from another type if both of its parts are disjoint from that type:
- if and
- if and
- An intersection type is disjoint from another type if at least one of its parts is disjoint from that type:
- if or
- if or
- A type lambda is disjoint from any other type that is not a type lambda with the same number of parameters:
=>>
=>>
=>>
=>>
=>>
=>>
=>> =>>
if
- Two type lambdas with the same number of type parameters are disjoint if their result types are disjoint:
=>> =>>
if
- An
enum
value case is disjoint from any otherenum
value case (identified by either not being in the sameenum
class, or having a different name):- if or
- Two literal types are disjoint if they are different:
- if
- An
enum
value case is always disjoint from a literal type: - An
enum
value case or a constant is disjoint from a class type if it does not extend that class (because it's essentially final):- if
baseType
is not defined - if
baseType
is not defined - if
baseType
is not defined - if
baseType
is not defined
- if
- Two class types are disjoint if the classes themselves are disjoint, or if there exists a common super type with conflicting type arguments.
- if
- if there exists a class such that
baseType
andbaseType
and there exists a pair such that- and it is in covariant position and there exists a field of that type parameter in , or
- and it is in invariant position, and:
- there exists a field of that type parameter in , or
- cannot be instantiated to
Nothing
, or - cannot be instantiated to
Nothing
.
It is worth noting that this definition disregards prefixes entirely. and are never provably disjoint, even if could be proven disjoint from . It also disregards type members.
We have a proof sketch of the following property for :
- If and , then .
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 and , then .
Reduction
The result of reducing match { case => case => }
can be a type, undefined, or a compile error.
For , it is specified as:
- If matches with type capture instantiations
:
- If , do not reduce.
- Otherwise, reduce as
.
- Otherwise,
- If , the result of reducing
match { case => case => }
(i.e., proceed with subsequent cases). - Otherwise, do not reduce.
- If , the result of reducing
The reduction of an "empty" match type 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 (val
s, var
s and def
s).
They are exclusively used temporarily during subtyping derivations.
Skolem types are stable types. A skolem type of the form represents a stable reference to unknown value of type . The identifier 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 , 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 , where is a sequence of parameter names and types for some and is a (value or method) type. This type represents named methods that take arguments named of types and that return a result of type .
Method types associate to the right: is treated as .
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 []
where []
is a type parameter section [ >: <: >: <: ]
for some and is a (value or method) type.
This type represents named methods that take type arguments which conform to the lower bounds
and the upper bounds
and that yield results of type .
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.
baseType(, )
: computes the smallest type of the form.[]
such that .asSeenFrom(, , )
: rebases the type visible inside the class "as seen from" the prefix .memberType(, )
: finds a member of a type (T.id
) and computes its underlying type or bounds.
These meta-functions are mutually recursive.
Base Type
The meta-function baseType(, )
, where is a proper type and is a class identifier, computes the smallest type of the form or
[]
such that .
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(, )
as follows.
For brevity, we write []
instead of with .
baseType([], )
baseType([], )
with≠
if is defined where- is declared as
extends
meet(baseType(, )
for all such thatbaseType(, )
is defined)
if or if is a package ref; otherwise,
asSeenFrom(, , )
(in that case, is a stable type and must be declared inside another class )the substitution of the declared type parameters of by the actual type arguments
- is declared as
baseType(, ) meetbaseType(, ), baseType(, )
baseType(, ) joinbaseType(, ), baseType(, )
baseType(, ) baseType(superType(), )
ifsuperType()
is defined
The definition above uses the following helper functions.
superType()
computes the "next upper bound" of , if it exists:
superType()
where is a stable type is its underlying typesuperType()
where is a non-class type designator is the upper bound of its underlying type definitionsuperType( =>> )
is(i.e., the beta-reduction of the type lambda redex)
superType()
issuperType()
ifsuperType()
is defined
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(, )
computes an intersection of two (parameterized) class types for the same class, and join
computes a union:
- if
is false, then it is not defined
- otherwise, let for be:
- for
meet
(resp. forjoin
) if the th type parameter of is covariant - for
meet
(resp. forjoin
) if the th type parameter of is contravariant - if and the th type parameter of is invariant
- not defined otherwise
- for
- if any of the are not defined, the result is not defined
- otherwise, the result is
We generalize meet()
for a sequence as:
- not defined for
- if
meet(meet(), )
ifmeet()
is defined- not defined otherwise
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:
baseType(List[Int], List) = List[Int]
baseType(List[Int], Iterable) = Iterable[Int]
baseType(List[A] & Iterable[B], Iterable) = meet(Iterable[A], Iterable[B]) = Iterable[A & B]
baseType(List[A] & Foo, Iterable) = Iterable[A]
(becausebaseType(Foo, Iterable)
is not defined)baseType(Int, Iterable)
is not definedbaseType(Map[Int, String], Iterable) = Iterable[(Int, String)]
baseType(Map[Int, String] & Map[String, String], Map)
is not defined (becauseK
is invariant)
As Seen From
The meta-function asSeenFrom(, , )
, where is a type or methodic type visible inside the class and is a stable type, rebases the type "as seen from" the prefix .
Essentially, it substitutes this-types and class type parameters in to appropriate types visible from outside.
Since T
is visible inside , it can contain this-types and class type parameters of itself as well as of all its enclosing classes.
This-types of enclosing classes must be mapped to appropriate subprefixes of , while class type parameters must be mapped to appropriate concrete type arguments.
asSeenFrom(, , )
only makes sense if has a base type for , i.e., if baseType(, )
is defined.
We define asSeenFrom(, , )
where baseType(, ) =
as follows:
- If is a reference to the th class type parameter of some class :
- If
baseType(, )
is defined, then - Otherwise, if or is a package ref, then
- Otherwise, is a type, must be defined in another class and
baseType(, )
must be defined, thenasSeenFrom(, , )
- If
- Otherwise, if is a this-type
.this
:- If is a subclass of and
baseType(, )
is defined, then (this is always the case when ) - Otherwise, if or is a package ref, then
- Otherwise, is a type, must be defined in another class and
baseType(, )
must be defined, thenasSeenFrom(, , )
- If is a subclass of and
- Otherwise, where each if of its type components is mapped to
asSeenFrom(, , )
.
For convenience, we generalize asSeenFrom
to type definitions .
- If is an alias , then
asSeenFrom(, , ) = asSeenFrom(, , )
. - If is an abstract type definition with bounds , then
asSeenFrom(, , ) = asSeenFrom(, , ) asSeenFrom(, , )
.
Member Type
The meta-function memberType(, , )
, where is a proper type, is a term or type identifier, and 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 .
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 of a memberType
is one of:
- undefined,
- a term result with underlying type or methodic type and a stable flag,
- a class result with class , or
- a type result with underlying type definition .
As short-hand, we define memberType(, )
to be the same as memberType(, , )
when is a stable type.
We define memberType(, , )
as follows:
- If is a possibly parameterized class type of the form (with ):
- Let be the class member of with name .
- If is not defined, the result is undefined.
- If is a class definition, the result is a class result with class .
- If is a term definition in class with declared type , the result is a term result with underlying type
asSeenFrom
(, , )
and stable flag true if and only if is stable. - If is a type member definition in class , the result is a type result with underlying type definition
asSeenFrom
(, , )
where is defined as follows:- If is an opaque type alias member definition with declared definition , then
- is if
this
or if we are computingmemberType
in a transparent mode, - is otherwise.
- is if
- is the declared type definition of otherwise.
- If is an opaque type alias member definition with declared definition , then
- If is another monomorphic type designator of the form :
- Let be
memberType(, )
- Let be the upper bound of
- The result is
memberType(, , )
- Let be
- If is another parameterized type designator of the form (with ):
- Let be
memberType(, )
- Let be the upper bound of
- The result is
memberType(, , )
- Let be
- If is a parameterized type lambda of the form
=>>
:- The result is
memberType(, , )
, i.e., we beta-reduce the type redex.
- The result is
- If is a refined type of the form
{ }
:- Let be the result of
memberType(, , )
. - If the name of the refinement is not , let be undefined.
- Otherwise, let be the type or type definition of the refinement , as well as whether it is stable.
- The result is
mergeMemberType(, )
.
- Let be the result of
- If is a union type of the form :
- Let be the join of .
- The result is
memberType(, , )
.
- If is an intersection type of the form :
- Let be the result of
memberType(, , )
. - Let be the result of
memberType(, , )
. - The result is
mergeMemberType(, )
.
- Let be the result of
- If is a recursive type of the form
{ => }
:- The result is
memberType(, , )
.
- The result is
- If is a stable type:
- Let be the underlying type of .
- The result is
memberType(, , )
.
- Otherwise, the result is undefined.
We define the helper function mergeMemberType(, )
as:
- If either or is undefined, the result is the other one.
- Otherwise, if either or is a class result, the result is that one.
- Otherwise, and must either both be term results or both be type results.
- If they are term results with underlying types and and stable flags and , the result is a term result whose underlying type is
meet(, )
and whose stable flag is . - If they are type results with underlying type definitions and , the result is a type result whose underlying type definition is
intersect(, )
.
- If they are term results with underlying types and and stable flags and , the result is a term result whose underlying type is
Relations between types
We define the following relations between types.
Name | Symbolically | Interpretation |
---|---|---|
Conformance | Type conforms to ("is a subtype of") type . | |
Equivalence | and conform to each other. | |
Weak Conformance | Augments conformance for primitive numeric types. | |
Compatibility | Type conforms to type after conversions. |
Conformance
The conformance relation is the smallest relation such that is true if any of the following conditions hold. Note that the conditions are not all mutually exclusive.
- (i.e., conformance is reflexive by definition).
- is
Nothing
. - is
AnyKind
. - is a stable type with underlying type and .
- and are term designators and
isSubPrefix(, )
.
- and are possibly parameterized type designators with and:
isSubPrefix(, )
, and- it is not the case that and are class type designators for different classes, and
- for each :
- the th type parameter of is covariant and 3, or
- the th type parameter of is contravariant and 3, or
- the th type parameter of is invariant and:
- and are types and , or
- is a type and is a wildcard type argument of the form and and , or
- is a wildcard type argument of the form and is a wildcard type argument of the form and and (i.e., the "interval" is contained in the "interval").
- with and
baseType(, )
is defined andbaseType(, )
. - and is non-class type designator and where is the upper bound of the underlying type definition of .
- and
.this
and is the hidden class of anobject
and:- or is a package ref, or
isSubPrefix(, .this)
where is the enclosing class of .
.this
and and is the hidden class of anobject
and:- either or is a package ref, or
isSubPrefix(.this, )
where is the enclosing class of .
- and and .
- and either or .
- and and .
- and either or .
@a
and .@a
and (i.e., annotations can be dropped).- and is a non-class type designator and where is the lower bound of the underlying type definition of .
- and is a non-class type designator and where is the upper bound of the underlying type definition of .
=>>
and=>>
, and given :- , and
- for each :
- the variance of conforms to the variance of ( conforms to and , conforms to and , and conforms to ), and
- is contained in (i.e., and ).
- and
=>>
and is a type constructor with type parameters and:=>>
where the are copies of the type parameters of (i.e., we can eta-expand to compare it to a type lambda).
{ }
and and, given if is a stable type and otherwise:type
andmemberType(, )
is a class result for and and , ortype
andmemberType(, )
is a type result with bounds and and , orval
andmemberType(, )
is a stable term result with type and , ordef
andmemberType(, )
is a term result with type and is a type and , ordef
andmemberType(, )
is a term result with methodic type and is a methodic type andmatches(, )
.
{ }
and .{ => }
and{ => }
and .{ => }
and is a proper type but not a recursive type and where:- is if is a stable type and otherwise, and
- is the result of replacing any top-level recursive type
{ => }
in with (TODO specify this better).
match <: { ... }
ifmatch ...
reduces to andmatch <: { ... }
ifmatch ...
reduces to andmatch <: { ... }
ifmatch <: { case => ; ...; case => } match <: { case => ; ...; => }
if and for each and for each=>
and=>
and .scala.Null
and:- with and does not derive from
scala.AnyVal
and is not the hidden class of anobject
, or - is a term designator with underlying type and
scala.Null
, or { }
andscala.Null
, or{ => }
andscala.Null
.
- with and does not derive from
- is a stable type and is a term designator with underlying type and is a stable type and .
{ }
and .{ => }
and .scala.Tuple
with , and*: ... *: *: scala.EmptyTuple
.
We define isSubPrefix(, )
where and are prefixes as:
- If both and are types, then .
- Otherwise, (for empty prefixes and package refs).
We define matches(, )
where and are types or methodic types as:
- If and are types, then .
- If and are method types and , then for each and
matches(, )
, where . - If and are poly types and , then and for each and
matches(, )
, where .
Note that conformance in Scala is not transitive.
Given two abstract types and , and one abstract type
available on prefix , we have and but not necessarily .
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.
- the least upper bound of
A
andB
is the smallest typeL
such thatA
<:L
andB
<:L
. - the greatest lower bound of
A
andB
is the largest typeG
such thatG
<:A
andG
<:B
.
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.
if and only if both and .
Weak Conformance
In some situations Scala uses a more general conformance relation. A type weakly conforms to a type , written , if or both and are primitive number types and precedes in the following ordering.
Byte Short
Short Int
Char Int
Int Long
Long Float
Float Double
A weak least upper bound is a least upper bound with respect to weak conformance.
Compatibility
A type is compatible to a type if (or its corresponding function type) weakly conforms to after applying eta-expansion. If 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:
- dropping by-name modifiers: if is of the shape
(and is not),
;
- SAM conversion: if corresponds to a function type, and declares a single abstract method whose type corresponds to the function type ,
.
- implicit conversion: there's an implicit conversion from to in scope;
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:
Int => String
is compatible toToString
-- when expecting a value of typeToString
, you may pass a function literal fromInt
toString
, as it will be SAM-converted to said function;ToString
is not compatible toInt => String
-- when expecting a function fromInt
toString
, you may not pass aToString
.
Realizability
A type is realizable if and only if it is inhabited by non-null values. It is defined as:
- A term designator with underlying type is realizable if is or a package ref or a realizable type and
memberType(, )
has the stable flag, or- the type returned by
memberType(, )
is realizable.
- A stable type that is not a term designator is realizable.
- Another type is realizable if
- is concrete, and
- has good bounds.
A concrete type has good bounds if all of the following apply:
- all its non-class type members have good bounds, i.e., their bounds and are such that ,
- all its type refinements have good bounds, and
- for all base classes of :
baseType(, )
is defined with some result , and- for all , is a real type or (when it is a wildcard type argument) it has good bounds.
Note: it is possible for baseType(, )
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 for the erasure of type .
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 erasure of
AnyKind
isObject
. - The erasure of a non-class type designator is the erasure of its underlying upper bound.
- The erasure of a term designator is the erasure of its underlying type.
- The erasure of the parameterized type
scala.Array
isscala.Array
. - The erasure of every other parameterized type is .
- The erasure of a stable type
is the erasure of the underlying type of .
- The erasure of a by-name type
=>
isscala.Function0
. - The erasure of an annotated type is .
- The erasure of a refined type
{ }
is . - The erasure of a recursive type
{ => }
and the associated recursive this type is . - The erasure of a union type is the erased least upper bound (elub) of the erasures of and .
- The erasure of an intersection type is the eglb (erased greatest lower bound) of the erasures of and .
The erased LUB is computed as follows:
- if both argument are arrays of objects, an array of the erased LUB of the element types
- if both arguments are arrays of same primitives, an array of this primitive
- if one argument is array of primitives and the other is array of objects,
Object
- if one argument is an array,
Object
- otherwise a common superclass or trait S of the argument classes, with the following two properties:
- S is minimal: no other common superclass or trait derives from S, and
- S is last: in the linearization of the first argument type there are no minimal common superclasses or traits that come after S. The reason to pick last is that we prefer classes over traits that way, which leads to more predictable bytecode and (?) faster dynamic dispatch.
The rules for 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
-
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. ↩
-
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. ↩
-
In these cases, if
T_i
and/orU_i
are wildcard type arguments, the simplification rules for parameterized types allow to reduce them to real types. ↩