Implementing Higher-Kinded Types in Dotty
Martin Odersky, Guillaume Martres, Dmitry Petrashko
EPFL, Switerland: {first.last}@epfl.ch

Abstract

proved to be challenging, so much so that we evaluated four
different strategies before settling on the current direct representation encoding. The strategies are summarized as follows:

dotty is a new, experimental Scala compiler based on DOT,
the calculus of Dependent Object Types. Higher-kinded
types are a natural extension of first-order lambda calculus,
and have been a core construct of Haskell and Scala. As longas such types are just partial applications of generic classes,
they can be given a meaning in DOT relatively straightforwardly. But general lambdas on the type level require extensions of the DOT calculus to be expressible. This paper
is an experience report where we describe and discuss four
implementation strategies that we have tried out in the last
three years. Each strategy was fully implemented in the dotty
compiler. We discuss the usability and expressive power of
each scheme, and give some indications about the amount of
implementation difficulties encountered.

• A simple encoding in the DOT-inspired [9] core typestructures that can express partial applications and notmuch more• A direct representation that adds support for full typelambdas and higher-kinded applications, without reusing much of the existing concepts of the calculus andthe compiler.
• A projection encoding, that encodes higher-kinded types

as first-order generic types using type projections T#A.
• A refinement encoding, that encodes higher-kinded types

Categories and Subject Descriptors D.3.3 [Language
Constructs and Features]: Polymorphism

as first-order generic types using refinements and pathdependent types.

General Terms Languages, Compilers, Experimentation
Keywords type constructor polymorphism, higher-kinded
types, higher-order genericity, Scala, dotty, DOT, dependent
object types

1.

Neither of the encodings is fully transparent, in that some
type checking operations still needed special provisions forencoded types.
These four strategies were implemented in the dotty research compiler for Scala over the course of three years(2013-2016). The purpose of the present paper is to givea high-level overview of the implementations and the language design choices they entail.
The perspective of the paper is experimental rather thantheoretical. One can regard it as a kind of lab notebook
describing and contrasting different experiments. The raw
data for the experiments exists in the form of commits in
the repository ‘lampepfl/dotty‘ on GitHub. Given the considerable implementation effort that went into higher-kinded
types we wanted to create a record of what was done, whatworked out, and what did not work as well as hoped for.
Overall, it’s fair to say that there were more failed than successful experiments, but failures are at least as important torecord as successes.
The rest of this paper is organized as follows. Section 3
describes the simple encoding of partial applications into
core DOT. Section 4 describes the direct representation ofhigher kinded types. Section 5 and Section 6 describe two
encodings based on projections and refinements, respec-

Introduction

Scala has first-class support for higher-kinded types [3], they
can be defined by users as follows:
type Foo[A] = List[A] // Foo has kind * -> *and abstracted over:def return[F[_], A](x: A): M[A]type Bar[M[_]] = M[Int] // Bar has kind (* -> *) -> *Implementing sound support for these higher-kinded
types in dotty [5] without restricting their expressive power

This is the author’s version of the work. It is posted here for your personal use. Not forredistribution. The definitive version was published in the following publication:

SCALA’16, October 30–31, 2016, Amsterdam, Netherlands
ACM. 978-1-4503-4648-1/16/10...
http://dx.doi.org/10.1145/2998392.2998400

51

tively. Section 7 compares the four implementation strategies described previously. Section 8 concludes.

2.

An application such as List[String] is then expanded
to List { type Elem = String }. If List were declared ascovariant (using [+Elem]), the type application is instead
expanded to a refinement with an upper bound:

Background

List { type Elem <: String }If we combine generics and subtyping in a language likeJava or Scala, we face the problem that we want to express
a generic type where the type argument is an unknown typethat can range over a set of possible types. The prototypical case is where the argument ranges over all subtypes orsupertypes of some type bound, as in List[_ <: Fruit].
Such partially undetermined types come up when wewant to express variance. We would like to express, say,that List[Apple] is a subtype of List[Fruit] since Apple isa subtype of Fruit. An equivalent way to express this is to
say that the type List[Fruit] includes Lists where the elements are of an arbitrary subtype of Fruit. By that reasoning, List[Apple] is a special case of List[Fruit]. We
can also express this notion directly using the wildcard type
List[_ <: Fruit]. Definition-site variance can be regarded
as a user-friendly notation that expands into use-site variance expressions using such wildcards.
The problem is how to model a wildcard type such as
List[_ <: Fruit]. Igarashi and Viroli’s original interpretation [1] was as an existential type ∃T <: Fruit.List[T]which would be written

