Chai: Traits for Java-like Languages

(1)

Chai : Traits for Java-like Languages

Charles Smith and Sophia Drossopoulou Department of Computing, Imperial College London

Abstract. Traits support the factoring out of common behaviour, and its integration into classes in a manner that coexists smoothly with inheritance-based structuring mechanisms.

We designed the language Chai , which incorporates statically typed traits into a simple Java-inspired base language, and we discuss three versions of the language: Chai1, where traits are only a mechanism for the creation of classes; Chai2where traits are a mechanism for the creation of classes, and can also introduce types, and Chai3where traits play a role at runtime, and can can be applied to objects, and change the objects’ behaviour. We give formal models for these languages, outline the proof of soundness, and our prototype implementation.

1 Introduction

Traits were designed to facilitate code reuse and to assist in structuring large programs. They are conceptually similar to classes, except that they contain no state, only behaviour, and can be combined using a set of simple composition and modification operators. Elements of behaviour that need to be reused in several different parts of a program can be encapsulated in a trait which may be referenced where necessary, avoiding the need to duplicate code.

Traits first appeared in the object-based language Self[22] where they took the form of parent objects to which an object can delegate some of its behaviour.

Subsequent work on Traits was based on the class-based language Smalltalk, for which an extension supporting Traits was created[18, 19]. Use of traits can significantly reduce the overall size of libraries[3].

Mixins[5, 4, 11], Multiple Inheritance[21, 14], Family Polymorphism [9], Del- egation Layers, and Aspect Oriented Programming share with Traits the aim of code reuse. Traits, like Mixins, and unlike classes in Multiple Inheritance, have no superclasses, and thus are not tied to a particular location in an inheritance hierarchy. Traits and Mixins usually represent composition of incomplete implementations, and thus support decomposition at a finer grain than classes. When a trait is used by a class have the semantics of the class is the same as if the trait methods were part of the class itself — this is called the flattening property.

Smalltalk is the first class based language on which traits have been applied. While Smalltalk is dynamically typed, our remit was to apply traits to a statically typed, class based language. In this paper we discuss the design and implementation of Chai , an extension of a small Java-like language with traits.

We identified three different rˆoles for traits in Chai , and so, we designed three languages:

(2)

Chai₁ A language like Java, where traits are purely a mechanism to create classes, and where the application of a trait can only be type-checked after the resulting class has been “flattened”.

Chai₂ Here we extend the remit of traits so that they may be used as types.

This permits checking of traits before their application.

Chai₃ Finally, we allow traits to be substituted for one another dynamically, supporting runtime changes in object behaviour.

In section 2 of this paper we introduce Chai through examples. In sections 3, 4 and 5 we present formal models for Chai1, Chai2 and Chai3. In section 6 we discuss a prototype implementation of these languages, and section 7 contains conclusions and future work.

The prototype implementation and the MSc thesis are available at http://chai-t.sourceforge.net/. An appendix with complete definitions and handwritten proofs is available at http://www.doc.ic.ac.uk/∼scd/ChaiApp.

2 An Example

Figure 1 gives an example of Chai1.¹We define four simple traits: TScreenShape, TPrintedShape, TEmptyCircle and TFilledCircle, which describe corresponding components in a simple graphics program: we can form on screen, or print, empty circles or filled circles in any combination in which we are interested, simply by creating a subclass of Circle that uses the traits providing the behaviour we want. In the example, we show only two of the four combinations, i.e., classes ScreenEmptyCircle and PrintedFilledCircle.

A trait T may declare requirements, i.e., a list of method signatures, for methods that must be provided by classes or traits using T. Here, trait TEmptyCircle requires a method drawPoint with return type void, and two int parameters, and method getradius with no parameters, and int return type.

Class SreenEmptyCircle uses TScreenEmptyCircle; there, the first method is provided by trait TScreenShape and the second by class Circle.

Forming the four combinations using single inheritance would mean consid- erable code duplication, although it could be implemented using multiple inheritance or mixins. See [20] for examples of situations where Traits give more elegant solutions than mixins, and also for examples where mixins give more elegant solutions than traits. Because the trait composition operators are so flexible, Chai1 allows much finer code reuse than Java.

Figure 2 gives an example of the additional features of Chai2, where we allow traits to be used as types. Any object of a class using the trait TScreenShape can be referenced through a variable of type TScreenShape. Allowing traits to define types supports more polymorphism, and it allows us to type check traits independently of the classes that use them.

1 For the sake of simplicity, Chai only allows methods with a single parameter called x, and does not permit sequences of expressions. These restrictions have minimal implications for the presentation of the features we are interested in, and are not adhered to by the examples in this section, nor by the prototype implementation.

(3)

class Circle { int radius;

int getRadius() { ... } }

trait TEmptyCircle { requires {

void drawPoint(int x,int y);

int getRadius();

}

void draw() { ... } }

trait TFilledCircle { requires {

void drawPoint(int x,int y);

int getRadius();

}

void draw() { ... } }

trait TScreenShape {

void drawPoint(int x,int y) { ...

} }

trait TPrintedShape {

void drawPoint(int x,int y) { ...

} }

class ScreenEmptyCircle extends Circle

uses TEmptyCircle,TScreenShape { } class PrintedFilledCircle

extends Circle

uses TFilledCircle,TPrintedShape { }

Fig. 1. Chai1Example

In the final example, in figure 3, we show how dynamic substitution of traits can change the behaviour of an object at runtime. The object circle starts out as an empty circle on screen, but by substitution of TFilledCircle for TEmptyCircle we can change it to a filled circle, and subsequently by substi- tuting TPrintedShape for TScreenShape we can change it to become a printed filled circle.

class ScreenShapeStack {

void push(TScreenShape shape) { ... } TScreenShape pop() { ... }

...

}

ScreenShapeStack stack = new ScreenShapeStack();

stack.push(new ScreenEmptyCircle());

stack.push(new ScreenFilledCircle());

TScreenShape shape = stack.pop();

(4)

class CircleShape extends Circle uses TEmptyCircle,TScreenShape {}

CircleShape circle = new CircleShape(); circle.draw();

// draws an empty circle on screen

circle<TEmptyCircle -> TFilledCircle>; circle.draw();

// draws a filled circle on screen

circle<TScreenShape -> TPrintedShape>; circle.draw();

// prints a filled circle

3 The language Chai

₁

3.1 Syntax

For Chai1 we adapted Traits from Smalltalk[18] to the Java setting. As in [18], traits can be used to add behaviour to classes or to other traits. Traits may contain method definitions, but no fields — as we said earlier, traits are pure behaviour [18]. A trait cannot itself take part in execution (i.e. it cannot be instantiated) — it (or a trait using it) can be used by some class, which can then be instantiated.

