Gradual Typing for Generics
Lintaro Ina

Atsushi Igarashi

Graduate School of Informatics, Kyoto University
ina@kuis.kyoto-u.ac.jp

Graduate School of Informatics, Kyoto University
igarashi@kuis.kyoto-u.ac.jp

Abstract
Gradual typing is a framework to combine static and dynamic typing in a single programming language. In this paper, we develop a gradual type system for class-based objectoriented languages with generics. We introduce a special
type to denote dynamically typed parts of a program; unlike dynamic types introduced to C♯ 4.0, however, our typesystem allows for more seamless integration of dynamicallyand statically typed code.
We formalize a gradual type system for Featherweight GJ
with a semantics given by a translation that inserts explicit
run-time checks. The type system guarantees that statically
typed parts of a program do not go wrong, even if it includes
dynamically typed parts. We also describe a basic implementation scheme for Java and report preliminary performance
evaluation.
Categories and Subject Descriptors D.3.1 [Programming
Languages]: Formal Definitions and Theory; D.3.2 [Programming Languages]: Language Classifications—objectoriented languages; D.3.3 [Programming Languages]: Language Constructs and Features—classes and objects, polymorphism
General Terms

Languages, Design, Theory

Keywords Gradual typing, generics, dynamic types

1. Introduction
Statically and dynamically typed languages have their own
benefits. On the one hand, statically typed languages enjoy
type safety properties; on the other hand, dynamically typed
languages are said to be suitable for rapid prototyping. Thereis a significant amount of work (e.g., [1, 3, 5, 6, 8, 10, 15, 16,
27–29] to cite some) to integrate both kinds of languages tohave the best of both worlds. Siek and Taha have coined theterm “gradual typing” [27] for a particular style of linguistic

Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. To copy otherwise, to republish, to post on servers or to redistributeto lists, requires prior specific permission and/or a fee.
OOPSLA’11, October 22–27, 2011, Portland, Oregon, USA.
Copyright c 2011 ACM 978-1-4503-0940-0/11/10. . . $10.00

support of the seamless integration of static and dynamic
typing in a single language. A typical gradual type system
introduces to a statically typed language a special type (often
called dynamic or dyn) to specify dynamically typed partsin a program and allows a program to be partially typed, oreven fully dynamically typed.
One of the main challenges in the design of a gradualtype system is to give a flexible type compatibility relation,
which is an extension of subtyping and used for assignments
and argument passing. For example, a gradual type system
usually assumes dyn to be compatible with any type so thata statically typed expression can be used where dyn is expected and vice versa. Moreover, when types have structures(as in function types), the compatibility relation usually allows structural comparison: for example, a function type, say
dyn → int, is compatible with int → int [27], which isuseful in higher-order programs.
Another, more technical challenge is to establish somesafety property even for partially typed programs. In fact, it
is possible to ensure that run-time errors are always due toa dynamically typed part in a program. Roughly speaking,the main idea is to insert run-time checks between the “border” between the statically and dynamically typed worlds toprevent statically typed code from going wrong. A key idea
here is that the insertion can be guided by the use of thecompatibility relation.
In this paper, we develop a gradual type system for classbased object-oriented languages with generics. Although
there are similar attempts at mixing static and dynamic typing in object-oriented languages [3, 5, 20, 28, 38], (to ourknowledge) very few take generics into account. One notable
exception is dynamic types for C♯ 4.0 [4], but the integrationof dynamic and static typing is not as smooth as one might
expect. For example, it requires tedious coding to convert
a collection whose element type is statically known, say, tobe integers to a collection of dynamically typed values. We
design a flexible compatibility relation, which allows, for example, List<Integer> to be used as List<dyn> and viceversa. Since the type system has inheritance-based subtyping, it is not a trivial task to give a reasonable compatibility
relation. We also introduce the notion of bounded dynamic
types, which have characteristics of both dynamic and static
types, to mediate bounded polymorphism and dynamic typ-ing. We formalize these ideas as FGJdyn , an extension of
Featherweight GJ (FGJ) [18] with bounded dynamic types
and prove the desired safety property, which states that statically typed parts in a program cannot go wrong. In particular,
it implies the standard type safety for a program that does notcontain any dynamic types. The semantics of FGJdyn —thesurface language in which programs are written—is given% , in which
by a translation to an intermediate language FGJ$
run-time checks are explicit. The translation is not only expediency for the formal proof but also a guide to implementation.
Our main contributions can be summarized as follows:

X x; Cell(X x){ this.x=x; }void set(X x){ this.x=x; }}Cell is a class of one-element containers, where the element type is parameterized as X. The element is accessed
through the field x and modified through method set. We
will also use classes Shape and its subclasses Rectangle
and Polygon. (Neither Rectangle nor Polygon extends
the other.) Moreover, class Shape has a method with the signatureboolean contains(double x, double y);• A flexible compatibility relation for parametric types;

which returns whether a given point at (x, y) is inside theshape.

• The introduction of bounded dynamic types;

2.1 Type dyn as Type Arguments• Formalization of the language with generics and dynamic

One natural consequence of the introduction of dyn as a type
is that dyn can be used as a type argument to a generic class.
For example, a programmer can use a variable c1 of type
Cell<dyn>. This type is similar to Cell<Object> in thesense that one can set anything to it.

types; and• Proof of safety properties, which show that statically

typed parts in a program never go wrong.
We are currently developing a compiler for gradually typed
Java. We also describe our basic implementation scheme.
This work at an earlier stage has been reported at the
STOP’09 workshop [19], where we have only sketched the
combination of generics and dynamic typing and its formalization. In this paper, we have revised the formal definitionof both surface and intermediate languages significantly andproved safety properties.
The rest of the paper is organized as follows. Section 2
gives an overview of gradual typing for a class-based language with generics. Then, Sections 3 and 4 give the formalization of our proposal and prove desired properties. Section 5 describes our implementation scheme for Java and reports very preliminary benchmark results. After Section 6
discusses related work, Section 7 gives concluding remarks.
Some of formal definitions and proofs of the theorems areomitted for brevity; they appear in a full version of this paper, available at http://www.sato.kuis.kyoto-u.ac.
jp/~igarashi/papers/gradual.html.