Analogously, applications of contravariant types lead to refinements with lower bounds.
This scheme has two immediate benefits. First, we only
need to explain one concept instead of two. Second, theinteraction between the two concepts, which was so difficult
before, now becomes trivial. Indeed, a type like
List[_ <: Fruit]is simply
List { type Elem <: Fruit }That is, wildcard parameters translate directly to refinementswith the same type bounds.

3.

The Simple Encoding

Following DOT, we model type parameters as type members
and type arguments as refinements. For instance, a parameterized class such as
Map[K, V]

List[T] forSome { type T <: Fruit }is treated as equivalent to a type with type members:in current Scala. However, existential types usually comewith explicit pack and unpack constructs [2], which areabsent in Scala’s setting. Moreover, actual subtyping rules
as e.g. implemented in the reference compilers for Java andScala are more powerful than what can be expressed withexistential types alone [12]. The theory of the rules that are
actually implemented is not fully known and the issues lookcomplicated. Tate, Leung and Learner have explored somepossible explanations in [11], but their treatment raises about
as many questions as it answers.
2.1

class Map { type Map$K; type Map$V }The type members are name-mangled (i.e. Map$K) to ensurethat they do not conflict with other user-defined members or
parameters named K or V.
A type-instance such as Map[String, Int] would then betreated as equivalent to
Map { type Map$K = String; type Map$V = Int }whereas a wildcard type such as Map[_, Int] is equivalentto:

A Uniform Representation of Types

The problem is solved in DOT and dotty by a radical reduction. Type parameters and type arguments are not primitive,
but are seen as syntactic sugar for type members and typerefinements. For instance, if List is declared like this:Map { type Map$V = Int }That is, _ arguments correspond to type members that areleft abstract. Wildcard arguments can have bounds. E.g.
Map[_ <: AnyRef, Int]

trait List[Elem] { ... }is equivalent to:then this would be expanded to a parameterless trait witha type member, like this:Map { type Map$K <: AnyRef; type Map$V = Int }trait List { type Elem; ... }3.1(For simplicity we re-use the name of the parameter Elemas the name of the type member, whereas in practice thecompiler would choose a mangled name like List$Elem inorder to avoid name clashes.)

Type Parameters and Partial Applications

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 of52

Non-linear parameter occurrences. It is also possible toexpress some patterns where type parameters occur nonlinearly on the right-hand side. An example is the definitionof Pair below.

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 thoseparameter fields declared in the class that are not yet
instantiated, in the order they are given. Type parameterfields of parents are not considered.

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

where Tuple2 is declared as• The type parameters of an abstract type are the typeclass Tuple2[+T1, +T2] ...

parameters of its upper bound.

The definition of Pair is expanded to the following parameterless type alias:• The type parameters of an alias type are the type param-

eters of its right hand side.
• The type parameters of every other type is the empty

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

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 parameterare then translated to references to the type member. The
type member itself is left uninstantiated.

This definition of type parameters leads to a simple modelof partial applications. Consider for instance:
type Histogram = Map[_, Int]
Histogram is a higher-kinded type that still has one typeparameter. Histogram[String] would be a possible type instance, and it would be equivalent to Map[String, Int].
One interesting consequence of this definition is thathigher-kinded types and existential types are identified witheach other by virtue of being mapped to the same construct.
Indeed, the type Map[_, Int] can be interpreted as both anexistential type, where the K field is unspecified and as ahigher-kinded type that takes a type argument for the K fieldand produces an instance of Map.
3.2

3.3

Limitations

The technique described in the previous section can expand
most polymorphic type aliases appearing in Scala codebases
but not all of them. Here are some examples of types thatcannot be expressed:
1.

type Rep[T] = T

This fails because the right hand side T does not have atype field named T.

Modeling Polymorphic Type Declarations

The partial application scheme gives us a new – and quite
elegant – way to express certain higher-kinded types. But
how do we interpret the polymorphic types that exist in
Scala?
More concretely, 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. Typealiases and abstract types do not allow the definition ofparameterized types so we have to interpret polymorphic
type aliases and abstract types specially.

2.

type LL[Elem] = List[List[Elem]]This fails because the occurrence of the parameter Elemon the right hand side is not a member binding of theouter List.
3.

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

This fails because the order of type parameters of the leftand right-hand sides of the definition differ.
Another restriction concerns the bounds of higher-kinded
type parameters. Consider the following pattern:

