In this paper we sketched several useful modifications to the simple type-checking systems of object-oriented languages like C++, Java, and Object Pascal. These included allowing method types to be replaced by subtypes in subclasses, introducing a name, MyType, for the type of self - supporting automatic updating of parameter types in important special cases, and introducing bounded matching as a means of expressing the desired restrictions on type parameters. These mechanisms provided us with a more expressive type system that allowed us to write a large number of subclasses that, while intuitively correct, were ruled out by the simple type system. Moreover, one can actually prove that this system is type safe, meaning that any program which type checks is guaranteed not to have run-time type errors. A more formal description of such a language is given in [BSvG95].
We believe that these constructs should become increasingly common in new or revised versions of statically-typed object-oriented programming languages. For instance, we have formulated a proposal to add MyType and match-bounded polymorphism to Java.
In the last section of this paper, we introduced a more recently developed type system that uses matching to replace subtyping. In this system subtyping (and the subsumption rule) were dropped, and the original version of matching was replaced by a much simpler relation in which methods could only be added in matching types, with no (explicit) changes allowed to the existing method types. (Of course the method bodies themselves could be overridden in subclasses, it is only the types which are frozen.) While very simple, this type system, which also included bounded matching, allowed us to easily express all of the difficult examples included in this paper that caused problems in the simple type system.
Our current personal choice for a type system for statically typing object-oriented languages is this pure matching language. We believe that it combines simplicity with the expressiveness to solve many of the most difficult typing problems that arise in object-oriented languages. The #-types in this language also allow the programmer to make an explicit choice between homogeneous and heterogeneous data structures, something generally not available in languages with subtyping.
The only negatives that arise in this language's use are the result of tradeoffs that may be worth taking on other grounds. While it is necessary to mark those formal parameters and variables that are capable of holding values of matching types, this provides information to the compiler that may be useful in producing optimized code. In particular, this may result in paying the extra implementation costs of subtyping only in those places where it is actually needed. It does, however, require the programmer to plan ahead as to where this kind of flexibility is desired. A restriction is that binary messages cannot be sent to objects whose only known types are #-types.
The author and Leaf Petersen have designed a language, LOOM, whose type system is based on the ideas in section 11. A technical report [BP96] presenting a more detailed explanation of the type system and a proof of type-safety is in preparation. The thesis [Pet96] presents an overview of LOOM along with the design of a module system providing better support for programming in the large.
The contents of this paper are based on the work of researchers working in type theory and semantics as well as language designers. In the body of this paper we attempted to provide fairly complete references to the ideas discussed here, but there were many important contributions that we did not have room to discuss. The paper [DT88] presents an interesting survey of the state of type theory in object-oriented languages as of 1987-88. The collection [GM94] contains many of the important early contributions to the theory of object-oriented programming languages. The forthcoming book [AC96] provides a more unified approach to the semantics and type theory of object-oriented programming languages. Other important sources of information in this area are the proceedings of the annual ECOOP (European Conference on Object-Oriented Programming) and OOPSLA (Object-Oriented Programming: Systems, Languages, and Applications) conferences. The Journal of Function Programming published a special issue in 1994 on the theory of object-oriented languages which contains the papers [Aba94,Bru94,PT94], while the journal Theory and Practice of Object-oriented Systems (TAPOS) will publish a special issue on types in object-oriented languages in late 1996.
Acknowledgements: Thanks to Luca Cardelli, Peter Wegner,
Tony Simons, Andrew Black and the anonymous referees for very helpful
comments and suggestions on earlier drafts of
this paper. Special thanks to Robert van Gent, Angela Schuett, and
Leaf Petersen, whose collaborative efforts in language design led to
a better understanding of the issues of static typing in
object-oriented languages. This paper was written in part while the author
was in residence at the Newton Institute for Mathematical Science at
the University of Cambridge. I thank the institute and its staff for
their hospitality and support during my stay.