2. Gradual Typing for Generics
Following the previous approaches to gradual typing [27,28], we introduce a special type dyn that represents dynamically typed portions in a program to a class-based languagewith generics. A variable can be declared to have the dynamic type; then, any expression can be assigned to it andthe variable can be used as an expression of any type. In thissection, we first describe how dyn interacts with generics bymeans of examples and then what kind of dynamic checks
are performed to prevent statically typed parts from goingwrong.
We use the following simple generic class as a running
example:class Cell<X> {Cell<dyn> c1 = ...;
c1.set(new Polygon(...));
c1.set(new Integer(1));

Unlike Cell<Object>, however, the type of field x is dyn,which represents dynamically typed code and accepts any
method invocation and field access, which are assumed toreturn dyn.
dyn fld = c1.x.anyField;
dyn ret = c1.x.anyMethod(...);

Also, dyn can be assigned to any variable.
boolean b = c1.x.contains(1,1);// The type of RHS is dyn

Of course, it must be checked at run time whether thesefields and methods really exists and whether an assignment
is valid.
In the previous work on gradual typing for a languagewith subtyping, the subtyping relation is replaced with thecompatibility relation [27, 28], which, for example, allows
statically typed expressions to be passed where dyn is expected and vice versa. The compatibility relation should berich enough to support flexible integration of statically anddynamically typed code and, for type systems with structural
subtyping, its definition requires careful examination.
We introduce a rich compatibility relation for parametric types. In particular, we allow an expression of a dynfree type, say Cell<Rectangle>, to be assigned to a variable whose type involves dyn as a type argument, say
Cell<dyn>. For example, the following code is accepted by
the type system:
Cell<dyn> c1= new Cell<Rectangle>(new Rectangle(...));

Note that c1 will point to an object that can store only
Rectangles, rather than anything (as indicated by dyn).

So, actually, the invocation of set should check at run time
whether the actual argument is a valid one.
c1.set( new Rectangle(...) ); // succeeds
c1.set( new Polygon(...) );// fails

The intuition behind a parametric type to which dyn
is given as an argument is that it denotes the set oftypes where dyn is replaced with any type. For example, a variable of type Cell<dyn> may point toobjects new Cell<Shape>(), new Cell<Rectangle>(),new Cell<Integer>(), and so on. In this sense, type
Cell<dyn> is closer to the wildcard type Cell<?> thanCell<Object>, but, unlike Cell<?>, potentially unsafe operations such as invocation of set are (statically) allowed.
Our compatibility relation allows the opposite directionof flow, too—that is, an expression whose type involves dyn
as a type argument can be assigned to a variable of a dynfree type as in the following code:
Cell<Rectangle> c2 = c1;
Cell<Polygon> c3 = c1;

Just as in an assignment of an expression of type dyn to a
concrete type, the run-time system will check whether theseare valid assignments: in this case, only the first assignment
will succeed.
In summary, our compatibility relation allows dyn in a
type expression to be replaced with a concrete type and viceversa. As we will see in the next section, however, its formal
definition is more subtle than might have appeared when we
take inheritance-based, nominal subtyping into account. Due
to nominal subtyping, we take an approach different from theprevious work.
Seamless Integration. Allowing dyn as a type argument
lets us easily evolve a class definition from its non-genericversion into a generic version. For example, at the beginning,a programmer had a non-generic class List, which has its
head item head and the rest of list tail, and some clientcode using it.
class List { dyn head; List tail; }List list = new List(...);
list.head.doSomething();Then, the programmer wanted to have a generic versionof List because he added another client code using List
containing Integers and nothing else. So, he modified thedefinition of class List.
class List<X> { X head; List<X> tail; }List<Integer> intlist = new List<Integer>(...);

This modification breaks other client code using Listand he need to fix them all, however, all he have to do isto replace List with List<dyn>.
List<dyn> list = new List<dyn>(...);
list.head.doSomething();

checks if the run-time type of thevalue of e is compatible with T, andthen returns the value.
get(e, f)checks if the value of e has field f,
and then reduces to the field value.
e.m[T|C<X>](e) checks if the types of arguments e
are correct (using the static type information T, C<X>), and then invoke
method m on receiver e.
invoke(e, m, e) checks if the value of receiver e
has method m and the types of arguments e are correct, and then invoke
the method on the receiver.

$T% eTable 1. Constructs for run-time checks.
If the compiler allows List as an abbreviation of
List<dyn>1, he could have done the modification even
without any other type-name fixes!
Note that we need to allow new List<dyn>(...). Thisis quite different from wildcards, since new List<?>(...)
is disallowed.
2.2 Run-time Checks
To ensure that statically typed code (or, more precisely, codethat would be well typed in the standard type system) will
not go wrong, errors due to dynamically typed code have to
be captured at the “border” between the two worlds. For thispurpose, we introduce an intermediate language, which has
explicit constructs for run-time checks; the semantics of thesurface language, which we describe above, will be given interms of the translation to the intermediate language.
Although there is no direct semantics for the surface language, a program in the surface language can be mostly
directly understandable because the translation only inserts
run-time checks and preserves the structure of a program.
Moreover, run-time checks are inserted only where dynamic
types are involved. So, as far as statically typed code is concerned, the translation is the identity map, inserting no runtime check. Then, to show that statically typed code nevergoes wrong, it suffices to show that all run-time failures are
due to those explicit checks.
We will give an overview of constructs for run-time
checks and the translation below. Table 1 shows constructs
for run-time checks and their intuitive meanings. In what
follows, we write ee′ to mean that a surface language
expression (or statement) e is translated to e′ .
First, when an expression of a type that involves dyn ispassed to where a type without dyn is expected, a cast $% isinserted:
1 List is a raw type of List<X> in the current Java specification, where

it is allowed to assign a value of List<T> to a variable of List. Since
this behavior is similar to List<dyn>, it is quite natural to allow theabbreviation instead of using raw types. See Section 6 for details.

Cell<dyn> c1; Cell<Rectangle> c2; Cell<Polygon> c3;
c2 = c1;
c2 = $Cell<Rectangle>% c1;
c3 = c1;
c3 = $Cell<Polygon>% c1;

We use different parentheses $% to denote casts because
the semantics is slightly different from Java’s. Note thatthe first cast above has to check that the run-time value of
c1 is an instance of Cell<Rectangle> and not that of,say, Cell<Integer>. So, this cast requires run-time typeargument information. There are other differences, which we
discuss later, as well.
A member access on dyn will be translated to special
forms get() or invoke(), which checks the existence ofthe member at run-time.
Cell<dyn> c1;
c1.x.radius;get(c1.x, radius);
c1.x.contains(1, 1);
invoke(c1.x, contains, 1, 1);

When c1.x has method contains, invoke above also
checks whether it can take two integers.
As we have already discussed, the invocation of set ontype Cell<dyn> will have to check whether the run-time
type of the argument is appropriate for the run-time type argument to the receiver’s class, even though the existence of
method set is statically guaranteed. For such cases, we use
method invocation of the form e0 .m[T|C<X>](e) (wherean overline denotes a list). For example, we have the following translation.

also aim at implementation by erasure translation [7].2 Actually, modular checking and erasure translation make it trickier to ensure the safety of “statically typed code”.
First of all, even if a class definition contains no occurrence of dyn, it should not be considered statically typed
because subexpressions may be given type dyn. So, a sensible definition of a statically typed class definition is something like “a class definition is statically typed if there is no
occurrence of dyn and every subexpression is given a ‘dynfree’ type.” In fact, as we will see later, in our translation, amethod invocation requires no run-time check if the receiver
and actual argument types are all dyn-free. Then, a class definition that passes the standard type checking will translate
to itself, without run-time checks.
However, the problem is more subtle than it might haveappeared, due to the presence of type variables. In general,
type variables should not be considered dyn-free simply
because type variables can be instantiated with dyn. In fact,
the following classes, which are typed under the standard
type system of generics
class StrCell extends Cell<String> {void set(String x){ ... x.length() ... }}class Foo<Y> {void bar(Cell<Y> c, Y x) {c.set(x);}}will raise a run-time error when combined with the following
code:
new Foo<dyn>().bar(new StrCell(...), new Object());

c1.set( new Polygon(...) );c1.set[X|Cell<X>]( new Polygon(...) );The annotations X and Cell<X> record a parameter type anda receiver’s static type before type parameters are instantiated and are used to check the argument. It works as follows:
When c1 evaluates to a value new Cell<T>(...) for some
type T, the actual receiver type Cell<T> is matched against
Cell<X> and X is bound to T. Then, the actual argument’s
type (here Polygon) is checked against T, which is obtainedby replacing X with T in the recorded parameter type. So,
this method invocation succeeds when c1’s value is an object of Cell<Polygon> (or Cell<T> where T is a supertypeof Polygon).
2.3 Ensuring “statically typed parts cannot go wrong”
One of our goals of the gradual type system is to ensurethat “statically typed parts in a program never go wrong”,
in particular, class definitions that pass the standard typechecker should not go wrong. Another desirable property ofthe system is modularity of type checking, that is, determining whether the given part of the program is statically typed
or not should be done by looking at no more than a single
class definition and type information that it depends on. We

The last expression passes a StrCell and an Object toFoo<dyn>.bar(), which expects a Cell<dyn> and dyn,and this is allowed due to the extended compatibility relation we have already mentioned. In Foo<Y>.bar(), an
object x is passed to Cell<Y>.set(). However, in thiscase, the receiver is a StrCell and StrCell.set() will
be called with an argument new Object(), which does nothave length()!
To avoid this problem, we separate type variables into two
kinds: one can only be replaced with dyn-free types, andthe other can be replaced with dynamic types. These kinds
are indicated in the class definition, for example, class
Foo<Y♦ >... for the former and class Foo<Y >... forthe latter. If Foo is defined as class Foo<Y♦ >..., thenno run-time check is inserted but the problematic expression above is rejected at compile time. Otherwise, if Foo isdefined as class Foo<Y >..., then the invocation of set
will check whether the actual argument types are valid forthe formal (by using e.m[T|C<X>](e)).
Although, in principle, a programmer can choose thekind for each type variable declaration in a single class
2 Our compilation scheme actually requires support for run-time type argu-

ments. However, method signatures are subject to erasure.

definition, we do not expect that a programmer wants to doit. A practical design would be that a compiler option will
decide the kind of all the type variables in a compiled fileat once. In the beginning of development, the programmer
may compile most generic classes with kind , and thenswitches some classes to ♦ gradually as the development
progresses—such a switch would force their client code toremove the use of dynamic types. In the rest of the paper,
we omit kinds of type variables when they do not makesignificant difference.
There can be another solution to the problem in which the
StrCell is “wrapped” with another object when it is passed
to Cell<dyn>. The wrapper object mimics the interfaceof StrCell by delegating member accesses to the original
object and performs run-time checks on every delegation.
In this case, the run-time check blames the misusage of the
StrCell on the invocation of set(). We do not choose thissolution mainly because of a difficulty of implementationand leave it for future work.
2.4 Bounded Dynamic Types
Another problem occurs when a type variable is given an upper bound. To illustrate the problem, consider the followingclass:
class ShapeCell<X  extends Shape> {X x; ShapeCell(X x){ this.x=x; }void set(X x){ this.x=x; }boolean contains(double px, double py){
return this.x.contains(px, py);}}

Class ShapeCell, which is similar to class Cell above,
specifies Shape as X’s upper bound. Note that ShapeCell
does not contain dyn anywhere and the whole class definition will be well typed in the standard type system of generics (by removing ).
Now consider type ShapeCell<dyn>. The question here
is what we can set to x. One choice would be to allow any
object to be set to x, as we did for Cell<dyn>:
ShapeCell<dyn> sc = ...;
sc.set( new Object() );However, this choice would not be compatible with the implementation by erasure, which translates the type of field x
to be Shape, the upper bound of X. In a language without erasure semantics, for example in C♯ , this choice would not conflict with the implementation, but, as long as homogeneoustranslation [25] is used, we would need to treat type variable
X with kind  as dyn. This leads to a major performance
disadvantage since operations on expressions of type X need
to be augmented with run-time checks that require membership tests: for example in the case above, the invocation ofcontains on this.x need to be replaced with an expensive run-time check by invoke, which checks the presenceof method contains and (if it exists) whether the types offormal and actual arguments match. Thus, our choice here
is to keep compatibility with implementation by erasure andto avoid performance penalty as much as possible: in otherwords, we reject the code above statically.
We introduce bounded dynamic types, written dyn<T>(where T stands for a parametric type). A type parameterwith an upper bound T can be instantiated by a bounded
dynamic type dyn<T′ > when T′ is a subtype of T. Thus,
ShapeCell<dyn<Shape>> is a well-formed type, whereas
ShapeCell<dyn<Object>> is not.
We define a bounded dynamic type dyn<T> to be compatible only with subtypes of T. So, the following code will
be ill typed and rejected by the type checker.
ShapeCell<dyn<Shape>> sc = ...;
sc.set( new Object() );// Object is not compatible with dyn<Shape>!

A bounded dynamic type has both static and dynamic typing
natures. While it still allows potentially unsafe operations
to be performed, it enforces static typing as far as members
defined in the bound are concerned. So, the first two lines
in the following code are still accepted (and checked at runtime) but not the third3 and fourth.
sc.x.anyField;
sc.x.anyMethod(...);
sc.x.contains(); // two arguments are expected!
Shape s = sc.x.contains(3, 4); // returns boolean!

In a real language, we do not expect programmers towrite those upper bounds explicitly. Rather, when dyn isused as a type argument, the compiler can recover its upper bound automatically by assigning the upper bounds ofthe corresponding type parameters in the generic class definition.4 For other uses of dyn, they can be regarded as
dyn<Object>; in fact, we use dyn as an abbreviation ofdyn<Object>, throughout the paper.
2.5 Two Compatibility Relations
As we have already mentioned, the type system of the surface language uses the compatibility relation, denoted by., to check argument passing and assignments. This relation has both co- and contra-variant flavors when dyn is
considered a top type: for example, both Cell<Shape> .
Cell<dyn> and Cell<dyn> . Cell<Shape> hold and so
bothCell<Shape> c1 = ...; Cell<dyn> c2 = c1;

andCell<dyn> c1 = ...;

Cell<Shape> c2 = c1;

are accepted (statically). The reason to allow contravariance(the latter kind of compatibility) is simply because it sometimes runs safely. For example, when c1 happens to be an
3 It could be allowed in the presence of overloading.
4 For F-bounded type variables, such automatic recovery is difficult. We
would have to have programmers write upper bounds explicitly.

object new Cell<Shape>(...), the latter code fragment isjust fine.
However, we should not use this compatibility relation
for casts. For example, consider the following (surface language) code:
Cell<dyn> c1 = new Cell<dyn>(new Polygon(...));
Cell<Rectangle> c2 = c1;// accepted thanks// to contravariancec2.x.methodOnlyInRectangle(); // accepted since// c2.x is RectangleOnthesecondline,
arun-time
check$Cell<Rectangle>% c1 is performed. Since the runtime type of c1 is Cell<dyn>, if $% used the compatibility
relation, the cast will succeed, resulting in the unexpected
method-not-found error! (Notice that the invocation of
methodOnlyInRectangle should involve no checks
because the receiver’s static type does not contain dyn.): called run-time compatThus, we use another relation ≺ibility for run-time checks. This relation is a subrelation of:. and disallows contravariance: for example, Cell<dyn> ≺Cell<Rectangle> does not hold. However, it still allows: Cell<dyn>),covariance (such as Cell<Rectangle> ≺so it is more permissive than subtyping. (It is not completely safe—that is why we still need argument checks by
e0 .m[T1 , . . . , Tn |C<X>](e1 , . . . , en ).)Having these discussions in mind, we formalize the coreof the surface and intermediate languages in the following
sections.

3. Featherweight GJ with Dynamic Types
In this section, we formalize the surface language FGJdyn , anextension of FGJ with dynamic types to model a type systemof gradually typed generics. For simplicity, we omit somefeatures found in FGJ: polymorphic methods and typecasts,
which would be easy to add. As in FGJ, we also omit method
overloading. We focus on the type system in this section
and leave the definition of the intermediate language called% and translation from FGJdyn to FGJ$
% to Section 4.
FGJ$
For those who are familiar with FGJ, we use gray boxes toshow main differences from FGJ.
3.1 Syntax and Lookup Functions
The abstract syntax of FGJdyn classes, constructors andmethod declarations, and expressions are defined as follows:
Definition 1 (Syntax of FGJdyn ).
κ, ι ::=  | ♦S, T, U, V ::= X | N | dyn<N>
N, P, Q ::= C<T>
e ::= x | new N(e) | e.f | e.m(e)κ
L ::= class C<X ⊳ N> ⊳ N {T f; K M}
K ::= C(T f){super(f); this.f=f;}
M ::= T m(T x){ return e; }The metavariables A, B, C, D and E range over class names;
W, X, Y and Z range over type variables; N, P and Q range
over class types (dyn<N> is not a class type); S, T, U and V
range over types; κ and ι range over kinds of type variables;
f and g range over field names; m ranges over method names;
x ranges over variables; d and e range over expressions;
L ranges over class declarations; K ranges over constructor
declarations; and M ranges over method declarations. We
assume that the set of variables includes the special variable
this.
We write f as shorthand for a possibly empty sequence
f1 ,f2 ,. . . ,fn (and similarly for C, X, N, T, x, e, etc.) andwrite M as shorthand for M1 . . . Mn (with no commas). The
length of a sequence f is written #(f). We write f ∈ f/ fwhen f equals to fi where 1 ≤ i ≤ #(f), and write f ∈otherwise. We also abbreviate various forms of sequencesof pairs, writing “T f” as shorthand for “T1 f1 ,. . . ,Tn fn ”
where #(T) = #(f), and similarly “T f;” for the sequence of declarations “T1 f1 ;· · · Tn fn ;”, “this.f=f;”
κfor “this.f1 =f1 ;· · · this.fn =fn ;”, and “X ⊳ N” for “Xκ1 1
κn⊳ N1 ,. . . ,Xn ⊳ Nn ” . We write the empty sequence as •and denote concatenation of sequences using a comma. Sequences are assumed to contain no duplicate names. We abbreviate the keyword extends to the symbol ⊳.
dyn<N> is a type of dynamically typed expressions. Since
it is not a class type, dyn<N> can neither be used to instantiate an object (by new expressions) nor be used as a bound ofa type variable. We always write the bound N in the formal
language.
A program in FGJdyn is a pair (CT, e) of a class table,
which is a finite mapping from class names C to class declarations L, and a closed expression corresponding to the bodyof the main method. We assume that CT satisfies some sanity conditions: (1) CT (C) = class C<X ⊳ N> ⊳ ... {...}
for every C ∈ dom(CT ); (2) Object ∈/ dom(CT ); (3) for
every class name C (except Object) appearing anywhere in
CT , we have C ∈ dom(CT ); and (4) there are no cycles
in the transitive closure of ⊳ (as a relation between classnames). In what follows, we fix a class table.
As in FGJ, we use functions fields and mtype to lookup field definitions and method types in a given class table.
We also use a predicate nomethod to state non-existenceof a method. We omit their straightforward definitions (seeappendix in the full version of this paper or Igarashi, Pierce,and Wadler [18] for the definitions of fields and mtype);
their functionalities are summarized in Table 2.
Some other auxiliary functions are defined in Figure 1.
We use a function bound to compute the upper bound of a
type in a bound environment ∆, which is a finite sequence of
triples of a type variable, its kind and its bound, where typevariables are pairwise distinct.5 When bound is used witha class type, it returns the given type itself. When boundis used with a dynamic type, it returns the bound of the
5 So, ∆ can be considered a finite mapping.

fields(N) = T fcollects fields in class N and its
super type.
mtype(m, N) = T → T looks up the type of method m inclass N or its super type.
nomethod (m, N)
holds when there is no method min class N or its super type.
Table 2. Definition of FGJdyn : Auxiliary functions andpredicates.
dynamic type. We have a function kind to look up kindsof type variables. We use a predicate dynfree to state that a
type is dynamic-free, i.e., it contains no dynamic type.
3.2 Subtyping and Compatibility
Now we define subtyping and compatibility relations. As wehave mentioned, there are two compatibility relations (writ: for run-time compatibility and . for static compatiten ≺bility). We write ∆ ⊢ S <: T to mean S is a subtype of: T
T under bound environment ∆. Similarly for ∆ ⊢ S ≺and ∆ ⊢ S . T. We abbreviate a sequence of judgments∆ ⊢ S1 <: T1 , . . . , ∆ ⊢ Sn <: Tn to ∆ ⊢ S <: T (and: and .).
similarly for ≺Definition 2 (FGJdyn subtyping and compatibility). The
subtyping and compatibility judgments ∆ ⊢ S <: T and: T and ∆ ⊢ S . T are defined by the rules in∆ ⊢ S ≺
Figure 2.
The subtype relation <: is mostly the same as that of FGJ.
The first two rules mean that it is reflexive and transitive;
the third rule that a type variable is a subtype of its bound;the fourth rule is about inheritance-based subtyping—any instance of a ⊳ clause gives subtyping. The last rule says abounded dynamic type dyn<N> is a subtype of its bound N.
In fact, dyn<N> and N denote the same set of instances—instances of N and its subtypes and dyn<N> allows more
operations (which are potentially unsafe, though) to be performed than N. So, dyn<N> <: N indeed agrees with thesubstitution principle [23].
The compatibility relations are defined with the help of
the auxiliary relation ≺. Intuitively, S ≺ T means that T
is obtained by replacing some class types in S with dynamic types (with an appropriate bound). For example,
Rectangle ≺ dyn<Object> and Cell<Rectangle> ≺Cell<dyn<Object>> hold (under any bound environment).
So, ≺ represents a form of covariance. Then, the compati: and . are defined as compositions of ≺bility relations ≺and <:—the former as (<:; ≺) (·; · is a composition of two
relations) and the latter as (≺−1 ; <:; ≺), where ≺−1 is theinverse of ≺ and represents a form of contravariance. As aresult, two types are statically compatible if replacing dynamic types with class types yields two types in the subtyping relation.

For example,∆ ⊢ Cell<dyn<Object>> . Cell<Rectangle>
can be derived since Cell<dyn<Object>>
Cell<Rectangle>. Also,≺−1∆ ⊢ Cell<dyn<Shape>> . Cell<dyn<Object>>since Cell<dyn<Shape>> ≺−1 Cell<Shape> andCell<Shape> ≺ Cell<dyn<Object>>. (Note that
Cell<dyn<Shape>> <: Cell<dyn<Object>> does nothold.)
dyn<Object> can be considered either a top type ora bottom type, i.e., ∆ ⊢ T . dyn<Object> and ∆ ⊢dyn<Object> . T are satisfied for any T, and the relation. is not transitive because otherwise ∆ ⊢ S . T would be
implied for any S,T (as mentioned in [27, 28]). dyn<N> canalso be considered as a top/bottom type for subtypes of N.
3.3 Type Well-formedness and Typing
We, then, define well-formed types and typing.
Definition 3 (FGJdyn type well-formedness). The type wellformedness judgment ∆ ⊢ T ok, read as “in bound environment ∆, type T is well formed,” is defined by the rules in
Figure 3.
The last rule means that a bounded dynamic type iswell formed if its upper bound is well formed. The third
rule means that a class type is well formed if it has
well formed type arguments that satisfy the correspond:
ing type parameters’ upper bounds. Note that we use ≺rather than <: or .. First, <: cannot be used because
we want to use dynamic types as type arguments. For
example, Cell<dyn<Object>> is well formed because: Object. . should not be used, either, bedyn<Object> ≺cause we want to reject a type like ShapeCell<Object>.
(Note that Object . Shape.) The third rule also requiresthat type arguments must be dynamic-free if the kind of thecorresponding type variable is ♦.
Now we are ready to define typing. We use Γ as a typeenvironment, which is a finite mapping from variables totypes, written x : C.
Definition 4 (FGJdyn typing). The type judgments ∆; Γ ⊢Ge : T, read as “in environment ∆ and Γ, expression e has type
T,” and M OK IN C<X ⊳ N>, read as “method M is well-formedin class C<X ⊳ N>” and L OK, read as “class L is well-formed”
are defined as in Figure 4.
Most of the rules are straightforward adaptation of thosein FGJ [18], except that the relation . is substituted for <:.
T G -F IELD 2 and T G -I NVK 2 are additional rules, used when
the receiver type is a bounded dynamic type. Note that theserules are applied only when it is not known whether thereceiver has a field or method to be accessed (the premises
f 6∈ f in T G -F IELD 2 and nomethod (m, N) in T G -I NVK 2).

Bound environment∆(X) = (κ, N)
bound ∆ (X) = N∆(X) = (κ, N)

bound ∆ (dyn<N>) = N

bound ∆ (N) = N

kind ∆ (X) = κ

Dynamic-free types
kind ∆ (X) = ♦dynfree ∆ (T)dynfree ∆ (X)dynfree ∆ (C<T>)

Figure 1. Definition of FGJdyn : Auxiliary functions and predicates.
Subtyping∆ ⊢ S <: U

∆ ⊢ T <: T

∆ ⊢ U <: T

∆ ⊢ S <: T

∆ ⊢ X <: bound ∆ (X)κclass C<X ⊳ N> ⊳ N {...}∆ ⊢ C<T> <: [ T/X ]N∆ ⊢ dyn<N> <: NCompatibility
∆⊢S≺U

∆⊢T≺T

∆ ⊢ S <: U

∆⊢U≺T

: T
∆⊢S≺

∆⊢S≺T
∆ ⊢ T <: S∆⊢S≺T∆ ⊢ C<S> ≺ C<T>

∆⊢U≺T

∆⊢S≺N

∆⊢U≺S

∆ ⊢ T ≺ dyn<N>

: T
∆⊢U≺

∆⊢S.T

Figure 2. Definition of FGJdyn : Subtyping and compatibility.
κclass C<X ⊳ N> ⊳ N {...}∆ ⊢ Object ok∆ ⊢ T okX ∈ dom(∆)∀κi ∈ κ.( κi = ♦ implies dynfree ∆ (Ti ) ): [T/X]N∆⊢T≺∆ ⊢ N ok∆ ⊢ X ok∆ ⊢ C<T> ok∆ ⊢ dyn<N> ok

Figure 3. Definition of FGJdyn : Type well-formedness.
In other words, T G -F IELD 1 or T G -I NVK 1 can be used forexpressions whose receiver type is dyn<N>, as long as themember is defined in the class definition of N.
The predicate override, used in method typing, is tocheck if a method m in class N can be overridden by a methodof type T → T. Parameter types must be the same between
the overriding and overridden methods6 and the return typeof the overriding method must be run-time compatible withthat of the overridden method. We cannot use . here: if .
were used, it would be possible to override a method that
returns T by one that returns dyn<Object> in a subclass,and then to override it by another that returns S for any S.
As a result, invoking a method, whose static return type is T,

6 This restriction can easily be relaxed by using the relation ≺: , but then weneed a careful examination when we add method overloading.

might actually invoke the third method that returns S, which
can be very different from T, due to late binding!
We write ⊢G (CT, e) : T to mean the program is wellformed, i.e, if all the classes in CT are well formed and e iswell typed under the empty environment.
We have not completed developing a type checking algorithm. In fact, it is not even clear that the compatibility relation . is decidable for the same reason as variance-based
subtyping [21].
Conservative Typing over FGJ. Even at this point, we
can show an interesting property that typing in FGJdyn isa conservative extension of that in FGJ. Namely, as far asa class table written in the FGJ syntax is concerned, it iswell typed under the FGJ rules if and only if it is well typed
under the FGJdyn rules. The following lemma is a key to theconservative extension property (Theorem 6).

Expression typing∆ ⊢G N ok∆; Γ ⊢G x : Γ(x) (Tg-Var)∆; Γ ⊢G e : U∆⊢U.T∆; Γ ⊢G new N(e) : N∆; Γ ⊢G e0 : T0
fields(bound ∆ (T0 )) = T f∆; Γ ⊢G e0 .fi : Ti∆; Γ ⊢G e0 : dyn<N>f∈/ffields(N) = T f(Tg-Field1)∆; Γ ⊢G e : V∆; Γ ⊢G e0 : T0

fields(N) = T f∆; Γ ⊢G e0 .f : dyn<Object>mtype(m, bound ∆ (T0 )) = S → S(Tg-Field2)∆⊢V.S∆; Γ ⊢G e0 .m(e) : S∆; Γ ⊢G e0 : dyn<N>∆; Γ ⊢G e : V

nomethod (m, N)∆; Γ ⊢G e0 .m(e) : dyn<Object>(Tg-New)(Tg-Invk1)(Tg-Invk2)

Method typing: U
mtype(m, N) = U → U implies T = U and ∆ ⊢ T ≺override ∆ (m, N, T → T)κ

∆ = X <: N∆⊢S.T

∆ ⊢ T, T ok∆; x : T, this : C<X> ⊢G e0 : S

κclass C<X ⊳ N> ⊳ N {...}

override ∆ (m, N, T → T)

T m(T x){ return e0 ; } OK IN C<X ⊳ N>

(Tg-Method)Class typingκ

X <: N ⊢ N, T, N ok
fields(N) = U g
M OK IN C<X ⊳ N>
K = C(U g, T f){super(g); this.f=f;}κclass C<X ⊳ N> ⊳ N {T f; K M} OK(Tg-Class)Figure 4. Definition of FGJdyn : Typing.
Lemma 5.
• If ∆ ⊢ S ≺ T and dynfree ∆ (T), then S = T.
• If ∆ ⊢ S ≺: T and dynfree ∆ (T), then ∆ ⊢ S <: T.
• If ∆ ⊢ S . T and dynfree ∆ (S), then ∆ ⊢ S ≺: T.
• If ∆ ⊢ S . T and dynfree ∆ (S) and dynfree ∆ (T), then∆ ⊢ S <: T.

% , we present formal translation from FGJdyn to FGJ$%
FGJ$
and state theorems that translation preserves typing. We haveweak and strong versions of type safety: the weak version
means that a well typed program can raise errors only at
run-time checks and the strong version means that a well
typed program without containing run-time checks nevergoes wrong in the usual sense.

We write ⊢FGJ (CT, e) : T if the program, which does notcontain dyn<N>, is well formed under the FGJ rules.
Theorem 6 (FGJdyn Typing is Conservative over FGJ Typκing). If κ = ♦ for every class C<X ⊳ N> ⊳ N {...} in CT
and none of dyn<P> appears in (CT, e), then ⊢FGJ (CT, e) :T ⇐⇒ ⊢G (CT, e) : T.

4. From FGJdyn to FGJ$%% of
In this section, we first define a formal model FGJ$
the intermediate language, into which source programs are% has operational semantics, as well as atranslated. FGJ$
type system. After stating theorems about type safety of%
4.1 The Target Language FGJ$
% extends that of FGJdyn , by including
The syntax of FGJ$
special forms for run-time checks and run-time errors. We
show only the grammar for expressions, values (used todefine the semantics), and errors; the others are the same.

% ).
Definition 7 (Syntax of FGJ$

e

::=

x | new N(e) | e.f | e.m(e)| get(e, f) | e.m[T|C<X>](e)v, w ::=
E::=| invoke(e, m, e) | $N% e| Error[E]
new N(v)
NoSuchField | NoSuchMethod| IllegalArgument | BadCast

We avoid repeating the definitions of the following functions, predicates, and relations since they are defined exactly
the same way as in FGJdyn .
Functions

bound
kind
fieldsmtype
Predicates dynfree
nomethodoverride
Relations Subtyping <::Compatibility ≺, ≺Judgments Type well-formedness

Figure 5 introduces an auxiliary function tyargs(N, C),
which is used in the reduction rules described later to gettype arguments from run-time types. We also use a function
mbody(m, N), which returns a pair x.e of a sequence offormal parameters and a method body expression, if N has
m. Its straightforward definition is omitted.
% in Figure 6.
We show the main typing rules of FGJ$
An important point to note is that we use only the run-time: and no . appears in the typing rules because
compatibility ≺: for its runa use of . compiles to a cast $% , which uses ≺time check. T R -I NVK 1 is the rule for a method invocation
without run-time checks. The receiver type must be dynfree. T R -I NVK 2 is the rule for a method invocation with runtime argument checking. C<T> can be considered an initial(i.e., compile-time) static type of receiver e0 ; the condition: C<T> is required since the receiver type may changeN ≺as reduction proceeds. T R -I NVK 3 is the rule for a method
invocation that checks whether the method m exists at run
time. The receiver and arguments can be arbitrary typeable
expressions and the type of the invocation is dyn<Object>.
T R -C AST is the rule for casts; and T R -E RROR is the rule forerrors.
We omit typing rules for object constructions, field accesses, methods and classes, since they are similar to those% proin FGJdyn . We write ⊢R (CT, e) : T to mean the FGJ$
gram (CT, e) is well formed.
We give main reduction rules in Figure 7. The evaluation order is, unlike FGJ, fixed to be left-to-right and call-byvalue to deal with run-time errors more precisely. R-F IELD 1
and R-I NVK 1 are quite standard. They check the existenceof a field/method in the receiver type but the check should

never fail for well-typed expressions as we will see later.
R-F IELD 2, R-I NVK 2, R-I NVK 3 and R-C AST are for runtime checks, which can raise a run-time error. In R-I NVK 2,
the type arguments in method parameter types are filled inaccording to the run-time class of the receiver value, andchecked against the run-time class of the actual arguments.
In R-I NVK 3, we need to look up the method argument types
by mtype to perform run-time checks for actual arguments.
The rule R-C AST means that a cast succeeds when the subject type is run-time compatible with the target type.
We also have reduction rules for errors shown in Figure 8.
Each rule has premises negating those in the corresponding
reduction rule. Note that only run-time checks have errorraising reductions. We also need rules that propagate raisederrors upwards, but we omit them.
% is (weakly) type-safe in the sense that a well-typed
FGJ$
program, if it terminates, yields a value or raises an error.
Moreover, if a program does not contain dynamic types, thenit is strongly type safe.
% weak type safety). If ⊢ (CT, e) : T and
Theorem 8 (FGJ$Re −→∗ e′ where e′ is a normal form, then e′ is either: T, or1. a value v with •; • ⊢R v : N and • ⊢ N ≺2. an error Error[E].
% strong type safety). If ⊢ (CT, e) : T
Theorem 9 (FGJ$
R

where (CT, e) does not contain run-time checks and e −→∗e′ where e′ is a normal form, then e′ is a value v with: T.
•; • ⊢R v : N and • ⊢ N ≺These theorems are proved in a standard manner of combining subject reduction and progress [37]. The statements
and proofs of both properties are, in fact, very similar to
those for FGJ. One non-trivial property required is transi:.
tivity of ≺Theorem 8 should be understood with the typing and% . First, in Figure 6,
error-raising reduction rules of FGJ$
T R -I NVK 1 says that the receiver type of an ordinary method
invocation is always dyn-free. Then, in Figure 8, Error[E]is reduced only from run-time checks, not from an ordinary
member access. Considering these and the subject reduction
property together, we can see that no member access on dynfree receiver raises an error.
%
4.2 Translation from FGJdyn to FGJ$
% is of the
The judgment of translation from FGJdyn to FGJ$
dyn′form ∆; Γ ⊢ e
e : T, read “FGJ expression e of type T% expression
under environments Γ and ∆ translates to FGJ$′e .” The translation is directed by typing in FGJdyn . We show
only the rules for method invocations in Figure 9.
hS ⇐ Ti∆ e inserts a cast when source type T is not
run-time compatible with S. This reduces unnecessary casts.
T RNS -I NVK 1 is for ordinary invocations; casts are inserted
for testing run-time compatibility of arguments. If V are
dyn-free, then actually no casts will be inserted, thanks to
Lemma 5. T RNS -I NVK 2 is for invocations whose arguments• ⊢ N <: P

tyargs(C<T>, C) = T

tyargs(P, C) = T

tyargs(N, C) = T% : Auxiliary function.
Figure 5. Definition of FGJ$∆; Γ ⊢R e0 : T0∆; Γ ⊢R e : V

dynfree ∆ (N)

: N
∆⊢P≺
:
≺
∆⊢V S

bound ∆ (T0 ) = P

mtype(m, N) = S → S∆; Γ ⊢R e0 .m(e) : S∆; Γ ⊢R e0 : T0

(Tr-Invk1): [T/X]C<X>
bound ∆ (T0 ) = N∆⊢N≺: [T/X]Umtype(m, C<X>) = U → U∆⊢V≺∆; Γ ⊢R e : V∆; Γ ⊢R e0 .m[U|C<X>](e) : [T/X]U∆; Γ ⊢R e0 : T0∆; Γ ⊢R e : V∆; Γ ⊢R invoke(e0 , m, e) : dyn<Object>(Tr-Invk3)∆; Γ ⊢R e : S∆; Γ ⊢R $T% e : T(Tr-Invk2)(Tr-Cast)∆; Γ ⊢R Error[E]: T (Tr-Error)% : Typing.
Figure 6. Definition of FGJ$
fields(N) = T f
new N(v).fi −→ vi
: T
•⊢N≺

$T% new N(v) −→ new N(v)(R-Field1)(R-Cast)mbody(m, N) = x.e0

fields(N) = T fget(new N(v), fi ) −→ vi(R-Field2)

mbody (m, N) = x.e0
new N(v).m(w) −→ [w/x, new N(v)/this]e0

w = new P(...): [tyargs(N, C)/X]U•⊢P≺

new N(v).m[U|C<X>](w) −→ [w/x, new N(v)/this]e0
mbody (m, N) = x.e0

mtype(m, N) = U → U

w = new P(...)(R-Invk1)(R-Invk2)

: U
•⊢P≺

invoke(new N(v), m, w) −→ [w/x, new N(v)/this]e0(R-Invk3)% : Reductions.
Figure 7. Definition of FGJ$
•⊢N≺
6: T

$T% new N(v) −→ Error[BadCast](E-Cast)fields(N) = T fget(new N(v), f) −→ Error[NoSuchField]

nomethod (m, N)
invoke(new N(v), m, w) −→ Error[NoSuchMethod]w = new P(...)• ⊢ Pi ≺6 : [tyargs(N, C)/X]Ui

new N(v).m[U|C<X>](w) −→ Error[IllegalArgument]
mtype(m, N) = U → U

f 6∈ fw = new P(...)• ⊢ Pi ≺6 : Uiinvoke(new N(v), m, w) −→ Error[IllegalArgument](E-Invk)(E-Invk-Arg1)(E-Invk-Arg2)% : Error-raising reductions.
Figure 8. Definition of FGJ$

(E-Field)

Cast insertiondef

hS ⇐ Ti∆ e =

(

e

: S)
(if ∆ ⊢ T ≺$S% e (otherwise)Translation of method invocation∆; Γ ⊢ e0
e′0 : T0∆; Γ ⊢ ee′ : Vdynfree ∆ (N)mtype(m, N) = S → S∆; Γ ⊢ e0 .m(e)e′0 .m(hS ⇐ Vi∆ e′ ) : S(Trns-Invk1)∆; Γ ⊢ ee′ : Vbound ∆ (T0 ) = [T/X]C<X>
mtype(m, C<X>) = U → U∆ ⊢ V . [T/X]U∆; Γ ⊢ e0
e′0 : T0
¬dynfree ∆ (C<T>)∆; Γ ⊢ e0 .m(e)∆; Γ ⊢ e0bound ∆ (T0 ) = N∆⊢V.S

e′0 .m[U|C<X>](h[T/X]U ⇐ Vi∆ e′ ) : [T/X]U

e′0 : dyn<N>∆; Γ ⊢ e0 .m(e)∆; Γ ⊢ ee′ : V

nomethod (m, N)

invoke(e′0 , m, e′ ) : dyn<Object>(Trns-Invk2)(Trns-Invk3)%.
Figure 9. Translation from FGJdyn to FGJ$
must be checked at run time. Note that the receiver type T0
in these two rules can be dyn<N> when there is an appropriate method m in N because the existence of m is staticallyguaranteed. T RNS -I NVK 3 is for invocations whose receiver
type is dyn<N> and N has no appropriate method m.
Although we omit its definition, we write (CT, e)(CT ′ , e′ ) to mean that the FGJdyn program (CT, e) is trans% program (CT ′ , e′ ). Then, the translation
lated to the FGJ$
preserves well-typedness, i.e., a well-typed FGJdyn program% program.
translates to a well-typed FGJ$
Theorem 10 (Weak translation). If ⊢G (CT, e) : T, then(CT, e)(CT ′ , e′ ) and ⊢R (CT ′ , e′ ) : T for some′ ′(CT , e ).
Theorem 11 (Strong translation). If κ = ♦ for everyκclass C<X ⊳ N> ⊳ N {...} in CT and none of dyn<P>
appears in (CT, e) and ⊢G (CT, e) : T, then (CT, e)(CT ′ , e′ ) and ⊢R (CT ′ , e′ ) : T for some (CT ′ , e′ ) and(CT ′ , e′ ) does not contain run-time checks.
Combining Theorem 8 and Theorem 10, we can see that amember access which translates to an ordinary member access without run-time checks will not fail. In other words, astatically typed portion (method invocations whose receiver
and argument types are dyn-free) will never fail. This is thetype safety of FGJdyn .

5. Implementation
In this section, we report the basic implementation scheme
for Java. Our plan is to add a new compilation phase totransform a code tree to have the run-time checks inserted
as the same way as the other existing compilation phasessuch as the type erasing transformation. The transformation
follows the rules in Section 4 and the run-time checks canbe implemented using existing reflective features of Java.
Since the current JVM has no run-time information of typearguments of generics, we need a mechanism to look up fullrun-time type information. We follow the technique of typepassing [32–34] for this.
5.1 Run-time Checks$T% e, get(e, f) andThe
run-time
checksinvoke(e, m, e) can be implemented by reflection APIs
such as java.lang.Class, java.lang.reflect.Field
and java.lang.reflect.Method. We implement aclass Cla to represent type descriptors and a static method
Cla.$() to get the run-time type information of obj including type arguments. The return value of Cla.$(...) is a
type descriptor d (an instance of class Cla described in moredetail later), which has field cl of a java.lang.Class
instance, field p of an array of type descriptors of typearguments, and h of an array of a superclass chain, where
d.h[0] is d itself and d.h[d.h.length-1] is Object.
The cast $T% e, which corresponds to R-C AST, can be
implemented as the following method cast(), which casts
obj to class klass.
Object cast(Cla klass, Object obj) {if ((obj instanceof Parametric &&isRuntimeCompatible(Cla.$(obj), klass)) ||klass.cl.isInstance(obj)) {return obj;
} else throw new ClassCastException();}If the type of obj has type arguments, thenisRuntimeCompatible() method checks if the typeof obj and the target type of the cast satisfy the relation: . Otherwise, the cast acts as a normal one, which uses≺
the subtype relation <:. The argument type checking fore.m[T|C<X>](e) in R-I NVK 2 can also be done by thismethod. Although not proved, we conjecture that the
explicit transitivity rule for ≺ is actually redundant. Withouttransitivity, it is easy to check run-time compatibility.
Since $T% is inserted by the translation and types T in
e.m[T|C<X>](e) are specified by the translation, the target
type of a cast can be determined mostly at compile time,
except that the type arguments for X have to be filled at run
time.
The implementation of get(e, f), which corresponds to
R-F IELD 2, is quite easy. We have Object.getClass() toget an instance of java.lang.Class, which has method
getField(), which looks up a field by a field nameand throws NoSuchField exception when no field isfound. The return value of getField() is an instance of
java.lang.reflect.Field, which has method get(),which retrieves the field value from the receiver.
Object get(Object r, String f) {Field fld = r.getClass().getField(f);return fld.get(r);}The special form invoke(e, m, e), which corresponds
to R-I NVK 3, can be implemented as the method invoke()below. Suppose Met is a class for parameter types of amethod, which has field m of java.lang.reflect.Method
and field params of method type descriptors. Also suppose
mtypes() is a method to look up method signatures by amethod name.
Object invoke(Object r, String m, Object[] args) {Met[] mets = mtypes(r, m);
M: for (int i=0, l=mets.length; i < l; i++) {if (mets[i].args.length != args.length)
continue M;
for (int j=args.length-1; 0 <= j; j--) {try {mets[i].params[j].cast(args[j]);} catch (ClassCastException e) {continue M;}}
return mets[i].m.invoke(r, args);}
throw new NoSuchMethodException();}This method looks up methods named m, and calls thefirst method7 whose parameter types match the argument
types. cast() is used to match parameters and arguments.
If the casts succeed, then java.lang.Method.invoke API
performs real invocation of the method. Otherwise, it throws
NoSuchMethodException. Note that the target type of thecast must be determined at run time because we have no
information of the receiver type at compile time.
7 We are not considering method overloading here for simplicity.

5.2 Information on Type Arguments at Run TimeAs we have already seen, we need information on type arguments at run time. It requires additional memory usage
and time costs, but a relatively high performance technique
is proposed by Viroli et al. [32–34]. We quickly review thistechnique.
The basic idea of this technique is to pass type information as a field of an object by transforming the code. For example, the following code describes how the transformation
goes.
Cell<Shape> c= new Cell<Shape>(new Rectangle(...));// Cell<Shape> c//= new Cell<Shape>(//
new Cla(Cell.class,//
new Cla[]{//new Cla(Shape.class) }),//new Rectangle(...));

The first line is the original code, and the comment is thetranslated code. The instance of Cla, which is a type descriptor class, is passed as a first argument of the constructor. Of
course, the definition of class Cell is also transformed to receive a type descriptor at the constructor, and to implement
an interface, which provides access to the type descriptor.
The transformation described above is not optimized atall: a new type descriptor is generated every time the constructor is called. So, a mechanism to reduce the number ofgenerations of type descriptors to one for a distinct type, using double hashing, is reported in [32–34].
5.3 Preliminary Benchmark Evaluation
Since we have no working compiler yet, we only give benchmarks for each run-time check with minimal hand-translated
code using those checks separately. These may help to see if
our implementation idea is reasonable and how much dynamic types slow down execution of the program. Executionof dynamically typed code is quite expensive especially formethod invocations on a receiver of dynamic type, but webelieve that the cost is not unacceptable.
Benchmarks for each run-time check is shown in Table 3.
For each run-time check, we used test code including a single expression with a run-time check and the same expression without it. Each test code iterates 100/10000/1000000
times and overall time consumptions are listed.
For the expression $T% e, we used a static type for thetarget type of the cast. The cast looks into type arguments
but we can say it is not so expensive according to the result.
We can say the same thing about the run-time check inthe expression e.m[T|C<X>](e) since it only needs a castfor each argument. The run-time check in the expression
get(e, f) is relatively expensive because it uses a featureof java.lang.reflect.Field. The run-time check in theexpression invoke(e, m, e) is quite expensive but the cost

# of iterations$T% eeget(e, f)e.fe.m[T|C<X>](e)e.m(e)
invoke(e, m, e)e.m(e)

100 10000 1000000
0.006 0.019
0.125
0.004 0.008
0.087
0.003 0.043
0.356
0.001 0.003
0.056
0.000 0.003
0.072
0.000 0.002
0.080
0.007 0.093
3.430
0.000 0.003
0.069

Table 3. Execution time of each run-time check (sec.)
seems somewhat inevitable since it must resolve a method
signature and check run-time types of the arguments.
In Table 4, we have tested casts with more complex target
types. We used a dynamic type argument for the target type.
The dynamic type argument has a bound, which is a classtype possibly including another dynamic type argument. We
count the nested dynamic type argument as depth and theresult for each target type of the depth is listed in the rows.
Depth(s) \ # of iterations
1
2
3
4
5

100 10000 1000000
0.000 0.004
0.105
0.000 0.007
0.171
0.001 0.009
0.235
0.001 0.008
0.268
0.001 0.009
0.301

Table 4. Execution time of casts (sec.)
We can conclude that the operation for checking the run: is not too expensive in comparison withtime compatibility ≺the other run-time checks.

6. Related Work
There is much work on mixing dynamic and static types (see,for example, Siek and Taha [27, 28] for a more extensive survey). Here, we compare our work mainly with related workon object-oriented programming languages and parametricpolymorphism.
We first review proposals to apply static type checking todynamically typed languages. Bracha and Griswold [6] haveproposed Strongtalk, which is a typechecker for a downward
compatible variant of Smalltalk, a dynamically typed classbased object-oriented programming language. The type system of Strongtalk is structural and supports subtyping andgenerics but does not accept partially typed programs. Thiemann [30] has proposed a type system for (a subset of)
JavaScript, which is a prototype-based object-oriented language, to avoid some kinds of run-time errors by static typechecking. Furr, An, Foster, and Hicks [11] have developed
Diamondback Ruby, an extension of Ruby with a static typesystem. Their type system, which seems useful to find bugs,
however, does not offer static type safety.
Anderson and Drossopoulou [3] have proposed a typesystem for (a subset of) JavaScript for the evolution fromJavaScript to Java. Although it is nominal and concernedwith script-to-program evolution, their type system does nothave subtyping, inheritance, or polymorphism; moreover,this work is not concerned about safety of partially typed
programs in the middle of the evolution.
Lagorio and Zucca [22] have developed Just, an extensionof Java with unknown types. Although there is some overlap
in the expected uses of this system and gradual typing, themain purpose of unknown types is to omit type declarations;
possibly unsafe use of unknown types is rejected by the typesystem. They use reflection to implement member access on
unknown types.
Gray, Findler, and Flatt [14] have implemented an extension of Java with dynamic types and contract checking [9]for interoperability with Scheme. They mainly focus on thedesign and implementation issues and give no discussion on
the interaction with generics. Their technique to implement
reflective calls can be used for our setting.
Gray [12, 13] studied mixing Java as a statically typed
language and JavaScript as a dynamically typed scripting
language. Unlike our language, classes with dynamically
typed methods are allowed to inherit from a class that is
statically typed, and vice versa.
As we have already mentioned, Siek and Taha have studied gradual typing for Abadi-Cardelli’s object calculus [28].
However, the language is object-based (as opposed to classbased) and parametric polymorphism is not studied. Anotherpoint is that the implementation of run-time checks for classbased languages seems easier than that for object-based
languages, since, in class-based languages, every value istagged with its run-time type information and the checkcan be performed in one step (unlike higher-order contract
checking, which checks inputs to and outputs from functions
separately).
Sage [15], a functional language based on hybrid typechecking [10], supports both parametric polymorphism anddynamic types. Matthews and Ahmed [24] and, more recently, Ahmed, Findler, Siek, and Wadler [2] give theoretical accounts for the combination of impredicative polymorphism with dynamic typing. In all of these works, a dynamic
type is compatible (in our terminology) with universal types
whereas there is no counterpart of universal types in our setting. None of them has addressed bounded polymorphism.
Wrigstad, Nardelli, Lebresne, Östlund and Vitek [5, 38]
have developed a language called Thorn, which integrates
static and dynamic types in a different way. They have introduced the notion of like types, which interface between
statically and dynamically typed code. A variable of like
C is treated as type C at compile time but any value can flow
into the variable at run time (subject to run-time checks).

This is different from dyn<C>, which allows any operations
statically but only subtypes of C can flow into a dyn<C>.
Bierman, Meijer and Torgersen[4] added dynamic types
to C♯ . They also translate a program of the surface language
into intermediate code, which has explicit run-time checks.
In their setting, dynamic types can be arguments of genericclasses, but their subtype relation is only invariant with respect to type parameters, so, for example, it is not possible
to pass Cell<Rectangle> to Cell<dyn>.
There is some work on applying the gradual approach toadvanced type systems for object-oriented programming languages. Wolff, Garcia, Tanter and Aldrich [36] developed agradual system for typestate-oriented programming, whereoperations on an object are restricted by the internal stateof the object. Potentially safe code which rejected by othertypestate-oriented type systems can be accepted in their system thanks to a dynamic type. Sergey and Clarke [26] proposed a gradual system for ownership types, which represent encapsulation of objects and are used as invariants intype checking. Their gradual system allows a programmer
to omit ownership annotations without losing encapsulation
properties of annotated code.
There are some related features that already exist in Java.
Wildcards, studied by Igarashi and Viroli [17] and Torgersen, Ernst, Hansen, Ahé, Bracha and Gafter [31], enable
a flexible subtyping with both co- and contra-variant parametric types, though only statically resolved members canbe accessed on a receiver of a wildcard type and it is not allowed to specify a wildcard type as a type argument in a new
expression. Raw types are proposed by Bracha, Odersky,
Stoutamire, and Wadler [7] to deal with compatibility between legacy monomorphic Java code and new polymorphic
Java code. A generic class C<X> can be used as a raw type C,
without type arguments, and assigning a value of C<T> to avariable of C, or even creating an instance of C via new expression are allowed. This behavior is similar to FGJdyn ’s if
we consider C to be an abbreviation of C<dyn, ..., dyn>.
However, with raw types, even statically typed code can gowrong.

compiler by extending an existing Java compiler without
modifying JVM.
Future Work. Our run-time compatibility does not allow argument passing, for example, from Cell<dyn> toCell<Rectangle>. It might be too early to abort the execution at this point since the value in the Cell may not be
used at all. We think we can relax the restriction by deferring
the check until the field is accessed. Then, we need a blame
assignment system [2, 35] for precise error reports. Implementation of the blame tracking system for this design wethink is done by “wrapping” an object with another object.
The wrapping object has the same interface as the original
one, but it performs a run-time check on every member access. In a simple setting, a subclass of the class of the original
object suffices for the class of the wrapping object. However,there are at least two problems in this implementation strategy for Java-like languages. First, we need some mechanism
to “wrap” an ordinary field access. Second, a wrapping classcannot extend a final class.
When bytecode of a generic library class compiled by thestandard Java compiler is used with client bytecode compiled by our compiler, the client is not allowed to use dynamic type arguments to the generic class since type variables in the generic class are declared without kind . We
think that converting the library bytecode at load time will
help to relax this restriction.
We also plan to investigate the interactions of dynamic
types with other features such as overloading to make thelanguage more realistic.

Acknowledgments
We thank the anonymous reviewers very much for thoughtful and thorough reviews. Ina is a Research Fellow of theJapan Society of the Promotion of Science. This work was
supported in part by Grant-in-Aid for Young Scientists (A)No. 21680002 and by Grant-in-Aid for JSPS Fellows No.
10J06019.

References
7. Conclusions
We have designed a language that combines dynamic types
and generics. The language allows dynamic types to be used
as type arguments of a generic class and realizes smoothinterfacing between dynamically and statically typed code
thanks to the flexible compatibility relation. We have introduced bounded dynamic types to deal with the case where atype parameter has an upper bound.
The language is formalized as a minimal core model ofJava including the feature of generics. As in other gradualtype systems, we have proved safety properties, which ensure that statically typed parts in a program never go wrong.
We have also reviewed the sketch of an implementation
scheme, which is an idea to develop a gradually typed Java

[1] M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin. Dynamic
typing in a statically typed language. ACM Trans. Prog. Lang.
Syst., 13(2):237–268, 1991.
[2] A. Ahmed, R. B. Findler, J. G. Siek, and P. Wadler. Blame forall. In Proc. of ACM POPL’11, pages 201–214, Austin, TX,
Jan. 2011.
[3] C. Anderson and S. Drossopoulou. BabyJ - from object based
to class based programming via types. In Proc. of WOOD’03,
volume 82 of Elsevier ENTCS, pages 53–81, 2003.
[4] G. Bierman, E. Meijer, and M. Torgersen. Adding dynamic
types to C♯ . In Proc. of ECOOP’10, volume 6183 of Springer
LNCS, pages 76–100, Maridbor, Slovenia, June 2010.
[5] B. Bloom, J. Field, N. Nystrom, J. Östlund, G. Richards,
R. Strniša, J. Vitek, and T. Wrigstad. Thorn — robust, con-

current, extensible scripting on the JVM. In Proc. of ACM
OOPSLA’09, pages 117–136, Orlando, FL, Oct. 2009.
[6] G. Bracha and D. Griswold. Strongtalk: Typechecking
Smalltalk in a production environment. In Proc. of ACM
OOPSLA’93, pages 215–230, 1993.
[7] G. Bracha, M. Odersky, D. Stoutamire, and P. Wadler. Making
the future safe for the past: Adding genericity to the Java
programming language. In Proc. of ACM OOPSLA’98, pages
183–200, Vancouver, BC, Oct. 1998.
[8] R. Cartwright and M. Fagan. Soft typing. In Proc. of ACM
PLDI’91, pages 278–292, 1991.
[9] R. B. Findler and M. Felleisen. Contracts for higher-orderfunctions. In Proc. of ACM ICFP’02, pages 48–59, 2002.
[10] C. Flanagan. Hybrid type checking. In Proc. of ACM
POPL’06, pages 245–256, Charleston, SC, Jan. 2006.
[11] M. Furr, J. An, J. S. Foster, and M. Hicks. Static type inference
for Ruby. In Proc. of ACM Symposium on Applied Computing(SAC’09), pages 1859–1866, Mar. 2009.
[12] K. E. Gray. Safe cross-language inheritance. In Proc. of
ECOOP’08, volume 5142 of Springer LNCS, pages 52–75,
2008.
[13] K. E. Gray. Interoperability in a scripted world: Putting
inheritance & prototypes together. In Proc. of FOOL’10, Oct.
2010.
[14] K. E. Gray, R. B. Findler, and M. Flatt. Fine-grained interoperability through mirrors and contracts. In Proc. of ACM
OOPSLA’05, pages 231–245, 2005.
[15] J. Gronski, K. Knowles, A. Tomb, S. N. Freund, and C. Flanagan. Sage: Hybrid checking for flexible specifications. In
Proc. of the Scheme and Functional Programming Workshop,
pages 93–104, Sept. 2006.
[16] F. Henglein. Dynamic typing. In Proc. of ESOP’92, volume
582 of Springer LNCS, pages 233–253, Rennes, France, Feb.
1992.
[17] A. Igarashi and M. Viroli. Variant parametric types: A flexible
subtyping scheme for generics. ACM Trans. Prog. Lang. Syst.,
28(5):795–847, Sept. 2006.
[18] A. Igarashi, B. C. Pierce, and P. Wadler. Featherweight Java:A minimal core calculus for Java and GJ. ACM Trans. Prog.
Lang. Syst., 23(3):396–450, May 2001.
[19] L. Ina and A. Igarashi. Towards gradual typing for generics.
In Proc. of STOP’09, pages 17–29, Genova, Italy, July 2009.
Available also in the ACM Digital Library.
[20] L. Ina and A. Igarashi. Gradual typing for Featherweight Java.
Computer Software, 26(2):18–40, Apr. 2009. In Japanese.
[21] A. J. Kennedy and B. C. Pierce. On decidability of nominal
subtyping with variance. In Proc. of FOOL/WOOD’07, Nice,
France, Jan. 2007.
[22] G. Lagorio and E. Zucca. Just: safe unknown types in Javalike languages. Journal of Object Technology, 6(2):69–98,
Feb. 2007.
[23] B. H. Liskov and J. M. Wing. A behavioral notion of subtyping. ACM Trans. Prog. Lang. Syst., 16(6):1811–1841, Nov.
1994.

[24] J. Matthews and A. Ahmed. Parametric polymorphism
through run-time sealing, or, thorems for low, low prices! In
Proc. of ESOP’08, volume 4960 of Springer LNCS, pages 16–
31, 2008.
[25] M. Odersky and P. Wadler. Pizza into Java: Translating theory
into practice. In Proc. of ACM POPL’97, pages 146–159, Jan.
1997.
[26] I. Sergey and D. Clarke. Towards gradual ownership types. In
Proc. of IWACO’11, Lancaster, UK, July 2011.
[27] J. G. Siek and W. Taha. Gradual typing for functional languages. In Proc. of the Scheme and Functional Programming
Workshop, pages 81–92, Sept. 2006.
[28] J. G. Siek and W. Taha. Gradual typing for objects. In Proc.
of ECOOP’07, volume 4509 of Springer LNCS, pages 2–27,
2007.
[29] S. Thatte. Quasi-static typing. In Proc. of ACM POPL’90,
pages 367–381, Jan. 1990.
[30] P. Thiemann. Towards a type system for analyzing JavaScript
programs. In Proc. of ESOP’09, volume 3444 of Springer
LNCS, pages 408–422, 2005.
[31] M. Torgersen, E. Ernst, C. P. Hansen, P. von der Ahé,
G. Bracha, and N. Gafter. Adding wildcards to the Java programming language. Journal of Object Technology, 3(11):97–
116, Dec. 2004. Special issue: OOPS track at SAC 2004.
[32] M. Viroli. A type-passing approach for the implementationof parametric methods in Java. The Computer Journal, 46(3):263–294, 2003.
[33] M. Viroli. Effective and efficient compilation of run-time
generics in Java. In Proc. of WOOD’04, volume 138 of
Elsevier ENTCS, pages 95–116, 2004.
[34] M. Viroli and A. Natali. Parametric polymorphism in Java: An
approach to translation based on reflective features. In Proc.
of ACM OOPSLA’00, pages 146–165, Oct. 2000.
[35] P. Wadler and R. B. Findler. Well-typed programs can’t beblamed. In Proc. of ESOP’09, volume 5502 of Springer
LNCS, pages 1–16, York, UK, Mar. 2009.
[36] R. Wolff, R. Garcia, É. Tanter, and J. Aldrich. Gradual typestate. In Proc. of ECOOP’11, volume 6813 of Springer LNCS,
pages 459–483, Lancaster, UK, July 2011.
[37] A. K. Wright and M. Felleisen. A syntactic approach totype soundness. Information and Computation, 115(1):38–94,
Nov. 1994.
[38] T. Wrigstad, F. Z. Nardelli, S. Lebresne, J. Östlund, and
J. Vitek. Integrating typed and untyped code in a scripting
language. In Proc. of ACM POPL’10, pages 377–388, 2010.