Inferred Type Instantiation for GJ

Martin Odersky, EPFL Lausanne

Note sent to the types mailing list, January 2002.

Abstract

The task of type instantiation is to substitute types for formal type parameters in applications of polymorphic methods. Instantiating these parameters automatically considerably reduces clutter in program code that applies polymorphic functions. GJ uses type instantiation in a type system that combines Java's nominal subtyping discipline with F-bounded polymorphism. The version of GJ distributed as the early access release for JSR14 was recently shown by Alan Jeffrey to be unsound. Specifically, code that uses polymorphic methods but no explicit type casts can still cause a ``ClassCastException'' to be thrown at run-time. The unsoundness is caused by the semantically unclear status of the ``undefined'' type ``*'' in local type inference. This note puts forward another system for inferred type instantiation for GJ which avoids the unsoundness problem of GJ's current scheme. The new scheme has been implemented in the latest version of javac. It was tested with several large examples, including the compiler itself and the GJL, a generified version of ObjectSpace's JGL. In all this code (roughly 30000 lines) there was not a single instance where a type annotation had to be given which was not there before. This is a good indication that the new type inference scheme is in practice at least as good as the previous one.

Paper

in .ps or .ps.gz or .dvi .dvi.gz

BibTeX Entry


@Misc{odersky:localti-note,
  author =	 {Martin Odersky},
  title =	 {Inferred Type Instantiation for GJ},
  howpublished = {Note sent to the types mailing list},
  month =	 {January},
  year =	 2002
}

Martin Odersky

Last modified: Tue May 14 14:04:09 DST 2002