By Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. In Informal Proceeings of the Eighth International Workshop on Foundations of Object-Oriented Languages (FOOL 8), London, January, 2001.
The design of GJ (Bracha, Odersky, Stoutamire and
Wadler), an extension of Java with parametric polymorphism, was
significantly affected by the issue of compatibility between legacy
Java code and new GJ code. In particular, the introduction of raw
types made it easier to interface polymorphic code with
monomorphic code. In GJ, for example, a polymorphic class
List<X>, parameterized by the element type
X, provides not only parameterized types such as
List<Object> or List<String> but
also the raw type List; then, a Java class using
List can be compiled without adding element types to
where List is used. Raw types, therefore, can reduce (or
defer, at least) programmers' burden of modifying their old Java code
to match with new polymorphic code.
From the type-theoretic point of view, raw types are close to
existential types in the sense that clients using a raw type
C expect some implementation of a polymorphic
class of the same name C. Unlike ordinary existential
types, however, raw types allow several unsafe operations such as
coercion from the raw type List, whose element type is
abstract, to List<T> for any concrete type
T. In this paper, basing on Featherweight GJ, proposed
by the authors as a tiny core language of GJ, we formalize a type
system and direct reduction semantics of raw types. The bottom type,
which is subtype of any type, plays a key role in our type-preserving
reduction semantics. In the course of the work, we have found a flaw
in the typing rules from the GJ specification; type soundness is
stated with respect to a repaired version of the type system.
$Date: 2005-12-24 00:37:08 +0900 (Sat, 24 Dec 2005) $