topical media & game development
objectoriented programming
The subtype relation
subsections:
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\; \backslash approx\; Int\; \backslash cup\; ...\; \backslash cup\; V\; \backslash times\; V\; \backslash cup\; V\; >\; V$
Ideals  over $V$
 subtypes  ordered by set inclusion
 lattice  $Top\; =\; V$, $Bottom\; =\; \backslash 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\; \backslash approx\; Int\; \backslash cup\; ...\; \backslash cup\; V\; \backslash times\; V\; \backslash 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\; \backslash 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 [9types].
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 userdefined) 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 9subtypes
characterize the subtyping relation for the
compound types mentioned.
Subrange inclusion
$<=$
 \ffrac{$n\; <=\; n\text{'}$ and $m\text{'}\; <=\; m$}{$n\text{'}..m\text{'}\; <=\; n..m$}
Functions
contravariance

\ffrac{ $\%s\; <=\; \%s\text{'}$ and $\%t\text{'}\; <=\; \%t$}{$\%s\text{'}\; >\; \%t\text{'}\; <=\; \%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\; \backslash /\; ...\; \backslash /\; a\_m:\%s\_m]\; <=\; [a\_1:\%t\_1\; \backslash /\; ...\; \backslash /\; 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$ if $\%s$ is (strictly) included in $\%t$
as a subset.
In other words, if $\%s\; =\; n\text{'}..m\text{'}$ and $\%t\; =\; n..m$ then the subtyping
condition is $n\; <=\; n\text{'}$ and $m\text{'}\; <=\; m$.
We may also write $n\text{'}..m\text{'}\; \backslash subseteq\; n..m$ in this case.
For functions we have a somewhat similar rule,
a function $f\text{'}\; :\; \%s\text{'}\; >\; \%t\text{'}$ (with domain $\%s\text{'}$
and range or codomain $\%t\text{'}$) is a subtype of a function
$f\; :\; \%s\; >\; \%t$ (with domain $\%s$ and codomain $\%t$)
if the subtype condition $\%s\; <=\; \%s\text{'}$ and $\%t\text{'}\; <=\; \%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 [9exsubtyping].
Examples
subtyping
 $8..12\; >\; 3..5\; <=\; 9..11\; >\; 2..6$
 $\{\; age\; :\; int,\; speed\; :\; int,\; fuel\; :\; int\; \}\; <=\; \{\; age\; :\; int,\; speed\; :\; int\; \}$
 $[\; yellow\; \backslash /\; blue\; ]\; <\; [\; yellow\; \backslash /\; blue\; \backslash /\; green\; ]$
slide: Examples of subtyping
As a first example,
when we define a function $f\text{'}\; :\; 8..12\; >\; 3..5$ and a function
$f\; :\; 9..11\; >\; 2..6$ then, according to our rules,
we have $f\text{'}\; <=\; 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\text{'}$ may be used everywhere
where f may be used, since $f\text{'}$ 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\text{'}$ (since the domain of
$f\text{'}$ 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\; \backslash /\; blue\; :\; color\; ]$ and
$[yellow\; :\; color\; \backslash /\; blue\; :\; color\; \backslash /\; 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\; \backslash /\; 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 [9functions].
Function refinement
 $f\text{'}\; :\; Nat\; >\; Nat\; \backslash 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\text{'}\; :\; 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\text{'}\; \backslash not<=\; f$,
since the domain of $f\text{'}$ 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 selfreference
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 [9objects].
In the previous section we have already characterized
the subtyping relation between records.
This characterization is repeated in slide [9exobjects].
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 nondeterminism 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 selfreference.
These issues will be treated in sections [existential] and [selfreference].
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 [9emerald]
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.
(C) Æliens
04/09/2009
You may not copy or print any of this material without explicit permission of the author or the publisher.
In case of other copyright issues, contact the author.