Dan Smith, Completing the Java Type System

The recent introduction of type variables and wildcards to the Java language, while greatly enriching the expressivity of the type system, comes with prohibitions against a variety of natural and useful expressions. Principal among these is the declaration of type variables with lower ("super") bounds, naturally motivated by the support for such bounds on wildcards. In this talk, I'll provide some background on the current Java type system. I'll then describe two variations that enhance the current language specification with support for these features. These variations must address the inference of method type arguments, and in so doing improve the inference algorithm so that it is both sound and complete. The first, simpler variation makes use of union types; the second more closely matches the current Java type system and formalizes its notion of "infinite types," as produced by static analysis.