Towards Gradual Typing for Generics
Lintaro Ina and Atsushi Igarashi
Graduate School of Informatics, Kyoto University{ina,igarashi}@kuis.kyoto-u.ac.jp

Abstract. Gradual typing, proposed by Siek and Taha, is a framework
to combine the benefits of static and dynamic typing. Under gradualtyping, some parts of the program are type-checked at compile time,
and the other parts are type-checked at run time. The main advantage
of gradual typing is that a programmer can write a program rapidly
without static type annotations in the beginning of development, then
add type annotations as the development progresses and end up witha fully statically typed program; and all these development steps arecarried out in a single language.
This paper reports work in progress on the introduction of gradual typing
into class-based object-oriented programming languages with generics. In
previous work, we have developed a gradual typing system for Featherweight Java and proved that statically typed parts do not go wrong. After
reviewing the previous work, we discuss issues raised when generics are
introduced, and sketch a formalization of our solutions.

1

Introduction

Siek and Taha have coined the term “gradual typing” [1] for a linguistic support of the evolution from dynamically typed code, which is suitable for rapid
prototyping, to fully statically typed code, which enjoys type safety properties,
in a single programming language. The main technical challenge is to ensure
some safety property even for partially typed programs, in which some part isstatically typed and the rest is dynamically typed.
The framework of gradual typing consists of two languages: the surface language in which programmers write programs and the intermediate language into
which the surface language translates. The type system of the surface language
allows dynamically and statically typed portions to be seamlessly mixed by, forexample, allowing an expression of dynamic type to be passed to a statically
typed parameter. In order to ensure safety of statically typed parts, run-time
checks are required on the “border” between the statically typed and dynamically typed worlds. The translation into the intermediate language makes theserun-time checks explicit. The expected safety property then would be that a welltyped surface language program translates to a well-typed intermediate language
program, which can fail only at run-time checks inserted by the translation.
When the program is fully statically typed, no checks will be inserted, hence norun-time type errors will occur.

In this paper, we discuss our work in progress on the theory of gradual typing for class-based object-oriented programming languages with generics, such
as Java and C#. C# 4.0 [2] is going to include dynamic types but it has notbeen mentioned how dynamic types and generics are combined. Although Siek
and Taha [3] have studied gradual typing for Abadi-Cardelli’s first-order objectcalculus with subtyping [4], (as far as we know) there have been no study on
gradual typing for a class-based language with a nominal type system and generics.
We first report on our previous work [5] on gradual typing for FeatherweightJava (FJ) [6]. As in Siek and Taha [1, 3], we have added the dynamic type ?, a(static) type identifier for dynamically typed expressions. Since FJ is a simplest
possible choice as the base language, actually, there is little additional technicalsubtlety compared to other settings. Nevertheless, we believe it is interesting
to review, since the formal translation shows how gradual typing can be implemented with the combination of typecasts and reflection. We also point out
another safety property of gradual typing: “potentially typeable programs do
not go wrong”, which is proved for gradually typed FJ. Intuitively, it means
that, if a given program can be made statically typed only by adding static type
annotations, then it can already run safely. In other words, the inserted run-time
checks would not prevent safe execution, which would have been ensured only
by adding static type annotations.
Then, we discuss issues in the combination of generics and gradual typing.
One natural consequence of this combination is that type variables may be instantiated with ?. To deal with such an instantiation in the presence of boundedpolymorphism, we introduce the notion of bounded dynamic types, which havecharacteristics of both ? and ordinary types. Another consequence, which we discuss, is that the run-time type of an object may involve ?. Finally, we sketch thehighlights of our formalization work, which is in the middle of the development.
Related Work. There is much work on mixing dynamic and static types (see, forexample, Siek and Taha [3] for a more extensive survey). Here, we compare ourwork mainly with related work on object-oriented programming languages.
Some type systems are proposed to achieve benefits of static type checking in
dynamically typed languages. Bracha and Griswold [7] have proposed Strongtalk,which is a typechecker for a downward compatible variant of Smalltalk, a dynamically typed class-based object-oriented programming language. The typesystem is structural and supports subtyping and generics. Strongtalk does not
accept partially typed programs. Thiemann [8] have proposed a type system for(a subset of) JavaScript, which is a prototype-based object-oriented language, toavoid some kind of run-time errors by static type checking. This work does not
attempt to support the evolution from dynamically typed program to statically
typed program. Furr, An, Foster, and Hicks [9] have developed Diamondback
Ruby, an extension of Ruby with a static type system. Their type system, which
seems useful to find bugs, however, does not offer static type safety.
Anderson and Drossopoulou [10] have proposed a type system for (a subsetof) JavaScript for the evolution from JavaScript to Java. Although it is nominaland concerned about 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 [11] have developed Just, an extension of Java with unknown types. Although there is some overlap in the expected uses of this system
and gradual typing, the main purpose of unknown types is to omit type declarations; possibly unsafe use of unknown types is rejected by the type system.
They use reflection to implement member access on unknown types.
Gray, Findler, and Flatt [12] have implemented an extension of Java with dynamic types and contract checking [13] for interoperability with Scheme. However, they mainly focus on the design and implementation issues and give no
discussion on the interaction with generics. Their technique to implement reflective calls can be used for our setting.
As we have already mentioned, Siek and Taha have studied gradual typing
for Abadi-Cardelli’s object calculus [3]. However, the language is object-based
and parametric polymorphism is not studied. Another point is that the implementation of run-time checks for class-based languages seems easier than thatfor object-based languages, since, in class-based languages, every value is taggedwith its run-time type information and the check can be performed in one step
(unlike higher-order contract checking, which checks inputs to and outputs fromfunctions separately).
Siek and Vachharajani [14] and Matthews and Ahmed [15] have discussed the
combination of dynamic typing and parametric polymorphism in the λ-calculus.
Aside from the difference in target languages, they have not addressed boundedpolymorphism.
The Rest of This Paper. In Section 2, we review our previous work on gradualtyping for Featherweight Java. Then, in Section 3, we discuss issues in extending
it to generics. Section 4 sketches our formalization work and Section 5 gives
concluding remarks. Throughout the paper, we assume basic knowledges about
the formalism of Featherweight Java [6].

