Scala 3/Internals/Higher-Kinded Types in Dotty

Higher-Kinded Types in Dotty

Edit this page on GitHub

Higher-Kinded Types in Dotty V2

This note outlines how we intend to represent higher-kinded types in Dotty. The principal idea is to collapse the four previously disparate features of refinements, type parameters, existentials and higher-kinded types into just one: refinements of type members. All other features will be encoded using these refinements.

The complexity of type systems tends to grow exponentially with the number of independent features, because there are an exponential number of possible feature interactions. Consequently, a reduction from 4 to 1 fundamental features achieves a dramatic reduction of complexity. It also adds some nice usablilty improvements, notably in the area of partial type application.

This is a second version of the scheme which differs in a key aspect from the first one: Following Adriaan's idea, we use traits with type members to model type lambdas and type applications. This is both more general and more robust than the intersections with type constructor traits that we had in the first version.

The duality

The core idea: A parameterized class such as

class Map[K, V]

is treated as equivalent to a type with type members:

class Map { type Map$K; type Map$V }

The type members are name-mangled (i.e. Map$K) so that they do not conflict with other members or parameters named K or V.

A type-instance such as Map[String, Int] would then be treated as equivalent to:

Map { type Map$K = String; type Map$V = Int }

Named type parameters

Type parameters can have unmangled names. This is achieved by adding the type keyword to a type parameter declaration, analogous to how val indicates a named field. For instance,

class Map[type K, type V]

is treated as equivalent to

class Map { type K; type V }

The parameters are made visible as fields.

Wildcards

A wildcard type such as Map[_, Int] is equivalent to:

Map { type Map$V = Int }

I.e. _'s omit parameters from being instantiated. Wildcard arguments can have bounds. E.g.

Map[_ <: AnyRef, Int]

is equivalent to:

Map { type Map$K <: AnyRef; type Map$V = Int }

Type parameters in the encodings

The notion of type parameters makes sense even for encoded types, which do not contain parameter lists in their syntax. Specifically, the type parameters of a type are a sequence of type fields that correspond to parameters in the unencoded type. They are determined as follows.

  • The type parameters of a class or trait type are those parameter fields declared in the class that are not yet instantiated, in the order they are given. Type parameter fields of parents are not considered.
  • The type parameters of an abstract type are the type parameters of its upper bound.
  • The type parameters of an alias type are the type parameters of its right hand side.
  • The type parameters of every other type is the empty sequence.

Partial applications

The definition of type parameters in the previous section leads to a simple model of partial applications. Consider for instance:

type Histogram = Map[_, Int]

Histogram is a higher-kinded type that still has one type parameter. Histogram[String] would be a possible type instance, and it would be equivalent to Map[String, Int].

Modelling polymorphic type declarations

The partial application scheme gives us a new -- and quite elegant -- way to do certain higher-kinded types. But how do we interprete the poymorphic types that exist in current Scala?

More concretely, current Scala allows us to write parameterized type definitions, abstract types, and type parameters. In the new scheme, only classes (and traits) can have parameters and these are treated as equivalent to type members. Type aliases and abstract types do not allow the definition of parameterized types so we have to interprete polymorphic type aliases and abstract types specially.

Modelling polymorphic type aliases: simple case

A polymorphic type alias such as:

type Pair[T] = Tuple2[T, T]

where Tuple2 is declared as

class Tuple2[T1, T2] ...

is expanded to a monomorphic type alias like this:

type Pair = Tuple2 { type Tuple2$T2 = Tuple2$T1 }

More generally, each type parameter of the left-hand side must appear as a type member of the right hand side type. Type members must appear in the same order as their corresponding type parameters. References to the type parameter are then translated to references to the type member. The type member itself is left uninstantiated.

This technique can expand most polymorphic type aliases appearing in Scala codebases but not all of them. For instance, the following alias cannot be expanded, because the parameter type T is not a type member of the right-hand side List[List[T]].

