A unifying type-theoretic framework for objects

Journal of Functional Programming - Tập 5 Số 4 - Trang 593-635 - 1995
Martin Hofmann1, Benjamin C. Pierce1
1Department of Computer Science, University of Edinburgh, The King's Buildings, Edinburgh, EH9 3JZ, UK

Tóm tắt

AbstractWe give a direct type-theoretic characterization of the basic mechanisms of object-oriented programming, including objects, methods, message passing, and subtyping, by introducing an explicit constructor for object types and suitable introduction, elimination, and equality rules. The resulting abstract framework provides a basis for justifying and comparing previous encodings of objects based on recursive record types (Cardelli, 1984; Cardelli, 1992; Bruce, 1994; Cook et al., 1990; Mitchell, 1990a) and encodings based on existential types (Pierce & Turner, 1994).

Từ khóa


Tài liệu tham khảo

Stroustrup, 1986, The C++ Programming Language

Reynolds, 1974, Proc. Colloque sur la Programmation, 408

Reichel H. 1995. An Approach to Object Semantics based on Terminal Co-algebras. Mathematical Structures in Computer Science. To appear.

Pierce B. C. , & Turner D. N. 1993 (Apr.). Statically Typed Friendly Functions via Partially Abstract Types. Technical Report ECS-LFCS-93-256. University of Edinburgh, LFCS. Also available as INRIA-Rocquencourt Rapport de Recherche No. 1899.

Moggi E. 1989. Computational lambda-calculus and monads. Pages 14–23 of: Fourth Annual Symposium on Logic in Computer Science (Asilomar, CA).IEEE Computer Society Press.

Mitchell, 1990, Logical Foundations of Functional Programming, 195

Läufer K. , & Odersky M. 1994. Polymorphic Type Inference and Abstract Data Types. ACM Transactions on Programming Languages and Systems (TOPLAS). To appear; an earlier version appeared in the Proceedings of the ACM SIGPLAN Workshop on ML and its Applications, 1992, under the title “An Extension of ML with First-Class Abstract Types”.

Kamin, 1994, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design, 464

Hofmann, 1994, Positive Subtyping

Goldberg, 1983, Smalltalk-80: The Language and Its Implementation

10.1145/62058.62060

Cook W. R. , Hill W. L. , & Canning P. S. 1990 (Jan.). Inheritance is not Subtyping. Pages 125–135 of: Seventeenth Annual ACM Symposium on Principles of Programming Languages. Also in Gunter Carl A. and Mitchell John C. , editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994).

10.1145/6041.6042

Mitchell J. C. 1990a (Jan.). Toward a Typed Foundation for Method Specialization and Inheritance. Pages 109–124 of: Proceedings of the 17th ACM Symposium on Principles of Programming Languages. Also in Gunter Carl A. and Mitchell John C. , editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994).

Cardelli, 1992, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design

10.1007/3-540-13346-1_2

Canning P. , Cook W. , Hill W. , Olthoff W. , & Mitchell J. 1989 (Sept.). F-Bounded Quantification for Object-Oriented Programming. Pages 273–280 of: Fourth International Conference on Functional Programming Languages and Computer Architecture.

10.1017/S0956796800001039

Bruce K. , & Mitchell J. 1992 (Jan.). PER models of subtyping, recursive types and higher-order polymorphism. In: Proceedings of the Nineteenth ACM Symposium on Principles of Programming Languages.

10.1017/S0956796800001052

Compagnoni A. B. 1994 (Jan.). Subtyping in F_{\caret}^{\omega} is decidable. Tech. rept. ECS-LFCS-94-281. LFCS, University of Edinburgh. To appear in the proceedings of Computer Science Logic, September 1994, under the title “Decidability of Higher-Order Subtyping with Intersection Types”.

Coquand, 1989, LNCS 389

10.1007/BFb0019443

Kock, 1970, Various Publications Series 11

10.1006/inco.1994.1013

Abadi M. 1992 (Feb.). Doing without F-bounded quantification. Message to Types electronic mail list.

Cardelli L. 1990 (Oct.). Notes about F_{\lt}^{\omega} Unpublished manuscript.

Cardelli L. 1988 (Jan.). Structural Subtyping and the Notion of Power Type. Pages 70–79 of: Proceedings of the 15th ACM Symposium on Principles of Programming Languages.

10.1145/44501.45065

Hofmann, 1992, An Abstract View of Objects and Subtyping (Preliminary Report)

Cook W. 1989. A Denotational Semantics of Inheritance. Ph.D. thesis, Brown University.

10.1017/S0956796800000198

Abadi, 1994, Theoretical Aspects of Computer Software (TACS)

10.1145/155183.155231

Barr, 1990, Category Theory for Computing Science

Wand M. 1987 (June). Complete type inference for simple objects. In: Proceedings of the IEEE Symposium on Logic in Computer Science.

Pierce, 1989, Programming in Higher-order Typed Lambda-Calculi

10.1017/S0956796800001040

Smith, 1990, Programming in Martin-Löf's Type Theory. An Introduction

Abadi M. , & Cardelli L. 1994b. A Theory of Primitive Objects: Second-order Systems. In: European Symposium on Programming (ESOP), Edinburgh, Scotland.

Castagna, 1994, Information and Computation

Steffen M. , & Pierce B. 1994 (June). Higher-Order Subtyping. In: IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET). An earlier version appeared as University of Edinburgh technical report ECS-LFCS-94-280 and Universität Erlangen-Nürnberg Interner Bericht IMMD7-01/94, January 1994.

Compagnoni A. B. , & Pierce B. C. 1993 (Aug.). Multiple Inheritance via Intersection Types. Tech. rept. ECS-LFCS-93-275. LFCS, University of Edinburgh. Also available as Catholic University Nijmegen computer science technical report 93–18.

Wraith, 1989, A note on categorical datatypes. Lecture Notes in Computer Science

10.1007/3-540-57887-0_128

Reynolds, 1978, Programming Methodology, A Collection of Articles by IFIP WG2.3., 309

Girard J.-Y. 1972. Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur. Ph.D. thesis, Université Paris VII.

Barendregt, 1992, Handbook of Logic in Computer Science, II