Traits are not required to be complete - that is, they may require func- tionality beyond their own to be provided by classes or traits using them. The requirements are declared explicitly in the form of a set of required methods.

program ::== ( trait | class )*

trait ::== trait tr [uses tr +] { (trait-glue | meth)* } field ::== type f ;

meth ::== meth-sig { exp } type ::== cl

trait-glue ::== requires { (meth-sig ; | super-sig ;)* } | exclude { (t.m ;)* } |

alias { (t.m as m ;)* } meth-sig ::== type m(type x)

super-sig ::== type super.m(type x)

class ::== class cl extends cl [uses tr +] { (field | meth)* } cl,tr,m,f ::== identifiers

Fig. 4. Chai1Syntax

A Chai₁program consists of trait and class declarations. A trait declaration consists of a name for the trait, an optional list of used traits (whose behaviour it incorporates), and a trait body. The trait body contains method definitions, and

(5)

“trait glue”, i.e., declaration of required methods, exclude declarations (which exclude methods that would otherwise be incorporated from used traits) and alias declarations (which give new labels to methods incorporated from a used trait).

In contrast to the language in [18] which is untyped and where requirements are inferred automatically, in Chai1 provided and required methods must be declared using a full type signature.² In common with [18], we distinguish required methods into those that must be provided by a class using the trait, and those that must be provided by the superclass of the using class. This was necessary because Java allows explicit access to superclass methods (through the super.m(...) construct), and so if a trait tr is used by a class cl, then superclass method calls inside methods of tr will resolve to methods from the superclass of cl.

A class declaration consists of a name for the class, its superclass, an optional list of used traits (whose behaviour it incorporates), and a class body. The class body contains method definitions and fields.

For simplicity, our model does not support method overloading or field hiding, however we believe it can be easily extended to do so — the implementation of Chai₁ supports it.

Note, that in Chai1classes form types, but traits do not.

3.2 Basic lookup functions

We consider that a program P implicitly defines the following eight (partial) lookup functions:

– P^sup(cl) returns the direct superclass of cl in P.

– P^fld(cl,f) returns the type of field f as defined in class cl.

– P^mth(cl,m) and P^mth(tr,m) return the (possibly empty) set of methods with identifier m defined in class cl or trait tr.

– P^use(cl), or P^use(tr) return the set of traits directly used in class cl, or trait tr.

– P^excl(tr) returns the set of trait and method identifier pairs excluded from trait tr.

– P^alias(tr,m) returns the set of trait and method identifier pairs which are aliases of method m in trait tr.

– P^req(tr) returns the set of method signatures mentioned as required in the declaration of tr.

– P^{req sup}(tr) returns the set of method signatures mentioned as required for the superclass (through t super.m(t⁰x)) in the declaration of tr.

Note that the above functions correspond to direct lookups in the program text, and do not take class inheritance nor traits use into account. In the next section we will define the functions F , F s, M, MSig, and M^orig, which lookup fields, and methods, and which do take class inheritance and traits use into account.

2 In a related work [17], a typed language with automatic inference of required methods is described.

(6)

3.3 Method or field acquisition through traits use and inheritance The function F (P, cl, f) looks up the field f in cl or its superclasses, and returns t where t is the type of f in cl. The function Fs(P, cl) returns the set of fields defined in cl, or inherited from cl’s superclasses. The two functions operate only on classes (traits have no fields).

F (P, Object, f) = ⊥ F (P, cl, f) =

P^fld(cl, f) if P^fld(cl, f) 6= ⊥ P^fld(P^sup(cl), f) otherwise

Fs(P, cl) = { f | F (P, cl, f) 6= ⊥ }

A class cl that uses a trait tr acquires the methods from tr in such a way that externally there is no way to tell that the methods were not declared by cl itself. This forms the basis of the flattening property of traits - a trait formed by using existing traits can be viewed as either a composite entity comprising the used traits and the definitions in the new trait, or as a flattened entity containing all the definitions of its constituents.

We now define M(P, cl, m) and M(P, tr, m), which recursively search the used traits and superclasses. Intuitively, these functions embody give precedence to

“local” declarations: methods defined in a trait body have highest precedence, and methods that have been aliased have higher precedence than methods acquired from used traits. Methods defined in a class body have highest precedence, and methods acquired from used traits have higher precedence than those acquired from superclasses.

M : program × (classId ∪ traitId) × methodId → ℘(methodBody) If tr is a trait :

M(P, tr, m) =







P^mth(P) if P^mth(P) 6= ∅

MsAlias if P^mth(P) = ∅ 6= MsAlias MsUsed if P^mth(P) = ∅ = MsAlias.

where MsAlias =S

tr⁰.m⁰∈P^alias(tr,m)M(P, tr⁰, m⁰) MsUsed =S

tr⁰⁰∈P^use(tr) , tr⁰⁰.m /∈P^excl(tr.m)M(P, tr⁰⁰, m) If cl is a class :

M(P, Object, m) = ∅ M(P, cl, m) =







P^mth(cl, m) if P^mth(cl, m) 6= ∅

MsUsed if P^mth(cl, m) = ∅ 6= MsUsed M(P, P^sup(cl), m) if P^mth(cl, m) = ∅ = MsUsed , where

MsUsed =S

tr∈P^use(cl)M(P, tr, m)

Because there are several ways a trait might acquire a method (from any of the traits it uses), the method lookup functions return sets of methods. If the

(7)

precedence rules do not resolve the method lookup to a single method, i.e., if in a class cl, |M(P, cl, m)| > 1 for some m, then a conflict occurs,³.

A class is complete if it has no conflicts, and if any call to super in any inherited method body resolves without conflict:⁴

∀m : e contains super.m(...) =⇒ |M(P, P^sup(cl), m⁰)| = 1 super resolves without conflict in e and cl

∀m : |M(P, cl, m)| ≤ 1

∀m, cl⁰ P `₁cl ≤ cl⁰, ...{e} ∈ M(P, cl⁰, m) =⇒

super resolves without conflict in e and cl’

P `₁cl cmpl

For class cl, and trait tr, we define the functions MSig₁(P, cl, m), MSig₁(P, tr, m), and MSig₁^sup(P, cl, m) which return the set of signatures for method m as found in cl, tr or the superclass of cl.

MSig₁(P, cl, m) = { t m(t⁰x) | t m(t⁰ x){...} ∈ M(P, cl, m) } MSig₁(P, tr, m) = { t m(t⁰x) | t m(t⁰ x){...} ∈ M(P, tr, m) } MSig₁^sup(P, cl, m) = MSig₁(P, P^sup(cl), m)

Note, that the look up functions M(P, cl, m) and MSig₁(P, cl, m) abstract from the use of traits. Therefore, as we will see later, we were able to write the operational semantics and type system of Chai1and Chai2without explicit mention of traits.

