Principles of Object-Oriented Software Development

[] readme course preface 1 2 3 4 5 6 7 8 9 10 11 12 appendix lectures resources

The subtype relation

subsections:

Types as sets
The subtype refinement relation
Objects as records

In this section, we will study the subtype relation in a more formal manner. First we investigate the notion of subtypes in relation to the interpretation of types as sets, and then we characterize the subtype relation for a number of constructs occurring in programming languages (such as ranges, functions and records). Finally, we will characterize objects as records and correspondingly define the subtype relation for simple record (object) types. These characterizations may be regarded as a preliminary to the type calculi to be developed in subsequent sections.

Types as sets

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.

Types as sets of values

$V \approx Int \cup ... \cup V \times V \cup V -> V$

Ideals -- over $V$

subtypes -- ordered by set inclusion
lattice -- $Top = V$ , $Bottom = \emptyset$

Type system

subtypes correspond to subsets

a collection of ideals of V

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


   $V \approx Int  \cup ... \cup   V \times V  \cup  V -> V$

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

V \times V

) and function types (being part of the function space

V -> V

). 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.

The subtype refinement relation

In determining whether a given type is a subtype of another type, we must make a distinction between simple (or basic) types built into the language and compound (or user-defined) types explicitly declared by the programmer. Compound types, such as integer subranges, functions, records and variant records, themselves make use of other (basic or compound) types. Basic types are (in principle) only a subtype of themselves, although many languages allow for an implicit subtyping relation between for example integers and reals. The rules given in slide 9-subtypes characterize the subtyping relation for the compound types mentioned.

Sub-range inclusion

$<=$

\ffrac{ $n <= n'$ and $m' <= m$ }{ $n'..m' <= n..m$ }

Functions

contravariance

\ffrac{ $%s <= %s'$ and $%t' <= %t$ }{ $%s' -> %t' <= %s -> %t$ }

Records

\ffrac{ $%s_i <= %t_i$ for $i = 1..m$ ( $m <= n$ ) }{ ${a_1: %s_1, ... , a_n: %s_n} <= {a_1: %t_1 , ... , a_m: %t_m}$ }

Variants

\ffrac{ $%s_i <= %t_i$ for $i = 1..m$ ( $m <= n$ ) }{ $[a_1:%s_1 \/ ... \/ a_m:%s_m] <= [a_1:%t_1 \/ ... \/ a_n:%t_n]$ }

slide: The subtype refinement relation

We use the relation symbol

<=

to denote the subtype relation. Types (both basic and compound) are denoted by

%s

and

%t

. For subranges, a given (integer) subrange

%s

is a subtype of another subrange

%t

%s

is (strictly) included in

%t

as a subset. In other words, if

%s = n'..m'

and

%t = n..m

then the subtyping condition is

n <= n'

and

m' <= m

. We may also write

n'..m' \subseteq n..m

in this case. For functions we have a somewhat similar rule, a function

f' : %s' -> %t'

(with domain

%s'

and range or codomain

%t'

) is a subtype of a function

f : %s -> %t

(with domain

%s

and codomain

%t

) if the subtype condition

%s <= %s'

and

%t' <= %t

is satisfied. Note that the relation between the domains is contravariant, whereas the relation between the ranges is covariant. We will discuss this phenomenon of contravariance below. Records may be regarded as a collection of labels (the record fields) that may have values of a particular type. The subtyping rule for records expresses that a given record (type) may be extended to a (record) subtype by adding new labels, provided that the types for labels which occur in both records are refined in the subtype. The intuition underlying this rule is that by extending a record we add, so to speak, more information concerning the individuals described by such a record, and hence we constrain the set of possible elements belonging to that (sub)type. Variants are (a kind of) record that leave the choice between a (finite) number of possible values, each represented by a label. The subtyping rules for variants states that we may create a subtype of a given variant record if we reduce the choice by eliminating one or more possibilities. This is in accord with our notion of refinement as improving our knowledge, since by reducing the choice we constrain the set of possible individuals described by the variant record. The subtyping rules given above specify what checks to perform in order to determine whether a given (compound) type is a subtype of another type. In the following we will look in more detail at the justification underlying these rules, and also hint at some of the restrictions and problems implied. However, let us first look at some examples. See slide 9-ex-subtyping.

Examples

subtyping

$8..12 -> 3..5 <= 9..11 -> 2..6$
${ age : int, speed : int, fuel : int } <= { age : int, speed : int }$
$[ yellow \/ blue ] < [ yellow \/ blue \/ green ]$

slide: Examples of subtyping

As a first example, when we define a function

f' : 8..12 -> 3..5

and a function

f : 9..11 -> 2..6

then, according to our rules, we have

f' <= f

. Recall that we required subtypes to be compatible with their supertypes, compatible in the sense that an instance of the subtype may be used at all places where an instance of the supertype may be used. With regard to its signature, obviously,

f'

may be used everywhere where f may be used, since

f'

will deliver a result that falls within the range of the results expected from f and, further, any valid argument for f will also be accepted by

f'

(since the domain of

f'

is larger, due contravariance, than the domain of f). As another example, look at the relation between the record types

{ age : int, speed : int, fuel : int }

and

{ age : int, speed : int }

. Since the former has an additional field fuel it delimits so to speak the possible entities falling under its description and hence may be regarded as a subtype of the latter. Finally, look at the relation between the variant records

[yellow : color \/ blue : color ]

and

[yellow : color \/ blue : color \/ green : color ]

. The former leaves us the choice between the colors yellow and blue, whereas the latter also allows for green objects and, hence, encompasses the set associated with

[yellow : color \/ blue : color ]

Contravariance rule

The subtyping rules given above are all rather intuitive, except possibly for the function subtyping rule. Actually, the contravariance expressed in the function subtyping rule is somewhat of an embarrassment since it reduces the opportunities for specializing functions to particular types. See slide 9-functions.

Function refinement

$f' : Nat -> Nat \not<= f : Int -> Int$

Functions -- as a service

contravariance

domain -- restrictions for the client
range -- obligations for server

slide: The function subtype relation

Consider, for example, that we have a function

f : Int -> Int

, then it seems quite natural to specialize this function into a function

f' : Nat -> Nat

(which may make use of the fact that Nat only contains the positive elements of Int). However, according to our subtyping rule

f' \not<= f

, since the domain of

f'

is smaller than the domain of f. For an intuitive understanding of the function subtyping rule, it may be helpful to regard a function as a service. The domain of the function may then be interpreted as characterizing the restrictions imposed on the client of the service (the caller of the function) and the codomain of the function as somehow expressing the benefits for the client and the obligations for the (implementor of the) function. Now, as we have already indicated, to refine or improve on a service means to relax the restrictions imposed on the client and to strengthen the obligations of the server. This, albeit in a syntactic way, is precisely what is expressed by the contravariance rule for function subtyping.

Objects as records

Our interest in the subtype relation is primarily directed towards objects. However, since real objects involve self-reference and possibly recursively defined methods, we will first study the subtyping relation for objects as (simple) records. Our notion of objects as records is based on the views expressed in [Ca84]. Objects may be regarded as records (where a record is understood as a finite association of values to labels), provided we allow functions to occur as the value of a record field.

Objects as records

record = finite association of values to labels

Field selection -- basic operation

$(a = 3, b = true ).a == 3$

Typing rule

\ffrac{ $e_1 : %t_1$ and ... and $e_n : %t_n$ }{ ${ a_1 = e1,..., a_n = e_n } : { a_1 : %t_1, ..., a_n : %t_n }$ }

slide: The object subtype relation

The basic operation with records is field selection which, when the value of the field accessed is a function, may be applied for method invocation. The typing rule for records follows the construction of the record: the type of a record is simply the record type composed of the types of the record's components. See slide 9-objects. In the previous section we have already characterized the subtyping relation between records. This characterization is repeated in slide 9-ex-objects. The following is meant to justify this characterization. Let us first look at a number of examples that illustrate how the subtype relation fits into the mechanism of derivation by inheritance.

