ThisType for Object-Oriented Languages: From Theory to Practice

Abstract

In object-oriented programs, objects often provide methods whose parameter types or return types are the object types themselves. For example, the parameter types of binary methods are the types of their receiver objects, and the return types of some factory methods are the types of their enclosing objects. However, most object-oriented languages do not support such methods precisely because their type systems do not support explicit recursive types, which lead to a mismatch between subclassing and subtyping. This mismatch means that an expression of a subclass may not always be usable in a context where an expression of a superclass is expected, which is not intuitive in an object-oriented setting. Researchers have proposed various type-sound approaches to support methods with types of their enclosing object types denoted by some variants of ThisType, but they reject reasonable and useful methods due to unpermissive type systems or they use less precise declared inexact types rather than runtime exact types. In this article, we present a thorough approach to support methods with ThisTypes: from a new encoding of objects in a typed lambda calculus that allows subtyping by subclassing to an open-source implementation as an extension of the Java programming language. We first provide real-world examples that motivate the need for ThisTyped methods to precisely describe desired properties of programs. We define a new object encoding that enables subtyping by subclassing even in the presence of negative occurrences of type recursion variables by distinguishing object types from existential object types. Based on this object encoding, we formalize language features to support ThisTyped methods with a core calculus CoreThisJava, and prove its type soundness. Finally, we provide ThisJava, a prototype implementation of the calculus, to show its backward compatibility, and we make it publicly available. We believe that our approach theoretically expands the long pursuit of an object-oriented language with ThisTypes to support more useful methods with more precise types