Object-oriented programming without recursive types

ABSTRACT

It is widely agreed that recursive types are inherent in the static typing of the essential mechanisms of object-oriented programming: encapsulation, message passing, subtyping, and inheritance. We demonstrate here that modeling object encapsulation in terms of existential types yields a substantially more straightforward explanation of these features in a simpler calculus without recursive types.

REFERENCES

• 1: Martin Abadi. Doing without F-bounded quantification. Message to Types electronic mail list, February 1992.
• 2: Henk Barendregt. Introduction to generalized type systems. Journal of Functional Programming, 1992. To appear.
• 3: Daniel G. Bobrow , Linda G. DeMichiel , Richard P. Gabriel , Sonya E. Keene , Gregor Kiczales , David A. Moon, Common Lisp Object System specification, ACM SIGPLAN Notices, v.23 n.SI, p.1-142, September 1988 [doi>10.1145/885631.885632]
• 4: A. H. Borning, Classes versus prototypes in object-oriented languages, Proceedings of 1986 ACM Fall joint computer conference, p.36-40, November 1986, Dallas, Texas, United States
• 5: 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
• 6: Kim B. Bruce. A paradigmatic object-oriented language: Design, static typing and semantics. Technical Report CS-92-01, Williams College, January 1992.
• 7: Kim B. Bruce , Giuseppe Longo, A modest model of records, inheritance, and unbounded quantification, Information and Computation, v.87 n.1-2, p.196-240, July/August 1990 [doi>10.1016/0890-5401(90)90062-M]
• 8: 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]
• 9: Timothy Budd, An introduction to object-oriented programming, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1991
• 10: 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]
• 11: 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]
• 12: 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]
• 13: Luca Cardelli. Notes about F~:.. Unpublished notes, October 1990.
• 14: Luca Cardelli. Extensible records in a pure calculus of subtyping. Research report 81, DEC Systems Research Center, January 1992.
• 15: Luca Cardelli. Typed foundations of objectoriented programming. Tutorial given at POPL '92, January 1992.
• 16: Luca Cardelli , Simone Martini , John C. Mitchell , Andre Scedrov, An Extension of System F with Subtyping, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.750-770, September 24-27, 1991
• 17: 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
• 18: 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]
• 19: Giuseppe Castagna. Strong typing in objectoriented paradigms. Rapport de Recherche LIENS- 92-11, Ecole Normale Supdrieure, Paris, May 1992.
• 20: Giuseppe Castagna, Giorgio Ghelli, and Giuseppe Longo. A calculus for overloaded functions and subtyping. Rapport de Recherche LIENS-92-4, Ecole Normale Sup~rieure, Paris, February 1992.
• 21: William R. Cook, A denotational semantics of inheritance, 1989
• 22: William R. Cook, Object-Oriented Programming Versus Abstract Data Types, Proceedings of the REX School/Workshop on Foundations of Object-Oriented Languages, p.151-178, May 28-June 01, 1990
• 23: 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]
• 24: M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Functional characters of solvable terms. Zeilschrifl fiir Mathematische Logik und Grundlagen der Malhematik, 27:45-58, 1981.
• 25: Pierre-Louis Curien and Giorgio Ghelli. Coherence of subsumption. Mathematical Structures in Computer Science, 1992. To appear.
• 26: Giorgio Ghelli, A static type system for message passing, Conference proceedings on Object-oriented programming systems, languages, and applications, p.129-145, October 06-11, 1991, Phoenix, Arizona, United States
• 27: Jean-Yves Girard. interpretation fonctioneile et dliminalion des coupures de l'arithmd~ique d'ordre supgrieur. PhD thesis, Universit~ Paris VII, 1972.
• 28: Adele Goldberg , David Robson, Smalltalk-80: the language and its implementation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1983
• 29: 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]
• 30: Martin Hofmann and Benjamin Pierce. An abstract view of objects and subtyping (preliminary report). Technical Report ECS-LFCS-92-226, University of Edinburgh, LFCS, 1992.
• 31: S. Kamin, Inheritance in smalltalk-80: a denotational definition, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.80-87, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73567]
• 32: 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]
• 33: John Mitchell , Sigurd Meldal , Neel Madhav, An extension of standard ML modules with subtyping and inheritance, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.270-278, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99620]
• 34: 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]
• 35: Benjamin Crawford Pierce, Programming with intersection types and bounded polymorphism, Carnegie Mellon University, Pittsburgh, PA, 1992
• 36: Benjamin C. Pierce and Robert Pollack. Higherorder subtyping. Unpublished manuscript, August 1992.
• 37: Benjamin C. Pierce and David N. Turner. Simple type-theoretic foundations for object-oriented programming. Submitted to the Journal of Functional Programming, August 1992.
• 38: Benjamin C. Pierce and David N. Turner. Statically typed multi-methods via partially abstract types. Draft technical teport, September 1992.
• 39: Uday Reddy, Objects as closures: abstract semantics of object-oriented languages, Proceedings of the 1988 ACM conference on LISP and functional programming, p.289-297, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62721]
• 40: D. Rémy, Type checking records and variants in a natural extension of ML, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.77-88, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75284]
• 41: John C. Reynolds. User defined types and procedural data structures as complementary approaches to data abstraction. In David Gries, editor, Programming Methodology, A Collection of Articles by IFIP WG2.3, pages 309-317. Springer-Verlag, New York, 1978. Reprinted from S. A. Schuman (ed.), New Advances in Algorithmic Languages 1975, Inst. de Recherche d'Informatique et d'Automatique, Rocquencourt, 1975, pages 157- 168.
• 42: John Reynolds. Three approaches to type structure. In Mathematical Foundations of Software Development. Springer-Verlag, 1985. Lecture Notes in Computer Science No. 185.
• 43: Edmund Robinson and Robert Tennent. Bounded quantification and record-update problems. Message to Types electronic mail list, October 1988.
• 44: Mitchell Wand. Complete type inference for simple objects. In Proceedings of the IEEE Symposium on Logic in Computer Science, ithaca, NY, June 1987.
• 45: Mitchell Wand. Corrigendum: Complete type inference for simple objects. In Proceedings of the IEEE Symposium on Logic in Computer Science, 1988.
• 46: M. Wand, Type inference for record concatenatiOn and multiple inheritance, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.92-97, June 1989, Pacific Grove, California, United States

INDEX TERMS

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

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.5 Object-oriented Programming
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures; Abstract data types

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Algorithms, Design, Languages, Theory