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 interval L1..U1 (i.e. L1 <: L2 and U2 <: 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.