Luca Cardelli
Abstract
Our objective is to understand the notion of type in programming languages, present a model of typed, polymorphic programming languages that reflects recent research in type theory, and examine the relevance of recent research to the design of practical programming languages.
Object-oriented languages provide both a framework and a motivation for exploring the interaction among the concepts of type, data abstraction, and polymorphism, since they extend the notion of type to data abstraction and since type inheritance is an important form of polymorphism. We develop a λ-calculus-based model for type systems that allows us to explore these interactions in a simple setting, unencumbered by complexities of production programming languages.
The evolution of languages from untyped universes to monomorphic and then polymorphic type systems is reviewed. Mechanisms for polymorphism such as overloading, coercion, subtyping, and parameterization are examined. A unifying framework for polymorphic type systems is developed in terms of the typed λ-calculus augmented to include binding of types by quantification as well as binding of values by abstraction.
The typed λ-calculus is augmented by universal quantification to model generic functions with type parameters, existential quantification and packaging (information hiding) to model abstract data types, and bounded quantification to model subtypes and type inheritance. In this way we obtain a simple and precise characterization of a powerful type system that includes abstract data types, parametric polymorphism, and multiple inheritance in a single consistent framework. The mechanisms for type checking for the augmented λ-calculus are discussed.
The augmented typed λ-calculus is used as a programming language for a variety of illustrative examples. We christen this language Fun because fun instead of λ is the functional abstraction keyword and because it is pleasant to deal with.
Fun is mathematically simple and can serve as a basis for the design and implementation of real programming languages with type facilities that are more powerful and expressive than those of existing programming languages. In particular, it provides a basis for the design of strongly typed object-oriented languages.
- AHO, A. V., SETSI, R., AND ULLMAN, J. D. 1985. Compilers: Principles, Techniques and Tools. Addison-Wesley, Reading, Mass. Google Scholar
- ALBANO, A., CARDELLI, L., AND ORSINI, R. 1985. Galileo: A strongly typed, interactive conceptual language. Trans. Database Syst. 10, 2 (June), 230-260. Google Scholar
- BOOCH, G. 1983. Software Engineering with Ada. Benjamin/Cummings, Menlo Park, Calif. Google Scholar
- BRUCE, K. B., AND MEYER, R. 1984. The semantics of second order polymorphic lambda calculus. In Semantics of Data Types. Lecture Notes in Computer Science, vol. 173, G. Kahn, D. B. MacQueen, and G. Plotkin, Eds. Springer-Verlag, New York. Google Scholar
- BURSTALL, R., AND LAMPSON, B. 1984. A kernel language for abstract data types and modules. In Semantics of Data Types. Lecture Notes in Computer Science, vol. 173, G. Kahn, D. B. MacQueen, and G. Plotkin, Eds. Springer-Verlag, New York. Google Scholar
- BURSTALL, R., MACQUEEN, D., AND SANNELLA, D. 1980. Hope: An experimental applicative language. In Conference Record of the 1980 LISP Conference (Stanford, Calif., Aug.). ACM, New York, pp. 136-143. Google Scholar
- CARDELLI, L. 1984a. Basic polymorphic typechecking. Computing Science Tech. Rep. 119, AT&T Bell Laboratories, Murray Hill, N.J. Also in Polymorph. Newslett. 2, 1 (Jan.).Google Scholar
- CARDELLI, L. 1984b. A semantics of multiple inheritance. In Semantics of Data Types. Lecture Notes in Computer Science, vol. 173, G. Kahn, D. B. MacQueen, and G. Plotkin, Eds. Springer- Verlag, New York, pp. 51-67. Google Scholar
- CARDELLI, L. 1985. Amber. In Combinators and Functional Programming Languages, Proceedings of the 13th Summer School of the LITP (Le Val d'Ajol, Vosges, France, May). Google Scholar
- COQUAND, T., AND HUET, G. 1985. Constructions: a higher-order proof system for mechanizing mathematics. Tech. Rep. 401, INRIA, Rocquencourt, France (May).Google Scholar
- CURRY, H. B., AND FEYS, R. 1958. Combinatory Logic. North-Holland Publ., Amsterdam.Google Scholar
- DAMAS, L. 1984. Ph.D. dissertation. Dept. of Computer Science, Univ. of Edinburgh, Edinburgh, Scotland.Google Scholar
- DAMAS, L., AND MILNER, R. 1982. Principal type-schemes for functional programs. In Proceedings of the 9th Annual Symposium on Principles of Programming Languages (Albuquerque, N. Mex., Jan. 25-27). ACM, New York, pp. 207-212. Google Scholar
- DEMERS, A., AND DONAHUE, J. 1979. Revised report on Russell. TR 79-389, Computer Science Dept., Cornell Univ., Ithaca, N.Y.Google Scholar
- DOD (U.S. DEPARTMENT OF DEFENSE) 1983. Ada reference manual. ANSI/MIS-STD 1815 (Jan.). U.S. Govt. Printing Office.Google Scholar
- FAIRBAIRN, J. 1982. Ponder and its type system. Tech. Rep. 31, Computer Laboratory, Univ. of Cambridge, Cambridge, England. (Nov.).Google Scholar
- GIRARD, J.-Y. 1971. Une extension de l'interpretation de Godel ~ l'analyse, et son application a l'/~limination des coupures dans l'analyse et la th~orie des types. In Proceedings of the 2nd Scandinavian Logic Symposium, J. E. Fenstad, Ed. North-Holland Publ., Amsterdam, pp. 63- 92.Google Scholar
- GOLDBERG, A., ANO ROBSON, D. 1983. Smalltalk-80: The Language and Its Implementation. Addison-Wesley, Reading, Mass. Google Scholar
- GOROON, M., MILNER, R., AND WADSWORTH, C. 1979. Edinburgh LCF. Lecture Notes in Computer Science, vol. 78. Springer-Verlag, New York.Google Scholar
- HENDLER, J., AND WEGNER, P. 1986. Viewing object-oriented programming as an enhancement of data abstraction methodology. In Proceedings of the Hawaii Conference on System Sciences (Jan.).Google Scholar
- HINOLEY, R. 1969. The principal type scheme of an object in combinatory logic. Trans. Am. Math. Soc. 146 (Dec.), 29-60.Google Scholar
- HOOK, J. G. 1984. Understanding Russell: A first attempt. In Semantics of Data Types. Lecture Notes in Computer Science, vol. 173, G. Kahn, D. B. MacQueen, and G. Plotkin, Eds. Springer- Verlag, New York. Google Scholar
- LISKOV, B. H. 1981. CLU Reference Manual. Lecture Notes in Computer Science, vol. 114. Springer- Verlag, New York. Google Scholar
- MACQUEEN, D. B. 1984. Modules for standard ML. In Proceedings of the Symposium on LISP and Functional Programming (Austin, Tex., Aug. 6-8). ACM, New York, pp. 198-207. Google Scholar
- MACQUEEN, D. B. 1986. Using dependent types to express modular structure. In Proceedings of the 13th Annual Conference on Principles of Programming Languages (St. Petersburg Beach, Fla., Jan. 13-15). ACM, New York, pp. 277-286. Google Scholar
- MACQUEEN, D. B., PLOTKIN, G. D., AND SETHI, R. 1984. An ideal model for recursive polymorphic types. In Proceedings of the 11th Annual Symposium on Principles of Programming Languages (Salt Lake City, Utah, Jan 15-18). ACM, New York, pp. 165-174. Google Scholar
- MARTIN-LOF, P. 1980. Intuitionistic type theory. Notes of Giovanni Sambin on a series of lectures given in Padova, Univ. of Padova, Italy (June).Google Scholar
- MATTHEWS, D. C. J. 1985. Poly manual. Tech. Rep. No. 63, Computer Laboratory, Univ. of Cambridge, Cambridge, England.Google Scholar
- MILNER, R. 1978. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348-375.Google Scholar
- MILNER, R. 1984. A proposal for Standard ML. In Proceedings o{ the Symposium on LISP and Functional Programming (Austin, Tex., Aug. 6-8). ACM, New York, pp. 184-197. Google Scholar
- MITCHELL, J. C. 1984. Type inference and type containment. In Semantics o{ Data Types. Lecture Notes in Computer Science, vol. 173, G. Kahn, D. B. MacQueen, and G. Plotkin, Eds. Springer- Verlag, New York, pp. 51-67. Google Scholar
- MITCHELL, J. C., AND PLOTKIN, G. D. 1985. Abstract types have existential type. In Proceedings o{ the 12th Annual Symposium on Principles o{ Programming Languages (New Orleans, La., Jan. 14-16). ACM, New York, pp. 37-51. Google Scholar
- MITCHELL, J. C., MAYBURY, W., AND SWEET, R. 1979. Mesa language manual. Rep. CSL-79-3, Xerox Palo Alto Research Center, Palo Alto, Calif. (Apr.).Google Scholar
- REYNOLDS, J. C. 1974. Towards a theory of type structure. In Colloquium sur la programrnation. Lecture Notes in Computer Science, vol. 19. Springer-Verlag, New York. Google Scholar
- REYNOLDS, J. C. 1985. Three approaches to type structure. In Mathematical Foundations o{ So{tware Development. Lecture Notes in Computer Science, vol. 185. Springer-Verlag, Berlin, pp. 97-138. Google Scholar
- ROBINSON, J. A. 1965. A machine-oriented logic based on the resolution principle. J. ACM 12, i (Jan.), 23-49. Google Scholar
- SCHMIOT, E. E. 1982. Controlling large software development in a distributed environment. Rep. CSL-82-7, Xerox Palo Alto Research Center, Palo Alto, Calif. (Dec.).Google Scholar
- SCOTT, D. S. 1976. Data types as lattices. SIAM J. Comput. 5, 3, 523-587.Google Scholar
- SOLOMON, M. 1978. Type definitions with parameters. In Proceedings of the Con{erence on Principles of Programming Languages (Tucson, Ariz., Jan.). ACM, New York. Google Scholar
- STRACHEY, C. 1967. Fundamental concepts in programming languages. Lecture notes for International Summer School in Computer Programming, Copenhagen, Aug.Google Scholar
- WEGNER, P. 1983. On the unification of data and program abstraction in Ada. In Proceedings of the 10th Annual Symposium on Principles of Programming Languages (Austin, Tex., Jan. 24- 26). ACM, New York, pp. 256-264. Google Scholar
- WEINREB, D., AND MOON, D. 1981. LISP Machine Manual, Chapter 20: Objects, Message-Passing, and Flavors. Symbolics Inc., Cambridge, Mass.Google Scholar
- WELSH, J., SNEERINGER, W. J., AND HOARE, C. A. R. 1977. Ambiguities and insecurities in Pascal. So{tw. Pract. Exper. (Nov.).Google Scholar
- WIRTH, N. 1983. Programming in Modula-2. Springer-Verlag, New York. Google Scholar
Recommendations
Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types
Bidirectional typechecking, in which terms either synthesize a type or are checked against a known type, has become popular for its applicability to a variety of type systems, its error reporting, and its ease of implementation. Following principles from ...
Reviews
Edward A. Schneider
With the large amount of work done in the last few years on types, this paper is long overdue. The second-order typed &lgr;-calculus is used as a model for typed programs. The model is shown to be very flexible, permitting both parametric and inclusion polymorphism, as well as information hiding. The data abstraction mechanism of Ada and the class hierarchies of object-oriented languages can be modeled. The paper starts with a short survey of types as found in current programming languages and what is meant by polymorphism. The typed &lgr;-calculus is then introduced. Types are considered to be sets of values and are not themselves considered to be values. Most of the last half of the paper describes quantification. Universal quantification over types is used to handle polymorphism, and existential quantification is used to represent information hiding. These two notions can be combined to obtain parametric data abstraction. The bounded quantification is used to model inclusion polymorphism. Finally, type checking and type inference are briefly discussed and a hierarchy of type systems is given. The paper presents only one model of types. It does not, for example, permit types to be first-class objects that can be manipulated. Also, as is pointed out, features that may be contained in languages but which cause problems with compile-time checking cannot be handled by the model. Perhaps a future survey will contrast this model with some of the others. The paper is very readable. There are many good examples to highlight the points made. Some knowledge of the &lgr;-calculus and of languages such as Ada, SIMULA, and Smalltalk is helpful.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments