[9] DejaVU Online: Principles of Object-Oriented Software Development (©)
[9] - [up] [top] - [I] [II] [III] [IV] - [1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12] - [A] [R]

Types as sets

Instructor's Guide

intro, inheritance, subtypes, polymorphism, types, hiding, self-reference, summary, Q/A, literature
A type, basically, denotes a set of elements. A type may be defined either extensionally, by listing all the elements constituting the type, or descriptively, as a constraint that must be satisfied by an individual to be classified as an element of the type.
slide: The interpretation of types as sets
Formally, we may define the value set of a type with subtypes as an isomorphism of the form
which expresses that the collection of values V consists of (the union of) basic types (such as Int) and compound types (of which V itself may be a component) such as record types (denoted by the product ) and function types (being part of the function space ). Within this value space V, subtypes correspond to subsets that are ordered by set inclusion. Technically, the subsets corresponding to the subtypes must be ideals, which comes down to the requirement that any two types have a maximal type containing both (in the set inclusion sense). Intuitively, the subtype relation may be characterized as a refinement relation, constraining the set of individuals belonging to a type. The subtype refinement relation may best be understood in terms of improving our knowledge with respect to (the elements of) the type. For a similar view, see  [GO90]. In case we have no knowledge of a particular element we simply (must) assume that it belongs to the value set V. Having no knowledge is represented by the maximal element of the lattice Top, which denotes the complete set V. Whenever we improve our knowledge, we may be more specific about the type of the element, since fewer elements will satisfy the constraints implied by our information. The bottom element Bottom of our type lattice denotes the type with no elements, and may be taken to consist of the elements for which we have contradictory information. See slide 9-types. Mathematically, a type system is nothing but a collection with ideals within some lattice V. In our subsequent treatment, however, we will primarily look at the refinement relation between two elements, rather than the set inclusion relation between their corresponding types.
[9] - [up] [top] - [I] [II] [III] [IV] - [1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12] - [A] [R]
Hush Online Technology
hush@cs.vu.nl
12/29/99