type List2[T] = List[List[T]]

We scanned the Scala standard library for occurrences of polymorphic type aliases and determined that only two occurrences could not be expanded. In io/Codec.scala:

type Configure[T] = (T => T, Boolean)

And in collection/immutable/HashMap.scala:

private type MergeFunction[A1, B1] = ((A1, B1), (A1, B1)) => (A1, B1)

For these cases, we use a fall-back scheme that models a parameterized alias as a Lambda type.

Modelling polymorphic type aliases: general case

A polymorphic type alias such as:

type List2D[T] = List[List[T]]

is represented as a monomorphic type alias of a type lambda. Here's the expanded version of the definition above:

type List2D = Lambda$I { type Apply = List[List[$hkArg$0]] }

Here, Lambda$I is a standard trait defined as follows:

trait Lambda$I[type $hkArg$0] { type +Apply }

The I suffix of the Lambda trait indicates that it has one invariant type parameter (named $hkArg$0). Other suffixes are P for covariant type parameters, and N for contravariant type parameters. Lambda traits can have more than one type parameter. For instance, here is a trait with contravariant and covariant type parameters:

trait Lambda$NP[type -$hkArg$0, +$hkArg$1] { type +Apply } extends Lambda$IP with Lambda$NI

Aside: the + prefix in front of Apply indicates that Apply is a covariant type field. Dotty admits variance annotations on type members.

The definition of Lambda$NP shows that Lambda traits form a subtyping hierarchy: Traits which have covariant or contravariant type parameters are subtypes of traits which don't. The supertraits of Lambda$NP would themselves be written as follows.

trait Lambda$IP[type $hkArg$0, +$hkArg$1] { type +Apply } extends Lambda$II
trait Lambda$NI[type -$hkArg$0, $hkArg$1] { type +Apply } extends Lambda$II
trait Lambda$II[type $hkArg$0, $hkArg$1] { type +Apply }

Lambda traits are special in that they influence how type applications are expanded: If the standard type application T[X1, ..., Xn] leads to a subtype S of a type instance

LambdaXYZ { type Arg1 = T1; ...; type ArgN = Tn; type Apply ... }

where all argument fields Arg1, ..., ArgN are concretely defined and the definition of the Apply field may be either abstract or concrete, then the application is further expanded to S # Apply.

For instance, the type instance List2D[String] would be expanded to

Lambda$I { type $hkArg$0 = String; type Apply = List[List[String]] } # Apply

which in turn simplifies to List[List[String]].

2nd Example: Consider the two aliases

type RMap[K, V] = Map[V, K]
type RRMap[K, V] = RMap[V, K]

These expand as follows:

type RMap  = Lambda$II { self1 => type Apply = Map[self1.$hkArg$1, self1.$hkArg$0] }
type RRMap = Lambda$II { self2 => type Apply = RMap[self2.$hkArg$1, self2.$hkArg$0] }

Substituting the definition of RMap and expanding the type application gives:

