Java type inference is broken: can we fix it?

ABSTRACT

Java 5, the most recent major update to the Java Programming Language, introduced a number of sophisticated features, including a major extension to the type system. While the technical details of these new features are complex, much of this complexity is hidden from the typical Java developer by an ambitious type inference mechanism. Unfortunately, the extensions to the Java 5 type system were so novel that their technical details had not yet been thoroughly investigated in the research literature. As a result, the Java 5 compiler includes a pragmatic but flawed type inference algorithm that is, by design, neither sound nor locally complete. The language specification points out that neither of these failures is catastrophic: the correctness of potentially-unsound results must be verified during type checking; and incompleteness can usually be worked around by manually providing the method type parameter bindings for a given call site.

This paper dissects the type inference algorithm of Java 5 and proposes a signficant revision that is sound and able to calculate correct results where the Java 5 algorithm fails. The new algorithm is locally complete with the exception of a difficult corner case. Moreover, the new algorithm demonstrates that several arbitrary restrictions in the Java type system---most notably the ban on lower-bounded type parameter declarations and the limited expressibility of intersection types---are unnecessary. We hope that this work will spur the evolution of a more coherent, more comprehensive generic type system for Java.

REFERENCES

• 1: Gilad Bracha , Martin Odersky , David Stoutamire , Philip Wadler, Making the future safe for the past: adding genericity to the Java programming language, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.183-200, October 18-22, 1998, Vancouver, British Columbia, Canada
• 2: Luca Cardelli. An Implementation of F:. Research report 97, DEC Systems Research Center, 1993.
• 3: James Gosling , Bill Joy , Guy Steele , Gilad Bracha, Java(TM) Language Specification, The (3rd Edition) (Java (Addison-Wesley)), Addison-Wesley Professional, 2005
• 4: Atshushi Igarashi , Benjamin Pierce , Philip Wadler, Featherwieght Java: a minimal core calculus for Java and GJ, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.132-146, November 01-05, 1999, Denver, Colorado, United States
• 5: Atsushi Igarashi , Mirko Viroli, On Variance-Based Subtyping for Parametric Types, Proceedings of the 16th European Conference on Object-Oriented Programming, p.441-469, June 10-14, 2002
• 6: Atsushi Igarashi & Hideshi Nagira. Union Types for Object-Oriented Programming. Journal of Object Technology, vol. 6, no. 2, February 2007.
• 7: Andrew J. Kennedy & Benjamin C. Pierce. On Decidability of Nominal Subtyping with Variance. FOOL/WOOD, 2007.
• 8: Benjamin C. Pierce & David N. Turner. Local Type Argument Synthesis with Bounded Quantification. Technical report TR495, Indiana University, 1997.
• 9: Benjamin C. Pierce , David N. Turner, Local type inference, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.252-265, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268967]
• 10: Daniel Smith. Completing the Java Type System. Master's thesis, Rice University, 2007.
• 11: Kresten Krab Thorup & Mads Torgersen. Unifying Genericity: Combining the Benefits of Virtual Types and Parameterized Classes. Lecture Notes in Computer Science, 1999.
• 12: Mads Torgersen , Christian Plesner Hansen , Erik Ernst , Peter von der Ahé , Gilad Bracha , Neal Gafter, Adding wildcards to the Java programming language, Proceedings of the 2004 ACM symposium on Applied computing, March 14-17, 2004, Nicosia, Cyprus [doi>10.1145/967900.968162]
• 13: Mads Torgersen, Erik Ernst, & Christian Plesner Hansen. Wild FJ. FOOL, 2005.
• 14: DrJava IDE. http://drjava.org.
• 15: Java Community Process. http://jcp.org.
• 16: "Type variables should have lower/super bounds." Java Request for Enhancement. http://bugs.sun.com/view_bug.do?bug_id=5052956.
• 17: "Please introduce a name for the "null' type." Java Request for Enhancement. http://bugs.sun.com/view_bug.do?bug_id=5060259.
• 18: "Multiply-bounded reference type expressions." Java Request for Enhancement. http://bugs.sun.com/view_bug.do?bug_id=6350706.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Object-oriented languages
      D.3.3 Language Constructs and Features
          Subjects: Polymorphism; Classes and objects

General Terms:
Design, Languages

Keywords:
bounded quantification, generics, intersection types, parameterized types, polymorphic methods, subtyping, type argument inference, type inference, union types, wildcards