Safe type checking in a statically-typed object-oriented programming language

ABSTRACT

In this paper we introduce a statically-typed, functional, object-oriented programming language, TOOPL, which supports classes, objects, methods, instance variable, subtypes, and inheritance. It has proved to be surprisingly difficult to design statically-typed object-oriented languages which are nearly as expressive as Smalltalk and yet have no holes in their typing systems. A particular problem with statically type checking object-oriented languages is determining whether a method provided in a superclass will continue to type check when inherited in a subclass. This program is solved in our language by providing type checking rules which guarantee that a method which type checks as part of a class will type check correctly in all legal subclasses in which it is inherited. This feature enables library providers to provide only the interfaces of classes with executables and still allow users to safely create subclasses. The design of TOOPL has been guided by an analysis of the semantics of the language, which is given in terms of a sufficiently rich model of the F-bounded second-order lambda calculus. This semantics supported the language design by providing a means of proving that the type-checking rules for the language are sound, ensuring that well-typed terms produce objects of the appropriate type. In particular, in a well-typed program it is impossible to send a message to an object which lacks a corresponding method.

REFERENCES

• AC90: Roberto Amadio and Luca Cardelli. Subtyping recursive types. Technical Report 62, Digital Systems Research Center, 1990.
• BM92: Kim Bruce , John C. Mitchell, PER models of subtyping, recursive types and higher-order polymorphism, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.316-327, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143230]
• Bru92a: Kim B. Bruce, The Equivalence of Two Semantic Definitions for Inheritance in Object-Oriented Languages, Proceedings of the 7th International Conference on Mathematical Foundations of Programming Semantics, p.102-124, March 25-28, 1991
• Bru92b: K. Bruce. A paradigmatic object-oriented programming language: design, static typing and semantics. Technical Report CS- 92-01~ Williams College, 1992.
• Car88a: Luca Cardelli, A semantics of multiple inheritance, Information and Computation, v.76 n.2-3, p.138-164, February/March 1988 [doi>10.1016/0890-5401(88)90007-7]
• Car88b: L. Cardelli, Structural subtyping and the notion of power type, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.70-79, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73566]
• Car92a: Luca Cardelli. Extensible records in a pure calculus of subtyping. Technical Report 81, DEC Systems Research Center, 1992.
• Car92b: Luca Cardelli. Typed foundations of object-oriented programming, 1992. Tutorial given at POPL '92.
• CCH+89: Peter Canning , William Cook , Walter Hill , Walter Olthoff , John C. Mitchell, F-bounded polymorphism for object-oriented programming, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.273-280, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99392]
• CCHO89: P. S. Canning , W. R. Cook , W. L. Hill , W. G. Olthoff, Interfaces for strongly-typed object-oriented programming, Conference proceedings on Object-oriented programming systems, languages and applications, p.457-467, October 02-06, 1989, New Orleans, Louisiana, United States
• CDG+88: L. Cardelli, J. Donahue, L. Galssman, M. Jordan, B. Kalsow, and G. Nelson. Modula-3 report. Technical Report SRC- 31, DEC systems Research Center, 1988.
• CG92: P.L. Curien and G. Ghelli. Coherence of subsumption,minimum typing and typechecking in F<. Mathematical Structures in Computer Science, 2:55-91, 1992.
• CHC90: William R. Cook , Walter Hill , Peter S. Canning, Inheritance is not subtyping, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.125-135, December 1989, San Francisco, California, United States [doi>10.1145/96709.96721]
• CL91: Luca Cardelli and Giuseppe Longo. A semantic basis for Quest. Journal of Functional Programming, 1(4):417-458, 1991.
• CM90: Luca Cardelli , John C. Mitchell, Operations on records, Proceedings of the fifth international conference on Mathematical foundations of programming semantics, p.22-52, July 1990, New Orleans, Louisiana, United States
• Coo89: W.R. Cook. A proposal for making Eiffel type-safe. In European Conf. on Object- Oriented Programming, pages 57-72, 1989.
• CW85: Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
• DM92: Allyn Dimock and Robert Muller. Private communication, 1992.
• Gir71: J.-Y. Girard. Une extension de l'interpretation de Ghdel ~ l'analyse, et son application ~ l'41imination des coupures dans l'analyse et la th4orie des types, in J.E. Fenstad, editor, 2nd Scandinavian Logic Symposium, pages 63-92. North-Holland, 1971.
• GJ90: Justin O. Graver , Ralph E. Johnson, A type system for Smalltalk, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.136-150, December 1989, San Francisco, California, United States [doi>10.1145/96709.96722]
• KPS93: Dexter Kozen , Jens Palsberg , Michael I. Schwartzbach, Efficient recursive subtyping, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.419-428, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158700]
• Mey92: Bertrand Meyer, Eiffel: the language, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
• Mit90: John C. Mitchell, Toward a typed foundation for method specialization and inheritance, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.109-124, December 1989, San Francisco, California, United States [doi>10.1145/96709.96719]
• MP88: John C. Mitchell , Gordon D. Plotkin, Abstract types have existential type, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.470-502, July 1988 [doi>10.1145/44501.45065]
• Omo91: Stephen M. Omohundro. The Sather language. Technical report, International Computer Science Institute, 1991.
• PH92: Benjamin C. Pierce and Martin Hoffman. An abstract view of objects and subtyping (preliminary report). Technical Report to appear, University of Edinburgh, 1992.
• Pie92: Benjamin C. Pierce, Bounded quantification is undecidable, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.305-315, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143228]
• PT92a: Benjamin C. Pierce and David N. Turner. Object-oriented programming without recursive types. Technical Report ECS- LFCS-92-226, University of Edinburgh, 1992.
• PT92b: Benjamin C. Pierce and David N. 25arner. Simple type-theoretic foundations for object-oriented programming. Technical report, University of Edinburgh, 1992.
• Rey74: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• SCB+86: Craig Schaffert , Topher Cooper , Bruce Bullis , Mike Kilian , Carrie Wilpolt, An introduction to Trellis/Owl, Conference proceedings on Object-oriented programming systems, languages and applications, p.9-16, September 29-October 02, 1986, Portland, Oregon, United States
• Str86: Bjarne Stroustrup, The C++ programming language, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• Tes85: L. Tesler. Object Pascal report. Technical Report 1, Apple Computer, 1985.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Object-oriented languages

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Algorithms, Design, Languages