1 Computing Surveys, Vol 17 n. 4, pp 471-522, December 1985On Understanding Types,Data Abstraction, and PolymorphismLuca CardelliAT&T Bell Laboratories, Murray Hill, NJ 07974(current address: DEC SRC, 130 Lytton Ave, Palo Alto CA 94301)Peter WegnerDept. of Computer Science, Brown UniversityProvidence, RI 02912AbstractOur 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 relevanceof recent research to the design of practical programming languages.Object-oriented languages provide both a framework and a motivation for exploring the interactionamong the concepts of type, data abstraction, and polymorphism, since they extend the notion of type todata 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, unencumberedby complexities of production programming languages.The evolution of languages from untyped universes to monomorphic and then polymorphic typesystems is reviewed. Mechanisms for polymorphism such as overloading, coercion, subtyping, andparameterization are examined. A unifying framework for polymorphic type systems is developed in termsof the typed λ-calculus augmented to include binding of types by quantification as well as binding of valuesby abstraction.The typed λ-calculus is augmented by universal quantification to model generic functions with typeparameters, existential quantification and packaging (information hiding) to model abstract data types, andbounded quantification to model subtypes and type inheritance. In this way we obtain a simple and precisecharacterization of a powerful type system that includes abstract data types, parametric polymorphism, andmultiple 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 illustrativeexamples. We christen this language Fun because fun instead of λ is the functional abstraction keywordand because it is pleasant to deal with.Fun is mathematically simple and can serve as a basis for the design and implementation of realprogramming languages with type facilities that are more powerful and expressive than those of existingprogramming languages. In particular, it provides a basis for the design of strongly typed object-orientedlanguages.2Contents1. From Untyped to Typed Universes1.1. Organizing Untyped Universes1.2. Static and Strong Typing1.3. Kinds of Polymorphism1.4. The Evolution of Types in Programming Languages1.5. Type Expression Sublanguages1.6. Preview of Fun2. The λ-Calculus2.1. The Untyped λ-Calculus2.2. The Typed λ-Calculus2.3. Basic Types, Structured Types and Recursion3. Types are Sets of Values4. Universal Quantification4.1. Universal Quantification and Generic Functions4.2. Parametric Types5. Existential Quantification5.1. Existential Quantification and Information Hiding5.2. Packages and Abstract Data Types5.3. Combining Universal and Existential Quantification5.4. Quantification and Modules5.5. Modules are First-Class Values6. Bounded Quantification6.1. Type Inclusion, Subranges, and Inheritance6.2. Bounded Universal Quantification and Subtyping6.3. Comparison with Other Subtyping Mechanisms6.4. Bounded Existential Quantification and Partial Abstraction7. Type Checking and Type Inference8. Hierarchical Classification of Type Systems9. ConclusionsAcknowledgementsReferencesAppendix: Type Inference Rules31. From Untyped to Typed Universes1.1. Organizing Untyped UniversesInstead of asking the question What is a type? we ask why types are needed in programminglanguages. To answer this question we look at how types arise in several domains of computer science andmathematics. The road from untyped to typed universes has been followed many times in many differentfields, and largely for the same reasons. Consider, for example, the following untyped universes:(1) Bit strings in computer memory(2) S-expressions in pure Lisp(3) λ-expressions in the λ-calculus(4) Sets in set theoryThe most concrete of these is the universe of bit strings in computer memory. ‘Untyped’ actuallymeans that there is only one type, and here the only type is the memory word, which is a bit string of fixedsize. This universe is untyped because everything ultimately has to be represented as bit strings: characters,numbers, pointers, structured data, programs, etc. When looking at a piece of raw memory there is generallyno way of telling what is being represented. The meaning of a piece of memory is critically determined byan external interpretation of its contents.Lisp's S-expressions form another untyped universe, one which is usually built on top of the previousbit-string universe. Programs and data are not distinguished, and ultimately everything is an S-expression ofsome kind. Again, we have only one type (S-expressions), although this is somewhat more structured(atoms and cons-cells can be distinguished) and has better properties than bit strings.In the λ-calculus, everything is (or is meant to represent) a function. Numbers, data structures andeven bit strings can be represented by appropriate functions. Yet there is only one type: the type offunctions from values to values, where all the values are themselves functions of the same type.In set theory, everything is either an element or a set of elements and/or other sets. To understand howuntyped this universe is, one must remember that most of mathematics, which is full of extremely rich andcomplex structures, is represented in set theory by sets whose structural complexity reflects the complexityof the structures being represented. For example, integers are generally represented by sets of sets of setswhose level of nesting represents the cardinality of the integer, while functions are represented by possiblyinfinite sets of ordered pairs with unique first components.As soon as we start working in an untyped universe, we begin to organize it in different ways fordifferent purposes. Types arise informally in any domain to categorize objects according to their usage andbehavior. The classification of objects in terms of the purposes for which they are used eventually results ina more or less well-defined type system. Types arise naturally, even