Type Lambdas - More Details
Syntax
Type ::= ... | TypeParamClause ‘=>>’ Type
TypeParamClause ::= ‘[’ TypeParam {‘,’ TypeParam} ‘]’
TypeParam ::= {Annotation} (id [HkTypeParamClause] | ‘_’) TypeBounds
TypeBounds ::= [‘>:’ Type] [‘<:’ Type]
Type Checking
A type lambda such as [X] =>> F[X]
defines a function from types to types. The parameter(s) may carry bounds. If a parameter is bounded, as in [X >: L <: U] =>> F[X]
it is checked that arguments to the parameters conform to the bounds L
and U
. Only the upper bound U
can be F-bounded, i.e. X
can appear in it.
Subtyping Rules
Assume two type lambdas
type TL1 = [X >: L1 <: U1] =>> R1
type TL2 = [X >: L2 <: U2] =>> R2
Then TL1 <: TL2
, if
- the type interval
L2..U2
is contained in the type intervalL1..U1
(i.e.L1 <: L2
andU2 <: U1
), R1 <: R2
Here we have relied on alpha renaming to match the two bound types X
.
A partially applied type constructor such as List
is assumed to be equivalent to its eta expansion. I.e, List = [X] =>> List[X]
. This allows type constructors to be compared with type lambdas.
Relationship with Parameterized Type Definitions
A parameterized type definition
type T[X] = R
is regarded as a shorthand for an unparameterized definition with a type lambda as right-hand side:
type T = [X] =>> R
If the type definition carries +
or -
variance annotations, it is checked that the variance annotations are satisfied by the type lambda. For instance,
type F2[A, +B] = A => B
expands to
type F2 = [A, B] =>> A => B
and at the same time it is checked that the parameter B
appears covariantly in A => B
.
A parameterized abstract type
type T[X] >: L <: U
is regarded as shorthand for an unparameterized abstract type with type lambdas as bounds.
type T >: ([X] =>> L) <: ([X] =>> U)
However, if L
is Nothing
it is not parameterized, since Nothing
is treated as a bottom type for all kinds. For instance,
type T[X] <: X => X
is expanded to
type T >: Nothing <: ([X] =>> X => X)
instead of
type T >: ([X] =>> Nothing) <: ([X] =>> X => X)
The same expansions apply to type parameters. For instance,
[F[X] <: Coll[X]]
is treated as a shorthand for
[F >: Nothing <: [X] =>> Coll[X]]
Abstract types and opaque type aliases remember the variances they were created with. So the type
type F2[-A, +B]
is known to be contravariant in A
and covariant in B
and can be instantiated only with types that satisfy these constraints. Likewise
opaque type O[X] = List[X]
O
is known to be invariant (and not covariant, as its right-hand side would suggest). On the other hand, a transparent alias
type O2[X] = List[X]
would be treated as covariant, X
is used covariantly on its right-hand side.
Note: The decision to treat Nothing
as universal bottom type is provisional, and might be changed after further discussion.
Note: Scala 2 and 3 differ in that Scala 2 also treats Any
as universal top-type. This is not done in Scala 3. See also the discussion on kind polymorphism
Curried Type Parameters
The body of a type lambda can again be a type lambda. Example:
type TL = [X] =>> [Y] =>> (X, Y)
Currently, no special provision is made to infer type arguments to such curried type lambdas. This is left for future work.