On understanding types, data abstraction, and polymorphism Export

@article{citeulike:271358, 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 lambda-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 lambda-calculus augmented to include binding of types by quantification as well as binding of values by abstraction. The typed lambda-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 lambda-calculus are discussed. The augmented typed lambda-calculus is used as a programming language for a variety of illustrative examples. We christen this language Fun because fun instead of lambda 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.}, address = {New York, NY, USA}, author = {Cardelli, Luca and Wegner, Peter}, citeulike-article-id = {271358}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=6042}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/6041.6042}, doi = {10.1145/6041.6042}, issn = {0360-0300}, journal = {ACM Comput. Surv.}, keywords = {functional-programming, lambda-calculus, objects, parametricity, polymorphism, subtyping, types}, month = {December}, number = {4}, pages = {471--523}, posted-at = {2005-09-14 08:16:21}, priority = {0}, publisher = {ACM}, title = {On understanding types, data abstraction, and polymorphism}, url = {http://dx.doi.org/10.1145/6041.6042}, volume = {17}, year = {1985} }

TY - JOUR ID - citeulike:271358 L3 - citeulike-article-id:271358 N2 - 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 lambda-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 lambda-calculus augmented to include binding of types by quantification as well as binding of values by abstraction. The typed lambda-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 lambda-calculus are discussed. The augmented typed lambda-calculus is used as a programming language for a variety of illustrative examples. We christen this language Fun because fun instead of lambda 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. IS - 4 JF - ACM Comput. Surv. SN - 0360-0300 AD - New York, NY, USA EP - 523 TI - On understanding types, data abstraction, and polymorphism PB - ACM VL - 17 SP - 471 KW - functional-programming KW - lambda-calculus KW - objects KW - parametricity KW - polymorphism KW - subtyping KW - types AU - Cardelli, Luca AU - Wegner, Peter PY - 1985/12// UR - http://dx.doi.org/10.1145/6041.6042 ER -