Type theories and object-oriented programmimg

ABSTRACT

Object-oriented programming is becoming a popular approach to the construction of complex software systems. Benefits of object orientation include support for modular design, code sharing, and extensibility. In order to make the most of these advantages, a type theory for objects and their interactions should be developed to aid checking and controlled derivation of programs and to support early binding of code bodies for efficiency. As a step in this direction, this paper surveys a number of existing type theories and examines the manner and extent to which these theories are able to represent the ideas found in object-oriented programming. Of primary interest are the models provided by type theories for abstract data types and inheritance, and the major portion of this paper is devoted to these topics. Code fragments illustrative of the various approaches are provided and discussed. The introduction provides an overview of object-oriented programming and types in programming languages; the summary provides a comparative evaluation of the reviewed typing systems, along with suggestions for future work.

REFERENCES

• 1: Gul Agha, Actors: a model of concurrent computation in distributed systems, MIT Press, Cambridge, MA, 1986
• 2: Hassan Ait-Kaci, A lattice theoretic approach to computation based on a calculus of partially ordered type structures (property inheritance, semantic nets, graph unification), 1984
• 3: AIT-KACI, H. 1985. Integrating data type inheritance into logic programming. In Persistence in Data Types, Papers for the Appin Workshop (Aug.). Dept. of Computational Science, Univ. of St. Andrews, Scotland.
• 4: Hassan Aït-Kaci , Roger Nasr, Logic and inheritance, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.219-228, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512664]
• 5: AIT-KACI, H., LINCOLN, P., AND NASR, R. 1987. A logic of inheritance, functions, and equations. Talk presented at joint U.S./Japan Workshop on Logic of Programs, Honolulu, Hawaii.
• 6: Pierre America , Jaco de Bakker , Joost N. Kok , Jan J. M. M. Rutten, Operational semantics of a parallel object-oriented language, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.194-208, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512662]
• 7: Pierre America, Pool-T: a parallel object-oriented language, Object-oriented concurrent programming, MIT Press, Cambridge, MA, 1987
• 8: Joseph L. Bates , Robert L. Constable, Proofs as programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.1, p.113-136, Jan. 1985 [doi>10.1145/2363.2528]
• 9: Andrew Black , Norman Hutchinson , Eric Jul , Henry Levy, Object structure in the Emerald system, Conference proceedings on Object-oriented programming systems, languages and applications, p.78-86, September 29-October 02, 1986, Portland, Oregon, United States
• 10: Daniel G. Bobrow , Kenneth Kahn , Gregor Kiczales , Larry Masinter , Mark Stefik , Frank Zdybel, CommonLoops: merging Lisp and object-oriented programming, Conference proceedings on Object-oriented programming systems, languages and applications, p.17-29, September 29-October 02, 1986, Portland, Oregon, United States
• 11: Alan H. Borning , Daniel H. H. Ingalls, A type declaration and inference system for smalltalk, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.133-141, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582168]
• 12: BRACHMAN, R. 1985. I lied about the trees. AI Magazine (fall).
• 13: Per Brinch Hansen, The Architecture of Concurrent Programs, Prentice Hall PTR, Upper Saddle River, NJ, 1977
• 14: BURSTALL, R., AND GOGUEN, J. 1982. Algebras, theories and freeness: An introduction for computer scientists. CSR-101-82, Dept. of Computer Science, Univ. of Edinburgh, Scotland.
• 15: R. Burstall , B. Lampson, A kernel language for abstract data types and modules., Proc. of the international symposium on Semantics of data types, p.1-50, July 1984, Sophia-Antipolis, France
• 16: CARDELLI, L. 1984a. Amber. Tech. Memo 11271- 840924-10TM, AT&T Bell Labs, Murray Hill, N.J.
• 17: Luca Cardelli, A semantics of multiple inheritance., Proc. of the international symposium on Semantics of data types, p.51-67, July 1984, Sophia-Antipolis, France
• 18: CARDELLI, L. 1986. A polymorphic lambda calculus with type: Type. DEC Systems Research Center Rep. No. 10, Digital Equipment Corp., Palo Alto, Calif.
• 19: Luca Cardelli, Basic polymorphic typechecking, Science of Computer Programming, v.8 n.2, p.147-172, April 1, 1987 [doi>10.1016/0167-6423(87)90019-0]
• 20: 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]
• 21: CARDELLI, L., AND MACQUEEN, D. 1985. Persistence and type abstraction. In Persistence in Data Types, Papers for the Appin Workshop (Aug.). Res. Rep. 16, Dept. of Computational Science, Univ. of St. Andrews, Scotland, pp. 231-240.
• 22: Robert L. Constable , Daniel R. Zlatin, The Type Theory of PL/CV3, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.94-117, Jan. 1984 [doi>10.1145/357233.357238]
• 23: COX, B. 1984. Message/object programming: An evolutionary change in programming technology. IEEE Software 1, I (Jan.).
• 24: CURRY, H., AND FEYS, R. 1958. Combinatory Logic. North-Holland, Amsterdam.
• 25: Ole-Johan Dahl , Kristen Nygaard, SIMULA: an ALGOL-based simulation language, Communications of the ACM, v.9 n.9, p.671-678, Sept. 1966 [doi>10.1145/365813.365819]
• 26: William James Dally, A VLSI architecture for concurrent data structures, California Institute of Technology, Pasadena, CA, 1986
• 27: DEMERS, A., AND DONAHUE, J. 1979. Revised report on Russell. TR79-389, Dept. of Computer Science, Cornell Univ., Ithaca, N.Y.
• 28: Alan Demers , James Donahue, Making variables abstract: an equational theory for Russell, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.59-72, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567075]
• 29: James Donahue , Alan Demers, Data types are values, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.3, p.426-445, July 1985 [doi>10.1145/3916.3987]
• 30: Kokichi Futatsugi , Joseph A. Goguen , Jean-Pierre Jouannaud , José Meseguer, Principles of OBJ2, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.52-66, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318610]
• 31: GIRARD, J. 1971. Une extension de l'interpretation de GSdel ~ l'analyse, et son application ~ l'61imination des coupures dans l'analyse et la th6orie des types. In Second Scandinavian Logic Symposium, J. E. Fenstad, Ed. North-Holland, Amsterdam.
• 32: GOGUEN, J., AND MESEGUER, J. 1986. EQLog: Equality, types, and generic modules for logic programming. In Logic Programming, D. DeGroot and G. Lindstrom, Eds. Prentice-Hall, Englewood Cliffs, N.J.
• 33: Joseph A. Goguen , José Meseguer, Unifying functional, object-oriented and relational programming with logical semantics, Research directions in object-oriented programming, MIT Press, Cambridge, MA, 1987
• 34: Adele Goldberg , David Robson, Smalltalk-80: the language and its implementation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1983
• 35: GUTTAO, J. 1980. Notes on type abstraction. IEEE Trans. So{tw. Eng. SE-6, i (Jan.), 13-23.
• 36: Carl Hewitt, The challenge of open systems: current logic programming methods may be insufficient for developing the intelligent systems of the future, BYTE, v.10 n.4, p.223-242, April 1985
• 37: HEXT, J. 1967. Compile time type-matching. Cornput. J. 9, 365-369.
• 38: James G. Hook, Understanding Russell–a first attempt, Proc. of the international symposium on Semantics of data types, p.69-85, July 1984, Sophia-Antipolis, France
• 39: Daniel H. H. Ingalls, The Smalltalk-76 programming system design and implementation, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.9-16, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512762]
• 40: Yutaka Ishikawa , Mario Tokoro, A concurrent object-oriented knowledge representation language Orient84/K: its features and implementation, Conference proceedings on Object-oriented programming systems, languages and applications, p.232-241, September 29-October 02, 1986, Portland, Oregon, United States
• 41: Ralph E. Johnson, Type-checking Smalltalk, Conference proceedings on Object-oriented programming systems, languages and applications, p.315-321, September 29-October 02, 1986, Portland, Oregon, United States
• 42: Neil D. Jones , Steven S. Muchnick, Binding time optimization in programming languages: Some thoughts toward the design of an ideal language, Proceedings of the 3rd ACM SIGACT-SIGPLAN symposium on Principles on programming languages, p.77-94, January 19-21, 1976, Atlanta, Georgia [doi>10.1145/800168.811542]
• 43: Marc A. Kaplan , Jeffrey D. Ullman, A Scheme for the Automatic Inference of Variable Types, Journal of the ACM (JACM), v.27 n.1, p.128-145, Jan. 1980 [doi>10.1145/322169.322181]
• 44: KAY, A. 1972. Smalltalk-72 instruction manual. Xerox PARC Rep. SSL-76-6, Xerox Palo Alto Research Center, Palo Alto, Calif.
• 45: Wilf R. LaLonde , Dave A. Thomas , John R. Pugh, An exemplar based Smalltalk, Conference proceedings on Object-oriented programming systems, languages and applications, p.322-330, September 29-October 02, 1986, Portland, Oregon, United States
• 46: P. J. Landin, The next 700 programming languages, Communications of the ACM, v.9 n.3, p.157-166, March 1966 [doi>10.1145/365230.365257]
• 47: Kevin J. Lang , Barak A. Pearlmutter, Oaklisp: an object-oriented scheme with first class types, Conference proceedings on Object-oriented programming systems, languages and applications, p.30-37, September 29-October 02, 1986, Portland, Oregon, United States
• 48: Henry Lieberman, Using prototypical objects to implement shared behavior in object-oriented systems, Conference proceedings on Object-oriented programming systems, languages and applications, p.214-223, September 29-October 02, 1986, Portland, Oregon, United States
• 49: Barbara Liskov , Alan Snyder , Russell Atkinson , Craig Schaffert, Abstraction mechanisms in CLU, Communications of the ACM, v.20 n.8, p.564-576, Aug. 1977 [doi>10.1145/359763.359789]
• 50: MACQUEEN, D. 1985. Modules for ML. Polymorphism Newsletter (Oct.).
• 51: David B. MacQueen, Using dependent types to express modular structure, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.277-286, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512670]
• 52: D. B. MacQueen , Ravi Sethi, A semantic model of types for applicative languages, Proceedings of the 1982 ACM symposium on LISP and functional programming, p.243-252, August 15-18, 1982, Pittsburgh, Pennsylvania, United States [doi>10.1145/800068.802156]
• 53: David MacQueen , Gordon Plotkin , Ravi Sethi, An ideal model for recursive polymorphic types, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.165-174, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800528]
• 54: MARTIN-LOF, P. 1982. Constructive logic and computer programming. In Proceedings o{ 6th International Congress for Logic, Methodology, and Philosophy of Science. North-Holland, Amsterdam.
• 55: MATTHEWS, D. 1983. Programming language design with polymorphism. Ph.D. dissertation, Computer Lab., Univ. of Cambridge, Cambridge, England.
• 56: MESEGUER, J., AND GOGUEN, J. 1983. Initiality, induction, and computability. Tech. Rep. CSL-140, Computer Science Laboratory, SRI, Menlo Park, Calif.
• 57: Norman Meyrowitz, Intermedia: The architecture and construction of an object-oriented hypemedia system and applications framework, Conference proceedings on Object-oriented programming systems, languages and applications, p.186-201, September 29-October 02, 1986, Portland, Oregon, United States
• 58: MEYROWITZ, N., ED. 1987. OOPSLA Conference Proceedings (Orlando, Fla., Oct.). ACM S{G- PLAN 22, 12 (Dec.).
• 59: MILNER, R. 1978. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348-375.
• 60: John C. Mitchell, Coercion and type inference, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.175-185, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800529]
• 61: John Mitchell, Type inference and type containment., Proc. of the international symposium on Semantics of data types, p.257-277, July 1984, Sophia-Antipolis, France
• 62: John C. Mitchell , Gordon D. Plotkin, Abstract types have existential types, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.37-51, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318606]
• 63: David A. Moon, Object-oriented programming with flavors, Conference proceedings on Object-oriented programming systems, languages and applications, p.1-8, September 29-October 02, 1986, Portland, Oregon, United States
• 64: D. L. Parnas, A technique for software module specification with examples, Communications of the ACM, v.15 n.5, p.330-336, May 1972 [doi>10.1145/355602.361309]
• 65: REYNOLDS, J. 1970. Transformational systems and the algebraic structure of atomic formulas. In Machine Intelligence, D. Michie, Ed., vol. 5. Edinburgh University Press, Edinburgh, Scotland, chap. 7.
• 66: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 67: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 68: 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
• 69: William L. Scherlis, Abstract datatypes, specialization, and program reuse, An international workshop on Advanced programming environments, p.433-453, January 1986, Trondheim, Norway
• 70: SCOTT, D. 1976. Data types as lattices. SIAM J. Comput. (Sept.), 522-587.
• 71: Bruce Shriver , Peter Wegner, Research directions in object-oriented programming, MIT Press, Cambridge, MA, 1987
• 72: Andrea H. Skarra , Stanley B. Zdonik, Type evolution in an object-oriented database, Research directions in object-oriented programming, MIT Press, Cambridge, MA, 1987
• 73: SNYDER, A. 1987. inheritance and the development of encapsulated software components. In Proceedings o{ the 20th Hawaiian International Conference on Systems Sciences. Software Track, Western Periodicals, North Hollywood, Calif., pp. 227-238.
• 74: Mark Stefik , Daniel Bobrow, Object-oriented programming: Themes and variations, AI Magazine, v.6 n.4, p.40-62, Winter 1986
• 75: Lynn Andrea Stein, Delegation is inheritance, ACM SIGPLAN Notices, v.22 n.12, p.138-146, Dec. 1987
• 76: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977
• 77: STROUSTRUP, B. 1986. C++. Addison-Wesley, Reading, Mass.
• 78: Daniel C. Swinehart , Polle T. Zellweger , Richard J. Beach , Robert B. Hagmann, A structural view of the Cedar programming environment, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.4, p.419-490, Oct. 1986 [doi>10.1145/6465.6466]
• 79: Raymond W. Turner, Logic for Artificial Intelligence, Prentice Hall PTR, Upper Saddle River, NJ, 1984
• 80: U.S. DEPARTMENT OF DEFENSE. 1983. Ada Reference Manual. ANSI/MIS-STD 1815, U.S. Printing Office (Jan.), Washington, D.C.
• 81: Akinori Yonezawa , Mario Tokoro, Object-oriented concurrent programming, MIT Press, Cambridge, MA, 1987
• 82: Akinori Yonezawa , Etsuya Shibayama , Toshihiro Takada , Yasuaki Honda, Modelling and programming in an object-oriented concurrent language ABCL/1, Object-oriented concurrent programming, MIT Press, Cambridge, MA, 1987

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Languages, Theory