Parameterized Aliases. A simple, and quite common caseof parameterized type definitions in Scala are parameterizedaliases. For instance, we find in the Scala package the definition

class Seq[X] extends Iterable[X] ...
def f[C[X] <: Iterable[X]]: C[String] = ...
def g[C[X] <: Seq[X]]: C[String] = f[C]type List[+T] =scala.collection.immutable.List[T]According to our rules for type parameters, the result type off is encoded as

Aliases like these can be expanded under the simple encoding by simply dropping the parameters on the left hand sideand the arguments on the right hand side of the equals sign.

C { type Iterable$X = String }On the other hand, the result type of g is encoded as

Partial Applications. Type definitions representing partial
applications like Histogram above are straightforward.

C { type Seq$X = String }53

The two types are incompatible, hence the example above
would be lead to an ill-typed encoding, even though it seems
completely natural. The problem here is that type parameters
are encoded as type fields with mangled names that containthe name of the enclosing class. This means that narrowingof bounds for type parameters is not supported. The root
problem in the example above is that the type parameter C
in g has a type parameter field named Seq$X whereas the typeparameter C in f has a type parameter named Iterable$X.
Therefore, it should not be allowed to pass C from f to g.
In a sense the simple encoding abandons the traditional
notion of kinds, but replaces it with the notion that the kindof a type is the sequence of the names of its type parameterfields. According to the new notion, the call f[C] above
would not be kind-correct.
This discussion also points to a need for a mechanism toenforce that the type parameters of a class have the samenames as the type parameters of a superclass. In the example
above, we would like to enforce that the type parameter ofclass Seq has the same (encoded) name as the type parameterof class Iterable. A possible way to do this would be by allowing explicitly named parameters that are available under
the same name as public fields. E.g.,

is now just syntactic sugar for:type Foo = [+X] -> T
• Higher-kinded applications
C[T1, ..., Tn ]where C is a higher-kinded type constructor and T1 , ..., Tn
are argument types. In such an application C is always ahigher-kinded abstract or alias type or a type parameter.
If C is a class, the usual encoding with refinement types
is applied. If C is a lambda abstraction, beta reduction isapplied:([v1 X1, ..., vn Xn ] -> T)[U1, ..., Un ]-->[X1 := U1, ..., Xn := Un ]TReducing applied aliases proceeds similarly, but this is
not done eagerly in general as it affects type inference,
see the example at the end of this section.
We now sketch the extra subtyping rules as they are implemented in the compiler (a more formal treatment would
require us to extend the soudness proof of DOT), for simplicity of presentation we only cover the case of singleparameter lambdas and we do not consider F-bounds or
kind-checking. The rule governing type lambdas is as follows (conforms(v1 , v2 ) specifies the conformance relation
between variances. It is true iff v1 = v2 or if v2 is nonvariant) :type Seq[type X] extends Iterable[X]A more detailed discussion of named type parameters isbeyond the scope of this paper.
3.4

Discussion

The simple encoding has the advantage that no new concepts
beyond those already covered by DOT are needed. It supports all forms of partial application naturally, with minimal
notational overhead.
On the other hand, the limitations of the simple encoding make it less expressive than the current implementationof higher-kinded types in Scala. Furthermore, the distinction
between what can be expressed and what cannot looks somewhat arbitrary and not well connected with the source-levelparameter syntax.

4.

conforms(v1 , v2 )Γ ` L1 <: L2
Γ ` U2 <: U1
Γ, X >: L1 <: U1 ` T1 <: T2
Γ ` [v1 X >: L1 <: U1 ] → T1 <: [v2 X >: L2 <: U2 ] → T2
Subtyping rules for higher-kinded applications are as follows (here, the syntax Γ ` S <:! T or Γ ` S >:! T meansthat the closest known upper (respectively, lower) bound oftype S is T ).

The Direct Representation

The direct representation of higher-kinded types keeps theencoding of type parameters of traits and classes in terms oftype members as before. Higher-kinded abstractions and applications are modeled by their own constructs. In particular,
we add explicit internal representations for:

Γ ` A1 <:! [v X] → U1
Γ ` [X := T1 ]U1 <: U2
Γ ` A1 [T1 ] <: U2• Type lambdas

Γ ` A2 >:! [v X] → U2
Γ ` U1 <: [X := T2 ]U2Γ ` U1 <: A2 [T2 ][v1 X1, ..., vn Xn ] -> Twhere v1 , . . . , vn are the variances of the type parameters. This is used internally but can also be written explicitly by the user (see Section 4.2), in factΓ ` A <:! [+X] → U
Γ ` T1 <: T2
Γ ` A[T1 ] <: A[T2 ]type Foo[+X] = T54Γ ` A <:! [−X] → U
Γ ` T2 <: T1
Γ ` A[T1 ] <: A[T2 ]2. The argument O does not have the right number of typeparameters to match the pattern C[Z] and is therefore
discarded.
3. The next base type in linearization order from O is
B[Int, String]. This type has enough type parameters,
and we therefore instantiate C to [X] -> B[Int, X].

