On Understanding Types, Data Abstraction, and Polymorphism
đź“ś 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.
✨ Summary
The paper develops a unified λ-calculus-based account of types, data abstraction, and polymorphism. It begins by contrasting untyped universes—such as memory words, Lisp S-expressions, λ-expressions, and sets—with typed systems, arguing that types constrain object interactions, protect representations, and enable earlier detection of errors. It distinguishes static typing from strong typing and separates monomorphic languages from polymorphic ones.
The central taxonomy divides polymorphism into ad-hoc polymorphism and universal polymorphism. Overloading and coercion are treated as ad-hoc mechanisms, while parametric polymorphism and inclusion polymorphism are treated as universal mechanisms. Parametric polymorphism supports functions that operate uniformly across types; inclusion polymorphism supports the use of subtype values in supertype contexts and provides a type-theoretic interpretation of inheritance.
The authors model types as ideals, or suitably well-behaved sets of values, ordered by inclusion. Under this interpretation, subtype relations correspond to set inclusion, and a polymorphic value may belong to multiple types. The model supplies a common semantic basis for simple types, recursive types, parametric polymorphism, abstract types, and inheritance.
The paper extends the typed λ-calculus with three forms of quantification. Universal quantification models generic functions and parametric types, including functions such as a polymorphic identity function and generic list operations. Existential quantification models abstract data types by packaging a representation together with an interface while hiding the representation from clients. The paper uses packages, points, stacks, and modules to show how existential types express information hiding, representation independence, and first-class modules. Combining universal and existential quantification yields generic abstract data types, such as stacks whose element type is polymorphic while their internal representation is hidden.
Bounded quantification restricts type variables to subtypes of a specified bound. This provides a formal account of subtype polymorphism and inheritance while preserving relationships between argument and result types. The paper gives record, variant, function, and subrange inclusion rules, explains how records can model multiple inheritance, and uses bounded existential quantification to express abstract types that themselves participate in subtype relations.
The language Fun serves as a compact illustrative notation rather than a proposed production language. Its type system integrates records, variants, functions, recursion, universal quantification, existential packaging, subtyping, and bounded quantification. The authors argue that explicit type information makes checking expressive features comparatively tractable, while fully automatic inference becomes difficult or unavailable once existential types and subtyping are added. They also identify complications involving polymorphic side effects.
The paper’s classification of type systems places first-order systems at the base, with higher-order functions and inheritance developing along separate dimensions, and with universal, existential, and bounded quantification providing increasingly expressive combinations. Its concrete influence is visible in subsequent type-theory and programming-language work: Pierce’s Types and Programming Languages treats universal and existential polymorphism, subtyping, bounded quantification, recursive types, and object-oriented encodings as core topics; later object-calculus work explicitly identifies its subtype formalism as an extension of the bounded-quantification calculus associated with Cardelli and Wegner; and later research on existential types and type classes cites the paper while developing implementations and formal systems for their combination. (mitpress.mit.edu)
Overall, the paper’s main contribution is a common conceptual and formal vocabulary for relating parametric polymorphism, abstract data types, modules, subtyping, and inheritance. Bibliographic databases identify it as a 1985 ACM Computing Surveys article by Luca Cardelli and Peter Wegner. (dblp.org)