Higher

 

Generics of a Higher Kind

Adri Ad riaan aan Moor Moorss

Fr Frank ank Pies Piesse sens ns

DistriNet, K.U.Leuven

EPFL

{adriaan, frank}@cs.kuleuven.be

martin.odersky@epfl.ch

Abstract With Java 5 and C# 2.0, first-order parametric polymorphism was introduced in mainstream object-oriented programming languages under the name of  generics  generics. Although the first-order variant of generics is very useful, it also imposes some restrictions: it is possible to abstract over a type, but the resulting type constructor cannot be abstracted over. This can lead to code duplication. We removed this restriction in Scala, by allowing type constructors as type parameters and abstract type members. This paper presents the design and implementation of the resulting type constructor polymorphism. Furthermore, we study how this feature interacts with existing object-oriented constructs, and show how it makes the language more expressive. Categorie Catego riess and Sub Subjec jectt Des Descri cripto ptors rs   D.3.3 D.3.3 [Programming Langu Languages ages]: Lan Langua guage ge Constr Construct uctss and Featur Features— es— Polymorphism General Terms   Design, Experimentat Experimentation, ion, Languages Languages  Keywords   type constructor polymorphism, polymorphism, higher-kinded higher-kinded types, higher-order genericity, Scala

1.

Martin Odersky

Intr Introd oduc ucti tion on

First-order parametric polymorphism is now a standard feature of statical statically ly typed typed prog programm ramming ing languages. languages. Starting Starting with System F [23 [23,,   50 50]] and functional programming languages, guage s, the constru constructs cts have found found their their way into objectobject# oriented languages such as Java, C , and many more. In these lang languages uages,, first first-ord -order er par paramet ametric ric polymorphi polymorphism sm is usually called generics. Generics rest on sound theoretical foundations, which were established by Abadi and Cardelli [2 [ 2,

