Type–Inference in JAVA 5.0

Jörg Bäuerle, Markus Melzer, Martin Plümicke

University of Cooperative Education Stuttgart m.pluemicke@ba-horb.de

September 11, 2005

1 Overview

We have developed for JAVA 5.0 a type inference system. This means that the user can write programs without any type annotations and the system determines the correct types. We have implemented a prototype for this system. Furthermore we have implemented a plugin for the integrated development environment eclipse.

2 The Type Inference Algorithm

Since then type inference in JAVA similar languages is known as the automatic parameter instantiation in polymorphic methods (local type inference) [PT00, OZZ01, Ode02]. It is proved that this type inference is unsound. Some techniques are presented, which solve these unsoundness. We extend these approaches to a global variant, where additionally the types of method parameters, methods’ return types and the types of local variables are determined automatically. The input of the algorithm are only the types of the fields of the respective classes. The type inference algorithm traverses the programming code as an abstract syntax tree and forms sets of type inequations. As it is known that even the local type inference is unsound, it is obvious that our approach is also unsound. We deal with this problem, as we allow different type assumptions for the parameters, the return type, the local variables, and the expressions of each method, respectively. During traversing the set of type assumptions is adapted, such that the set contains exactly the assumptions, which are possible assumptions at the respective position during the traverse. The adaption is done by solving the inequations as far as possible by a type unification algorithm [Plü04]. The type unification is not unitary but finitary. This means that each unification step reduces the set of type assumptions if there is no solution for one set of inequations. On the other hand the set of type assumptions is extended, if there is more than one solution for a set of inequations. The result of the type inference algorithm is the set of all correct combinations of types of the parameters, the return type, and the local variables. After the type inference step during the compilation, there are two possibilities. Either for each combination of types of each method, byte code could be built, respectively. This would lead to the property that method names, which are declared only once, could be overloaded. On the other hand one combination could be selected. Then, for this combination of types byte code would be built. We implemented the second possibility (cp. section 4). Furthermore, we have done comparisons to other type inference approaches. We considered the type system of Cecil [Lit98], which is a static type system providing type checking and local type inference. Furthermore we considered a type system for a language oriented at Smalltalk [PS91, PS94]. In this approach the types are computed by a least fixed point derivation. In [PC94] type inference for the language Concurrent Aggregates is described, which contains a data flow analysis. Finally, we considered the type system of ocaml [CMP00]. The approach of this type system differs from our’s, as ocaml allows higher-order functions.

3 Implementation

We have done the implementation in JAVA. The implementation consists of two parts. First we describe the implementation of the type unification algorithm. Then we present the implementation of the actual type inference via code traverse.

3.1 Type Unification

The implementation of the type unification [Ott04] contains as the main datastructure a vector of type term pairs. The algorithm itself is implemented as an extension of the usual unification algorithm. Pairs of the form a ≤^{∗} ty respectively ty ≤^{∗} a, where a is a variable and ty is a term but no variable, generate multiple solutions.

3.2 Type Inference

The idea of the implementation of the actual type inference algorithm [Bäu05] is that each construct in a JAVA 5.0 program (method, parameter, return type, variable, expression) get first a variable as its type assumption. Then, for each variable a type is determined by the algorithm. There are two main datastructures. The first one represents type assumptions for methods, fields, and variables. During runtime a set of instances of this datastructure represent the different possibilities of type assumptions. The second main datastructure represents the substitutions of the variables to types, calculated step by step. During runtime each construct of the abstract syntax tree is registered as a listener by the corresponding type variable. These registrations finally allow to substitute the variables in the abstract syntax tree by the calculated types.

4 Integrated Development Environment (IDE)

For JAVA 5.0 without explicite type declaration a plugin for eclipse is developed [Mel05]. The IDE allows to show all different correct possibilities to give types to the methods, parameters, return types, and local variables, which are determined by the type inference algorithm. Then, the user can select the favored type for each construct step by step. Finally, the selected types are substituted in the respective constructs of the abstract syntax tree.

5 Summary and Outlook

We have developed a system, which allows to give typeless JAVA 5.0 programs. The system calculates the correct types. The soundness problem is solved such that all different possibilities are determined and the user himself decides, which type should be used. In the moment only a subset of JAVA 5.0 is implemented. Interfaces and F–bounded type parameters are not implemented yet. This should be done henceforth.

References

[Bäu05] Jörg Bäuerle. Typinferenz in Java. Studienarbeit, BA Stuttgart/Horb, 2005. (in german).

[CMP00] Emmanuel Chailloux, Pascal Manoury, and Bruno Pagano. Développement d’applications avec Objective Caml. O’Reilly, avril 2000. in french, translation http://caml.inria.fr/oreilly-book.

[Lit98] Vassily Litvinov. Constraint-based polymorphism in Cecil: Towards a practical and static type system. In OOPSLA ’98 Conference Proceedings, volume 33(10), pages 388–411, 1998.

[Mel05] Markus Melzer. Integration der Java–Typeinferenz in eine Programmierumgebung. Studienarbeit, BA Stuttgart/Horb, 2005. Studienarbeit (in german).

[Ode02] Martin Odersky. Inferred type instantiation for GJ. Note sent to the types mailing list, January 2002.

[Ott04] Thomas Ott. Typinferenz in Java. Studienarbeit, BA Stuttgart/Horb, 2004. (in german).

[OZZ01] Martin Odersky, Christoph Zenger, and Matthias Zenger. Colored local type inference. ACM SIGPLAN Notices, 36(3):41–53, 2001.

[PC94] John Plevyak and Andrew A. Chien. Precise concrete type inference for object-oriented languages. In Proceedings of the ninth annual conference on Object-oriented programming systems, language, and applications, pages 324–340. ACM Press, 1994.

[Plü04] Martin Plümicke. Type unification in Generic–Java. In Michael Kohlhase, editor, Proceedings of 18th International Workshop on Unification (UNIF’04), July 2004.

http://www.faculty.iu-bremen.de/mkohlhase/event/unif04.

[PS91] Jens Palsberg and Michael I. Schwartzbach. Object-oriented type inference. Proceedings of OOPSLA’91, ACM SIGPLAN Sixth Annual Conference on Object-Oriented Programming Systems, Languages and Applications, pages 146–161, October 1991.

[PS94] Jens Palsberg and Michael I. Schwartzbach. Object-oriented type systems. John Wiley & Sons, 1994.

[PT00] Benjamin C. Pierce and David N. Turner. Local type inference. ACM Trans. Program. Lang. Syst., 22(1):1–44, 2000.