Γ ` A <:! [X] → U1
Γ ` T1 <: T2
Γ ` T2 <: T1
Γ ` A[T1 ] <: A[T2 ]4. After instantiation we obtain the constraint
B[Int, String] <: B[Int, Z],

Type inference also has to be adapted to higher-kinded
types. The main addition needed concerns the case where
the compiler needs to satisfy a subtyping constraint
S <:which leads to the instantiation of Z = String.
5. The call is hence expanded toC[T1, ..., Tn ]f[[X] -> B[Int, X], String](O)where C is an instantiable higher-kinded type parameter and
S and T1 , ..., Tn are types. We need to find an instantiation of
C that satisfies the constraint.
The scheme to find this instantiation is essentially thesame as for the most recent version of scalac (including
support for partial unification of type constructors [10]). We
first find a base type of S that has a constructor with at leastn type parameters where the variances of the rightmost nparameters conform to those of C’s type parameters. Let thatbase type be

and its result type is B[Int, String].
6. One could have alternatively chosen to instantiate C to[X] -> A[X]. But since B came first in linearization order,
this alternative was discarded. If subsequently we were
faced with the constraint that the result type of f should
be a subtype of A[String] this constraint will fail.
Inference takes abstract types and type aliases into account when trying to find possible type parameter instances.
For instance, given the type alias

B[S1, ... Sm, U1, ..., Un].

type Transform[X] = Map[X, X]

Then, try to instantiate C to

and the definition[X1, ..., Xn ] -> B[S1, ... Sm, X1, ..., Xn ]val trans: Transform[String]

and, if this succeeds, continue with the subtyping checkthe call f(trans) would be expanded toB[S1, ... Sm, U1, ..., Un ] <:B[S1, ... Sm, T1, ..., Tn ]f[Transform, String](trans)

That is, Transform is a valid candidate for the decompositionof the type of t into a type constructor and a type argument.
For this to work, it is important that aliases are not dereferenced eagerly in the compiler. If the compiler had expanded
the binding

The search for suitable base types proceeds according to
the linearization order of C. This is a deviation from scalac,
which uses a slightly different order in which base types are
visited. In both compilers, once a base type satisfies boththe type parameter instantiation and the subtyping check, thetype parameter stays instantiated to that base type, even if
subsequent subtyping checks fail. This is analogous to Prolog’s “cut” operator that prevents backtracking from undoinga partial success. The cut is necessary to prevent a combinatorial explosion by limiting the search space.

trans: Transform[String]totrans: Map[String, String]type inference would have yielded a different, and less intuitive expansion:

Example: Assume the following definitions:trait A[X]trait B[X, Y]
object O extends A[String]with B[Int, String]def f[C[X], Z](x: C[Z]) : C[Z] = x

f[[X] -> Map[String, X], String](trans)

4.1

Higher-Kinded Wildcard Applications

Recall that one of the main motivations of dotty’s encodingof type parameters was to give a simple semantics to wildcard arguments. With the introduction of higher-kinded applications, the problem resurfaces. For example, consider thedefinition:

Then the type parameters for f in the call f(O) are inferred
as follows.
1. The constraint to be satisfied is O <: C[Z], where C and Z
are instantiable type variables.

55

type M[X] <: Map[X, X]([X] -> M[X, X])[_]

What should be the meaning of M[_] be? One might betempted to simply disallow higher-kinded applications towildcard arguments. But unfortunately, Scala libraries docontain occurrences of such applications, which are hard towork around. Another possible interpretation would be as anexistential type - i.e. M[_] corresponds tois semantically not the same as M[_, _]. The former type implies a coupling between the two unknown type parameterswhich the latter type lacks.
The reducibility restriction does not seem to be very burdensome in practice. The dotty test suite, which includes
Scala’s standard collection library did not contain any occurrences of irreducible applications that would have to be
rejected.

Map[X, X] forSome { type X }.

If we follow that line, every existential type in Scala could
be expressed as a higher-kinded application to wildcard arguments. Indeed,

4.2

Implementation