2Summary of Gradual Typing for FJ

In this section, we review the previous work [5] on gradual typing for Featherweight Java (FJ) [6]. Just as other work on gradual typing, there are two
languages: the surface language called FJ? , which is equipped with the dynamic
type ?;1 and the intermediate language called FJrefl , which has reflective member access operations. The relation between the two languages is illustrated in
Figure 1 with some of the judgment forms in these languages. Although FJ? hasa type system, its semantics is given only by a translation, denoted by , tomake run-time checks explicit. FJrefl is given both a type system and a direct
operational semantics.
1

Note that ? is already reserved in Java proper for wildcard types [16]; here, we follow
the notational convention used in other work on gradual typing.

FJ? = FJ + dynamic typetyping (Γ ⊢G eg : T)translation(Γ ⊢ eg

FJrefl = FJ + reflection
typing (Γ ⊢R er : T)er : T)
reduction (er −→R e′r )Fig. 1. FJ? and FJrefl .

We first describe typing in FJ? and translation to FJrefl informally by meansof a small example, and then give an excerpt from the formalization and thetheorems of safety properties.
2.1

Informal Review?

In FJ , ? can be used, instead of class names, where types are expected; and itmeans the expression is dynamically typed. For example, in the following classtable, class W has field f of dynamic type. (⊳ is an abbreviation for extends.)
class X ⊳ Object {Object m(A x) { return x.f; }}class A ⊳ Object { Object f; }class B ⊳ Object { }class W ⊳ Object { ? f; }? resembles Object in that a variable of type ? can be bound to any object;however, it is more permissible than Object. First, an expression of type ? canbe passed to anywhere. Consider the following example.
new X().m(new B());
new X().m(new W(new B()).f);// rejected// well typed

The first expression will be rejected in type checking because it attempts to pass
the expression of type B as an argument of type A. The second expression, on
the other hand, is well typed since the static type of the field access is ?, eventhough new B() will be eventually passed through to the method m. Second, any
method invocation or field access on ? is allowed and the whole expression is,again, given type ?, while Object (in FJ) does not allow any.
The semantics of FJ? is given by translation into FJrefl , in which run-time
checks are explicit. Since FJrefl does not have dynamic types, all occurrences of? will be simply replaced by Object. When an expression of type ? is passed toa typed parameter, a run-time typecheck is inserted to prevent erroneous values
from flowing into a typed context. Method invocations and field accesses whose
receiver is of type ? in FJ? are translated into reflective member accesses, written
invoke() and get(), respectively, of FJrefl . The following example shows how
this goes.
new X().m(new W(new B()).f)

