On understanding types, data abstraction, and polymorphism

Reviewer: 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.