We define the function M^orig which determines the “origin” of a method, i.e., the most specific superclass of a class cl which contains a body for m. We will use M^orig to model the behaviour of super.m( ).⁵

M^orig(P, cl, m) =











cl if P^mth(cl, m) 6= ∅ or ∃tr with tr ∈ P^use(cl) and M(P, tr, m) 6= ∅,

⊥ if cl = Object,

M^orig(P, cl⁰, m) otherwise, for cl⁰= P^sup(cl).

3.4 Operational Semantics

We give a large step semantics for Chai1, where programs map expressions, stacks and heaps, onto results and new heaps. A stack, σ∈ stack, is a triple consisting of the address of the current receiver, the value of the actual parameter

3 Conflicts can be avoided by overriding the conflicting method in the class where the conflict occurs, or by excluding one of the conflicting methods - in our system without overloading this works only if all conflicting methods have the same signature.

4 A simpler, but more restrictive, requirement would be to require no conflicts in any of cl’s superclasses.

5 This formalization of super has been suggested to us by Andrew Black and Chuan- Kai Lin, and slightly adapted by Rok Strnisa.

(8)

; : program → exp × stack × heap → (val ∪ dev) × heap stack = addr × val × classId

heap = addr → object val = { null } ∪ addr

object = { [[ cl || f1: v1, . . . , fr: vr]] | cl ∈ classId, f1,...,fr∈ fldId, v1,...,vr∈ val } addr = { ιn| n is a natural number }

dev = { nllPntrExc, stuckExc }

Fig. 5. Chai1 Runtime

and the class containing the method body currently being executed. The notation σ(this), σ(x), and σ(this class) selects the first, second and third component of σ. A heap, χ∈heap, maps addresses to objects. Objects contain the class of the object (cl), and values (vi) for the object’s fields (fi).

The operational semantics of Chai1 does not mention traits explicitly, and operates entirely in terms of classes; thus it is very similar to that of a small Java-like language (e.g., ClassicJava[11] or Fickle[7]), and is rather standard.

It is given in figure 6. The receiver and the parameter are looked up in the heap (var). If null is dereferenced, a nullPnterExc exception is thrown (null- exception). Field access is evaluated by looking up the particular field in the object (field). Field assignment overrides the corresponding field with the value of the right hand side (field-assign). Object creation creates a new object of the appropriate class, and initializes all its fields with null (new). Method call evaluates the method body found in the dynamic class of the receiver; evaluation takes place in a stack consisting of the receiver and actual parameter of the call, and the identifier of the class containing the method body (method-call). For the call to super the evaluation is similar, but the method is looked up in the static superclass of the class given by σ(this class), i.e., the superclass of the class containing the method currently being executed (super-call). We require the method lookup functions to return a singleton set, i.e., there should be no conflicting method definitions.

For brevity, we omitted the rules throwing stuckErr when conflicting methods are called, or non-existent fields or methods are accessed or called, as well as the rules propagating exceptions stuckExc or nullPntrExc.

3.5 Type System

In figure 7 we define the judgements P ` cl ≤ cl⁰ indicating subtypes, and P ` cl class and P ` tr trait indicating that cl is a class or tr is a trait. We also define the judgement P ` t typeindicating that t is a type.

For type checking we use a typing environment Γ which maps the receiver, this, and the method parameter, x, to a class name. The typing judgement P, Γ `₁ e : t means that in the context of program P and environment Γ, in the type system of Chai1, the expression e has type t. Although in Chai1only classes

(9)

null null-exception

null, σ, χ ;P null, χ

e, σ, χ ;P null, χ⁰

e.f := e⁰, σ, χ ;P nllPntrExc, χ⁰ e.f, σ, χ ;P nllPnterExc, χ⁰ e.m(e⁰), σ, χ ;^P nllPntrExc, χ⁰

field var

e, σ, χ ;P ι, χ⁰

e.f, σ, χ ;P χ⁰(ι)(f), χ⁰

x, σ, χ ;P σ(x), χ this, σ, χ ;P σ(this), χ

field-assign new

e, σ, χ ;P ι, χ⁰⁰ e⁰, σ, χ⁰⁰ ;P v, χ⁰⁰⁰ χ⁰ = χ⁰⁰⁰[ι 7→ χ⁰⁰⁰(ι)[f 7→ v]]

e.f := e⁰, σ, χ ;P v, χ⁰

Fs(P, cl) = f1, . . . fr

∀k ∈ 1, . . . r : vk= null ι is new in χ

new cl, σ, χ ;P ι, χ[ι 7→ [[ cl || f1: v1, . . . fr: vr]]]

method-call super-call

er, σ, χ ;P ι, χ0

ea, σ, χ0 ;P v1, χ1

χ1(ι) = [[ cl || . . . ]]

M(P, cl, m) = { t m(t⁰x) { e } } M^orig(P, cl, m) = cl⁰

σ⁰= (ι, v1, cl⁰) e, σ⁰, χ1 ;P v, χ⁰ er.m(ea), σ, χ ;P v, χ⁰

ea, σ, χ ;P v1, χ1

σ(this class) = cl P^sup(cl) = cl⁰⁰

M(P, cl⁰⁰, m) = { t m(t⁰x) { e } } M^orig(P, cl⁰⁰, m) = cl⁰

σ⁰= (σ(this), v1, cl⁰) e, σ⁰, χ1 ;P v, χ⁰

super.m(ea), σ, χ ;P v, χ⁰ Fig. 6. Chai1Operational Semantics

can be types, the type rules in figure 8 mention types t rather than classes cl;

this generality allows us to reuse these type rules for Chai₂.

P = ... class cl extends cl⁰ . . . P `₁cl ≤ cl

P `₁cl ≤ cl⁰ P ` cl class

P `₁cl type

P `₁cl ≤ cl⁰ P `1cl⁰≤ cl⁰⁰ P `1cl ≤ cl⁰⁰

P = ... trait tr ...

P ` tr trait

Fig. 7. Subclasses and Subtypes in Chai1

(10)

subsumption var-this P, Γ `₁ e : t

P `1t ≤ t⁰ P, Γ `1 e : t⁰

P, Γ `₁ x : Γ(x) P, Γ `1 this : Γ(this)

new null

P `₁cl cmpl

P, Γ `₁ new cl : cl

P `₁t type

P, Γ `₁ null : t

field field-assign

P, Γ `₁ e : cl F (P, cl, f) = t P, Γ `1 e.f : t

P, Γ `₁ e : cl P, Γ `₁ e⁰ : t F (P, cl, f) = t P, Γ `₁ e.f := e⁰ : t

method-call super-call

P, Γ `1 er : tr