new X().m($A% new W(new B()).f)→ new X().m($A% new B())
new W(new X()).f.m(new B())
invoke(new W(new X()).f, m, new B())→ invoke(new X(), m, new B())→ ($A% new B()).f

Here,
denotes the translation from FJ? into FJrefl ; → denotes a reduction stepin FJrefl ; and $C% denotes a run-time typecheck inserted by the translation—
actually, its semantics is the same as ordinary typecasts in this setting, so we
use the ordinary notation (C) in what follows in this section. invoke(e,m,e)
invokes method m of (the value of) e; it is checked whether the method exists,
whether the number of arguments agree, and whether the (run-time) type of
the actual argument ei is a subtype of the formal argument type. In the translation/reduction sequences above, the underlined parts denote run-time errors.
The first one shows that an invalid argument is detected before m has been invoked and the second shows that an invalid argument is detected at a reflective
method invocation.2
As we will see below, we have proved that an FJrefl program translated froma well-typed FJ? program is also well typed and a well-typed FJrefl program
never yields run-time errors except one caused by reflective member accesses or
run-time typechecks inserted by the translation.
2.2

Formalization

As we have mentioned earlier, the syntax of FJ? is the same as FJ except that
we can use ? as a type. We show the two typing rules for method invocations,which are most interesting. The judgment Γ ⊢G e : T means that expression e isof type T in the environment Γ (T, U, and V range over types).
Definition 1 (Typing).
Γ ⊢G e 0 : C 0
Γ ⊢G e : U
mtype(m, C0 ) = V → T
U.VΓ ⊢G e0 .m(e) : TΓ ⊢G e 0 : ?
Γ ⊢G e : UΓ ⊢G e0 .m(e) : ?

The first rule is usual except that a new relation . (called consistent-subtyping
after Siek and Taha [3]) is used for ordinary subtyping < :. This new relation
takes into account the dynamic type and is defined by: T . U if and only if either(1) one of the two types is ? or (2) both types are class names and T <: U. Noticethat . is not (nor should it be—see [3]) a transitive relation. Other typing rules
are mostly straightforward adaptations of those from FJ. We write ⊢G (CT, e) : T
to mean a program (CT, e) is well typed with expression e being of type T.
The syntax of FJrefl is the same as FJ except that it has reflective member
accesses get(e, f) and invoke(e, m, e). The judgment for translation from FJ?
to FJrefl is of the form Γ ⊢ ee′ : T, read “FJ? expression e of type T underenvironment Γ translates to FJrefl expression e′ .” The translation is directed bytype derivations. We show only the rules for method invocations:2

In this case, this error could have been detected at the same time as the method
invocation. In general, however, the check for actual arguments cannot be performedat the same time, since FJrefl is not a call-by-value language (like FJ). The semantics
of invoke() is given in such a way that a run-time check is inserted for every actualargument.

Definition 2 (Translation).
Γ ⊢ e0e′0 : C0Γ ⊢ee′ : UU.VΓ ⊢ e0e′0 : ?
Γ ⊢ee′ : Umtype(m, C0 ) = V → TΓ ⊢ e0 .m(e)e′0 .m(hhV ⇐ Uiie′ ) : TΓ ⊢ e0 .m(e)invoke(e′0 , m, e′ ) : ?
(C)e (if V = C and U = ?)defhhV ⇐ Uiie =e(otherwise)
The first rule is for ordinary invocations; hhV ⇐ Uii inserts a run-time check when
U is the dynamic type. The second rule deals with the case where the receiver
type is ?; the method invocation is translated into invoke(). The translationof type T (written |T|) is obtained by replacing ? with Object and that of classtable CT (written |CT |) is by replacing every type and method body with theirtranslations.
The form of typing judgments of expressions in FJrefl is Γ ⊢R e : T and weuse ⊢R (CT, e) : T for typing of a program. We omit typing rules, since they arestraightforward. Reduction −→R in FJrefl is basically the same as in FJ (i.e., full
reduction) except the additional rules below for reflective member accesses.
Definition 3 (Reduction).
fields(C) = T fget(new C(e), fi ) −→R ei

2.3