The changes for supporting the direct representation are contained in pull request #1343 of the lampepfl/dotty repository on GitHub. The base-line of that pull request is the refinement encoding presented in Section 6.
The changes can be summarized as follows.

T forSome { type X >: L <: H }is equivalently expressed as([X] -> T)(_ >: L <: H).

• New syntax for type lambdas. The additional syntax is:

On the other hand, getting rid of existential types was another design objective of the dotty project. In the absence of
explicit pack and unpack constructs, their interactions withmany other concepts are unclear. Furthermore, existential
types are semantically quite close to path-dependent types
and it seems undesirable to have two concepts that largely
overlap.
The solution pursued in dotty is to disallow applicationsof higher-kinded types to wildcards unless these applications
can be ultimately reduced to wildcard arguments of classtypes. More precisely we restrict applications to wildcard
arguments to reducible type constructors, where a type constructor is reducible if one of the following is true.

Type ::=
HkTypeParamClause ‘->’ TypeHkTypeParamClause ::=‘[’ HkTypeParam {‘,’ HkTypeParam} ‘]’
HkTypeParam::={Annotation} [’+’ | ‘-’](Id[HkTypeParamClause] | ‘_’)TypeBounds• Internal representations for type lambdas and higher-

kinded applications as two new forms of types.
• A “smart” constructor for type application C[T1, .., Tn]

that picks the member-based encoding if C is a classreference, beta-reduces if C is a type lambda, and returns
a higher-kinded application otherwise.

• The constructor is a reference to a class or trait• Extractors for type lambdas and type applications that

• The constructor is a type lambda of the form

work independently of the underlying representation.

[X] -> B[... X ...]• Implementation of subtyping and inference rules for typelambdas and applications as outlined above.

where B is a reference to a class or trait and X appears at
most once, in argument position to B.

4.3• The constructor is an alias of a reducible constructor.

Comparison with scalac

The direct representation shares many characteristics withscalac’s implementation of higher-kinded types, which was
originally done by Adriaan Moors. In particular, the algorithms for subtyping and type inference are quite similar. But
there are also differences to note.
In scalac, all forms of type applications are represented
the same way. Type arguments are recorded as an additional
list-valued field in a TypeRef node, which is one of the fundamental constructors with which the compiler represents
types. Furthermore, all type definitions have a field thatrecords the definition’s type parameters. Type lambdas are
not a primitive concept in scalac; the Scala community has
instead settled on a rather elaborate encoding using structural types with type members and type projection, whichbears some resemblance to the projection encoding in thenext section.

• The constructor is an abstract type, and any bounds given

for it are reducible constructors.
Example: Assume the declarations
type C[X] <: Iterable[X]type M[X] = Map[X, X]

Then C[_] is legal because C is reducible but M[_] is illegal
because M is irreducible.
The idea is that it is safe to beta-reduce an application of a
type lambda of the form given above to a wildcard argument.
For instance,([X] -> C[X])[_]

is simply C[_]. On the other hand,56

By contrast, in dotty type parameters of classes are simply
specially marked type members. For alias and abstract types,
type parameters are expressed in the form of type lambdas.
E.g., a source level definition likenon-variant parameter, P (positive) a covariant parameter,
and N (negative) a contravariant parameter. An n-ary basetrait defines parameters hki for i = 1, ..., n with the given
variances, as well as an abstract type member $Apply. For
instance, the base trait

type C[X] <: Iterable[X]trait Lambda$NP {type $hk0
type $hk1
type $Applyis represented in the equivalent form
type C <: [X] -> Iterable[X].

}In summary, type parameters in dotty are a derived concept,
not a fundamental one.
Type arguments are represented in dotty as refinements
as long as the type constructor is a reference to a class ora trait. For type constructors that are abstract or alias types,
there is a special type node called HKApply which has the type
constructor and its arguments as fields.
4.4

is used for binary type lambdas where the first type parameter is contravariant and the second is covariant.
• An application of a non-variant higher kinded type C toan argument T is encoded as
C { type $hk0 = T } # $Apply

Discussion

Covariant and contravariant type applications lead to refinements with upper and lower bounds instead.