1], Igarashi et al.   [31], 31], and many others others;; they they are wellunderstood by now now.. One standard application area of generics are collections. For instance, the type  List[A]  represents lists of a given element type  A , which can be chosen freely. In fact, generics can be seen as a generalisation of the type of arrays, which has always been parametric in the type of its elements. First-or Firs t-order der parametr parametric ic polym polymorphi orphism sm has some limi limitatations, however. Although it allows to abstract over types, which yields type constructors such as List, these type constructors cannot be abstracted over. For instance, one cannot pass a type constructor as a type argument to another type constructor.. Abstractions that require this are quite common, constructor ev even en in object-or object-orient iented ed progr programmi amming, ng, and this restrict restriction ion thus leads to unnecessary duplication of code. We provide several examples of such abstractions in this paper. The genera generalis lisati ation on of firs first-o t-orde rderr pol polymo ymorph rphism ism to a higher-order system was a natural step in lambda calculus  50,, 7  7]]. This theoretical advance has since been incorpo[23, 23, 50 rated into functional programming languages. For instance, the Haskell programming language [28 [28]]  supports type constructor stru ctor polymor polymorphis phism, m, whic which h is also integr integrated ated with its type class concept [33 [ 33]. ]. This generalisation to types that abstract over types that abstract over types (“higher-kinded types”) has many practical applications. For example, com[30,,   35 35], ], as well as prehensions [54 [54]], parser combinators [30 more recent work on embedded Domain Specific Languages (DSL’s) [14 [14,, 26  26]] critically rely on higher-kinded types. The same needs – as well as more specific ones – arise in object-oriented programming. LINQ brought direct sup 37]], Scala port for comprehensions to the .NET platform [5 [5,  37 [43] 43]  has had a similar feature from the start, and Java 5 introduced a lightweight variation [24 [24,,  Sec. 14.14.2]. Parser combinators are also gaining momentum: Bracha uses them as the underlying technology for his Executable Grammars [6], and Scala’s distribution includes a library [[39 39]] that implements an embedded DSL for parsing, which allows users to express parsers directly in Scala, in a notation that closely resembles EBNF. Type constructor polymorphism is crucial

This is the author’s version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in: OOPSLA’08,   October 19–23, 2008, Nashville, Ten Tennessee, nessee, USA. c 2008 ACM 978-1-60558-215-3/08/10.. . $5.00 Copyright  

in common parser interface that is implemented by defining differentaback-ends.

 

In this paper, we focus on our experience with extending Scala with type constructor polymorphism, and on the resulting gain in expressivity of the language as a whole. A similar extension could be added to, for example, Java in the same way [ way  [3 3]. Our extension was incorporated in Scala 2.5, which was released in May 2007. The main contributions of this paper are as follows: •

We illustrate the utility practicality of type constructor polymorphism usingand a realistic example. •

We develop a kind system that captures both lower and upper bounds, and variances of types.

•

We survey how the integration with existing features of  Scala (such as subtyping, definition-site variance annotations, and implicit arguments) makes the language more powerful.

•

We relate relate our expe experien rience ce with impleme implementing nting the kind system in the open-source Scala compiler.

For the reader who is not yet familiar with Scala, the next section provides a brief introduction. The rest of this paper is divided in three parts, which each consider a different facet of the evaluation of type constructor polymorphism. First, Section   3   demonstrates that our extension reduces boilerSection plate that arises from the use of genericity. We establish intuitions with a simple example, and extend it to a realistic implementation of the comprehensions fragment of Iterable. Second, we present the type and kind system. Section 4 Section  4 discusses the surface syntax in full Scala, and the underlying model of kinds. Based on the ideas established in the theoretical part, Section 5 Section  5  refines  Iterable, so that it accommodates collections that impose bounds on the type of  their elements. Third, we have validated the practicality of our design by implementing our extension in the Scala compiler, and we report on our experience in Section 6 Section  6.. Throughout the paper, we discuss various interactions of type constructor polymor polymor- focusses on phism with existing features in Scala. Section 7 Section  7 focusses the integration with Scala’s implicits, which are used to encode Haskell’s type classes. Our extension lifts this encoding to type  constructor  classes.   classes. Furthermore, due to subtyping, Scala supports abstracting over type class contexts, so that the concept of a bounded monad can be expressed cleanly, which is not possible in (mainstream extensions of) Haskell. Finally Fina lly,, we summ summaris arisee related related work in Sect Section ion   8   and conclude in Section 9 Section  9..

2.

Prelu Prelude: de: Scala Scala Basics Basics

This section introduces the basic subset of Scala [[43 43,, 45  45]] that is used in the examples of this familiarity with a Java-like language, andpaper. focusWe on assume what makes Scala different.

2.1

Out Outlin linee of of the the syn syntax tax

A Scala program is roughly structured as a tree of nested definitions. A definition starts with a keyword, followed by its name, a classifier, and the entity to which the given name is bound, if it is a concrete definition. If the root of the tree is the compilation unit, the next level consists of objects (introduced by the keyword   object) and classes (class, trait), which in turn contain members. A member may again aga in be a class class or an object object,, a con consta stant nt value value memb member er (val), a mutable value member (var), a method (def), or a type member (type). Note that a type annotation always follows the name (or, more generally, the expression) that it classifies. On the one hand, Scala’s syntax is very regular, with the keyword/name/classifier  keyword/name/classifier/bound /bound entity-sequence being its lead motif. Another important aspect of this regularity is nesting, which is virtually unconstrained. On the other hand, syntactic sugar enables flexibility and succinctness. For example,   buff buffer er += 10   is sho short rthan hand d for the met method hod call call buffer.+=(10), where  +=  is a user-definable identifier. 2.2

Fun Functi ctions ons

Since Scala is a functional language, functions are first-class values. Thus, like an integer, a function can be written down directly:  x: Int Int   ⇒   x + 1 is the successor function on integers. Furthermore, Furthermore, a function can be passed as an argument to a (higher-order) function or method. Functions and methods are treated similarly in Scala, the main difference is that a method is called on a target object. The following definition introduces a function   len   that takess a   String   and yie take yields lds an   Int   by calling calling   String’s length method on its argument  s : val   len: String String   ⇒   Int Int = s   ⇒   s.length

In the classifier of the definition, the type  String   ⇒ Int, the arrow ⇒ is a type constructor constructor,, whereas it introduces an anonym anonymous ous functi function on on the rig rightht-han hand d side side (wh (where ere a value value is expected). This anonymous function takes an argument  s of type  String  and returns  s.length. Thus, the application  len("four") yields  4 . Note that the Scala compiler infers [46 [46]]  the type of the argument   s, based on the expected type of the value   len. The direction of type inference can also be reversed: val   len len = (s (s: : St Strin ring) g)   ⇒   s.length

The right-han right-hand d side side’s ’s anonymous anonymous function function can be abbre breviat viated ed using using syntactic syntactic sugar that impl implicit icitly ly introduce introducess function func tional al abstr abstracti action. on. This can be thought thought of as turning turning String’s length  method into a function: val   len: String String   ⇒   Int = _. _.le lengt ngth h

Finally, since Scala is purely object-oriented at its core, a function is represented internally internally as an object with an apply

 

method that is derived straightforwardly from the function. Thus, one more equivalent definition of  len  len : object   len len { def   apply(s apply(s: : String) String): : Int = s.l s.lengt ength h }

2.3

Clas Classes, ses, traits, traits, and objects objects

In Scala, a class can inherit from another class and one or more traits. A trait is a class that can be composed with other traits using mixin composition. Mixin composition is a restricted form of multiple inheritance, which avoids ambiguities by linearising the graph that results from composing classes that are themselves composites. The details are not relevant for this paper, and we simply refer to both classes and traits as “classes”. The feature that is relevant to this paper, is that classes may contain type members. An abstract type member is similar ilar to a typ typee parame parameter ter.. The ma main in dif differ ferenc encee bet betwee ween n paramparameters and members is their scope and visibility. A type parameter is syntactically part of the type that it parameterises, whereas a type member – like value members – is encapsulated, and must be selected explicitly. Similarly, type mem-

function with type  (Int   ⇒   Int, Int, Int   ⇒   Boolean)   ⇒ List[Int]. Note that the type parameter T was inferred to be  Int  from the type of  a  a . Finally, an   object  introduces a class with a singleton instance, which can be referred to using the object’s name.

3.

Reduci Reducing ng Code Duplicatio Duplication n with with Type Constructor Polymorphism

This section illustrates the benefits of generalising genericity to type constructor polymorphism using the well-known Iterable  abstraction. The first example, which is due to Lex Spoon, illustrates the essence of the problem in the  extends it to more realistic proportions. small. Section 3.1 Section 3.1 extends Listing   1   shows shows a Scala Scala imp implem lement entati ation on of the trait trait Iterable[T]. It contains an abstract method filter and a convenience method  remove. Subclasses should implement filter so that it creates a new collection by retaining only the elements of the current collection that satisfy the predicate   p. This predicate is modelled as a function that takes an element of the collection, collection, which has type  T, and returns a  Boolean. As  remove   simply inverts the meaning of the  filter

bers inherited, while type parameters local to their class.are The complementary strengths of typeare parameters and abstract type members are a key ingredient of Scala’s recipe for scalable component abstractions [ abstractions  [47 47]. ]. Type parameters are made concrete using type application. Thus, given the definition  class   List[T],  List is a type constructor (or type function), and  List[Int]  is the application of this function to the argument   Int. Abstract type members are made concrete using   abstract type member refinement , a special form of mixin composition. Note that  List  is now an abstract class1 , since it has an abstract member T : trait   List List { type   T }

This abstract member is made concrete as follows: List{type   T=Int}

Note that, with our extension, type members may also be parameterised, as in  type   Container[X]. Methods typically define one or more lists of value parameters, in addition to a list of type parameters. Thus, a method can be seen as a value that abstracts over values and types.. For example, types example,   def   iterate[T] iterate[T](a: (a: T)(ne T)(next: xt: T ⇒   T, do done ne: : T   ⇒   Boolean): Boolean): List List[T] [T]   introduces a method with one type parameter   T, and two argument lists. Methods with multiple argument lists may be partially applied. For example, for some object   x  on which  iterate is defined,  x.iterate(0)   corresponds to a higher-order 1

For brevity brevity,, we use the   trait   keyword keyword instead instead of   abstract class.

predicate, it iswhen implemented of  expects .to again reNaturally, filteringina terms list, one ceive a list. Thus,  List overrides  filter to refine its result type covariantly covariantly.. For brevity, brevity,  List’s subclasses, which implement this method, are omitted. For consistency,  remove should have the same result type, but the only way to achieve this is by overriding it as well. The resulting code duplication is a clear indicator of a limitation of the type system: both methods in  List  are redundant, but the type system is not powerful enough to express them at the required level of  abstraction in  Iterable. Our solution, depicted in Listing   2,   is to abstract over the type constructor that represents the container of the result of  filter   filter  and  remove. The improved  Iterable  now takes two type parameters: the first one,   T, stands for the type of its elements, and the second one,  Container, represents the  type constructor  that   that determines part of the result type of the  filter and  remove methods. More specifically, Container is a type parameter that itself takes one type parameter.. Although the name of this higher-order type paramrameter eter (X) is not needed here, more sophisticated examples will show the benefit of explicitly naming2 higher-order type parameters. Now,, to denote Now denote that applyin applying g   filter   or   remove   to a   List[T]   returns a   List[T],   List   simply instantiates Iterable’s type parameter to the  List  type constructor. In this simple example, one could also use a construct like 9]. However, this scheme breaks down in Bruce’s  MyType  [  [9 more complex cases, as demonstrated in the next section. 2 In

full Scala ‘ _ ’ may be used as a wild-card name for higher-order type parameters.

 

trait   Iterable[ Iterable[T] T] def   filter( filter(p: p: def   remove( remove(p: p:

{

T   ⇒   Boolean): Iterabl Iterable[T] e[T] T   ⇒   Boolean Boolean): ): Iter Iterabl able[ e[T] T] = fil filter ter (x   ⇒   !p(x))

} trait   List[T]   extends   Iterable[ Iterable[T] T] def   filter( filter(p: p:

{ T   ⇒   Boolean): Boolean): List[ List[T] T]

T   ⇒   Boolean): Boolean): List[T List[T] ] = filt filter er (x   ⇒   !p(x))

legend:

overrid over ride e def   remove remove(p: (p:

copy/paste redundant code

}

Listing 1.  Limitations of Genericity

Iterable[T, [T, trait   Iterable

Container Container[X]] [X]] { filter(p: (p: T   ⇒   Boolea Boolean): n): Container[ Container[T] T] def de f   filter remove(p: (p: T   ⇒   Boolean Boolean): ): Contai Container ner[T] [T] = filter filter (x   ⇒   !p(x)) def de f   remove

} legend:

Iterable[T, , trait   List[T]   extends   Iterable[T

List]

abstraction instantiation

Listing 2.  Removing Code Duplication

3.1

Impr Improvin oving g Itera Iterable ble

In this section we design and implement the abstraction that underlies comprehensions [54 [54]. ]. Type constructor polymorphism plays an essential role in expressing the design constraints, as well as in factoring out boilerplate code without losing type safety. More specifically, we discuss the signature and implementation of  Iterable   Iterable’s  map,  filter, and flatMap  methods. The LINQ project brought these to the ]. .NET platform as  Select,  Where, and  SelectMany [36  [ 36]. Comprehensions provide a simple mechanism for dealing with),collections transforming(filter their elements ( map retrieving aby sub-collection ,  Where), and, Select collecting the elements from a collection of collections in a single collection (flatMap,  SelectMany). To achieve this, each of these methods interprets a usersupplied function in a different way in order to derive a new collection from the elements of an existing one:   map  transforms the elements as specified by that function,   filter interprets the function as a predicate and retains only the elements that satisfy it, and  flatMap  uses the given function to produce a collection of elements for every element in the original collection, and then collects the elements in these collections in the resulting collection. The only collection-specific operations that are required by a method such as   map, are iterating over a collection, and producing a new one. Thus, if these operations can be abstracted over, these methods can be implemented in

trait   Builder[Co Builder[Container ntainer[X], [X], T] { def   +=(el +=(el: : T) T): : Unit Unit def   finalise(): finalise(): Container[T] Container[T] } trait   Iterator[T Iterator[T] ] { def   next(): next(): T def   hasNext: hasNext: Boolean def   foreach(op: foreach(op: T   ⇒   Unit): Unit): Unit =   while(hasNex (hasNext) t) op(next()) op(next())

}

Listing 3.   Builder and  Iterator

terms of these abstractions. Listing   3   shows the well-known, lightweight, Iterator abstraction that encapsul cap sulate atess iterat iterating ing over over a col collec lectio tion, n, as wel welll as the Builder abstraction, which captures how to produce a collection, and thus may be thought of as the dual of  Iterator. Builder  crucially relies on type constructor polymorphism, as it must abstract over the type constructor that represents the collection that it builds. The   +=  method is used to supply the elements in the order in which they should Iterable  in

appear appe ar in the .collection. collecti on. Thethe collection collecti on itse itself lf is retu returned rned by   finalise For example,   finalise   method of a Builder[L Buil der[List, ist, Int] returns a  List[Int].

 

trait   Buildable[Container Buildable[Container[X]] [X]] { def   build[T]: build[T]: Builder[Container Builder[Container, T]

Listing 4 Listing  4  shows a minimal  Buildable  with an abstract

def   buildWith buildWith[T](f: [T](f: Builder[Containe Builder[Container,T] r,T]⇒ Unit): Unit ): Cont Containe ainer[T r[T] ] ={ val   buff buff = buil build[T d[T] ] f(buff) buff.finalise() }

method hod,, and a con conve venie nience nce method method,, buildWith, th that at build met captures the typical use-case for  build. By analogy to the proven design that keeps  Iterator and   Iterable  separated,   Builder   and   Buildable   are modelled as separate abstractions as well. In a full implementation,  Buildable   would contain several more meth]), which should ods, such as  unfold  (the dual of  fold   fold  [22  [ 22]), not clutter the lightweight  Builder interface. Note that   Iterable   uses a type constructor member, Container, to abstract over the precise type of the container, whereas  Buildable  uses a parameter. Since clients of   Iterable   generally are not concerned with the exact type of the container (except for the regularity that is imposed by our design), it is neatly encapsulated as a type member.  Buildable’s primary purpose is exactly to create and populate a specific kind of container. Thus, the type of  an instance of the  Buildable  class should specify the type of container that it builds. This information is still available with a type member, but it is less manifest.

} trait   Iterable[T Iterable[T] ] { type   Container[X]   <:   Iterable[X] def   elements: Iterator[T] Iterator[T] def   mapTo[U, mapTo[U, C[X]]( C[X]](f: f: T   ⇒   U) (b (b: : Builda Buildable ble[C [C]) ]): : C[ C[U] U] = { val   buff = b.b b.build uild[U] [U] val   elems elems = elem elements ents while(elems.hasNext){ buff += f(elems f(elems.nex .next) t) } buff.finalise()

filter / flatMap flatMap   methods The   map / filter methods are implemen implemented ted in terms of the even more flexible trio   mapTo / filterTo filterTo  / flatMapTo flatMapTo. The generalisation consists of decoupling the original collection from the produced one – they need not be the same, as long as there is a way of building the target collection. Thus, these methods take an extra argument of type Buildable[C]. Section 7 Section 7 shows  shows how an orthogonal feature of Scala can be used to relieve callers from supplying this argument explicitly. For simplici simplicity ty,, the   mapTo   method method is impl implemen emented ted as straightforwardly straightforwa rdly as possible. The  filterTo method shows how the  buildWith convenience method can be used. The result types of   map,   flatMap, and their generalisations illustrate why a   MyType-based solution would not   this  would be  C[T], the result work: whereas the type of  this

} def   filterTo[C[X]]( filterTo[C[X]](p: p: T   ⇒   Boolean) (b (b: : Builda Buildable ble[C [C]) ]): : C[T C[T] ] = { val   elems elems = elem elements ents b.buildWith[T]{ b.buildWith[ T]{ buff   ⇒ while(elems.hasNext){ val   el = el elems ems.n .next ext if(p (p(el (el)) )) buf buff f += el } } } def   flatMapTo[U,C[X flatMapTo[U,C[X]](f: ]](f: T ⇒Iterable[U]) (b (b: : Bui Builda ldable ble[C [C]) ]): : C[U] C[U] = { val   buff = b.b b.build uild[U] [U] val   elems elems = elem elements ents

type of these methods is  C[U]: it is the same type  constructor , but it is applied to different type  arguments! Listings   5   and   6   show the objects that implement the Listings Buildable   interface interface for   List   and   Option. An   Option corresponds to a list that contains either 0 or 1 elements, and is commonly used in Scala to avoid  null’s. With all this in place,  List   can easily be implemented as a subclass of  Iterable  Iterable, as shown in Listing 7 Listing  7..  The type constructor of the container is fixed to be List itself, and the standard Iterator  trait is implemented. This implementation does not offer any new insights, so we have omitted it. 3.2

while(elems.hasNext){ f(elems.next).elements.foreach{ el   ⇒ bu buff ff += el } } buff.finalise()

} def   map[U]( map[U](f: f: T   ⇒   U) (b: Buildable[Contai Buildable[Container]) ner]): : Container Container[U] [U] = mapTo[U mapTo[U, , Container](f)(b Container](f)(b) ) def   filter(p filter(p: : T   ⇒   Boolean) (b: Buildable[Contai Buildable[Container]) ner]): : Container Container[T] [T] = filterTo[Contai filterTo[Container]( ner](p)(b) p)(b) def   flatMap[U](f: flatMap[U](f: T   ⇒   Container[U]) (b: Buildable[Contai Buildable[Container]) ner]): : Container Container[U] [U]

Exam Example: ple: using using Iterable Iterable

This example demonstrates how to use  map  and  flatMap to compute the average agedo ofnot thehave userstoof, say,their a social networking site. Since users enter birthday, the input is a  List[Option[Date]]. An  Option[Date]

}

= flatMapTo[U, flatMapTo[U, Container](f)(b) Container](f)(b)

Listing 4.   Buildable and  Iterable

 

object   ListBuildable   extends   Buildable[List]{ def   build[T]: build[T]: Builder Builder[Lis [List, t, T] =   new ListBuffer[T]   with   Builder Builder[Lis [List, t, T] { // += is inheri inherite ted d fro from m Lis ListB tBuff uffer er (S (Scal cala a standard library library) ) def   finalise finalise(): (): List[T] List[T] = toLi toList st } }

val   bdays: bdays: List[O List[Option[ ption[Date]] Date]] = List( Some(new   Date("1981/08/07 Date("1981/08/07")), ")), None, Some(new   Date("1990/04/10"))) def   toYrs( toYrs(bd: bd: Date): Date): Int =   // omit omitted  ted  val   ages: List[I List[Int] nt] = bdays. bdays.flatMapTo flatMapTo[Int, [Int, List]{ optBd   ⇒ optBd.map{d   ⇒   toYrs(d)}(OptionBuildable) }(ListBuildable)

Listing 5.  Building a  List val   avgAge avgAge = ages ages.re .reduce duceLeft Left[Int [Int](_ ](_ + _) / ages.length object   OptionBuildable   extends Buildable[Opt Buildabl e[Option] ion] { def   build[T]: build[T]: Builder[Option Builder[Option, , T] =   new   Builder[ Builder[Opti Option on, , T] { var   res: res: Option[ Option[T] T] = None None() () def   +=(el: +=(el: T) =   if(res (res.is .isEmpt Empty) y) res = Some Some(el (el) ) else els e throw throw new   UnsupportedOperation -Exception(" -Excep tion(">1 >1 elements") elements") def   finalise finalise(): (): Opti Option[ on[T] T] = res

} }

Listing 6.  Building an  Option

class   List[T]   extends   Iterable[T]{ type   Container Container[X] [X] = List List[X] [X] def   elements: Iterator Iterator[T] [T] =   new   Iterator[T] Iterator[T] { // standard implementation implementation }

}

Listing 7.   List subclasses  Iterable

either holds a date or nothing. Listing 8 Listing  8  shows how to proceed. First, a small helper is introduced that computes the current age in years from a date of birth. To collect the known ages, an optional date is transformed into an optional age using   map. Then, the results are collected into a list using flatMapTo. Note the use of the more general  flatMapTo. With flatMap, the inner inner  map  would have had to convert its result from an  Option   to a  List, as  flatMap(f)  returns its results in the same kind of container as produced by the function f (the inner map). Finally, the results are aggregated using  reduceLeft  (not shown here). The full code of the example is available on the paper’s homepage3 . Note that the Scala compiler infers most proper types (we added add ed som somee annota annotatio tions ns to aid und unders erstan tandin ding), g), but but it does does not 3 http://www.cs.kuleuven.be/

adriaan/?q=genericshk

∼

Listing 8.  Example: using  Iterable

infer type constructor arguments. Thus, type argument lists that contain type constructors, must be supplied manually. Finally, the only type constructor that arises in the example is the  List  type argument, as type constructor inference has not been implemented yet. This demonstrates that the complexity of type constructor polymorphism, polymorphism, much like with genericity, genericity, is concentrated in the internals of the library library.. The upside is that library designers and implementers have more control over the interfaces of the library, while clients remain blissfully ignorant of the underlying complexity complexity.. (As  will show how the arguments of type noted earlier, Section 7 Section 7 will Buildable[C] can be omitted.) 3.3

Memb Members ers vers versus us param parameters eters

The relative merits of abstract members and parameters have been discussed in detail by many others [8 [ 8,   53 53,,   21 21]. ]. The Scala philosophy is to embrace both: sometimes parameterisation is the right tool, and at other times, abstract members provide a better solution. Technically, it has been shown how to safely encode parameters as members [ members  [40 40], ], which – sur44]. ]. prisingly – wasn’t possible in earlier calculi [ calculi  [44 Our examp examples les have have used used both both styles styles of abs abstra tracti ction. on. Buildable’s main purpose is to build Thus,  Container  is a type parameter:

a certain container. a characteristic that is manifest to external clients of  Buildable, as it is (syntactically) part of the type of its values. In  Iterable a type member is used, as its external clients are generally only interested in the type of its elements. Syntactically, type members are less visible, as  Iterable[T] is a valid proper type. To make the type member explicit, one may write Iterable [T]{type   Container[X]=List[X]}. Alternati Alternatively vely,, the Container type type me memb mber er can can be sele select cted ed on a sing single leto ton n type type that is a subtype of  Iterable[T]  Iterable[T].

4.

Of Types ypes and Kinds Kinds

Even though proper types and type constructors are placed on equalone footing as parametric polymorphism is con-a cerned, mustasbefar careful not to mix them up. Clearly, type parameter that stands for a proper type, must not be

 

Type TypePa Para ramC mCla laus use e TypeParam

::= ::= ‘[’ ‘[’ Type TypePa Para ram m {‘,’ {‘,’ Type TypePa Para ram} m} ‘]’ ‘]’ ::= id [TypeParamClause use] [‘>:’ Type] [‘<:’ Type]

Ab Abst stra ract ctTp TpMe Mem m

:: ::= =

‘t ‘typ ype’ e’ Ty Type pePa Para ram m

Figure 1.  Syntax for type declarations (type parameters and abstract type members)     

∗

∗

 ∗

∗

 ∗  ∗

K   ::=

 

∗

  |

  K   

→

  K 

   

    

 

        

      



 



 

 

  

  



Figure 2.  Diagram of levels

applied to type arguments, whereas a type constructor parameter cannot classify a value until it has been turned into a proper type by supplying the right type arguments. In thi thiss sectio section n we give give an inf inform ormal al overv overvie iew w of ho how w programmers may introduce higher-kinded type parameters and abstract type members, and sketch the rules that govern their use. We describe the surface syntax that was introduced with the release of Scala 2.5, and the underlying conceptual model of kinds.

As a more complicated example, C[X   <:   Ordered[X]] <:   Iterable[X] introduces a type constructor parameter C, with an F-bounded higher-order type parameter  X , which occurs in its own bound as well as in the bound of the type parameter that it parameterises. Thus,  C  abstracts over a type constructor so that, for any  Y  that is a subtype of  Ordered[  Ordered[ Y],  C[Y] is a subtype of  Iterable[Y]  Iterable[Y] 4. 4.2 2

Kind Kindss

4.1 Surf Surface ace synt syntax ax for types  1  shows a simplified fragment of the syntax of type Figure 1 Figure parameters and abstract type members, which we collectively call “type declarations”. The full syntax, which additionally includes variance annotations, is described in the Scala language specification [42 [ 42]]. Syntactically, our extension introduces an optional  TypeParamClause as part of  a type declaration. The scope of the higher-order type parameters that may thus be introduced, extends over the outer type declaration to which they belong. For example,   Container[X]   is a valid   TypeParam, which introduces a type constructor parameter that expects one type type ar argum gument ent.. To illust illustrat ratee the scopin scoping g of higher higher-order type parameters,  Container[X]   <:   Iterable[X]

Conceptually, kinds are used to distinguish a type parameter that stands for a proper type, such as  List[Int], from a type parameter that abstracts over a type constructor, such as List. An initial, simplistic kind system is illustrated in the diagram in Fig. 2 Fig.  2,,  and it is refined in the remainder of this section. The figure shows the three levels of classification, where entities in lower levels are classified by entities in the layer immediately above them. Kinds populate the top layer. The kind  *  classifies types that classify values, and the → kind constructor is used to construc cons tructt kind kindss that classify type const construct ructors. ors. Note that kinds are inferred by the compiler. They cannot appear in Scala’ss surface syntax. Scala’ Nonetheless, Fig.  Fig.   3  introduces syntax for the kinds that classify the types that can be declared as described in the

declares type parameter that, when –applied to aa subtype type argument  Y  –awritten as  Container[Y] must be of  Iterable[Y].

(T, (T, U), classifies proper previous section. The first kind,   *without types (such as type declarations higher-order type parameters), and tracks their lower (T) and upper bounds

 

Kind Ki nd :: ::= = ‘*(’ Ty Type pe ‘,’ ‘,’ Type Type ‘) ‘)’ ’ | [id [id ‘@ ‘@’ ’ ] Kind Kind ‘->’ ‘->’ Ki Kind nd

Figure 3.  Kinds (not in surface syntax)

class   Iterable[Containe Iterable[Container[X], r[X], T] trait   NumericList[T   <:  Number]   extends Iterable[Numeric Iterable [NumericList List, , T]

 Iterable Listing 9.   NumericList: an illegal subclass of  Iterable

class   Iterable[Container[X   <:   Bound Bound], ], T   <: Bound, Bound]

(U). It should be clear that this kind is easily inferred, as type declarations either explicitly specify bounds or receive the minimal lower bound,  Nothing, and the maximal upper bound,   Any. Note that intersection types can be used to specify a disjunction of lower bounds, and a conjunction of upper bounds. Since we mostly use upper bounds, we abbreviate   *(Noth (Nothing, ing, T)   to   *(T), and   *(Nothing, Any) is written as  * . We refine the kind of type constructors by turning it into a  dependent  function   function kind, as higher-order type parameters may appear in their own bounds, or in the bounds of their outer type parameter. parameter. In the examples that was introduced above,  Container [X]  introduces a type constructor parameter of kind   *   → *, and  Container[X]   <:   Iterable[X]  implies the kind X @   *   →   *(Iterable[X]) for  Container. Finally, the declaration   C[X   <:   Ordered[X]]   <:   Iterable[X]   results in   C  receiving the kind   X @   *(Ordered[X])   →   *( Iterable[X]). Again, the syntax for higher-order type parameters provides all the necessary information to infer a (dependent) function kind for type constructor declarations. Informally,, type constructor polymorphism introduces an Informally indirection through the kinding rules in the typing rule for typee app typ applic licati ation, on, so tha thatt it unifor uniforml mly y applie appliess to gen generi ericc classes, type constructor parameters, and abstract type constructor struc tor members. members. These type constructo constructors, rs, whether whether concrete concrete or abstract, are assigned function kinds by the kind system. Thus, if   T   has kind   X @ K   →   K’, and   U   has kind   K, in  X which been replaced by   U, a type application   T[U] has kind  has   K’, with the same substitution applied. Multiple type arguments are supported through the obvious generalisation (taking the necessary care to perform simultaneous substitutions).

4.3

Sub Subkin kindin ding g

Similar to the subtyping relation that is defined on types, subkinding relates kinds. Thus, we overload <: to operate on kinds as well as on types. As the bounds-tracking kind stems from Scala’s bounds on type declarations, subkinding for this kind simply follows the rules that were already defined for type member conformance: *(T, (T, U)   <:   *(T’ (T’, , U’) if    <:

  <:

  U’. Intuitively, this amounts to interval inclusion. For the dependent function kind, we transpose subtyping of dependent function types [4 [ 4] to the kind level.

T’

  T  and  U

trait   NumericList[T   <:  Number]   extends Iterable[Numeric Iterable [NumericList List, , T, Number]

Listing 10.  Safely subclassing  Iterable

4.4

Exam Example: ple: why kinds trac track k bo bounds unds

Listing  9..  This proSuppose Iterable4 is subclassed as in Listing 9 gram gra m is reject rejected ed by the com compil piler er bec becaus ausee the typ typee app applic licati ation on Iterable[NumericList, Iterable[Numeri cList, T]  is ill-kinded. The kinding rules classify  NumericList  as a  * (Number)   →   *, which must be a subkind of the expected kind of  Iterable’s first type parameter,   *   →   *. Now,   *(Number)   <:   *, whereas subkinding for function kinds requires the argument kinds to vary contravariantly. Intuitively, this type application must be ruled out, because passing  NumericList  as the first type argument to Iterable   would “forget” “forget” that   NumericList   may onl only y contain Number’s: Iterable  is kind-checked under the assumption that its first type argument does not impose any bounds on its higher-order type parameter, and it could thus apply NumericList to, say, String. The next section elaborates on this. Fortunately,  Iterable  can be defined so that it can ac10.. commodate bounded collections, as shown in Listing   10 To achi achieve eve this, this,   Iterable   abstrac abstracts ts ov over er the bou bound nd on Container’s type para paramete meterr.   NumericList   instantiates this bound to  Number. We refine this example in Section 5 Section  5.. 4.5 Kind Kind sou soundn ndness ess Analogous to type soundness, which provides guarantees about value-level abstractions, kind soundness ensures that type-level abstractions do not go “wrong”. At the value level, passing, e.g., a  String  to a function that expects an  Integer  goes wrong  when that function invokes an  Integer-specific operation on that  String. Type soundness ensures that application is type-preserving, in the sense that a well-typed application evaluates to a well-typed result. As a type-level example, consider what happens when a type function that expects a type of kind  *   →   *, is applied to a type of kind   *(Number)   →   *. This application  goes 4 For

simplicity, we define   Iterable   using simplicity, using type paramete parameters rs in this example.

 

trait   Builder[Container[X   <:  B[X]]  B[X]], , T   <:  B[T], B[Y]] trait   Buildable[Container[X   <:   B[X B[X]], ]], B[ B[Y]] Y]] { def   build[T   <:  B[T]]: Builder[Containe Builder[Container,T r,T,B] ,B] } trait   Iterable[T   <:   Bound[ Bound[T], T], Boun Bound[X d[X]] ]] { type   Container[X   <:   Bound[X]]   <:  Iterable[X, Bound] def   map[U   <:   Bound[U] Bound[U]](f: ](f: T   ⇒   U) (b: Buildable[Cont Buildable[Container ainer, , Bound]) Bound]): : Containe Cont ainer[U r[U] ] = ...

}

Listin Lis ting g 11.   Essent Essential ial change changess to ext extend end Ite Iterab rable le wit with h support for (F-)bounds

class   List[T]   extends   Iterabl Iterable[T e[T, , Any] { type   Container Container[X] [X] = List List[X] [X] } trait   OrderedCollection[T   <:   Ordered[T]] extends   Iterable[ Iterable[T, T, Ordered Ordered] ] { type   Container[X   <:   Ordered[X]]   <: OrderedCollection[X] } trait   Wrap1[T]{type   Apply[X]=T} trait   Number class   NumericList[T   <:  Number]   extends Iterable[T, Iterable [T, Wrap1[Number]# Wrap1[Number]#Apply] Apply] { type   Container[X   <:   Number Number] ] = NumericL NumericList[X] ist[X] }

Listing 12.  (Bounded) subclasses of Iterable wrong, even though the type function itself is well-kinded, if it does something with that type constructor that would be admissible with a type of kind   *   →   *, but not with a type of kind  * (Number)   →   *, such as applying it to  String. If  the first, erroneous, type application were considered well-

kinded, typea well-kinded application would notabe kind-preserving, as it would turn type into nonsensical, ill-kinded, one (such as   NumericList[String] NumericList[String]). As our kind kind sys system tem is closel closely y rel relate ated d to depend dependent ently ly typed lambda calculus with subtyping, it is reasonable to assume that it is sound. Proving this conjecture, as well as the more familiar meta-theoretic results, is ongoing work. The underlying theory – an object-oriented calculus – has been described in earlier work [40 [40]. ]. Finally Fina lly,, it is importan importantt to note that kind unsoundness unsoundness results in type applications “going wrong”  at compile time. Thus, the problem is less severe than with type unsoundness, but these errors can be detected earlier in the development process, without effort from the programmer.

5.

Bou Bounded nded Itera Iterable ble

As motivated in Section 4.4 Section 4.4,, in order for Iterable to model collections that impose an (F-)bound on the type of their elements, it must accommodate this bound from the start. To allow allow sub subcla classe ssess of Iterable to declar declaree an (F(F-)bo )bound und on the type of their elements,  Iterable  must abstract over this bound. Listing 11 Listing  11  generalises the interface of the original  Iterable   from Listing  Listing   4. The implementation is not affected by this change. Listing 12 Listing  12 illustrates  illustrates various kinds of subclasses, including  List, which does not impose impose a bound on the type of its elements, and thus uses  Any  as its bound (Any and  Nothing are kind-overloaded). Note that  NumericList  can also be derived, by encoding the anonymous type function   X   → Number as   Wrap1[Number]#Apply Wrap1[Number]#Apply.

Again, the client of the collections API is not exposed 11..  However, without to the relative complexity of Listing  Listing   11

it, a significant fraction of the collection classes could not be unified under the same  Iterable  abstraction. Thus, the clients of the library benefit, as a unified interface for collections, whether they constrain the type of their elements or not, means that they need to learn fewer concepts. Alternatively, it would be interesting to introduce kindlevel abstraction to solve this problem. Tentatively,  Iterable and  List  could then be expressed as: trait   Iterab Iterable le[T [T : ElemK ElemK, , El ElemK emK : Kin Kind] d] class   List[T]   extends   Iterable[T,   *]

This approach is more expressive expressive than simply abstracting over the upper bound on the element type, as the interval kind can express lower and upper bounds simultaneously. This would become even more appealing in a language that allows the user to define new kinds [51 [ 51]].

6.

Fu Full ll Sc Scal ala a

In section we discuss our constructor experience with extending the fullthis Scala compiler with type polymorphism. As discussed below, the impact impact5 of our extension is mostly restricted to the type checker. Finally, we list the limitations of our implementation, and discuss the interaction with variance. The implementation supports variance annotations on higherhigh er-order order type paramete parameters, rs, but this has not been integrated in the formalisation yet. 6.1

Impl Implemen ementati tation on

Extending Extend ing the Sca Scala la com compil piler er wit with h sup suppor portt for typ typee const construc ruc-tor polymorphism came down to introducing another level of  indirection in the well-formedness checks for types. Once abstract abstract types could be paramete parameterise rised d (a simple simple extension to the parser and the abstract syntax trees), the 5 The

initial patch to the compiler can be viewed at   http://lampsvn.

epfl.ch/trac/scala/changeset/10642

 

check that type parameters parameters must always always be prope properr types had to be relaxed. Instead, a more sophisticated mechanism tracks the kinds that are inferred for these abstract types. Type application then checks two things: the type that is used as a type constructor must indeed have a function kind, and the kinds of the supplied arguments must conform to the expected kinds. Additionally, one must ensure that type constructors do not occur as the type of a value. Since Scala uses type erasure in the back-end, the extent of the changes is limited to the type checker. Clearly, our extension thus does not have any impact on the run-time characteristics of a program. Ironically, as type erasure is at the root of other limitations in Scala, it was an important benefit in implementing type constructor polymorphism. Similar extensions in languages that target the .NET platform face a tougher challenge, as the virtual machine has a richer notion of types and thus enforces stricter invariants. Unfortunate Unfortunately ly,, the model of types does not include higher-k highe r-kinde inded d type types. s. Thus, to ensur ensuree full interope interoperabil rability ity with genericity in other languages on this platform, compilers for languages with type constructor polymorphism must resort to partial erasure, as well as code specialisation in order to construct the necessary representations of types that result from abstract type constructors being applied to arguments. 6.1.1

Lim Limitat itations ions

Syntactically, there are a few limitations that we would like to lift in upcoming versions. As it stands, we do not directly support partial type application and currying, or anonymous type functions. However, these features can be encoded, as illustrated in Section 5 Section 5.. We have not yet extended the type inferencer to infer higher-kinded types. In all likelihood, type constructor inference will have to be limited to a small subset in order to ensure decidability. 6.2

Varianc ariancee

should not be glossed over when passing around type constructors. The same strategy as for including bounds into   * can be applied here, except that variance is a property of type constructors, so it should be tracked in →, by distinguishing +  − →   and →   [52 52]. ]. Without going in too much detail, we illustrate the need for varianc variancee annot annotatio ations ns on high higherer-order order type paramete parameters rs and how they influence kind conformance. Listing 13 Listing  13 defines  defines a perfectly valid Seq abstraction, albeit with a contrived   lift   method. Because   Seq  declares   C’s type parameter   X  to be covariant, it may use its covariant type parameter  A  as an argument for  C , so that  C[A]   <:   C[ B] when  A   <:   B. Seq   declares the type of its   this  variable to be   C[A] (sel self: f: C[A C[A] ]   ⇒ declares  self  as an alias for   this, and gives it an explicit type). Thus, the  lift method may return this, as its type can be subsumed to  C[B]. Suppose that a type constructor that is invariant in its first type parameter could be passed as the argument for a type constructor parameter that assumes its first type parameter to be covariant. This would foil the type system’s first-order variance checks:  Seq ’s definition would be invalid if  C  C  were invariant invariant in its first type parameter. The remainder of Listing 13 Listing  13  sets up a concrete example that would result in a run-time error if the type application Seq[A, Seq[ A, Cell] were not ruled out statically. More generally, a type constructor parameter that does not declare any variance for its parameters does not impose any restrictions on the variance of the parameters of its type argument. However, when either covariance or contravariance is assumed, the corresponding parameters of the type argument must have the same variance.

7.

Leve Leveragin raging g Scala’s Scala’s implicit implicitss

Another facet of the interaction between subtyping and type constructo const ructors rs is seen in Scala’ Scala’ss support support for defin definitio ition-si n-site te variance annotations [19 [19]. ]. Variance annotations provide the information required to decide subtyping of types that result from applying the same type constructor to different types. As the classical example, consider the definition of the class of immutable lists,   class   List[+T]. The   +  before List’s type parameter denotes that  List[T] is a subtype of  List[U]   if   T   is a subtype of   U. We say that   +  introduces a covariant type parameter,   -   denotes contravariance (the subtyping relation between the type arguments is the inverse inverse of the resulting relation between the constructed types), and the lack of an annotation means that these type arguments must be identical.

In this section we discuss how the introduction of type constructor polymorphism has made Scala’s Scala’s support for implicit arguments more powerful. Implicits have been implemented in Scala since version 1.4. They are the minimal extension to an object-oriented language so that Haskell’s type classes [ 41]]. [56] 56] can be encoded [41 We first show how to improve the example from Section 3 tion  3 using  using implicits, so that clients of  Iterable  Iterable no longer need to supply the correct instance of  Buildable[C]. Since there generally is only one instance of  Buildable[C]  Buildable[C]  for a particul part icular ar type constructo constructorr C, it beco become mess qu quit itee tedi tediou ouss to supsupply it as an argument whenever calling one of  Iterable’s methods that requires it. Fortunately, Scala’s implicits can be used to shift this burde den n to the the comp compil iler er.. It suffi suffice cess to add add the the implicit keyword

the same of challenge to theVariance model ofannotations kinds as didpose bounded typekind parameters: kinds must encompass encompass them as they represent represent info informat rmation ion that

Build Buildable[ able[C] C] to the parameter contains the   b: objects. parameter, and tolist thethat  XXXIsBuildable With this change, which is sketched in Listing 14 Listing  14,, callers (such as in

 

trait   Seq[+A Seq[+A, , C[+X]] C[+X]] { sel self: f: C[ C[A] A]   ⇒ def   lift lift[B [B >: A]: A]: C[B] C[B] =   this } class   Cell[A]   extends Seq[A Seq [A, , Cel Cell] l] {   // the onl only y (s (sta tatic tic) ) err error  or   privat  pri vate e var   ce cell: ll: A = _  def   set set(x (x: : A) = ce cell ll = x def   get get: A = ce cell ll }

trait   Iterable[T Iterable[T] ] { def   map[U]( map[U](f: f: T   ⇒   U) (implicit   b: Buildable Buildable[Contai [Container ner ]): Container[U] Container[U] = mapTo[U mapTo[U, , Container](f) Container](f) // no need need to pass pass b expl explic icit itly  ly  // sim simila ilar r for ot other her me metho thods ds }

class   Top class   Ext   extends   Top Top { def   bar() = println println("b ("bar" ar") ) }

implicit object   ListBuildable extends   Buildable[List]{...} implicit object   OptionBuildable extends   Buildable[Option]{..}

val   exts: exts: Cell Cell[Ext [Ext] ] =   new   Cell[Ext] val   tops: Cell Cell[Top [Top] ] = exts exts.lif .lift[T t[Top] op] tops.set(new   Top) exts.get.bar()   // method method not found erro error r, if  // the above static static error error is ign ignore ored  d 

// clie client nt code (previous (previous example example, , using  using  succinct function syntax): syntax): val   ages: List[I List[Int] nt] = bdays. bdays.flatMapTo flatMapTo[Int, [Int, List]{ List]{_.map{ _.map{toYrs(_ toYrs(_)}} )}}

Listing 14.  Snippet: leveraging implicits in  Iterable

Example le of uns unsoun oundne dness ss if hig higher her-or -order der Listing Listin g 13.   Examp variance annotations are not enforced.

the example of Listing 8 Listing  8)) typically do not need to supply this argument. In the rest of this section we explain this feature in order to illustrate the interaction with type constructor polymorphism. With the introduction of type constructor polymorphism, our encoding of type classes is extended to constructor classes, such as  Monad, as discussed in Section 7.3 Section  7.3.. Moreover, our encoding exceeds the original because we integrate type constructor polymorphism with subtyping, so that we can abstract over bounds. This would correspond to abstracting over type class contexts, which is not supported  32, 34  34,, 15  15]. ]. Section 7.3 Section 7.3 discusses  discusses this in more in Haskell [29 [29,, 32, detail. 7.1

Intr Introduct oduction ion to implicit implicitss

The principal idea behind implicit parameters is that arguments for them can be left out from a method call. If the arguments corresponding to an implicit parameter section are missing, they are inferred by the Scala compiler. Listing 15 Listing  15 introduces  introduces implicits by way of a simple example. It defines an abstract class of monoids and two concrete implementations, StringMonoid and IntMonoid. The two implementations are marked with an  implicit  modifier. implements ts a   sum   method, method, which work workss Listing   16   implemen over arbitrary monoids.   sum’s second parameter is marked implicit. Note that   sum’s recursive call does not need to pass along the  marguments  implicit argument. The actual that are eligible to be passed to an implicit parameter include all identifiers that are marked

abstract class   Monoid[T Monoid[T] ] { def   add add(x (x: : T, y: T) T): : T def   unit: unit: T } object   Monoids Monoids { implicit object   stringMonoid extends   Monoid[String Monoid[String] ] { def   add(x: add(x: String String, , y: String) String): : String String = x.conca x.concat(y) t(y) def   unit unit: : St Strin ring g = "" } implicit object   intMonoid extends   Monoid[Int Monoid[Int] ] { def   add(x add(x: : Int, Int, y: Int): Int): Int = x + y def   unit unit: : In Int t = 0 } }

Listing 15.  Using implicits to model monoids

def   sum[T](xs: sum[T](xs: List[T])( List[T])(implicit   m: Mono Monoid[ id[T T ]) ]): : T =   if(xs.is (xs.isEmpty) Empty) m.unit   else   m.add(xs.head, sum(xs.tail))

Listing 16.  Summing lists over arbitrary monoids

 

class   Or Ord d a   where (<= <=) ) :: a   →   a   →   Bool instance   Ord Dat Date e   where (<=) = ...

max :: Ord a   ⇒   a   →   a   →   a m a x x y =   if   x < = y   then   y   else   x

Listing 17.  Using type classes to overload  <=  in Haskell

implicit,

and that can be accessed at the point of the method call without a prefix. For instance, the scope of the Monoids   object can be opened up using an import statement, such as   import   Monoids._   This makes the two implicit definitions of  stringMonoid   stringMonoid  and  intMonoid  eligible to be passed as implicit arguments, so that one can write: sum(List("a" sum(Li st("a", , "bc", "def") "def")) ) sum(List(1 sum(Li st(1, , 2, 3))

These applications of   sum  are equivalent to the following two applications, where the formerly implicit argument is now given explicitly.

trait   Ord[T Ord[T] ] { def   <= (o (othe ther: r: T) T): : Boolea Boolean n } import   java.util.Date implicit implici t def   dateAsOrd(self: dateAsOrd(self: Date) =   new   Ord[Date Ord[Date] ] { def   <= (ot (other her: : Date) Date) = self.eq self.equals uals(ot (other her) ) || self.b self.before( efore(other) other) } def   max[ max[T T <% Ord[ Ord[T] T]]( ](x: x: T, y: T): T): T =   if(x <= y) y   else   x

Listing 18.  Encoding type classes using Scala’s implicits

“method dictionary”. An instance declaration specifies the contents of the method dictionary for this particular type.

Listing   17  defines a simplified version of the well-known Listing  Ord   type class. This definition says that if a type   a   is in the   Ord  type class, the function   <=   with type   a   →   a   → Bool is available. The  instance declaration instance   Ord Date  gives a concrete implementation of the  <=  operation on Date’s and thus adds  Date as an instance to the  Ord  type class. To constrain an abstract type to instances of a type class,  contexts  are employed. For example,   max’s signature constrains a  to be an instance of  Ord  Ord  using the context  Ord a, which is separated from the function’s type by a ⇒.

7.2.2 7.2. 2 Enco Encoding ding the example example in in Sc Scala ala It is natural to turn a type class into a class, as shown in 18..   Thus, an instance of that class corresponds to Listing   18 Listing a method dictionary, as it supplies the actual implementations of the methods declared in the class. The instance declaration  instance   Ord Date Date  is translated into an implicit method that converts a  Date into an  Ord[Date]. An object of type  Ord[Date]  encodes the method dictionary of the Ord type class for the instance  Date. Because of Scala’s object-oriented nature, the creation of  method dictionaries is driven by member selection. Whereas the Haskell compiler selects selects the righ rightt method method dict dictionar ionary y fully automatically, automatically, this process is triggered by calling missing methods on objects of a type that is an instance (in the Haskell sense) of a type class that does provide this method. When a type class method, such as  <= , is selected on a type T  that does not define that method, the compiler searches an implicit value that converts converts a value of type T into a value that does support this method. In this case, the implicit method dateAsOrd is selected when  T  equals  Date. Note that Scala’s scoping rules for implicits differ from Haskell’s. Briefly, the search for an implicit is performed locally in the scope of the method call that triggered it, whereas this is a global process in Haskell. Contexts are another trigger for selecting method dictionaries. The   O Ord rd a  context of the  max  method is encoded as a view bound  T <% Ord[ Ord[T] T], which is syntactic sugar for an implicit parameter that converts converts the bounded type to its view bound. Thus, when the   max  method is called, the compiler

 a , is transConceptually, context that constrains type lated into an extraa parameter that suppliesathe implementations of the type class’s methods, packaged in a so-called

 19 re remust appropriate implicit conversion. Listing  20 goes  goesListing 19 even further movesfind thisthe syntactic sugar, and Listing 20 Listing and makes the implicits explicit. Clients would then have

sum(List("a" sum(Li st("a", , "bc", "def") "def"))(stri )(stringMonoi ngMonoid) d) sum(List(1, 2, 3))(i sum(List(1, 3))(intMonoid ntMonoid) )

If there are several eligible arguments that match an implicit parameter’s type, a most specific one will be chosen using the standard rules of Scala’s static overloading resolution. If there is no unique most specific eligible implicit definition, the call is ambiguous and will result in a static error. 7.2

Encoding Haskell’s Haskell’s typ typee classes classes with implicits

Haskell’s type classes have grown from a simple mechanism Haskell’s that deal dealss with overloa overloading ding   [56], 56], to an important tool in dealing with the challenges of modern software engineering. Its success has prompted others to explore similar features in Java [57 [57]]. 7.2.1

An exam example ple in Haskell Haskell

 

def   max[T max[T]( ](x: x: T, y: T) (implicit   conv: conv: T   ⇒   Ord[T]) Ord[T]): : T =   if(x <= y) y   else   x

Listing 19.  Desugaring view bounds

class   Monad Monad m   where (>>=) >=) :: m a   →   (a   →   m b)   →   m b data   (Ord (Ord a)   ⇒   Set Set a = ... instance   Monad Monad Set   where -- (>>= (>>=) ) :: Set a   →   (a   →   Set b)   →   Set Set b

Listing 21.   Set cannot be made into a  Monad in Haskell def   max[T max[T]( ](x: x: T, y: T) T)(c (c: : T   ⇒   Ord[T]) Ord[T]): : T =   if(c(x). (c(x).<=(y)) <=(y)) y   else   x

Listing 20.  Making implicits explicit

trait   Monad[ Monad[A, A, M[X]] M[X]] { def   >>= >>= [B [B]( ](f: f: A   ⇒   M[B]): M[B]): M[B] M[B] }

Listing 22.   Monad in Scala

to supply the implicit conversion explicitly:  max(dateA, dateB)(dateAsOrd). 7.2.3

Cond Conditio itional nal implicit implicitss

By defining implicit methods that themselves take implicit parameters, Haskell’s conditional instance declarations can be encoded: instance   Ord Ord a   ⇒   Ord (List (List a)   where (<=) = ...

trait   BoundedMonad[A   <:   Bound[A] Bound[A], , M[X   <:  Bound[ X]], Bound[X]] Bound[X]] { def   >>= >>= [B   <:   Bound[B] Bound[B]](f: ](f: A   ⇒   M[B]): M[B]): M[B] M[B] } trait   Set[T   <:  Ord[T]] implicit implici t def   SetIsBoundedMonad[T   <:  Ord[T]]( s: Set[T]) Set[T]): : Boun BoundedM dedMonad onad[T, [T, Set, Ord] = ...

This is encoded in Scala as: implicit def  listAsOrd[T]( implicit  listAsOrd[T](self: self: List[T]) List[T])( ( implicit   v: T   ⇒   Ord[T]) Ord[T]) = new   Ord[List[T]] Ord[List[T]] { def   <= (o (othe ther: r: Lis List[ t[T]) T]) =   // comp compare are eleme ele ments nts in sel self f and oth other  er  }

Thus, two lists with elements of type  T  can be compared as long as their elements are comparable. Type classes and implicits both provide ad-hoc polymorphism. Like parametric polymorphism, this allows methods or classes to be applicable to arbitrary types. However, parametric polymorphism implies that a method or a class is truly indifferent to the actual argument of its type parameter, whereas ad-hoc polymorphism maintains this illusion by selecting different methods or classes for different actual type arguments. This ad-hoc nature of type classes and implicits can be seen as a retroact retroactive ive extens extension ion mechanism. mechanism. In OOP, OOP, vir vir-20]] have been proposed as an alternative tual classes [48 [48,,   20 that is better suited for retroactive extension. However, adhoc polymorphism also allows types to drive the selection of functionality as demonstrated by the selection of (implicit) instances of  Buildable[C]  Buildable[C]  in our  Iterable  exam6 ple .  Buildable  clearly could not be truly polymorphic in its parameter, as that would imply that there could be one Buildable that knew how to supply a strategy for building any type of container.

Listing 23.   Set as a  BoundedMonad in Scala

7.3

Exce Exceedin eding g type class classes es

 abstraction [  [55 55]] As shown in Listing 21 Listing 21,, Haskell’s  Monad abstraction does not apply to type constructors with a constrained type parameter, such as   Set, as explained below. Resolving this 15,, 16  16,,  29].  29]. issue in Haskell is an active research topic [ topic  [15 7 In this example, the  Monad abstraction does not accommodate constraints on the type parameter of the  m  type constructor that it abstracts over over.. Since  Set  is a type constructor that constrains its type parameter, it is not a valid argument for Monad’s m  type parameter:  m a is allowed for any type  a, whereas  Se Set t a is only allowed if  a  a  is an instance of the  Ord type class. Thus, passing   Set   as   m  could lead to violating this constraint. shows a dir direct ect encoding encoding of  For referenc reference, e, List Listing ing   22   shows the   Monad   type class. To solve the problem in Scala, we generalise   Monad   to  BoundedMonad   in Listing   23 23 to  to deal with bounded type constructors. Finally, the encoding from  7.2 is  is used to turn a  Set  into a  BoundedMonad. Section 7.2 Section

6 Java’s

static overloading mechanism is another example of ad-hoc poly-

morphism. 7 In fact, the main differen difference ce betwe between en our   Iterable   and Haskell’s Monad is spelling.

 

8.

Rela Relate ted d Wor ork k

8.1

Roots Roots of our kinds kinds

Since the seminal work of Girard and Reynolds in the early 1970’s, fragments of the higher-order polymorphic lambda calculus or System Fω  [  [23 23,, 50,  50, 7]  7] have served as the basis for many programming languages. The most notable example is Haskell [28 [28]], which has supported higher-kinded types for

therr’s work on extending Featherweight Generic Java with higher-kinded types   [18] 18] partly inspired the design of our syntax. However, since they extend Java, they do not model type members and path-dependent types, definition-site definition-site variance, or intersection types. They do provide direct support for anon anonymou ymouss type cons construct tructors. ors. Furtherm Furthermore, ore, although although their work demonstrates that type constructor polymorphism can be integrated into Java, they only provide a prototype of 

over 15ough years Haskell [27]].ell has highe [27 Although Alth Hask higher-k r-kinded inded types, it eschews eschews subtyp sub typing ing.. Most Most of the use use-ca -cases ses for subtyp subtyping ing are subsum subsumed ed by type classes, which handle overloading systematically [56] 56]. However, it is not (yet) possible to abstract over class  32,,  34  34,,  15]  15 ]. In our setting, this corresponds to contexts [29 [29,,  32 abstracting over a type that is used as a bound, as discussed in Section 7.3 Section 7.3.. The interaction between higher-kinded types and subtyp13,,  12,  12 ,  10,  10 ,  49,  49 ,  17]  17 ]. As far as ing is a well-studied subject [ subject  [13 we know, none of these approaches combine bounded type constructors, subkinding, subtyping  and  variance, although all of these features are included in at least one of them. A similarity of interest is Cardelli’s notion of power types [11 11]], which corresponds to our bounds-tracking kind  * (L, (L, U).

a compiler and an interpreter. Howev However, er, they have developed a mechanised soundness proof and a pencil-and-paper proof  of decidability. Finally, we briefly mention OCaml and C++. C++’s template mechanism is related, but, while templates are very flexible, this comes at a steep price: they can only be typechecked after they have been expanded. Recent work on “concepts” alleviates this [25 [25]]. In OCaml (as in ML), type constructors are first-order. Thus, although a type of, e.g., kind   *   →   *   →   *   is supported, types of kind   (*   →   *)   →   *   →   *  cannot be expressed directly. directly. Howev However, er, ML dialects that support applicative functors, such as OCaml and Moscow ML, can encode type constructor polymorphism in much the same way as languages with virtual types.

In summary, the presented type system can be thought of  as the integration of an object-oriented system with Polar52], ], Cardelli’s power type, and subkinding. Subized Fω  [  [52 sub kinding is based on interval inclusion and the transposition of subtyping of dependent function types [ types  [4 4] to the level of  kinds.

9.

Concl Conclus usio ion n

Then, a concrete instantiation of  List   List could be modelled as a type refinement, as in  List{type   Elem Elem = Str String ing} }. The crucial point is that in this encoding  List is a type, not a type constructor. So first-order polymorphism suffices to pass the  List  constructor as a type argument or an abstract type member refinement. Compared to type constructor polymorphism, polymorphism, this encoding has a serious disadvantage, as it permits the definition of certain accidentally empty type abstractions that cannot be instantiated to concrete values later on. By contrast, type constructor polymorphism has a   kind soundness soundness   property that guarantees that well-kinded type applications never re-

Genericity is a proven technique to reduce code duplication in object-oriented libraries, as well as making them easier to use by clients. The prime example is a collections library, where clients no longer need to cast the elements they retrieve from a generic collection. Unfortunately, though genericity is extremely useful, the first-order variant is self-defeating in the sense that abstracting over proper types gives rise to type constructors, which cannot be abstracted over. Thus, by using genericity to reduce code duplication, other kinds of boilerplate arise. Type constructor polymorphism allows to further eliminate these redundancies, as it generalises genericity to type constructors. As with genericity, most use cases for type constructor polymorphism arise in library design and implementation, where it provides more control over the interfaces that are exposed to clients, while reducing code duplication. Moreover, clients are not exposed to the complexity that is inherent to these advanced abstraction mechanisms. In fact, clients   benefit   from from the more prec precise ise interfa interfaces ces that can be expressed with type constructor polymorphism, just like genericity reduced the number of casts that clients of a collections library had to write. We implemented type constructor polymorphism in Scala 2.5. The essence of our solution carries over easily to Java, see Altherr et al. for a proposal [3 [ 3].

sultType in nonsensical types. constructor polymorphism has recently started to trickle down to object-oriented languages. Cremet and Al-

Finally, reported with. on one of severaldomain applications that we we have have only experimented Embedded specific languages (DSL’s) [14 [14]] are another promising appli-

8.2

Type cons constructor tructor polymorphism in OO OOPL PL’s ’s

Languages with virtual types or virtual classes, such as gbeta 20]], can encode type constructor polymorphism polymorphism through ab[20 stract type members. The idea is to model a type constructor such as  List  as a simple abstract type that has a type member describing the element type. Since Scala has virtual types, List could also be defined as a class with an abstract type member instead of as a type-parameterised class: abstract abst ract class class   List List {   type   Elem Elem }

 

cation area of type constructor polymorphism. We are currently applying these ideas to our parser combinator library, a DSL for writing EBNF grammars in Scala   [39]. 39]. Hofer, Ostermann et al. are investigating similar applications [26 [26]], which critically rely on type constructor polymorphism.

[11] L. Carde Cardelli. lli. Struc Structural tural subt subtyping yping and the notion of power type. In POPL, pages 70–79, 1988.

Acknowledgments

[13] L. Carde Cardelli lli and P. We Wegner gner.. On understa understanding nding types, data abstraction, and polymorphism.   ACM Computing Surveys,

The authors would like to thank Dave Clarke, Marko van Dooren, Burak Emir, Erik Ernst, Bart Jacobs, Andreas Rossberg, Jan Smans, and Lex Spoon for their insightful comments and interesting discussions. We also gratefully acknowle kno wledge dge the Scala Scala com commun munity ity for provid providing ing a fer ferti tile le testbed for this research. Finally, we thank the reviewers for their detailed comments that helped us improve the paper. An older version of this paper was presented at the MPOOL ]. workshop [38 [38]. The first author is supported by a grant from the Flemish IWT. Part of the reported work was performed during a 3month stay at EPFL.

References [1] M. Abadi and L. Cardel Cardelli. li. A theory of primitive primitive objec objects: ts: Second-order 116, 1995. systems.  Sci. Comput. Program., 25(2-3):81– [2] M. Abadi and L. Cardel Cardelli. li. A theory of primitive primitive objec objects: ts: Untyped and first-order systems.   Inf. Comput., 125(2):78– 102, 1996. [3] P. Altherr and V. Cremet. Adding type constructor parameterization to Java. Accepted to the workshop on Formal Techniques for Java-like Programs (FTfJP’07) at the European Conference on Object-Oriented Programming (ECOOP), 2007. [4] D. Aspinall Aspinall and A. B. Compagno Compagnoni. ni. Subtyp Subtyping ing depend dependent ent types.  Theor. Comput. Sci., 266(1-2):273–309, 2001.

[12] L. Cardelli. Cardelli. Types for data data-orie -oriented nted lan language guages. s. In J. W. Schmidt, S. Ceri, and M. Missikoff, editors,  EDBT , volume 303 of   Lecture Notes in Computer Science, pages 1–15. Springer, 1988.

17(4):471–522, 1985. [14] J. Carette, O. Kiselyo Kiselyov, v, and C. chieh Shan. Finally tagless, partiall part ially y evalu evaluated ated.. In Z. Shao, editor editor,,  APLAS , volume 4807 of  Lecture  Lecture Notes in Computer Science, pages 222–238. Springer, 2007. [15] M. Chakravarty, S. L. P. Jones, M. Sulzmann, and T. Schri jvers. Class families, 2007. On the GHC Developer wiki,   http://hackage. http://hackage.haskell.org/trac/ haskell.org/trac/ghc/ ghc/ wiki/TypeFunctions/ClassFamilies. [16] M. M. T. Chakr Chakrav avarty arty,, G. Kel Keller ler,, S. L. P. Jones, and S. Marlow Marlow.. Assoc Associate iated d types wit with h class class.. In J. Pals Palsberg berg and M. Abadi, editors,  POPL, pages 1–13. ACM, 2005. [17] A. B. Compagnoni and H. Goguen. T Typed yped operational semantics for higher-order subtyping.   Inf. Comput., 184(2):242– 297, 2003. [18] V. Cremet and P P.. Altherr. Adding type constructor parameterization to Java. Journal of Object Technology, 7(5):25–65, June 2008. Special Issue: W Workshop orkshop on FTfJP FTfJP,, ECOOP 07. http://www.jot.fm/issues/ http://www .jot.fm/issues/issue issue 2008 06/article2/. [19] B. Emir Emir,, A. Kenn Kennedy edy,, C. V. Russo, and D. Yu Yu.. Varia ariance nce # and generalized constraints for C gener generics. ics. In D. Thomas, editor,  ECOOP, volume 4067 of  Lecture  Lecture Notes in Computer  Science, pages 279–303. Springer, 2006. [20] E. Ernst.   gbeta – a Langua Language ge with Virtual Attrib Attributes, utes,  Block Structur Structure, e, and Prop Propagating agating,, Dynamic Inheritance Inheritance. PhD thesis, Department of Computer Science, University of  ˚ Aarhus,  Arhus, Denmark, 1999.

[5] G. M. Bierma Bierman, n, E. Meijer Meijer,, and W. Schul Schulte. te. The essen essence ce of data access in Comega. Comega. In A. P. Black, editor editor,,  ECOOP, volume 3586 of  Lecture   Lecture Notes in Computer Science, pages

[21] E. Ernst. Fami Family ly polymo polymorphis rphism. m. In J. L. Knudse Knudsen, n, edito editor, r,  ECOOP, volume 2072 of  Lecture   Lecture Notes in Computer Science ,

287–311. Springer, 2005. [6] G. Bracha. Exe Executa cutable ble gramma grammars rs in New Newspeak speak..   Electron.  Notes Theor. Theor. Comput. Sci., 193:3–18, 2007.

pages 303–326. Springer, 2001. [22] J. Gibbon Gibbonss and G. Jones Jones.. The under-appre under-appreciat ciated ed unfold. In  ICFP, pages 273–279, 1998.

[7] K. B. Bruce, A. R. Meyer, and J. C. Mitchell. The semantics of second-order lambda calculus.   Inf. Comput., 85(1):76– 85(1):76– 134, 1990.

[23] J. Gira Girard. rd. Inter Interpreta pretation tion foncti fonctionell onellee et elimin elimination ation des ´ coupures de l’arithmetique d’ordre superieur. superieur. Th Th`ese e` se d’Etat, Paris VII, 1972.

[8] K. B. Bruce, M. Odersky, and P P.. Wadl Wadler. er. A statically safe alternative to virtual types. In E. Jul, editor,  ECOOP, volume 1445 of  Lecture  Lecture Notes in Computer Science, pages 523–549. Springer, 1998.

[24] J. Gosling, B. Joy, G. Steele, and G. Bracha.   Java(TM)  Language  Langua ge Specific Specification, ation, The (3rd Edition) (Java (AddisonWesley)). Addison-Wesley Professional, 2005.

[9] K. B. Bruce, A. Schuett, and R. van Gent. PolyTOIL: A typesafe polymorphic object-oriented language. In W. G. Olthoff, editor,  ECOOP, volume 952 of  Lecture   Lecture Notes in Computer  Science, pages 27–51. Springer, 1995. [10] P. S. Canning, W. R. Cook, W. L. Hill, W. G. Olthoff, and J. C. Mitchell. F-bounded polymorphism for object-oriented programming. In  FPCA, pages 273–280, 1989.

[25] D. Gregor, J. J¨aarvi, rvi, J. G. Siek, B. Stroustrup, G. D. Reis, and A. Lumsdaine. Concepts: linguistic support for generic programming in C++. In P. L. Tarr and W. R. Cook, editors, OOPSLA , pages 291–310. ACM, 2006. [26] C. Hofer, K. Ostermann, T. Rendel, and A. Moors. Polymorphic embedding embedding of DSLs. In Y Y.. Smaragdakis Smaragdakis and J. Siek, editors, GPCE . ACM, 2008. To appear.

 

[27] P P.. Hudak, J. Hughe Hughes, s, S. L. P P.. Jones, and P. W Wadle adler. r. A history histo ry of Hask Haskell: ell: bei being ng lazy with clas class. s. In B. G. Ryder and B. Hailpern, editors,  HOPL, pages 1–55. ACM, 2007. [28] P. Hudak, S. L. P. Jones, P. Wadler, B. Boutel, J. Fairbairn, J. H. Fasel, M. M. Guzm´an, an, K. Hammond, J. Hughes, T. Johnsson, R. B. Kieburtz, R. S. Nikhil, W. Partain, and J. Peterson. Report on the programming langua language ge Haskell, a non-strict, purely functional language.  SIGPLAN Notices, 27(5):R1–R164, 1992. [29] J. Hughes. Restricted datatypes in Haskell. Technical Report UU-CS-1999-28, Department of Information and Computing Sciences, Utrecht University, University, 1999. 19 99.

EPFL, Nov. 2007.   http://www.scala-lang.org/ docu/files/ScalaReference.pdf. [43] M. Odersky, P. Altherr, V. Cremet, I. Dragos, G. Dubochet, B. Emir, S. McDirmid, S. Micheloud, N. Mihaylov, M. Schinz, Schinz, L. Spoon Spoon,, E. Stenma Stenman, n, and M. Zen Zenger ger.. An Overview of the Scala Programming Language (2. edition). Technical report, 2006. [44] M. Odersky, V. Cremet, C. R¨o ockl, ckl, and M. Zenger. A nominal theory of objects with dependent types. In L. Cardelli, editor,  ECOOP, volume 2743 of  Lecture   Lecture Notes in Computer Science , pages 201–224. Springer, 2003. [45] M. Odersky, L. Spoon, and B. Venners.   Programming in Scala. Artima, 2008.

[30] G. Hutton and E. Meijer Meijer.. Monad Monadic ic Parser Comb Combinato inators. rs. Technical Report NOTTCS-TR-96-4, Department of Computer Science, University of Nottingham, 1996.

[46] M. Odersky Odersky,, C. Zenger, and M. Zenger Zenger.. Colored local type inference. In POPL, pages 41–53, 2001.

[31] [31] A. Igaras Igarashi, hi, B. C. Pie Pierce rce,, and P. Wadl adler er.. Feathe Featherwe rweigh ightt Ja Java va:: a minimal core calculus for Java and GJ.  ACM Trans. Program.  Lang. Syst., 23(3):396–450, 2001.

[47] M. Oders Odersky ky and M. Zenger. Zenger. Scal Scalable able compo component nent abstra abstractio ctions. ns. In R. Johnson and R. P. Gabriel, editors,  OOPSLA, pages 41– 57. ACM, 2005.

[32] [32] M. P P.. Jon Jones. es. con constr struct uctor or cla classe ssess & ”se ”set” t” monad monad?, ?, 1994.   http://groups.goo http://groups.google.com/group/com gle.com/group/comp. p. lang.functional/msg/e10290b2511c65f0.

[48] H. Ossher and W W.. H. Harrison. Combination of inheritanc inheritancee hierarchies. In OOPSLA, pages 25–40, 1992.

[33] M. P. Jones. A system of constructor classes classes:: Overloading and implicit higher-order polymorphism.  J. Funct. Program. , 5(1):1–35, 1995. [34] E. Kidd. How to make dat data.se a.sett a monad, 2007.   http: //www.randomhacks.net/articles/2007/03/ 15/data-set-monad-haskell-macros .

[35] D. Leijen and E. Meijer. Parsec: Direct style monadic parser combinators for the real world. world. Technical Technical Report UU-CS2001-27, Department of Computer Science, Universiteit Utrecht, 2001. [36] E. Meijer. Meijer. There is no impe impedance dance mism mismatch atch:: (languag (languagee integrated query in Visual Basic 9). In P P.. L. Tarr and W. W. R. Cook, editors,  OOPSLA Companion, pages 710–711. ACM, 2006. [37] E. Meij Meijer er.. Confe Confession ssionss of a used programming programming language salesman. sale sman. In R. P. Gabriel, D. F. Bacon, C. V. Lopes Lopes,, and G. L. S. Jr., editors,  OOPSLA, pages 677–694. ACM, 2007. [38] A. Moors, F. Piessens, and M. Odersky. Towards equal rights for higher-kinded types. Accepted for the 6th International International Workshop on Multiparadigm Programming with ObjectOriented Languages at the European Conference on ObjectOriented Programming (ECOOP), 2007. [39] A. Moors Moors,, F. Piesse Piessens, ns, and M. Oders Odersky ky.. Pars Parser er combinacombinators in Scala. Techni echnical cal Report CW491 CW491,, Departme Department nt of  Computer Science, K.U. Leuven, 2008.   http://www. cs.kuleuven.be/publicaties/rapporten/cw/ CW491.abs.html.

[40] A. Moors Moors,, F. Piesse Piessens, ns, and M. Oders Odersky ky.. Safe type-lev type-level el abs abstra tracti ction on in Sc Scala ala.. In   Proc. Proc. FOOL ’08 , Jan. 2008. http://fool08.kuis.kyoto-u.ac.jp/. [41] M. Odersky. Poor man’s type classes, July 2006. Talk at IFIP WG 2.8, Boston. [42] M. Odersky.  The Scala Language Specification, Version 2.6 .

[49] B. C. Pierce and M. Steffen. Higher-order subtyping.   Theor. Comput. Sci., 176(1-2):235–282, 1997. [50] J. C. Reynolds Reynolds.. Towa owards rds a the theory ory of type struct structure. ure. In B. Robinet, editor,   Symposium on Programming, volume 19 of   Lecture Lecture Notes in Compute Computerr Science, pages 408–423. Springer, 1974. [51] T T.. Shea Sheard. rd. Type-leve ype-levell comp computati utation on using narro narrowing wing in Ωmega.   Electr. Notes Theor. Comput. Sci., 174(7):105–128, 2007. [52] M. Steffen.   Polarized Higher-Order Subtyping. PhD the thesis, sis, Universit¨aatt Erlangen-N¨u urnberg, rnberg, 1998. [53] K. K. Thorup and M. Torgerse Torgersen. n. Unify Unifying ing generi genericity city combining the benefits of virtual types and parameterized classes. clas ses. In R. Guerra Guerraoui, oui, editor, editor,  ECOOP, volume 1628 of   Lecturee Notes in Compute  Lectur Computerr Science, pages 186–20 186–204. 4. Springer Springer,, 1999.  Mathematical Structures [54] P Wadler. r. Comprehending monads. 1992. in. Wadle Computer Science, 2(4):461–493,

[55] P. Wadler. Monads for functional programming. In J. Jeuring and E. Meijer, editors,   Advanced Functional Programming, volume 925 of  Lecture   Lecture Notes in Computer Science, pages 24–52. Springer, 1995. [56] P. Wadl Wadler er and S. Blott. How to make ad-hoc polymorphism less ad-hoc. In  POPL, pages 60–76, 1989. [57] S. Wehr, R. L¨ Lammel, a¨ mmel, and P. Thiemann. JavaGI : Generalized interfac inte rfaces es for Java Java.. In E. Ernst, edito editor, r,  ECOOP, volume 4609 of  Lecture  Lecture Notes in Computer Science, pages 347–372. Springer, 2007.