path: root/docs/HigherKinded-v2.md

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, +$hkArg1] { type +Apply } extends Lambda$IP with Lambda$PI

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, +$hkArg1] { type +Apply } extends Lambda$II
    trait Lambda$NI[type -$hkArg$0, $hkArg1] { type +Apply } extends Lambda$II
    trait Lambda$II[type -hkArg$0, $hkArg1] { 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 >: S1 <: 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.