P, Γ `₁ ea : ta

MSig₁(P, tr, m) = { t m(tax) } P, Γ `1 er.m(ea) : t

Γ(this) = tr

P, Γ `₁ ea : ta

MSig^sup₁ (P, tr, m) = { t m(tax) } P, Γ `₁ super.m(ea) : t

Fig. 8. Chai1Type Rules

The type rules, given in figure 8, do not explicitly mention traits, because traits have already been taken into account through MSig₁( , , ) and MSig^sup₁ ( , , ). They are standard in all other respects: An expression of a certain type also has any of its supertypes (subsumption). The type of the formal parameter and receiver are looked up in the type environment (var-this). The creation of a new object has the type of that class, provided that the class is complete (new), while null has any type (null). The type of a method call is the return type of the function found by looking in the class of the first expression through MSig

1(P, cl, m), provided that the second expression has the type of the formal parameter type (method-call). Similarly for (super-call), where the method is looked-up in the superclass through MSig^sup₁ (P, cl, m).

Note, that required methods do not play any rˆole in Chai1 type-checking (they do play a rˆole in Chai2and Chai3type checking).

In figure 9 we define the notion of a well-formed Chai1class, i.e., P `1 cl . A class cl is well-formed if:

(11)

1. Any field defined in that class has a valid type, and is not defined in its superclass cl⁰;

2. Any method defined in the class, or acquired though usage of a trait or inheritance from a superclass, has return and parameter type which are valid types, and, in a typing environment which maps x to the argument type t1

and this to cl (such an environment is written as t1x, cl this), the method body has the declared return type t0. Additionally, if this method is present in the superclass, or any used traits, then it must be defined there with the same return type and parameter type.

The requirement 2. from above is very strong: It checks all inherited and acquired methods in a class - rather than just the methods defined in the class itself. Thus, a method defined in a trait will be type checked in all classes using that trait;

this is unavoidable, because in Chai₁ method bodies cannot be checked in the traits.

A program is well-formed, `₁P, if all its classes are well-formed. Note that the traits are not checked. Note also, that we do not require the inheritance hierarchy to be acyclic; although this is convenient, it is not necessary for soundness; in a program with cyclic inheritance, meaning can be given to lookup functions (M, M^orig) through least fixed points.

P^sup(cl) = cl⁰

∀f : P^fld(cl, f) = t =⇒ F (P, cl⁰, f) = ⊥, P `₁t type

∀m : t0m(t1x){e} ∈ M(P, cl, m) =⇒

P `₁t0type

P `1t1type

P, t1x, cl this `₁e : t0

M(P, cl⁰, m) = ∅ ∨ M(P, cl⁰, m) = { t0m(t1x) {. . .} } P `1 cl

for all classes cl defined in P: P `1 cl

`₁P

Fig. 9. Well formed classes and programs in Chai1

3.6 Type Soundness

The judgement P, σ ` v / t in figure 10 means that the value v agrees with the type t. In particular, if v is an address, it requires that the object at v belongs to a class cl which is a subtype of t, and for all fields defined in cl, the object contains values which agree with the types of the fields as declared in

(12)

cl.⁶The judgement P, Γ `₁σ, χ means that the objects in the heap χ agree with their classes, and belong to complete classes (i.e., no conflicts), that the receiver object and argument value agree with their type as given in Γ, and that the class containing the method currently being executed (σ(this class)) is the same as the type of the receiver in the type environment (Γ(this)).

P `1t type

P, χ `1null / t

χ(ι) = [[ cl || . . . ]]

P `1cl ≤ t

F (P, cl, f) = t⁰=⇒ P, χ `₁χ(ι)(f) / t⁰ P, χ `₁ι / t

∀ι : χ(ι) = [[ cl || . . . ]] =⇒ P, χ `1ι / cl, and P `1cl cmpl

P, σ `₁σ(this) / Γ(this) P, σ `1σ(x) / Γ(x) σ(this class) = Γ(this) P, Γ `₁σ, χ

Fig. 10. Agreement in Chai1

The following lemma is crucial in the proof of soundness, and guarantees that 1-2) the existence and types of fields and methods is preserved to subclasses, 3) that there are no more than one method signature per method in a superclass of a complete class (although there can be several method bodies, and 4) that if a method has a certain signature in a superclass cl’, then method lookup in the subclass cl will return a method body which type checks with this signature in the class cl⁰⁰which contains this method body (or inherits it from a trait).

Lemma 1 If `₁P and P `₁cl ≤ cl⁰ then:

1. F (P, cl⁰, f) = t =⇒ F (P, cl, f) = t.

2. MSig

1(P, cl⁰, m) ⊆ MSig₁(P, cl, m).

3. P `₁cl cmpl =⇒ | MSig₁(P, cl⁰, m) | ≤ 1.

4. t m(t⁰x) ∈ MSig₁(P, cl⁰, m) =⇒ ∃cl⁰⁰, e :

– M^orig(P, cl, m) = cl⁰⁰, t m(t⁰x){e} ∈ M(P, cl, m), – P `₁cl ≤ cl⁰⁰ P, t⁰x, cl⁰⁰this `₁e : t.

We can now prove soundness of the type system:

Theorem 2 (Type Soundness of Chai1) For program P, typing environment Γ, expression e, so that super resolves without conflict in e and Γ(this class), stack σ, heap χ, and type t:

If

`₁P and P, Γ `₁ e : t and P, Γ `₁σ, χ and e, σ, χ ;P r, χ⁰

6 Although the definition of P, χ `1ι / t is recursive, there exists an equivalent non- recursive definition for it.

(13)

then:

P, Γ `₁σ, χ⁰ and P, χ⁰ `₁r / t or r = nllPntrExc.

In other words, execution of well typed expressions preserves well formedness of the heap and stack, does not get stuck (since r is either a value or a null pointer exception), and if it returns a value, then this value is of the same type as the original expression.

4 The language Chai

₂

In Chai2 we extended the remit of traits, so that they may be used as types.

This has three important repercussions:

First, we can treat in a uniform way objects whose class uses a given trait, e.g., we can write a stack for screenshapes, as in figure 2. Thus, traits support polymorphism, play the role of interfaces, and introduce multiple supertypes.

Second, we can typecheck traits in isolation, and therefore, we will be able to type check a method defined in a trait only once, rather than having to check it again in all the classes using that trait.

Third, we can take required methods into account, and can type check calls to required methods which do not have a method body in the receiver’s class or trait. This is safe, because we allow object creation only for complete classes, and Chai2complete classes are those that provide method bodies for all required methods.

4.1 Chai2 Syntax and Operational Semantics

The only difference between the syntax of Chai2and that of Chai1is that Chai2

allows traits to be types, i.e:

type ::= cl | tr

The operational semantics of Chai2 is identical to that of Chai1.

4.2 Required Methods

We fist define indirect use of traits, where U se^∗(P, tr) collects the transitive closure of the traits used in tr, and U se^∗(P, cl) collects all traits indirectly used by traits used in cl, or in cl’s superclasses.

U se^∗(P, tr) = S

tr⁰∈P^use(tr)U se^∗(P, tr⁰) ∪ { tr } U se^∗(P, cl) = S

P `₁cl≤cl⁰, tr∈P^use(cl⁰)U se^∗(P, tr)

A trait tr may define a list of required methods. A second trait tr⁰ which uses tr inherits tr’s required methods and may add new requirements of its own, through explicit requirements or through exclusion. A class using tr inherits the requirements of tr.

(14)

MReq(P, tr, m) = S

tr⁰∈U se^∗(P,tr)P^req(tr⁰) ∪ S

tr⁰∈U se^∗(P,tr){ t m(t⁰x) | ∃tr⁰⁰: (tr⁰⁰, m) ∈ P^excl(tr⁰), t m(t⁰x) ∈ MSig

1(P, tr⁰⁰, m) ∪ MReq(P, tr⁰⁰, m) )}

MReq(P, cl, m) = S

tr∈U se^∗(P,cl)MReq(P, tr, m) MReq^sup(P, tr, m) = S

tr⁰∈U se^∗(P,tr)P^{req sup}(tr⁰) MReq^sup(P, cl, m) = S

tr∈U se^∗(P,cl)MReq^sup(P, tr, m)

Note, that it is possible for a signature to be required in a trait tr, and for the trait to have a method body for this signature. Similarly for classes.

A class which is complete in the sense of Chai1, and where all required methods have a body is complete for Chai2:

∀m : t m(t⁰x) ∈ MReq(P, cl, m) =⇒ ∃e : t m(t⁰x){e} ∈ M(P, cl, m)

∀m : |M(P, cl, m)| ≤ 1

∀m, cl⁰ P `₁cl ≤ cl⁰, ...{e} ∈ M(P, cl⁰, m) =⇒

super resolves without conflict in e andcl⁰ P `₂cl cmpl

Thus, a complete subclass of t will provide a method body for any method required by t. The function MSig₂(P, t, m) returns the signatures of the method that will be provided for m by a complete subclass of t, while the function MSig^sup

2 (P, t, m) returns the signatures of all methods that will be provided in the superclass of a complete subclass of t:

MSig₂(P, tr, m) = MSig₁(P, tr, m) ∪ MReq(P, tr, m) MSig₂(P, cl, m) = MSig₁(P, cl, m) ∪ MReq(P, cl, m) MSig^sup₂ (P, tr, m) = MSig₁^sup(P, cl, m) ∪ MReq^sup(P, tr, m) MSig^sup₂ (P, cl, m) = MSig₁^sup(P, cl, m) ∪ MReq^sup(P, cl, m) Notice, that t ∈ P^use(t⁰) implies that MSig₂(P, t, m) ⊆ MSig₂(P, t⁰, m) for all m, and class or trait t, and t⁰.

4.3 Type System

As we define in figure 11, a class or trait is a subtype of any trait that it uses - possibly indirectly. Thus, a class cl or trait tr that uses a trait tr⁰is a subtype of tr⁰, even if tr requires more methods than tr⁰. This may seem surprising, but it is safe for the following reason: even though traits are types, the runtime entities (i.e. the objects) will belong to complete classes, which, by definition, provide a method body for any required method. The ensuing subtype relationship is transitive.

Note that P `₂t⁰ ≤ t implies that MSig₂(P, t, m) ⊆ MSig₂(P, t⁰, m) - we could have defined subtypes in a structural, rather than a nominal way using the above property.

(15)

P ` tr class

P `₂cl type

P ` tr trait

P `₂tr type

P `₁cl ≤ cl⁰ P `₂cl ≤ cl⁰

tr ∈ U se^∗(P, cl) P `₂cl ≤ tr

tr ∈ U se^∗(P, tr⁰) P `₂tr⁰≤ tr Fig. 11. Types and Subtypes in Chai2

In Chai2 traits can be types, therefore in Chai2 typing environments may map this, and x to a trait or a class. The typing rules are the same as those for Chai1, with three exceptions. First, the subsumption rule uses the new subtype relation P `2t⁰≤ t. Second, the rules method-call and super-call take the required method into account, i.e., use MSig₂(P, t, m) and MSig^sup₂ (P, t, m).

Third, the rule new requires the class to be complete according to P `2cl cmpl. A trait tr is well formed, i.e., P `2 tr in figure 12, if the methods directly defined in that trait are well-typed, and have the same signature as any method with the same identifier acquired from a used trait.

A class cl is well formed, i.e., P `2 cl, if the fields in that class have well- formed types; and if the methods directly defined in that class are well-typed, and have the same signature as any method acquired from a used trait, or inherited from a superclass. A program is well formed, if all its classes and traits are well formed.

Notice that, to establish P `₂ t we only check the methods directly defined in class or trait t; (we use P^mth(cl, m) - as opposed to M(P, cl, m) in Chai1). Also, P `₁ t does not imply P `₂ t, and nor does P `₂ t imply P `₁ t.

4.4 Type Soundness

In Chai₂we retain the definition of agreement between objects and classes from figure 10, but use the subtype relation P `₂t ≤ t⁰, and the definition of complete classes P `₂cl cmpl from this section.

Thus, we were able to give “uniform” definitions of Chai₁ and Chai₂, and distill their similarities and differences.

The following lemma is the counterpart to lemma 1; the difference is that here we talk of types (and thus also of traits) rather than just of classes, we use the Chai2 subtype relationship with also incorporates traits usage, and in the Chai2 signature lookup function we also take the requirements into account.

Lemma 3 If `₁P and classes cl, cl⁰ and types t and t⁰, with P `₂cl ≤ cl⁰, P `₂t ≤ t⁰, and P `₂cl ≤ t⁰, then:

1. MSig₂(P, t⁰, m) ⊆ MSig₂(P, t, m).

2. P `₂cl cmpl, =⇒ | MSig

2(P, t⁰, m) | ≤ 1.

3. P, tax, t⁰this `₂e : t⁰⁰ =⇒ P, t_ax, t this `₂e : t⁰⁰. 4. P `2cl cmpl, t⁰⁰ m(t⁰⁰⁰x) ∈ MSig₂(P, t⁰, m) =⇒ ∃cl⁰⁰, e :

– M^orig(P, cl, m) = cl⁰⁰, t⁰⁰ m(t⁰⁰⁰x){e} ∈ M(P, cl⁰⁰, m),

(16)

∀m : t0m(t1x){e} ∈ P^mth(P) =⇒

P `2t0type

P `₂t1type

P, t1x, tr this `2e : t0

∀tr⁰: tr⁰∈ P^use(tr) =⇒

MSig₂(P, tr⁰, m) = ∅ ∨ MSig₂(P, tr⁰, m){t0m(t1x)}

P `2 tr cl⁰= P^sup(cl)

∀f : P^fld(cl, f) = t =⇒ P `2t type, F (P, cl⁰, f) = ⊥

∀m : t0m(t1x){e} ∈ P^mth(cl, m) =⇒

P `2t0type

P `₂t1type

P, t1x, cl this `2e : t0

MSig₂(P, cl⁰, m) = ∅ ∨ MSig₂(P, cl⁰, m) = {t0m(t1x)}

∀tr ∈ P^use(cl) : MSig

2(P, tr, m) = ∅ ∨ MSig

2(P, tr, m) = {t0m(t1x)}

P `2 cl

for all classes cl defined in P : P `2 cl for all traits tr defined in P : P `₂ tr

`₂P

Fig. 12. Well-formed traits, classes and programs in Chai2

– P `₁cl ≤ cl⁰⁰ P, t⁰⁰⁰x, cl⁰⁰this `₂e⁰⁰ : t⁰⁰.

With the above lemma we can prove soundness for the type system of Chai2: Theorem 4 (Type Soundness of Chai₂) For any program P, environment Γ, expression e with super resolves without conflict in e and Γ(this class), stack σ, type t, where `₂P, and P, Γ `₂ e : t and P, Γ `₂σ, χ and e, σ, χ ;P r, χ⁰:

P, Γ `₂σ, χ⁰ and P, χ `₂r / t or r=nllPntrExc.

5 The language Chai

₃

Chai3introduces dynamic trait substitution. Since traits specify pure behaviour, it should be possible to substitute one trait for another at runtime in order to change the behaviour of an object. Outwardly, the interface of the object would remain the same, providing the same fields and methods, but internally the implementation of various methods could be altered.

Although the idea of objects changing behaviour at runtime (dynamic object re-classification) has been presented in several different forms[7, 22], the only time this concept has been explored in the existing literature on traits⁷is relation to the object-based language SELF[1, 22], where dynamic changes in behaviour

7 The authors of [18] mention using traits to dynamically change object behaviour as an element of future work.

(17)

can be obtained by changing which object acts as the parent of the current object. We present a mechanism supporting dynamic traits inspired by the ideas from SELF, but in a class-based language.

5.1 Example

Consider a graphical windowing system: A window in this system may be an OpenedWindow or an IconifiedWindow. In each state the window will behave differently, and a window may change between these two states at any time.

To implement this in traditional Object Oriented programming, we would need to use wrappers, or some form of the state pattern.

Using dynamic substitution of traits, we can offer a more elegant, and direct solution: we define a class Window, and two traits TOpened and TIconified, where TOpened and TIconified provide and require the same sets of method signatures, but provide different implementations of the methods and so different behaviour. We define the class Window as class Window uses TOpened ... (the window begins in the opened state). Then, for a Window object w (Window w = new Window();) we can change to the iconified state using the statement w<TOpened 7→TIconified>. This will result in the substitution of the trait TIconified for the trait TOpened inside the object w.

Since the class Window was declared as using the trait TOpened, the label TOpened becomes a “placeholder” for that trait used by Window, and a trait

“compatible” with TOpened can be substituted for TOpened at any time. We use the label TOpened in all further substitutions for that trait “placeholder” of w.

For example, to switch back to the original behaviour of w, we write w<TOpened 7→TOpened> (and not, as might be imagined, w<TIconified 7→TOpened>).

5.2 Chai3 Syntax and Operational Semantics

We extended the syntax of expressions to allow trait substitution.

exp ::= exp< tr 7→ tr > | ...

Resolving Method Calls Consider the program given in figure 13. If we create an object of class C, e.g C x = new C, then obviously executing x.m1() will return the value 3, and executing x.m2() will also return the value 3.

If we execute x < TrtB 7→ TrtB2 > followed by x.m1(), then the version of m1 provided by TrtA will be used, since the method m1 was originally provided to class C by trait TrtA, and no trait has replaced TrtA in c.

If we execute x < TrtB 7→ TrtB2 > followed by x.m2(), then the situation is more complex. Obviously, the method m2 defined in TrtB2 will be executed (since TrtB originally provided m2, and TrtB has been replaced by TrtB2). However, there are three possibilities for the binding of m1 from within the body of m2:

1. The version of m1 from TrtA will be used; because invoking a method from within a trait should have the same semantics as invoking it from within the class using the trait. Thus, we resolve methods based on the flattened version of the class using the traits.

(18)

trait TrtA { int m1() { 3 } } trait TrtB {

requires { int m1(); } int m2() { this.m1() } }

trait TrtB2 {

int m2() { this.m1() } int m1() { 5 }

}

class C uses TrtA,TrtB { }

Fig. 13. Resolving Method Calls in Chai3

2. The version of m1 from TrtB2 will be used; because the methods in TrtB2 are interrelated, it is likely that the implementor of TrtB2 intended the call to m1 to resolve to the method in TrtB2. Thus, we resolve methods based on the trait in which the call was found.

3. The situation is illegal; i.e., trait TrtB2 cannot be substituted for trait TrtB because it creates this “ambiguity” regarding the definition of method m1.

In this paper, we chose option 1 from above, because of its close relationship to the flattening property which is a crucial element of Traits philosophy.

Object Representation Substitution of traits at runtime is on a per-object basis (rather than a per-class basis). This means that while the list of traits used by any class remains constant, for every object of that class, each used trait may be associated with some (possibly different) trait. Therefore, we extend the representation objects from figure 5 with a list of trait substitutions that have been made to the object.

object = { [[ cl || f₁: v₁, ...f_r: v_r || tr1: tr⁰₁, ...tr_n: tr⁰_n]] |

cl, f₁, ...f_r, tr₁, ...tr_n, tr⁰₁, ...tr⁰_nidentifiers; v₁, ...v_r∈ val } To access and update these trait substitutions for an object o = [[ cl || ... || tr1: tr⁰₁, ...trn: tr⁰_n ]], we define trait lookup o(tr) which finds the current substitution for a given trait name, and object mutation o[tr 7→ tr⁰] which replaces the trait named tr by tr⁰.

o(tr) =

tr⁰_k if tr=trk for some k∈1, ...n

⊥ otherwise.

o[tr 7→ tr⁰] = [[ cl || ... || tr1: tr⁰₁... trk: tr⁰...trn: tr⁰_n ]] for tr=trk, k∈ 1,...,n

⊥ otherwise.

Runtime Method Lookup and Operational Semantics Trait substitutions must be taken into account for method call. The function M₃finds the appropriate method body, taking both the class of the object, and the object itself

(19)

into account – the latter is needed, in order to find the traits that have replaced the original ones. M₃first determines which class or trait name is “responsible”

for the corresponding method through M₃^resp(P, cl, m), which first searches the current class, then the used traits, and then continues with the superclass. If M3resp(P, cl, m) is a class cl⁰ then the method body is found directly in cl⁰. If M3resp(P, cl, m) is a trait tr then the method body is found in trait tr⁰, which replaces tr in the current object (i.e., o(tr) = tr⁰).

M3resp

(P, tr, m) = { tr } if P^mth(tr, m) 6= ∅ S

tr⁰∈P^use(tr)M3resp

(P, tr⁰, m) otherwise.

M3resp(P, cl, m) =











{ cl } if P^mth(cl, m) 6= ∅

Trts where Trts =S

tr∈P^use(cl)M3resp(P, tr, m) if Trts 6= ∅ = P^mth(cl, m)

M3resp

(P, P^sup(cl), m) otherwise.

M3(P, cl, o, m) =







P^mth(cl⁰, m) if M3resp

(P, cl, m) = {cl⁰} P^mth(tr⁰, m) if M3resp

(P, cl, m) = {tr}, and o(tr) = tr⁰

⊥ otherwise.

A class cl is complete in Chai3 if it provides a method body for any required method, if there are no conflicts for any superclass (this simplifies the treatment of super), and if M3resp(P, cl, m) is empty or a singleton.

∀m : t m(t⁰x) ∈ MReq(P, cl, m) =⇒ ∃e : t m(t⁰x){e} ∈ M(P, cl, m)

∀m, cl⁰ P `₁cl ≤ cl⁰, |M(P, cl⁰, m)| ≤ 1

∀m : | M3resp(P, cl, m) | ≤ 1 P `₃cl cmpl

The operational semantics of Chai₃differs from that of Chai₁and Chai₂in the handling of mutation, object creation, and method call, therefore, we extend the semantics from figure 6. A mutate expression substitutes one trait by another (mutate). Object creation initializes the fields and the list of trait substitutions for new objects through the identity substitution, i.e. associates all traits with themselves (new).

mutate

e, σ, χ ;P ι, χ⁰⁰

χ⁰ = χ⁰⁰[ι 7→ χ⁰⁰(ι)[tr 7→ tr⁰]]

e < tr 7→ tr⁰ >, σ, χ ;P ι, χ⁰

new Fs(P, cl) = { f1, . . . , fr }

{ tr1, . . . trn } = U se^∗(P, cl) ι is new in χ

o = [[ cl || f1: null...fn: null ||

tr₁: tr1...trn: trn]]

new cl, σ, χ ;P ι, χ[ι 7→ o]

In method call we use the new method lookup function M3(P, c, o, m) (method-call). Thus, if a trait is used in class cl through two different paths

(20)

(e.g., used by cl, and also by cl⁰, where cl⁰ is cl’s superclass), then mutation of the trait will affect the behaviour of its methods regardless of the path used to access the object (e.g., as a value of type cl, or cl⁰) - this is consistent with the flattening property. On the other hand, if a trait tr which uses trait tr⁰ is replaced by tr⁰⁰, then only the methods directly provided by tr will be looked up in trait tr⁰⁰; the ones that were inherited by tr⁰ will remain unaffected. This is, in some sense, inconsistent with the flattening property, and in further work we would like to investigate alternatives.

method-call e_r, σ, χ ;P ι, χ0

e_a, σ, χ0 ;P v₁, χ1

χ1(ι) = [[ cl || . . . ]]

M3(P, cl, χ₁(ι), m) =

{ t m(t⁰ x) { e } } M^orig(P, cl, m) = cl⁰

σ⁰= (ι, v1, cl⁰) e, σ⁰, χ₁ ;P v, χ⁰ e_r.m(ea), σ, χ ;P v, χ⁰

super-call e_a, σ, χ ;P v₁, χ1

σ(this class) = cl P^sup(cl) = cl⁰⁰ M3(P, cl⁰⁰, χ₁(ι), m) =

{ t m(t⁰ x) { e } } M^orig(P, cl⁰⁰, m) = cl⁰

σ⁰= (σ(this), v1, cl⁰) e, σ⁰, χ₁ ;P v, χ⁰

super.m(e_a), σ, χ ;P v, χ⁰

5.3 Type System

The judgment P ` tr⁰. tr says that trait tr⁰ may replace another trait tr. It requires that tr⁰provides all the methods that tr does (with the same signatures, but possibly different bodies), and that any methods provided or required by tr⁰ are also provided or required in tr.

P ` tr trait P ` tr⁰trait

∀m : t0m(t₁x){. . . } ∈ P^mth(tr, m) =⇒ t0m(t₁x){. . . } ∈ P^mth(tr⁰, m)

∀m : MSig₂(P, tr⁰, m) ⊆ MSig₂(P, tr, m) P ` tr⁰. tr

We require MSig₂(P, tr⁰, m) ⊆ MSig₂(P, tr, m)⁸ because P ` tr⁰. tr and P, t⁰ x, tr⁰ this `₃e : t should imply P, t⁰ x, tr this `₃e : t – namely, if an object contains a trait placeholder tr, which is replaced by tr⁰, then it may execute method body e which was defined in tr⁰. To satisfy P, t⁰ x, tr this `₃e : t for the case where e=this, we need P `₃tr ≤ tr⁰, which requires MSig₂(P, tr⁰, m) ⊆ MSig₂(P, tr, m).

In our example, ` TrtB2 . TrtB, and 6` TrtB . TrtB2 – because TrtB2 has a method body for m1, and TrtB has not.

Because trait substitutability implies subtypes, in Chai₃we extend the subtype relationship from figure 7 as follows:

8 Andrew Black suggested to us that we could weaken our original requirement of MSig₂(P, tr⁰, m) = MSig₂(P, tr, m).

(21)

P `₂t⁰ ≤ t P `₃t⁰ ≤ t

P ` tr⁰ . tr P `₃tr ≤ tr⁰

P `₃t⁰≤ t⁰⁰ and P `₃t⁰⁰≤ t P `₃t⁰ ≤ t

The type system of Chai3 is identical to that of Chai2, except for the new definition of subtypes (P `3t⁰≤ t) and complete classes (P `3cl cmpl), and the addition of the rule for mutation expressions. It requires that the type of e should be any class or trait t, that t should be using a trait tr, and that tr⁰may replace trin t. Then, the substitution of tr through tr⁰ in e has type t:

mutate P, Γ `₃ e : t

tr ∈ U se^∗(P, t) P ` tr⁰. tr

