Hostname: page-component-7c8c6479df-r7xzm Total loading time: 0 Render date: 2024-03-28T16:30:04.476Z Has data issue: false hasContentIssue false

Operations on records

Published online by Cambridge University Press:  04 March 2009

Luca Cardelli
Affiliation:
Digital Equipment Corporation, Systems Research Center, USA
John C. Mitchell
Affiliation:
Department of Computer Science, Stanford University, USA

Abstract

We define a simple collection of operations for creating and manipulating record structures, where records are intended as finite associations of values to labels. A second-order type system over these operations supports both subtyping and polymorphism. We provide typechecking algorithms and limited semantic models.

Our approach unifies and extends previous notions of records, bounded quantification, record extension, and parametrization by row-variables. The general aim is to provide foundations for concepts found in object-oriented languages, within a framework based on typed lambda-calculus.

Type
Research Article
Copyright
Copyright © Cambridge University Press 1991

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Breazu-Tannen, V., Coquand, T., Gunter, C. and Scedrov, A. (1989) Inheritance and explicit coercion. Proc. Fourth IEEE Symp. on Logic in Computer Science, pp. 112129Google Scholar
Bruce, K.B. and Longo, G. (1988) A modest model of records, inheritance and bounded quantification. Proc. Third IEEE Symp. on Logic in Computer Science, pp. 3850Google Scholar
Bruce, K.B., Meyer, A.R. and Mitchell, J.C. (1990) The semantics of second order lambda calculus. Informat. Computat. Vol. 85, No. 1, pp. 76134CrossRefGoogle Scholar
Cardelli, L. (1988) A semantics of multiple inheritance. In Information and Computation 76 138164 (First appeared in Semantics of Data Types, eds G. Kahn, D. B. MacQueen and G. Plotkin. Springer Lecture Notes in Computer Science 173, Springer-Verlag, 1984.)Google Scholar
Cardelli, L., Donahue, J., Glassman, L., Jordan, M., Kalsow, B. and Nelson, G. (1989) Modula-3 report (revised). Research Report no. 52, DEC Systems Research Center.Google Scholar
Cardelli, L. and Wegner, P. (1985) On understanding types, data abstraction and polymorphism. Comput. Surv. 17(4) 471522Google Scholar
Curien, P.-L. and Ghelli, G. (1991) Coherence of subsumption. Math. Struct. Comp. Sci, to appear.CrossRefGoogle Scholar
Dahl, O. and Nygaard, K. (1966) Simula, an Algol-based simulation language. Commun. ACM 9 671678CrossRefGoogle Scholar
Girard, J.-Y. (1971) Une extension de Interpretation de Gödel é l’analyse, et son application à l’élimination des coupures dans l’analyse ct la théorie des types. Proc. Second Scandinavian Logic Symposium, ed. Fenstad, J.E.. North-Holland, pp. 6392Google Scholar
Girard, J.-Y. (1972) Interprétation fonctionelle et élimination des coupures dans 1’arithmétique d’ordre supérieur. Thèse de doctorat d’état, University of Paris.Google Scholar
Jategaonkar, L.A. and Mitchell, J.C. (1988) ML with extended pattern matching and subtypes. Proc. ACM Conf. on Lisp and Functional Programming, pp. 198211Google Scholar
Longo, G. and Moggi, E. (1988) Constructive natural deduction and its ‘w-set’ interpretation. Report CMU-CS-88–131, CMU, Dept. of Computer Science, Math. Struct. Comput. Set. 1 (2) to appear.Google Scholar
Meyer, B. (1988) Object-oriented Software Construction. Prentice-Hall.Google Scholar
Milner, R. (1978) A theory of type polymorphism in programming. J. Comput. Sys. Sci. 17 348375CrossRefGoogle Scholar
Mitchell, J.C. (1984) Coercion and type inference. Proc. 11th ACM Symp. on Principles of Programming Languages, pp. 175185CrossRefGoogle Scholar
Mitchell, J.C. (1986) A type inference approach to reduction properties and semantics of polymorphic expressions. Proc. Symp. on Lisp and Functional Programming, pp. 308319 (Revised version in Logic Foundations of Functional Programming, ed. G. Huet, Addison-Wesley, 1989, pp. 195–212)Google Scholar
Mitchell, J.C. (1990) Type systems for programming languages. In: Handbook of Theoretical Computer Science, Volume B, eds Leeuwen, J. vanet al., North-Holland, pp. 365458Google Scholar
Ohori, A., Buneman, P. and Breazu-Tannen, V. (1988) database programming in Machiavelli – a polymorphic language with static type inference. Report MS-CIS-88–103, University of Pennsylvania, Computer and Information Science Department.Google Scholar
Ohori, A. and Buneman, P. (1988) Type inference in a Database programming language. Proc. ACM Conf on LISP and Functional Programming, pp. 174183Google Scholar
Rémy, D. (1989) Typechecking records and variants in a natural extension of ML. Proc. 16th ACM Symp. on Principles of Programming Languages, pp. 7788Google Scholar
Reynolds, J.C. (1974) Towards a theory of type structure. In: Colloquium sur la Programmation. Springer Lecture Notes in Computer Science 19, pp. 408423Google Scholar
Schaffert, C., Cooper, T., Bullis, B., Kilian, M. and Wilpolt, C. (1986) An introduction to Trellis/Owl. Proc. ACM Conf. Object-Oriented Programming Systems, Languages and Applications, pp. 916Google Scholar
Stroustrup, B. (1986) The C++ Programming Language. Addison-Wesley.Google Scholar
Wand, M. (1987) Complete type inference for simple objects. Proc. Second IEEE Symp. on Logic in Computer Science, pp. 3744Google Scholar
Wand, M. (1989) Type inference for record concatenation and multiple inheritance. Proc. Fourth IEEE Symp. on Logic in Computer Science, pp. 9297Google Scholar