)
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 
to denote the subtype relation.
Types (both basic and compound) are denoted by 
and 
.
For subranges, a given (integer) subrange 
is a subtype
of another subrange 
if 
is (strictly) included in 
as a subset.
In other words, if 
and 
then the subtyping
condition is 
and 
.
We may also write 
in this case.
For functions we have a somewhat similar rule,
a function 
(with domain 
and range or codomain 
) is a subtype of a function
(with domain 
and codomain 
)
if the subtype condition 
and 
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.
and a function
then, according to our rules,
we have 
.
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, 
may be used everywhere
where f may be used, since 
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 
(since the domain of
is larger, due contravariance, than the domain of f).
As another example, look at the relation between
the record types
and
.
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
and
.
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
.
, then it seems quite natural to specialize
this function into a function 
(which may make use of the fact that Nat only contains
the positive elements of Int).
However, according to our subtyping rule 
,
since the domain of 
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.
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 }
then we may restrict
the speed range of a car safely to 
.
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 
.
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 |
Hush Online Technology
hush@cs.vu.nl
12/29/99 |
|
|