Intersection types in Java

ABSTRACT

In the past we analyzed typeless Java programs. One of our results was, that there may be different correct typings for one method. This means that the principal types of such methods are intersection types. We presented a type-inference algorithm. For typeless Java methods the algorithm infers its principal intersection type. Unfortunately, like Java byte-code, Java does not allow intersection types.

In this paper we present an algorithm, which resolves intersection types of Java methods, such that Java programs with standard typings are generated.

In the algorithm we have to differentiate two cases of intersection types. On the one hand there are methods with intersection types, where for all types the same code is executed. On the other hand there are methods, which call in dependence to its typings different methods. These two cases have to be treated differently during type resolving.

Finally, we will see that this differentiation leads to a refined definition of Java method principal types.

REFERENCES

• 1: Egon Börger , Wolfram Schulte, A Programmer Friendly Modular Definition of the Semantics of Java, Formal Syntax and Semantics of Java, p.353-404, January 1999
• 2: G. Boudol and P. Zimmer. On type inference in the intersection type discipline. Electronic Notes in Theoretical Computer Science, 136:23--42, 2005.
• 3: M. Coppo and M. Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame J. Formal Logic, 21(4):685--693, 1980.
• 4: Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
• 5: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 6: J. R. Hindley. Types with intersection: An introduction. Formal Aspects of Computing, 4(5):470--486, 1992.
• 7: A. J. Kfoury , J. B. Wells, Principality and type inference for intersection types using expansion variables, Theoretical Computer Science, v.311 n.1-3, p.1-70, 23 January 2004 [doi>10.1016/j.tcs.2003.10.032]
• 8: Daniel Leivant, Polymorphic type inference, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.88-98, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567077]
• 9: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 10: Martin Plümicke, Typeless programming in Java 5.0 with wildcards, Proceedings of the 5th international symposium on Principles and practice of programming in Java, September 05-07, 2007, Lisboa, Portugal [doi>10.1145/1294325.1294336]
• 11: Martin Plümicke , Jörg Bäuerle, Typeless programming in Java 5.0, Proceedings of the 4th international symposium on Principles and practice of programming in Java, August 30-September 01, 2006, Mannheim, Germany [doi>10.1145/1168054.1168079]
• 12: S. van Bakel. Principal type schemes for the strict type assignment system. Journal of Logic and Computing, 3(6):643--670, 1993.
• 13: Steffen van Bakel, Intersection type assignment systems, Theoretical Computer Science, v.151 n.2, p.385-435, Nov. 27, 1995

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.5 Object-oriented Programming

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Modules and interfaces
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

General Terms:
Algorithms, Theory

Keywords:
code generation, language design, program design and implementation, type inference, type system