mbody(m, C) = x.e0
mtype(m, C) = V → T
invoke(new C(e), m, d)−→R [(V)d/x, new C(e)/this]e0

Properties

Soundness of FJ? consists of the following two theorems, which we have proved:
the first states type soundness for the intermediate language FJrefl and is proved
via subject reduction and progress. The second states that a well-typed FJ?
program translates into a well-typed FJrefl program. Combining these two, we
can see that a member access whose receiver is of class type is translated to an
ordinary, non-reflective access, which will not fail. In other words, a statically
typed portion without ? will never fail.
Theorem 1 (Type safety of FJrefl ). If a program (CT, e) satisfies ⊢R (CT, e) : T
and there exists a normal form expression e′ where e −→∗R e′ , then one of thefollowing statements holds.
1. e′ is a value v where ∅ ⊢R v : C and C <: T.
2. A subexpression e0 in e′ satisfies ∃C, D, e.(e0 = (D)new C(e) ∧ C 6<: D).
3. A subexpression e0 in e′ satisfies∃C, e, f.(e0 = get(new C(e), f) ∧ ∀T, f.(fields(C) = T f ⇒ f ∈/ f)).
4. A subexpression e0 in e′ satisfies∃C, e, m, d.(e = invoke(new C(e), m, d) ∧ ∀x, e0 .(mbody(m, C) = x.e0 ⇒#(x) 6= #(d))).

Theorem 2 (Type safety of FJ? ). If ⊢G (CT, e) : T, then there exists a translation from (CT, e) into (|CT |, e′ ) satisfying ⊢R (|CT |, e′ ) : |T|.
Another interesting property we have proved (but other previous work hasnot) is that, if an FJ? program can evolve to an FJ program (without ?) only
by changing type declarations, the FJ? program yields the same result as theevolved program, without failures at run-time checks. In the statement below,
the subscript FJ means that the judgment is derived with the rules of FJ.
Theorem 3 (Safety of potentially typeable programs). Assume that ⊢G(CT1 , e) : T1 and (CT1 , e) is translated into (|CT1 |, e′ ) ∈ FJrefl . If ⊢FJ (CT2 , e) : T2
and CT2 is obtained by replacing every ? in CT1 with a class name, then e −→∗FJ
v under CT2 implies e′ −→∗R v under |CT1 |.

3

Combining Gradual Typing and Generics

In this section, we informally discuss design questions raised when combining
gradual typing and generics. As we introduce generics, the syntax of types has
a structure: a type is not a simple name, rather a combination of a class nameas a type constructor and an appropriate number of types as arguments to it.
So, the first (perhaps rather obvious) question is “Can the dynamic type ? be a
type argument?”
Our answer is definitely yes, since it will allow more flexible evolution, inparticular, from a non-generic class to its generic version. For example, whenclass List is evolved to a generic version List<X>, the occurrences of List in
old client code is not a type any longer, breaking the client code, but, if we think
List (lacking a type argument) as an abbreviation of List<?>, there is morechance for the client code to remain well typed without modification. Indeed,
the need for such an evolution was the main motivation for raw types [17, 18]
in GJ (and Java 5.0). Our gradual typing for generics can be considered anenhancement of raw types with some safety guarantee3 (the formal proof ofwhich we leave for future work).
In what follows, we discuss two questions raised when we allow ? to be a
type argument. One is concerned about the interaction between ? and the upperbounds of type variables. The other is about the meaning of an object whose
run-time type involves ?.
3.1

Bounded Dynamic Types

To discuss the interaction between the upper bounds of type variables and the
dynamic type, first consider the following class C and type expression C<?>.
3

For possibly unsafe use of raw types, the compiler issues an unchecked warning but
there is no guarantee that the code portion without raw types is safe.

class C<X ⊳ Number> ⊳ Object {X f;
int m(X x){ return x.intValue(); }}Since a method signature is supposed to be obtained by substituting actual typearguments for corresponding type variables, it seems that the invocation of m
on C<?> can take ?, namely anything. However, this interpretation is obviously
wrong, since passing, say, a String to m would make the program crash at the
invocation of intValue(). In other words, instantiating with ? a type variable
that is given a non-trivial upper bound will break the promise of gradual typingthat a statically typed portion without ? will never fail.
One possible remedy would be to weaken the promise and to say “A statically
typed portion will never fail as long as type variables are instantiated with types
without ?.” This sounds like a reasonable option since it is the client who abuses
the class C by “polluting” statically typed code with ?.
However, we do not think it is really a good idea mainly from the implementation point of view. In this case, the method m would have to behave in
two different ways, according to what X is bound to: on the one hand, if X is
instantiated with an ordinary type such as Integer, m works as usual; on theother hand, if X is instantiated with ?, the invocation of intValue() will involvea reflective method call and run-time checks. Such an implementation will not
be easy.
Another remedy, which we propose here, is to prevent non-Number objects
from flowing into x both statically and dynamically. By “statically,” we mean thatan expression of an unrelated type, say String, as an argument to m is staticallyrejected by the compiler. By “dynamically,” we mean that an expression of
dynamic type as an argument to m is accepted by the compiler but it is checked
at run time whether the value is really a Number.
To formally express the idea above in the type system, we introduce thenotion of bounded dynamic types. A bounded dynamic type, written ?N where
N is a parameterized type (or a non-variable type in the FGJ terminology), issimilar to the dynamic type ?, which is now an abbreviation of ?Object , in thefollowing sense. The type system allows (1) members that do not exist in class
N to be accessed and (2) an expression of type ?N to be passed where a subtype
of N is expected. For example, the following statements are well typed.
new C<?Number >(new Float(1.0)).f.isNaN();// (1)
Double d = new C<?Number >(new Float(1.0)).f; // (2)In these statements, new C<?Number >(...).f has type ?Number . In the first statement, method isNaN(), which does not exist in class Number, is called. In thesecond statement, an expression of type ?Number is passed where Double, which isa subtype of Number, is expected. It differs from ?, however, in that (1) the usual
typing rule is applied when a method existing in N is invoked, (2) an expressionof type ?N cannot be passed to where an unrelated type is expected, and (3) avariable (or parameter) of type ?N cannot accept an expression of an unrelated
type. For example, consider the following statements.
int i = new C<?Number >(new Long(1)).f.intValue(); // (1) well typed
String s = new C<?Number >(new Integer(1)).f;// (2) rejected
new C<?Number >(new Integer(1)).m("foo");// (3) rejected
Again, new C<?Number >(...).f has type ?Number . The first statement is well typed
because Number.intValue() exists with the return type int. The second statement is rejected because String and Number are not related (that is, neither isa subtype of the other). The third expression is also rejected because "foo" hastype String but it is not related to the expected type Number.
We use . to perform type checking mentioned above in a way similar to FJ? .
It differs from FJ? in that a type has a structure and it may involve bounded
dynamic types. Intuitively, S . T means that replacing each ? in S, T with anappropriate type (without ?) below its bound will satisfy S < : T. The formal
definition of . in this meaning is described in Section 4.
By the introduction of bounded dynamic types, we do not have to weaken
the above-mentioned promise of gradual typing, since erroneous values cannot be
flown into a statically typed part even when a type variable is instantiated by a(bounded) dynamic type. Also, implementation is not hard since the behavior ofa statically typed part does not depend on how type variables are instantiated.
We do not expect that programmers write upper bounds for occurrences of?. Rather, it is the compiler’s job to infer them: for each ?, its upper boundwill be the same as that of the corresponding type parameter.4 Nevertheless, it
may be a good idea to let programmers write upper bounds (and, possibly, evenlower bounds as in wildcards) when they want to.
3.2

Bounded Dynamic Types and Run-Time Checks

For run-time checking, expressions are translated into the language with reflective member accesses and cast operations for explicit run-time checks in the same
way as in FJ? . However, we have to be careful with the cast operation since both
source and target types of the cast may involve ? like C<?N >.
We first consider the case where the target type includes ?:C<?Number > c = e

C<?Number > c = $C<?Number >% e

The expression assigning e to the variable of type C<?Number > translates into theexpression with the cast operation. It states that e must be reduced to a value oftype C with its type argument being a subtype of Number. So, when e is reduced,
for example, to new C<Integer>(...), the cast operation should succeed, on
the other hand, when e is reduced, for example, to new C<Object>(...), theoperation should fail.
For the case where the source type includes ?, consider the following example.
4

Strictly speaking, if a type variable has an F-bound—a bound that refers to the typevariable recursively, it is not clear what should be attached. We leave this issue for
future work and F-bounds are omitted from the current formalization.

C<?Number > c1 = new C<?Number >(n);C<Integer> c2 = c1;
where n is given type Number. Then, the variable reference c1 in the second
statement will be translated to $C<Integer>% c1. When does this cast succeed?
We conclude that it always fails no matter what n is: if n is not an Integer,
c2 will point to an invalid value. Another, possibly interesting option may be
to allow this check to succeed when n happens to be an Integer; however, it is
not clear how to achieve safety with this option—for example, when a Float is
assigned to c1.f, which is of type ?Number , it becomes an invalid value for c2.f,
an alias of c1.f of type Integer.
The run-time check required by the cast expression $T2% new C<T1 >(...)
can be implemented by checking |C<T1 >| . T2 , where |T| denotes replacing every? in T with its bound. Here, ? in the source type needs to be replaced to implement checks as in the second case above correctly. Without |·|, $C<Integer>% c1
would succeed since C<?Number > . C<Integer> but |C<?Number >| = C<Number> 6.
C<Integer>.

4

Formalization

In this section, we sketch a formalization of our design discussed in the previous
section. We formalize FGJ? as an extension of FGJ and FJ? . For simplicity, we
omit some features found in FGJ. They include F-bounded polymorphism, polymorphic methods, and typecasts, which would be easy to add. (F-bounded polymorphism makes the inference of appropriate bounds for ? non-trivial, though.)
The work is still in progress and we focus on typing of the surface language here.
We follow the metavariable convention of FGJ [6]. The syntax of FGJ? ismostly the same as FGJ except bounded dynamic types and the omitted features.
Definition 4 (Types and syntax of FGJ? ).
S, T, U, V ::= X | N | ?N
L ::= class C<X ⊳ N> ⊳ N {T f; K M}
N ::= C<T>
K ::= C(T f){super(f); this.f=f;}e ::= x | e.f | e.m(e) | new N(e) M ::= T m(T x){ return e; }The bound for a bounded dynamic type must be a nonvariable type N.
The main judgments used in the type system are: (1) ∆ ⊢ S <: T for subtyping; (2) ∆ ⊢ S . T for consistent-subtyping; (3) ∆ ⊢ T ok for well-formed types;and (4) ∆; Γ ⊢ e : T for expression typing, where ∆ is a bound environment,
which is a finite mapping from type variables to nonvariable types.
The subtyping relation is basically the same as that in FGJ. Note thatbounded dynamic types are related only to themselves by reflexivity. When actual and formal argument types are compared, we use the consistent-subtyping
relation . as in FJ? . It is defined via the consistency relation ∼, which relates
dynamic types and ordinary types:
Definition 5 (Consistent-subtyping).

∆⊢S∼T∆ ⊢ C<S> ∼ C<T>∆⊢T∼N
∆ ⊢ T ∼ ?N

∆ ⊢ T <: N
∆ ⊢ T ∼ ?N

∆ ⊢ S <: T
∆⊢T∼U
∆⊢S.U

∼ is reflexive and symmetric (we omit rules for these). As seen from the lastrule, the rules are not algorithmic. The development of a decision algorithm for. is not yet finished.
Typing rules are actually obtained by combining those of FJ? and of FGJ ina straightforward manner. Here are the two rules of method invocation.
Definition 6 (Typing rules of expressions).
∆; Γ ⊢G e0 : T0 ∆; Γ ⊢G e : V
mtype(m, bound∆ (T0 )) = U → U ∆ ⊢ V . U∆; Γ ⊢G e0 .m(e) : U∆; Γ ⊢G e0 : ?N ∆; Γ ⊢G e : V
nomethod (m, bound∆ (?N ))∆; Γ ⊢G e0 .m(e) : ?Object

The first rule is the typing rule of method invocation when the method definitely exists, i.e., mtype(m, bound∆ (T0 )) = U → U, in the receiver. We definebound∆ (?N ) = bound∆ (N), which means that, even if the receiver type is dynamic, the number of arguments and actual argument types are checked statically (by using .). The second rule is the other typing rule of method invocation, applied when the receiver type is dynamic and the method may not exist.
nomethod (m, bound∆ (?T0 )) means that the specified class and its super classes
do not have method named m. Nevertheless, this method invocation is allowed
statically, since, at run time, the value of e0 may have method named m. Thiskind of method invocation will be translated into a reflective call, which checks
if method m really exists.
The definitions of the intermediate language and the translation to it areomitted but mostly complete along the line described in the previous section. We
need to prove desired properties, including type soundness of the intermediate
language, type preservation of the translation, and safety of potentially typeable
programs, as we have done for FJ? .

5Conclusion

This paper reports work in progress on the introduction of gradual typing intoclass-based object-oriented languages with Java-style generics. We have reviewed
the development of the gradual typing system FJ? , which translates into a language with reflective member accesses for explicit run-time checks. Then, we
have informally discussed issues raised when gradual typing and generics are
combined and sketched an extension FGJ? of FJ? with generics.
The main question is how to deal with the instantiation of a type variablewith the dynamic type, especially, when the type variable has a non-trivial upperbound. To address the question, we have introduced the notion of bounded dynamic types, which have characteristics of both ordinary types and the dynamic
type. They allow us to avoid weakening the partial safety of gradual typing.
Immediate future work is, of course, to complete the theoretical development,
including proofs of desired properties. The usefulness of bounded dynamic types
in real program evolution scenarios should be examined.

Acknowledgments. This work was supported in part by Grant-in-Aid for Young
Scientists (A) No. 21680002. We thank anonymous reviewers for valuable comments.

References
1. Siek, J.G., Taha, W.: Gradual typing for functional languages. In: Proc. of the
Scheme and Functional Programming Workshop. (September 2006)
2. Torgersen, M.: New features in C# 4.0. http://code.msdn.microsoft.com/
csharpfuture
3. Siek, J.G., Taha, W.: Gradual typing for objects. In: Proc. of ECOOP’07. Volume4509 of Springer LNCS. (2007) 2–27
4. Abadi, M., Cardelli, L.: A Theory of Objects. Springer Verlag (1996)
5. Ina, L., Igarashi, A.: Gradual typing for Featherweight Java. Computer Software
26(2) (April 2009) In Japanese.
6. Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: A minimal core calculus
for Java and GJ. ACM TOPLAS 23(3) (May 2001) 396–450
7. Bracha, G., Griswold, D.: Strongtalk: Typechecking Smalltalk in a production
environment. In: Proc. of OOPSLA’93. (1993) 215–230
8. Thiemann, P.: Towards a type system for analyzing JavaScript programs. In: Proc.
of ESOP’09. Volume 3444 of Springer LNCS. (2005) 408–422
9. Furr, M., An, J., Foster, J.S., Hicks, M.: Static type inference for ruby. In: Proc.
of ACM Symposium on Applied Computing (SAC’09). (March 2009) 1859–1866
10. Anderson, C., Drossopoulou, S.: BabyJ - from object based to class based programming via types. In: Proc. of WOOD’03. Volume 82 of ENTCS. (2003)
11. Lagorio, G., Zucca, E.: Just: safe unknown types in Java-like languages. Journalof Object Technology 6(2) (February 2007) 69–98
12. Gray, K.E., Findler, R.B., Flatt, M.: Fine-grained interoperability through mirrors
and contracts. In: Proc. of ACM OOPSLA’05. (2005) 231–245
13. Findler, R.B., Felleisen, M.: Contracts for higher-order functions. In: Proc. of
ACM ICFP’02. (2002) 48–59
14. Siek, J.G., Vachharajani, M.: Gradual typing with unification-based inference. In:
Proc. of Dynamic Language Symposium (DLS’08). (July 2008)
15. Matthews, J., Ahmed, A.: Parametric polymorphism throught run-time sealing,or, thorems for low, low prices! In: Proc. of ESOP’08. Volume 4960 of Springer
LNCS. (2008) 16–31
16. Torgersen, M., Hansen, C.P., Ernst, E., von der Ahé, P., Bracha, G., Gafter, N.:
Adding wildcards to the Java programming language. In: Proc. of ACM Symposium on Applied Computing (SAC’04). (March 2004) 1289–1296
17. Bracha, G., Odersky, M., Stoutamire, D., Wadler, P.: Making the future safe forthe past: Adding genericity to the Java programming language. In: Proc. of ACM
OOPSLA’98. (1998) 183–200
18. Igarashi, A., Pierce, B.C., Wadler, P.: A recipe for raw types. In: Informal Proc.
of FOOL8, London, England (January 2001) 65–82