A foundational perspective -- types as constraints

intro, types, algebra, modules, classes, summary, Q/A, literature

Object-oriented programming may be regarded as a declarative method of programming, in the sense that it provides a computation model (expressed by the metaphor of encapsulation and message passing) that is independent of a particular implementation model. In particular, the inheritance subtype relation may be regarded as a pure description of the relations between the entities represented by the classes. Moreover, an object-oriented approach favors the development of an object model that bears close resemblance to the entities and their relations living in the application domain. However, the object-oriented programming model is rarely introduced with the mathematical precision characteristic of descriptions of the other declarative styles, for example the functional and logic programming model. Criticizing, [DT88] remark that {\em OOP is generally expressed in philosophical terms, resulting in a proliferation of opinions concerning what OOP really is}. From a type-theoretical perspective, our interest is to identify abstract data types as elements of some semantic (read mathematical) domain and to characterize their properties in an unambiguous fashion. See slide 8-mathematical.

Abstract data types -- foundational perspective

unambiguous values in some semantic domain

Mathematical models -- types as constraints

algebra -- set oriented
second order lambda calculus -- polymorphic types
constructive mathematics -- formulas as types

slide: Mathematical models for types

There seems to be almost no limit to the variety and sophistication of the mathematical models proposed to characterize abstract data types and inheritance. We may make a distinction between first order approaches (based on ordinary set theory) and higher order approaches (involving typed lambda calculus and constructive logic). The algebraic approach is a quite well-established method for the formal specification of abstract data types. A type (or sort) in an algebra corresponds to a set of elements upon which the operations of the algebra are defined. In the next section, we will look at how equations may be used to characterize the behavioral aspects of an abstract data type modeled by an algebra. Second order lambda calculus has been used to model information hiding and the polymorphism supported by inheritance and templates. In the next chapter we will study this approach in more detail. In both approaches, the meaning of a type is (ultimately) a set of elements satisfying certain restrictions. However, in a more abstract fashion, we may regard a type as specifying a constraint. The better we specify the constraint, the more tightly the corresponding set of elements will be defined (and hence the smaller the set). A natural consequence of the idea of types as constraints is to characterize types by means of logical formulas. This is the approach taken by type theories based on constructive logic, in which the notion of formulas as types plays an important role. Although we will not study type theories based on constructive logic explicitly, our point of view is essentially to regard types as constraints, ranging from purely syntactical constraints (as expressed in a signature) to semantic constraints (as may be expressed in contracts). From the perspective of types as constraints, a typing system may contribute to a language framework guiding a system designer's conceptualization and supporting the verification (based on the formal properties of the types employed) of the consistency of the descriptive information provided by the program. Such an approach is to be preferred (both from a pragmatic and theoretical point of view) to an ad hoc approach employing special annotations and support mechanisms, since these may become quite complicated and easily lead to unexpected interactions.

Formal models

There is a wide variety of formal models available in the literature. These include algebraic models (to characterize the meaning of abstract data types), models based on the lambda-calculus and its extensions (which are primarily used for a type theoretical analysis of object-oriented language constructs), algebraic process calculi (which may be used to characterize the behavior of concurrent objects), operational and denotational semantic models (to capture structural and behavioral properties of programs), and various specification languages based on first or higher-order logics (which may be used to specify the desired behavior of collections of objects). We will limit ourselves to studying algebraic models capturing the properties of abstract data types and objects (section algebra), type calculi based on typed extensions of the lambda calculus capturing the various flavors of polymorphism and subtyping (sections flavors--self-reference), and an operational semantic model characterizing the behavior of objects sending messages (section behavior). Both the algebraic and type theoretical models are primarily intended to clarify the means we have to express the desired behavior of objects and the restrictions that must be adhered to when defining objects and their relations. The operational characterization of object behavior, on the other hand, is intended to give a more precise characterization of the notion of state and state changes underlying the verification of object behavior by means of assertion logics. Despite the numerous models introduced there are still numerous approaches not covered here. One approach worth mentioning is the work based on the pi-calculus. The pi-calculus is an extension of algebraic process calculi that allow for communication via named channels. Moreover, the pi-calculus allows for a notion of migration and the creation and renaming of channels. A semantics of object-based languages based on the pi-calculus is given in [Walker90]. However, this semantics does not cover inheritance or subtyping. A higher-order object-oriented programming language based on the pi-calculus is presented in [PRT93]. Another approach of interest, also based on process calculi, is the object calculus (OC) described in [Nier93]. OC allows for modeling the operational semantics of concurrent objects. It merges the notions of agents, as used in process calculi, with the notion of functions, as present in the lambda calculus. For alternative models the reader may look in the {\tt comp.theory} newsgroup to which information concerning formal calculi for OOP is posted by Tom Mens of the Free University, Brussels.