The direct encoding supports higher-kinded types in theirfull generality. Partial applications are supported through theintroduction of type lambdas, which are notationally heavier
than the solution of the simple encoding, but are much morelegible than the workarounds using structural types and typeprojections in current Scala.
The direct representation is in a sense less elegant andeconomical than the simple encoding. It feels a bit awkwardthat type applications are encoded as refinements in the firstorder case but remain as a primitive constructs in the higherorder case. On the other hand, this aligns well with the handling of wildcard arguments, which were the original motivation for encoding type applications as type member refinements. Wildcard arguments are expressible only if it can be
guaranteed that they can be eventually reduced away. So ina sense, one of the main benefits of making the distinction
between encoded and unencoded applications is that this obviates the need for existential types.
The conceptual and implementation cost of the direct
representation suggests that it might be advantageous to
study other encodings of higher-kinded types. Two suchcandidate encodings are presented in the next sections.

5.

• Beta reduction is supported by dereferencing the typeprojection. Indeed,([X] -> T)[A]is encoded as
Lambda$I {type $hk0
type $Apply = [X := this.$hk0]T} {type $hk0 = A} # Apply

which reduces to[this.$hk0 := A][X := this.$hk0]Twhich is equivalent to[X := A]T.

Ideally, an encoding of higher-kinded types into typemembers and refinements would be sufficiently expressive;an encoded term should be type-checkable in the base calculus without special provisions that account for the fact thattypes were originally higher-kinded. Unfortunately, there
are a number of areas where higher-kinded types do shine
through. To make, e.g. the standard Scala collections compile, all of the following tweaks are necessary:

The Projection Encoding

The type projection approach was originally suggested byAdriaan Moors. It uses the following basic encodings.
• A type lambda [X >: S <: U] -> T is encoded as the re-fined type

1. $Apply refinements are covariant. If T <: U thenLambda$I {type $hk0 >: S <: Utype $Apply = [X := this.$hk0]T}S { type $Apply = T }<: S { type $Apply = U }This makes use of a family of synthetic base traits
Lambda$..., one for each vector of variances of possible higher-kinded parameters. A suffix of I indicates aThis subtyping relationship does not hold for ordinary
type refinements. It would hold for upper bound refinements, of course. But we cannot model $Apply refine-

57

6.

ments as upper bound refinements because that would
lose beta reduction.

The Type Refinement Encoding