Subtyping -- examples


  type any = { }
  type entity = { age : int }
  type vehicle = { age : int, speed : int }
  type machine = { age : int, fuel : string }
  type car = { age : int, speed : int, fuel : string }

Subtyping rules

$%t <= %t$
\ffrac{ $%s_1 <= %t_1, ..., %s_n <= %t_n$ }{ ${ a_1 : %s_1, ..., a_{n + m} : %s_{n + m} } <= { a_1 : %t_1 , ..., a_n : %t_n }$ }

slide: Examples of object subtyping

Suppose we define the type any as the record type having no fields. In our view of types as constraints, the empty record may be regarded as imposing no constraints. This is in agreement with our formal characterization of subtyping, since according to the record subtyping rule the record type any is a supertype of any other record type. Subtyping in the sense of refinement means adding constraints, that is information that constrains the set of possible elements associated with the type. The record type entity, which assumes a field age, is a subtype of any, adding the information that age is a relevant property for an entity. Following the same line of reasoning, we may regard the types vehicle and machine as subtypes of the type entity. Clearly, we may have derived the respective types by applying inheritance. For example, we may derive vehicle from entity by adding the field speed, and machine from entity by adding the field fuel. Similarly, we may apply multiple inheritance to derive the type car from vehicle and machine, where we assume that the common field age (ultimately inherited from entity) only occurs once. Obviously, the type car is a subtype of both vehicle and machine. Each of the successive types listed above adds information that constrains the possible applicability of the type as a descriptive device. The other way around, however, we may regard each object of a particular (sub)type to be an instance of its supertype simply by ignoring the information that specifically belongs to the subtype. Mathematically, we may explain this as a projection onto the fields of the supertype. Put differently, a subtype allows us to make finer distinctions. For example, from the perspective of the supertype two entities are the same whenever they have identical ages but they may be different when regarded as vehicles (by allowing different speeds).

Conformance

The importance of subtyping for practical software development comes from the conformance requirement (or substitutability property) stating that any instance of a subtype may be used when an instance of a supertype is expected. This property allows the programmer to express the functionality of a program in a maximally abstract way, while simultaneously allowing for the refinement of these abstract types needed to arrive at an acceptable implementation. For objects as records, the refinement relation concerns both attributes and functions (as members of the object record). For attributes, refinement means providing more information. Syntactically, with respect to the (signature) type of the attribute, this means a restriction of its range. In other words, the possible values an attribute may take may only be restricted. Alternatively, the refinement relation may be characterized as restricting the non-determinism contained in the specification of the supertype, by making a more specific choice. For example, if we specify the speed range of a vehicle initially as

0..300.000

then we may restrict the speed range of a car safely to

0..300

. However, to stay within the regime of subtyping we may not subsequently enlarge this range by defining a subtype racing car with a speed range of

0..400

. Intuitively, subtyping means enforcing determinism, the restriction of possible choices. Our (syntactic) characterization of the subtyping relation between object types does not yet allow for data hiding, generics or self-reference. These issues will be treated in sections existential and self-reference. However, before that, let us look at the characterization of the subtyping relation between object types as defined (for example) for the language Emerald. The characterization given in slide 9-emerald is taken from [DT88].

Subtyping in Emerald -- S conforms to T

S provides at least the operations of T
for each operation in T, the corresponding operation in S has the same number of arguments
the type of the result of operations of S conform to those of the operations of T
the types of arguments of operations of T conform to those of the operations of S

slide: The subtype relation in Emerald

The object subtyping relation in Emerald is characterized in terms of conformance. The rules given above specify when an object type S conforms to an object (super) type T. These rules are in agreement with the subtyping rules given previously, including the contravariance required for the argument types of operations. Taken as a guideline, the rules specify what restrictions to obey (minimally) when specifying a subtype by inheritance. However, as we will discuss in the next section, polymorphism and subtyping is not restricted to object types only. Nor are the restrictions mentioned a sufficient criterion for a semantically safe use of inheritance.

[] readme course preface 1 2 3 4 5 6 7 8 9 10 11 12 appendix lectures resources

eliens@cs.vu.nl

draft version 0.1 (15/7/2001)