type RRMap = Lambda$II { self2 => type Apply =
               Lambda$II { self1 => type Apply = Map[self1.$hkArg$1, self1.$hkArg$0] }
                 { type $hkArg$0 = self2.$hkArg$1; type $hkArg$1 = self2.$hkArg$0 } # Apply }

Substituting the definitions for self1.$hkArg${1,2} gives:

type RRMap = Lambda$II { self2 => type Apply =
               Lambda$II { self1 => type Apply = Map[self2.$hkArg$0, self2.$hkArg$1] }
                  { type $hkArg$0 = self2.$hkArg$1; type $hkArg$1 = self2.$hkArg$0 } # Apply }

Simplifiying the # Apply selection gives:

type RRMap = Lambda$II { self2 => type Apply = Map[self2.$hkArg$0, self2.$hkArg$1] }

This can be regarded as the eta-expanded version of Map. It has the same expansion as

type IMap[K, V] = Map[K, V]

Modelling higher-kinded types

The encoding of higher-kinded types uses again the Lambda traits to represent type constructors. Consider the higher-kinded type declaration

type Rep[T]

We expand this to

type Rep <: Lambda$I

The type parameters of Rep are the type parameters of its upper bound, so Rep is a unary type constructor.

More generally, a higher-kinded type declaration

type T[v1 X1 >: S1 <: U1, ..., vn XN >: SN <: UN] >: SR <: UR

is encoded as

type T <: LambdaV1...Vn { self =>
  type v1 $hkArg$0 >: s(S1) <: s(U1)
  ...
  type vn $hkArg$N >: s(SN) <: s(UN)
  type Apply >: s(SR) <: s(UR)
}

where s is the substitution [XI := self.$hkArg$I | I = 1,...,N].

If we instantiate Rep with a type argument, this is expanded as was explained before.

Rep[String]

would expand to

Rep { type $hkArg$0 = String } # Apply

If we instantiate the higher-kinded type with a concrete type constructor (i.e. a parameterized trait or class), we have to do one extra adaptation to make it work. The parameterized trait or class has to be eta-expanded so that it comforms to the Lambda bound. For instance,

type Rep = Set

would expand to:

type Rep = Lambda1 { type Apply = Set[$hkArg$0] }

Or,

type Rep = Map[String, _]

would expand to

type Rep = Lambda1 { type Apply = Map[String, $hkArg$0] }

Full example

Consider the higher-kinded Functor type class

class Functor[F[_]] {
   def map[A, B](f: A => B): F[A] => F[B]
}

This would be represented as follows:

class Functor[F <: Lambda1] {
   def map[A, B](f: A => B): F { type $hkArg$0 = A } # Apply  =>  F { type $hkArg$0 = B } # Apply
}

The type Functor[List] would be represented as follows

Functor {
   type F = Lambda1 { type Apply = List[$hkArg$0] }
}

Now, assume we have a value

val ml: Functor[List]

Then ml.map would have type

s(F { type $hkArg$0 = A } # Apply  =>  F { type $hkArg$0 = B } # Apply)

where s is the substitution of [F := Lambda1 { type Apply = List[$hkArg$0] }]. This gives:

Lambda1 { type Apply = List[$hkArg$0] } { type $hkArg$0 = A } # Apply
 =>  Lambda1 { type Apply = List[$hkArg$0] } { type $hkArg$0 = B } # Apply

This type simplifies to:

List[A] => List[B]

Status of #

In the scheme above we have silently assumed that # "does the right thing", i.e. that the types are well-formed and we can collapse a type alias with a # projection, thereby giving us a form of beta reduction.

In Scala 2.x, this would not work, because T#X means x.X forSome { val x: T }. Hence, two occurrences of Rep[Int] say, would not be recognized to be equal because the existential would be opened each time afresh.

In pre-existentials Scala, this would not have worked either. There, T#X was a fundamental type constructor, but was restricted to alias types or classes for both T and X. Roughly, # was meant to encode Java's inner classes. In Java, given the classes

class Outer { class Inner }
class Sub1 extends Outer
class Sub2 extends Outer

The types Outer#Inner, Sub1#Inner and Sub2#Inner would all exist and be regarded as equal to each other. But if Outer had abstract type members this would not work, since an abstract type member could be instantiated differently in Sub1 and Sub2. Assuming that Sub1#Inner = Sub2#Inner could then lead to a soundness hole. To avoid soundness problems, the types in X#Y were restricted so that Y was (an alias of) a class type and X was (an alias of) a class type with no abstract type members.

I believe we can go back to regarding T#X as a fundamental type constructor, the way it was done in pre-existential Scala, but with the following relaxed restriction:

In a type selection T#x, T is not allowed to have any abstract members different from X

This would typecheck the higher-kinded types examples, because they only project with # Apply once all $hkArg$ type members are fully instantiated.

It would be good to study this rule formally, trying to verify its soundness.