Whereas the type projection encoding makes use of an operator (type projection #) not covered in DOT but present incurrent Scala, the type refinement encoding uses general recursive types which are part of DOT but absent in Scala. The
idea is as follows.

2. Encodings of type lambdas distribute over intersections
and unions. For instance,
Lambda$I { ... type $Apply = T } &Lambda$P { ... type $Apply = U }• A type lambda [X >: S <: U] -> T is encoded as the re-needs to be normalized to

fined type

Lambda$I { ... type $Apply = T & U }[X := this.$hk0]T {type $hk0 >: S <: U}

3. A subtype test of the encoded version of([X1, ..., Xn ] -> T) <: C

• An application of a non-variant higher kinded type C toan argument T is encoded aswhere C is a class constructor is rewritten to:T <:C { type $hk0 = T }C[X1, ..., Xn].

Covariant and contravariant type applications lead to refinements with upper and lower bounds instead.

Analogously, the subtype test of the encoded version ofC <:([X1, ..., Xn ] -> T)• Beta reduction is a little bit problematic:is rewritten to([X] -> T)[A]C[X1, ..., Xn ] <: T.

is encoded as

4. Inference of higher-kinded type parameters is handledusing an algorithm analogous to the one described in
Section 4.

[X := this.$hk0]T {type $hk0} {type $hk0 = A}

One problematic aspect of the projection encoding isthat generalized type projections have been shown to beunsound [7]. The known examples of unsoundness do not
overlap with the images of the projection encoding, so it isconceivable that one could have a restricted form of typeprojection that permits the encoding of higher-kinded types
and that is at the same time sound. But the rules for sucha restricted form of type projection have not been worked
out, and indeed the plan for future Scala is to allow onlyclasses as prefixes of type projections. This can still model
Java’s inner classes (i.e. C#I is Scala’s version of Java’s innerclass reference C.I), but it cannot model higher-kinded types
which relies on the abstract type $Apply appearing in prefix
positon of type projections.

5.1

This is equivalent to (i.e. both a subtype and a supertypeof):[this.$hk0 := A][X := this.$hk0]T {type $hk0 = A}

which simplifies to[X := A]T { type $hk0 = A }The latter type is a subtype of the beta-reduced type
[X := A]T but it is not a supertype, because of the occurrence of the additional refinement { type $hk0 = A }.
To make beta reduction work correctly, we have to add a“garbage collection” rule along the following lines.

Discussion

The projection encoding can model full higher-kinded types.
It is based on two concepts already present in current Scala,type members and type projections. However, the latter concept is about to be phased out because it has been shown tobe unsound.
The implementation overhead of the projection encoding
was considerable and debugging was hard because encoded
types can become quite large. But ultimately, it succeeded in
representing all higher-kinded types in the standard library.

T is a first-order type
T <: T {$hki = U }To encode all higher-kinded types, the refinement encoding needs the full power of recursive types. For instance, thetype
type Rep[T] = T

58

SimpleProjection [4]Refinement [8]Direct [6]Lines of code
0
719
1216
2000

Full hk types
no
yes
yes
yes

Type lambdas
no
no
yes
yes

Full inference
no
no
no
yes

Implementation effort
1 person-month
4 person-months
1 person-month
1 person-month

Table 1. Implementation characteristics
would lead to the encoding

In theory, such circular types are harmless, but naive implementations of most type operations would send the compiler
into an infinite loop. So cycles like these had to be detected
and eliminated, which turned out to be difficult.

type Rep = { z => z.$hk0; type $hk0 }Here, the right hand side is a path-dependent recursive type,where “self” is represented by the variable z. Scala cannot
currently express types like this, but DOT can. We haveextended the dotty compiler to be able to cope with suchgeneral recursive types.
Like the projection encoding, the refinement encoding needed several tweaks in the compiler. The necessary changes are contained in pull request #1282 of thelampepfl/dotty repository on GitHub.
The main changes necessary were, in addition to tweaks(2) - (4) of the type projection encoding:

6.1

Discussion

The refinement encoding has the advantage that it is very
closely integrated with DOT. It uses the full power of recursive types of DOT to model higher-kinded types. Unlike theprojection encoding it does not need additional fundamental concepts like type projection whose status in future Scalais unclear. On the other hand, the abstraction presented by
the refinement encoding is also leaky. Additional subtyping
rules for garbage collection and type lambdas are needed,
and the compiler needed a subtle combination of two typenormalization rules. Also, one of these type normalization
rules follows higher-kinded aliases when a type was applied,which leads to suboptimal type inference.

1. Support for general recursive types, as outlined above.
2. Two “normalization functions” that essentially perform
beta reduction. One of these (called betaReduce) was applied eagerly whenever a type application was formed;
the other (normalizeHkApply) was applied every time theapplication was accessed.

7.

Comparison of Implementations

Table 1 gives some of the characteristics of the different implementations. The lines of code number gives approximate
additional lines of code relative to the simple encoding. It includes whitespace, comments, and other documentation but
excludes tests. The numbers are taken from the pull requests
that implemented the proposals; Smaller changes to the different proposals that occurred after the initial pull requests
are not taken into account.
The other columns in Table 1 indicate whether higher
kinded types are supported in full generality, whether typelambdas are supported, and whether type inference is ascomplete as in current scalac with the inclusion of the fix
to SI-2712.
The implementation of the simple encoding is smallest,
but lacks all three of these properties. The refinement encoding is about 500 lines larger than the projection encoding,but includes syntactic support for type lambdas, and also
includes several ameliorations in the handling of recursive
types. The direct representation has the largest implementation footprint. On the other hand, it is the only one that
supports type inference on a par with scalac.
The final column in Table 1 gives estimated implementation cost in (full-time) person months. These are rough estimates derived from personal recollections with the help ofsome GitHub archaeology. As all effort estimates, they haveto be taken with a grain of salt. The projection encoding took

3. A special case that disregards superfluous bindings ofhigher-kinded type parameters, as outlined in the garbage
collection rule above.
4. A special case that disregards parameter bounds checking when comparing two encodings of type lambdas. The
problem here is that naturally parameter bounds are contravariant whereas in the encoding they become member
bounds, which are covariant. Disabling bounds checking for encodings of type lambdas thus avoids spurious
type errors. Type soundness can still be guaranteed if one
type-checks all type applications instead. In that case,type errors are simply reported reported later, on firstorer type formation. However, it turned out subsequently
that checking all type applications, including in types inferred by the compiler is not very practical; so one might
be better off enforcing the proper contravariant bounds
relationship for type lambdas.
A recurring problem in the implementation of the refinement encoding was that circular types would arise during
type simplification. An example of such a circular type isC { type $hk0 = this.$hk0 }.

59

Acknowledgments

much longer than the others not just because of its implementation difficulties but also because it was our first attempt
at implementing full higher-kinded types. Subsequent implementation schemes were implemented faster in part becauseof what was learned before.

8.

The dotty compiler has profited from the contributions ofmany people; Main contributors besides the authors include
Felix Mulder, Ondřej Lhoták, Liu Fengyun, Vladimir Nikolayev, Samuel Grütter, Vera Salvis, Sébastien Doeraene, Jason Zaugg, and Nicolas Stucki. Adriaan Moors did the original implementation of higher-kinded types in scalac which
informed our implementatio to no small degree. He as well
as Rex Kerr, Daniel Spiewak, Sandro Stucki and Jason Zaugg provided important feedback on some of the implementations presented in this paper.

Conclusion

The work on the four different implementations of higherkinded types was done 2013-2016 in the context of the dotty
compiler. Initially, dotty supported the simple encoding. Because of its lack of expressiveness this was discarded in favorof the projection encoding. Once it became clear that general
type projection was unsound, we investigated the refinement
encoding as an alternative to the projection encoding.
Neither encoding turned out to be fully satisfactory. Bothwere leaky in the sense that they demanded certain rulesthat applied specifically to constructs that resulted from encodings. Both also posed considerable difficulties for implementation and debugging. In retrospect, the biggest problem
with the projection encoding was the size of the encoded
types, which made diagnostics and debugging hard. The refinement encoding added somewhat less bulk, but sufferedfrom the fact that cyclic bindings were often created inadvertently. Both encodings posed the problem that, being encodings, they were not reflected in static types. So the safety netof static typing was largely unavailable to the type checker
itself.
In the end, dotty settled for a direct representation ofhigher-kinded types. This implementation was larger thanthe others, due to the fact that less typing infrastructure
could be re-used. On the other hand, each of the higherkinded constructs of type lambdas and type applications now
was represented by its own static type, which was a big
help in ensuring the correctness and completeness of theimplementation.
In a sense, the direct representation gives an honest account of the additional implementation overhead caused byhigher-kinded types. The overhead is non-negligible: about
2’000 lines compared to a total of about 28’000 lines whichtaken up by core data-structures and the type-checker.
In retrospect, we believe the simple encoding is an interesting alternative for a language that wants to provide mostof the benefits of higher-kinded types at minimal cost to
specification and implementation, provided one can arrive ata crisp definition of what is legal and what is not. But Scalais not that language, since it has a large installed code basethat makes essential use of full higher-kinded types. The lesson learned from the work on the dotty compiler was that
one is best off supporting full higher-kinded types directly.
Encodings seem attractive at first for the code reuse they canprovide, but in the end they cause more difficulties than they
remove.

References[1] A. Igarashi and M. Viroli. On variance-based subtyping for parametric types.
In ECOOP 2002 - ObjectOriented Programming, 16th European Conference, Malaga,
Spain, June 10-14, 2002, Proceedings, pages 441–469,
2002.
URL http://link.springer.de/link/service/series/0558/bibs/2374/23740441.htm.
[2] J. Mitchell and G. Plotkin. Abstract types have existential
types. ACM Trans. on Programming Languages and Systems,
10(3):470–502, 1988.
[3] A. Moors, F. Piessens, and M. Odersky. Generics of a higher
kind. In Proc. OOPSLA, pages 432–438, 2008.
[4] M. Odersky. Projection encoding of higher-kinded types,
2014. URL https://github.com/lampepfl/dotty/pull/
137.
[5] M. Odersky. Compilers are databases. In JVM Languages
Summit, 2015. URL https://www.youtube.com/watch?v=
WxyyJyB_Ssc.
[6] M. Odersky. Direct representation of higher-kinded types,
2016. URL https://github.com/lampepfl/dotty/pull/
1343.
[7] M. Odersky. Type projection is unsound, 2016. URL https://github.com/lampepfl/dotty/issues/1050.
[8] M. Odersky. Type refinement encoding of higher-kinded
types, 2016. URL https://github.com/lampepfl/dotty/
pull/1282.
[9] T. Rompf and N. Amin. Type Soundness for Dependent
Object Types (DOT). OOPSLA, 2016. To appear.
[10] M. Sabin. SI-2712 add support for partial unification oftype constructors, 2016. URL https://github.com/scala/scala/pull/5102.
[11] R. Tate, A. Leung, and S. Lerner. Taming wildcards in java’s
type system. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011, pages
614–627, 2011. .
[12] M. Torgersen, E. Ernst, C. P. Hansen, P. von der Ahé,
G. Bracha, and N. M. Gafter. Adding wildcards to the java
programming language. Journal of Object Technology, 3(11):
97–116, 2004. . URL http://dx.doi.org/10.5381/jot.
2004.3.11.a5.

60