Recursive types in object-oriented languages

Abstract

Object-oriented languages have long suffered from insufficient expressiveness due to the lack of recursive types. Though recursive types are useful to define binary methods and some kind of factory methods, current object-oriented languages do not support recursive types because it has been known that using them entails mismatch between subclassing and subtyping. This mismatch means that an object of a subclass cannot be safely used in any context where an object of a superclass is expected, which is unacceptable for most programmers.

The most important contribution of the thesis is to show that subclassing can match subtyping even in the presence of recursive types in a language, which is contrary to the general perception of programming language research community. This result is based on the new perspective on object types and subtyping presented in the thesis, which clearly distinguishes object types and some-object types and defines a new subtype relation on some-object types. The thesis formally proves that the new subtype relation can successfully replace the traditional one and that subclassing always matches subtyping even in the presence of recursive types under the new definition of subtyping. This effectively removes the biggest obstacle for a language to adopt recursive types to increase its expressiveness.

The thesis also present various language features to support recursive types in an object-oriented language, such as exact class types and This types, virtual constructors and four kinds of typing techniques for flexible use of binary methods. Formal properties of these language features, such as type soundness, decidable typechecking and subtyping-by-subclassing, are proved in a distilled nominal type system named CoreThisJava.

In addition to proving the formal results, we also implemented the language features to test their feasibility in real situations; we extended a full-fledged open source Java compiler JastAddJ ...