P, Γ `₃ e < tr 7→ tr⁰> : t

5.4 Type Soundness

Agreement for Chai3is defined in the following. In addition to the properties for agreement in Chai2, for Chai3 we use the new subtype relation (P `3cl ≤ t), and require that all traits used by class cl should appear in the representation of the objects, and that all traits have been replaced by substitutable traits:

χ(ι) = [[ cl || . . . || tr₁: tr⁰₁, ..., tr_n: tr⁰_n ]]

{ tr₁...tr_n } = U se^∗(P, cl)

∀i ∈ 1, ...,n : P ` tr⁰_i. tri

P `₃cl ≤ t

F (P, cl, f) = t⁰ =⇒ P, χ `₃χ(ι)(f) / t⁰ P, χ `₃ι / t

The counterparts to the properties from lemmas 1 and 3 hold for Chai3. Lemma 5 For program P with `₃P, classes cl, cl⁰, types t, t⁰, t⁰⁰, with P `₃cl ≤ cl⁰, and P `3t ≤ t⁰:

1. F (P, cl⁰, f) = t =⇒ F (P, cl, f) = t.

2. MSig

2(P, t⁰, m) ⊆ MSig₂(P, t, m).

3. P, t_ax, t⁰this `₃e : t⁰⁰ =⇒ P, t_ax, t this `₃e : t⁰⁰.

4. P, σ `₃ι / cl, and P `₃cl cmpl, and M^orig(P, cl⁰, m) = { cl⁰⁰ }, and t0 m(t₁x){e} ∈ M₃(P, cl, χ(ι), m), =⇒

– P `₃cl⁰≤ cl⁰⁰

– P, t1x, cl⁰⁰this `₃e⁰⁰ : t0.

5. t0m(t₁x) ∈ MSig₂(P, t, m), and P, σ `₃ι / cl, and P `₃cl⁰ ≤ t, and P `₃cl cmpl =⇒ M3(P, cl⁰, χ(ι), m) = { t0m(t₁x){ ... } }.

We can now prove soundness for the type system of Chai3:

(22)

Theorem 6 (Type Soundness of Chai₃) For any program P, environment Γ, expression e, stack σ, heap χ, type t, where `₃P, and P, Γ `₃ e : t and P, Γ `₃σ, χ and e, σ, χ ;P r, χ⁰:

P, χ⁰ ` r / t or r = nullPointerExc and P, Γ `₃σ, χ⁰.

6 Implementation

This section describes the translation of a program in Chai (the source language) to one in Java (the target language). This is implemented by a mapping from traits and classes in Chai to entities in Java⁹ There are several possible mappings we could have chosen for this purpose; we could map a class (and all the behaviour it includes from traits) in Chai to a single class in Java. Instead, we choose a slightly more complex mapping, which represents traits in Java by classes which are instantiated to give proxy objects to which behaviour can be delegated by a class which uses those traits. This allows us to implement the dynamic trait substitution of Chai₃.

Every trait tr is represented by an object of type tr impl, and contains a field called user proxy of type tr user. The user proxy field always stores a reference to an object of the trait or class that uses this trait. Also, for any class or trait, there are fields tr⁰ proxy for all traits tr⁰ used by the class or trait.

Each of these is a reference to an object of the relevant type tr⁰ interface Take, for example, a class D which uses a trait T3, and T3 uses traits T1 and T2. Because T3 ∈ Pûse(D), the D object contains a reference to a T3 impl object. Similarly because T1 ∈ Pûse(T3) and T2 ∈ Pûse(T3), the T3 object contains references to T1 impl and T2 impl objects.

In order for this arrangement to be type correct, all classes tr impl must implement tr interface, and also tr⁰ user for all tr⁰ such that tr⁰∈ P^use(tr).

Additionally, classes that use traits must implement the appropriate tr user interfaces (in the example, T3 ∈ P^use(D) and so D must implement T3 user).

The reason that the type of the fields tr proxy is tr interface (and not tr impl) is to allow different values stored in the field to refer to different trait implementation objects (provided that they implement tr interface), and support trait substitutions (under the restrictions described by Chai3).

In more detail, every trait tr in Chai is mapped to three entities in Java:

1. A trait interface containing all the provided methods of tr.

2. A trait-user interface containing all the required method signatures (i.e.

those expected to be provided by the user of the trait tr), as well as all the provided method signatures of tr (see below).

3. A trait implementation class which contains the definitions for the provided methods of the trait, proxy fields for the user of the trait and all used traits, as well as delegation method stubs for acquired methods, which forward method calls to the used trait proxy objects.

9 Similarly, Java-mixins were implemented through a mapping from Jam into Java[2].

(23)

A class in Chai is mapped to a class in Java, with the addition of proxy fields for used traits, implements declarations for the trait-user interfaces of traits used by the class, and method stubs for acquired methods and superclass methods required by a used trait.

To preserve the intended semantics of the flattening property (see section 3.3), it is necessary that the use of the expression this within a trait proxy is translated to refer the object belonging to the class which uses the trait (note that there may be several levels of intervening trait proxies between the trait proxy and this object). The reason that this is necessary, is that declarations of methods

“most local” to the eventual user of a trait have precedence, therefore to preserve the flattening property, we must start the search for a method implementation from this user object itself and work upward into traits represented by proxy objects.

Prototype The prototype implementation of the compiler is written in Java. At present it supports all of the features of Chai₁, and would easily accommodate extensions to support Chai₂and Chai₃. The compiler, including full source code, is available from http://chai-t.sourceforge.net/.

7 Conclusions, related and further Work

We have developed three extensions to a minimal Java-like language incorpo- rating traits, have proven soundness of the type systems, and have outlined our prototype implementation.

The main issues we had to address during the design of Chai were:

– The precise semantics of using a trait as part of a class in Java;

– How to perform type-checking on traits, and in particular how to avoid having to type-check the same method body in each class that uses a trait;

– The reflection of calls to super in the requirements part of traits

– In how far classes have to be complete, i.e., provide method bodies for all the methods required by the traits they are using;

– Subtype relationships between classes and traits, as required in Chai2; interestingly, a trait may require more methods than a supertype trait;

– Dynamic substitution of traits, and the semantics of method lookup in Chai3; – The trait substitutability relationship in Chai3; interestingly, substitutability

in Chai3does not imply subtype in Chai2.

Recently, and especially after the application of traits to Smalltalk [18, 19], the interest in traits has boomed. In [10] a imperative calculus for traits in the language Moby is developed. The acquisition of methods trough the use of traits is modeled through “class evaluation” which returns flattened classes. As in our work, alias and exclusion of methods in [10] is accompanied by method signatures; unlike our work, traits in [10] may require the presence of fields.