topical media & game development
objectoriented programming
Polymorphism
From a theoretical perspective,
object orientation
may be characterized
as combining abstract data types
and polymorphism.
These notions may be considered as the theoretical counterparts
of the more operational notions of encapsulation
and inheritance.
Polymorphism
9
 abstract inheritance
 subtypes
 type abstraction
 selfreference
Additional keywords and phrases:
exceptions, type calculi,
parametric types, coercion, ad hoc polymorphism,
universal types, existential types,
unfolding, intersection types
slide: Polymorphism
In this chapter we will study the notion of polymorphism.
We start our exploration by looking at the
role of inheritance in knowledge representation.
Then we will formally characterize the (signature)
subtype relation and explain the contravariance rule
for function subtypes.
To better understand polymorphism and its relation to
inheritance, we will
develop a type calculus,
allowing us to define abstract types using
universally and existentially quantified type
expressions.
In a similar way, we will look at polymorphism due
to overloading and generic type definitions.
Finally, we will look at the role of
selfreference in typing object descriptions derived by inheritance.
Together with developing the calculi,
examples will be given that illustrate
the properties of the C++ and Eiffel
type systems.
objectoriented programming
Abstract inheritance
Inheritance hierarchies play a role both in
knowledge representation systems and objectoriented
programming languages,
see [LNS90].
In effect, historically, the notions of frames
and isa hierarchies (that play a role in
knowledge representation) and the notions
of classes and inheritance (that
have primarily been developed in a programming language context)
have mutually influenced each other.
In objectoriented programming languages, classes and inheritance are
strongly related to types and polymorphism, and directed
towards the construction of reliable programming
artifacts.
In contrast, the goal of knowledge representation is to
develop a semantically consistent description
of some real world domain, which allows us to reason about
the properties of the elements in that domain.
Abstract inheritance
 declarative relation among entities
Inheritance networks
 isatrees  partial ordering
 isa/isnot  bipolar, isnot inference
Nonmonotonic reasoning
Nixon isa Quaker
Nixon isa Republican
Quakers are Pacifists
Republicans are not Pacifists
Incremental system evolution is in practice nonmonotonic!
slide: Knowledge representation and inheritance
One of the first formal analyses of the declarative
aspects of inheritance systems was given in
[To86].
The theoretical framework developed in [To86]
covers the inheritance formalisms found in
frame systems such as FRL, KRL, KLONE and NETL,
but also to some extent the inheritance mechanisms
of Simula, Smalltalk, Flavors and Loops.
The focus of [To86], however, is to develop a formal
theory of inheritance networks including
defaults and exceptions.
The values of
attributes play a far more important role in such networks
than in a programming context.
In particular, to determine whether the relationships expressed
in an inheritance graph are consistent, we must be able to
reason about the values of these attributes.
In contrast, the use of inheritance in programming languages
is primarily focused on sharing instance variables and
overriding (virtual) member functions, and is not so much concerned
with the actual values of instance variables.
Inheritance networks in knowledge representation systems
are often non monotonic as a result
of having isnot relations in addition to isa
relations
and also because properties (for example canfly)
can be deleted.
Monotonicity is basically the requirement that all
properties are preserved, which is the case for
strict inheritance satisfying the substitution principle.
It is a requirement that should be adhered to
at the risk of jeopardizing the integrity of the
system.
Nevertheless, strict inheritance may be regarded
as too inflexible to express real world
properties in a knowledge representation system.
The meaning of isa and isnot relations in
a knowledge representation inheritance graph may
equivalently be
expressed as predicate logic statements.
For example, the statements
 $\backslash A\; x\; .\; Quaker(x)\; >\; Human(x)$
 $\backslash A\; x\; .\; Republican(x)\; >\; Human(x)$
express the relation between, respectively,
the predicates Quaker and Republican
to the predicate Human in the graph above.
In addition, the statements
 $\backslash A\; x\; .\; Quaker(x)\; >\; Pacifist(x)$
 $\backslash A\; x\; .\; Republican(x)\; >\; \backslash neg\; Pacifist(x)$
introduce the predicate Pacifist that
leads to an inconsistency when considering the
statement that Nixon is a Quaker and a Republican.
Some other examples of statements expressing
relations between entities in a taxonomic structure
are given in slide [9logic].
Taxonomic structure
$\backslash A\; x\; .\; Elephant(x)\; >\; Mammal(x)$
$\backslash A\; x\; .\; Elephant(x)\; >\; color(x)\; =\; gray$
$\backslash A\; x\; .\; Penguin(x)\; >\; Bird(x)\; /\backslash \; \backslash neg\; CanFly(x)$
slide: Taxonomies and predicate logic
The latter is often used as an example of
nonmonotonicity that may occur when using defaults
(in this case the assumption that all birds can fly).
The mathematical semantics for declarative taxonomic hierarchies,
as given in [To86], are based on the notion of
constructible lattices of predicates,
expressing a partial order between the predicates
involved in a taxonomy (such as, for example, Quaker and Human).
A substantial part of the analysis presented in [To86],
however, is concerned with employing the graph
representation of inheritance structures
to improve on the efficiency of reasoning
about the entities populating the graph.
In the presence of multiple inheritance and nonmonotonicity
due to exceptions and defaults, care must be taken
to follow the right path through
the inheritance graph when searching for the value
of a particular attribute.
Operationally, the solution presented by [To86]
involves an ordering of inference paths (working upwards)
according to the number of intermediate nodes.
Intuitively, this corresponds to the distance
between the node using an attribute and the node defining
the value of the attribute.
In strictly monotonic situations such a measure plays
no role, however!
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.
objectoriented programming
Flavors of polymorphism
Polymorphism is not a feature exclusive to objectoriented
languages.
For example the ML language is a prime example
of a non objectoriented language
supporting a polymorphic type system
(see Milner {\it et al.}, 1990).
Also, most languages, including Fortran and Pascal,
support implicit conversion between integers
and floats, and backwards from floats to integers,
and (in Pascal) from integer subranges to integers.
Polymorphism (including such conversions) is a means
to relieve the programmer from the rigidity imposed
by typing.
Put differently, it's a way in which to increase
the expressivity of the type system.
Typing  protection against errors
 static  type checking at compile time
 strong  all expressions are type consistent
Untyped  flexibility
 bitstrings, sets, $\%l$calculus
Exceptions to monomorphic typing:
 overloading, coercion, subranging, valuesharing (nil)
slide: The nature of types
Typing, as we have argued before, is important as
a means to protect against errors.
We must distinguish between static typing
(which means that type checking takes place at compile time)
and strong typing
(which means that each expression must be type consistent).
In other words, strong typing allows illegal
operations to be recognized and rejected.
Objectoriented languages (such as Eiffel, and
to a certain extent C++) provide strong typing
which is a mixture of static typing and runtime
checks to effect the dynamic binding of method
invocations.
See slide [9typing].
Typed languages impose rather severe constraints
on the programmer.
It may require considerable effort to arrive at
a consistently typed system and to deal with
the additional notational complexity of defining
the appropriate types.
In practice, many programmers and mathematicians
seem to have a preference for working in
an untyped formalism, like bitstrings, (untyped) sets
or (untyped) lambda calculus.
We may further note that languages such as Lisp,
Prolog and Smalltalk are popular precisely
because of the flexibility due to the absence
of static type checking.
Flavors of polymorphism
 inclusion polymorphism  to model subtypes and inheritance
 parametric polymorphism  uniformly on a range of types
 intersection types  coherent overloading
slide: Flavors of polymorphism
For reliable software development, working in an untyped
setting is often considered as not satisfactory.
However, to make typing practical, we need to relieve
the typing regime by supporting wellunderstood
exceptions to monomorphic typing, such as overloaded
functions, coercion between data types and value sharing
between types (as provided by a generic nil value).
More importantly, however, we must provide for controlled
forms of polymorphism.
In [CW85], a distinction is made between
ad hoc polymorphism
(which characterizes the mechanisms mentioned
as common exceptions to monomorphic typing)
and universal polymorphism
(which allows for theoretically wellfounded
means of polymorphism).
Universal polymorphism may take the form of
inclusion polymorphism
(which is a consequence of derivation by inheritance)
or parametric polymorphism
(which supports generic types,
as the template mechanism offered
by C++).
See slide [9flavors].
The term inclusion polymorphism may be understood
by regarding inheritance as a means to
define the properties of a (sub)type incrementally,
and thus (by adding information) delimiting a subset of
the elements corresponding to the supertype.
When overloading is done in a systematic fashion we may
speak of intersection types, which allows for
polymorphism based on a finite enumeration of types.
See section [calculi].
The notion of inheritance as incremental
modification was originally introduced
in [WZ88].
Abstractly, we may characterize derivation by inheritance
in a formula as $R\; =\; P\; +\; M$, where R is the result
obtained by modifying the parent P by (modifier) M.
See slide [9inheritance].
Inheritance  incremental modification
 Result = Parent + Modifier
Example: $R\; =\; \{\; a1,\; a2\; \}\; +\; \{\; a2,\; a3\; \}\; =\; \{\; a1,\; a2,\; a3\; \}$
Independent attributes: M disjoint from P
Overlapping attributes: M overrules P
Dynamic binding
 $R\; =\; \{...,P\_i:\; self\; !\; A,...\}\; +\; \{\; ...,M\_j:\; self\; !\; B,\; ...\; \}$
slide: Inheritance as incremental modification
For example, we may define the record consisting
of attributes $a\_1\; ...\; a\_n$ by adding
$\{\; a\_2,\; a\_3\; \}$ to the parent $\{\; a\_1,\; a\_2\; \}$.
Clearly, we must make a distinction between
independent attributes (that occur in either
P or M) and overlapping attributes (that occur
in both P and M and are
taken to be overruled by the definition given in M).
An important property of objects,
not taken into account in our interpretation
of object as records given before, is that
objects (as supported by objectoriented languages)
may be referring to themselves.
For example, both in the parent and the modifier
methods may be defined that refer to a variable this or
self (denoting the object itself).
It is important to note that the variable self is dynamically
bound to the object and not (statically) to
the textual module in which the variable self occurs.
[WZ88] make a distinction between attributes that
are redefined in M, virtual attributes
(that need to be defined in M) and recursive
attributes (that are defined in P).
Each of these attributes may represent methods
which (implicitly) reference self.
(In many objectoriented languages, the variable self
or this is implicitly assumed
whenever a method defined within the scope of the
object is invoked.)
Selfreference (implicit or explicit) underlies
dynamic binding and hence is where
the power of inheritance comes from.
Without selfreference
method calls
would reduce to statically bound function invocation.
Generic abstract data types
Our goal is to arrive at a type theory with sufficient power
to define generic (polymorphic) abstract data types.
In the following section, we will develop a number of type
calculi (following Pierce, 1993)\index{Pierce (1993)} that enable
us to define polymorphic types
by employing type abstraction.
Type abstraction may be used to define generic
types, data hiding and (inheritance) subtypes.
The idea is that we may characterize generic types
by quantifying over a type variable.
For example, we may define the identity
function id generically as $\backslash A\; T.\; id(\; x:T\; )\; =\; x$,
stating that for arbitrary type T and element x of
type T, the result of applying id to x
is x. Evidently this holds for any T.
In a similar way, we may employ type parameters
to define generic abstract data types.
Further, we may improve on our notion
of objects as records
by defining a packaging construct that allows for data hiding
by requiring merely that there exists
a particular type implementing the hidden component.
Also, we may characterize the (inheritance) subtyping relation
in terms of bounded quantification,
that is quantification over a restricted collection
of types (restricted by imposing constraints
with respect to the syntactic structure of the type
instantiating the type parameter).
objectoriented programming
Type abstraction
subsections:
In this section we will study type
calculi that allow us to express
the various forms of polymorphism, including
inclusion polymorphism (due to inheritance),
parametric polymorphism (due to generics)
and intersection types (due to overloading),
in a syntactic way, by means of appropriate
type expressions.
The type calculi are based on the typed lambda calculus
originally introduced in [Ca84] to study the semantics
of multiple inheritance.
We will first study some simple extensions to the typed
lambda calculus and then discuss examples
involving universal quantification (defining parametric types),
existential quantification (hiding implementation details)
and bounded quantification (modeling subtypes
derived by inheritance).
For those not familiar with the lambda calculus,
a very elementary introduction is given below.
For each calculus, examples will be given to relate
the insights developed to properties of the
C++ type system.
The lambda calculus
The lambda calculus provides a very concise,
yet powerful formalism to reason about
computational abstraction.
The introduction given here has been taken from
[Barend], which is a standard reference on this subject.
Lambda calculus  very informal
$\%l$
 variables, abstractor $\%l$, punctuation $(,)$
Lambda terms  $ %L $
 $x\; \backslash e\; \%L$ \zline{variables}
 $M\; \backslash e\; \%L\; =>\; \%l\; x.\; M\; \backslash e\; \%L$ \zline{abstraction}
 $M\; \backslash e\; \%L$ and $N\; \backslash e\; \%L\; =>\; M\; N\; \backslash e\; \%L$ \zline{application}
slide: The lambda calculus  terms
Syntactically, lambda terms are built from a very simple syntax,
figuring variables, the abstractor $\%l$ (that is
used to bind variables in an expression), and punctuation
symbols.
Abstractors may be used to abstract a lambda term M into
a function $\%l\; x.M$ with parameter x.
The expression $\%l\; x.M$ must be read as denoting the
function with body M and formal parameter x.
The variable x is called the bound variable, since it
is bound by the abstractor $\%l$.
In addition to function abstraction, we also
have (function) application, which is written
as the juxtaposition of two lambda terms.
See slide [lambdaterms].
Behaviorally, lambda terms have a number of properties,
as expressed in the laws given in slide [lambdalaws].
Laws
 $(\; \%l\; x.M)\; N\; =\; M\; [\; x\; :=\; N\; ]$ \zline{conversion}
 $M\; =\; N\; =>\; MZ\; =\; NZ$ and $ZM\; =\; ZN$
 $M\; =\; N\; =>\; \%l\; x.M\; =\; \%l\; x.N$
slide: The lambda calculus  laws
The most important rule is the beta conversion
rule, which describes in a manner of speaking how
parameter passing is handled.
In other words function call, that is the application
$(\%l\; x.M)N$, results
in the function body M in which N is substituted
for x.
Two other laws are the socalled extensionality axioms,
which express how equality of lambda terms
is propagated into application and function abstraction.
These laws impose constraints upon the models
characterizing the meaning of lambda terms.
Substitution
 $x[x:=N]\; ==\; N$
 $y[x:=N]\; ==\; y$ if $x\; !=\; y$
 $(\%l\; y.M)[x:=N]\; ==\; \%l\; y.(M[x:=N])$
 $(M\_1\; M\_2\; )\; [x:=N]$ $==$ $(M\_1\; [x:=N])\; (M\_2[x:=N])$
slide: The lambda calculus  substitution
Substitution is defined by induction on the
structure of lambda terms.
A variable y is replaced by N (for a substitution $[x:=N]$)
if y is x and remains y otherwise.
A substitution $[x:=N]$ performed on an abstraction
$\%l\; y.M$ results in substituting N for x in M
if x is not y.
If x is identical to y, then y must first
be replaced by a fresh variable (not occurring in M).
A substitution performed on an application simply
results in applying the substitution to both
components of the application.
See slide [lambdasubstitution].
Some examples of beta conversion are given
in slide [lambdaexamples].
In the examples, for simplicity we employ
ordinary arithmetical values and operators.
This does not perturb the underlying $\%l$theory,
since both values and operations may be expressed
as proper $\%l$terms.
Examples
$($\%l x.x) 1 = x[x:=1] = 1
$($\%l x.x+1) 2 = (x+1)[x:=2] = 2 + 1
$($\%l x.x+y+1) 3 = (x+y+1)[x:=3] = 3+y+1
$($\%l y.(\%l x.x+y+1) 3) 4) =
$(($\%l x.x+y+1) 3)[y:=4] = 3 + 4 + 1
slide: Beta conversion  examples
Note that the result of a substitution may still contain
free variables (as in the third example) that
may be bound in the surrounding environment
(as in the fourth example).
Lambda calculus may be used to state properties
of functions (and other programming constructs)
in a general way.
Properties
 $\backslash A\; M\; (\%l\; x.x)\; M\; =\; M$ \zline{identity}
 $\backslash A\; F\; \backslash E\; X.\; F\; X\; =\; X$ \zline{fixed point}
Proof: take $W\; =\; \%l\; x.F\; (\; xx\; )$ and $X\; =\; WW$, then
$X\; =\; WW\; =\; ($\%l x.F ( xx ) ) W = F ( WW ) = FX
slide: The lambda calculus  properties
Consider, for example, the statement
that the identity function works for each lambda term
as expected.
The quantification with respect to M indicates
that in each possible model for the lambda calculus
(that respects the extensionality axioms given above)
the identity $(\%l\; x.x)M\; =\; M$ holds.
See slide [lambdaproperties].
As another example, consider the statement that each function F
has a fixed point, that is a value X for which $FX\; =\; X$.
The proof given above, however, does not give us any information
concerning the actual contents of the fixed point,
but merely proves its existence.
In the following (see section [selfreference])
we will write $\backslash Y(F)$ for the fixed
point of a function F.
In [Barend], an extensive account is given of how to
construct mathematical models for the lambda calculus.
A semantics of our type calculus may be given in terms
of such models; however we will not pursue this
any further here.
A simple type calculus
In our first version of a type calculus
we will restrict ourselves to a given set
of basic types (indicated by the
letter $\%r$) and function types (written
$\%s\; >\; \%t$, where $\%s$ stands for the domain
and $\%t$ for the range or codomain).
This version of the typed lambda calculus
(with subtyping) is called $\%l\_\{\; <=\; \}$ in
[Pierce93] from which most of the material is taken.
The $\%l\_\{<=\}$ calculus is a first order calculus, since it
does not involve quantification over types.
See slide [9csubtypes].
The structure of type expressions is given by the
definition
$$\%t ::= \%r  \%t_1 > \%t_2
where we use $\%t$ as a type identifier and $\%r$
as a meta variable for basic types.
The expressions of our language, that we indicate with
the letter e, are similar to lambda terms,
except for the typing of the abstraction variable in
$\%l\; x:\; \%t.e$.
A simple type calculus  subtypes
$\%l\_\{\; <=\; \}$
 $\%t\; ::=\; \%r\; \; \%t\_1\; >\; \%t\_2$
 $e\; ::=\; x\; \; \%l\; x\; :\; \%t\; .\; e\; \; e\_1\; e\_2$
Type assignment
 \ffrac{$\%G\; \; x\; :\; \%s$ \hspace{1cm} $\%G\; \; e\; :\; \%t$}{
$\%G\; \; \%l\; x\; :\; \%s\; .\; e\; \backslash e\; \%s\; >\; \%t$
}
 \ffrac{$\%G\; \; e\_1\; :\; \%s\; >\; \%t,\; e\_2\; :\; \%s$}{
$\%G\; \; e\_1\; e\_2\; \backslash e\; \%t$
}
Refinement
 \ffrac{ $\%G\; \; e\; :\; \%s$ \hspace{1cm} $\%G\; \; \%s\; <=\; \%t$}{
$\%G\; \; e\; :\; \%t$
}
slide: The subtype calculus
To determine whether an expression e
is correctly typed (with some type expression $\%t$)
we need type assignment rules, as given above.
Typing is usually based on a collection
of assumptions $\%G$, that contains the typing of
expressions occurring in the expression
for which we are determining the type.
In the type assignment rules and the (subtyping)
refinement rules, the phrase $\%G\; \; e\; :\; \%t$ means that
the expression e has type $\%t$, under the assumption that
the type assignments in $\%G$ are valid.
When $\%G$ is empty, as in $\; e\; :\; \%t$, the type assignment
holds unconditionally.
Occasionally, we write $\%G\; \; e\; \backslash e\; \%t$ instead of
$\%G\; \; e\; :\; \%t$ for readability.
These two expressions have identical meaning.
The premises of a type assignment rule
are given above the line. The type assignment
given below the line states the assignment
that may be made on the basis of these premises.
For example, the first type assignment rule states that,
assuming $\%G\; \; x\; :\; \%s$ (x has type $\%s$) and
$\%G\; \; e\; :\; \%t$ (e has type $\%t$)
then $\%G\; \; \%l\; x\; :\; \%s.\; e\; \backslash e\; \%s\; >\; \%t$, in other words
the abstraction $\%l\; x:\%s.e$ may be validly typed
as $\%s\; >\; \%t$.
Similarly, the second type assignment rule
states that applying a function $e\_1\; :\; \%s\; >\; \%t$
to an expression $e\_2$ of type $\%s$ results
in an (application) expression $e\_1\; e\_2$ of type $\%t$.
We may assume the basic types denoted by $\%r$
to include (integer) subranges, records and variants.
As a consequence, we may employ the subtyping rules
given in section [subtypes] to determine the subtyping
relation between these types.
The (subtyping) refinement rule repeated here
expresses the substitutability property of subtypes,
which allows us to consider an expression
e of type $\%s$, with $\%s\; <=\; \%t$, as being
of type $\%t$.
In slide [9exsubtypes], some examples are given illustrating
the assignment of types to expressions.
Type assignment may to a certain extent be done
automatically, by type inference, as for example in ML,
see [ML90].
However, in general, typing is not decidable
when we include the more powerful type expressions
treated later.
In those cases the programmer is required to
provide sufficient type information to enable the
type checker to determine the types.
Examples
 $S\; =\; \%l\; x:Int.\; x\; +\; 1$
$S\; :\; Int\; >\; Int$
 $twice\; =\; \%l\; f:Int\; >\; Int.\; \%l\; y\; :\; Int\; .\; f\; (\; f\; (\; y\; )\; )$
$twice\; :\; (\; Int\; >\; Int\; )\; >\; Int\; >\; Int$
Application
 $S\; 0\; =\; 1\; \backslash e\; Int$
 $twice\; (\; S\; )\; =\; \%l\; x.\; S\; S\; x\; \backslash e\; Int\; >\; Int$
slide: Subtypes  examples
When we define the successor function S as
$\%l\; x\; :\; Int.\; x\; +\; 1$ then we may type S
straightforwardly as being of type $Int\; >\; Int$.
Similarly, we may type the (higher order) function
twice as being of type $(Int\; >\; Int)\; >\; Int\; >\; Int$.
Note that the first argument to twice must be a function.
Applying twice to a function argument only results
in a function.
When applied to S it results in a function
of type $Int\; >\; Int$ that results in applying S
twice to its (integer) argument.
The subtyping rules (partly imported from section [subtypes])
work as expected.
We may define, for example, a function
$+\; :\; Real\; \backslash *\; Real\; >\; Int$ as a subtype of
$+\; :\; Int\; \backslash *\; Int\; >\; Int$ (according
to the contravariant subtyping rule for functions).
Subtyping in C++
Subtyping is supported in C++ only to
a very limited extent.
Function subtypes are completely absent.
However, class subtypes due to derivation by
inheritance may be employed.
Also, builtin conversions are provided,
some of which are in accordance with the subtyping
requirements,
and some of which, unfortunately,
violate the subtyping requirements.
Builtin conversions exist, for example,
between double and int, in both ways.
However, whereas the conversion from int to double
is safe, the other way around may cause loss of
information by truncation.
The type system sketched in slide [9csubtypes]
is quite easily mapped to a C++ context.
For example, we may mimic the functions S
and twice as given in slide [9exsubtypes]
in C++ as:
int S(int x) { return x+1; }
int twice(int f(int), int y) { return f(f(y)); }
int twice_S(int y) { return twice(S,y); }
slide: Types in C++
Nevertheless, the type system of C++ imposes
some severe restrictions.
For example, functions may not be returned
as a value from functions.
(Although we may provide a workaround, when we employ
the $operator()$ function for objects.)
The absence of function subtyping becomes clear
when, for example, we call the function twice
with the function SD, which is defined as:
int SD(double x) { return x+1; } // twice(SD) rejected
slide: SD example
According to the subtyping rules and in accordance
with the substitutability requirement,
we employ SD whenever we may employ S.
But not so in C++.
We run into similar limitations when we try
to refine an object class descriptions following
the object subtype refinement rules.
class P { P
public:
P() { _self = 0; }
virtual P* self() {
return _self?_self>self():this;
}
virtual void attach(C* p) {
_self = p;
}
private:
P* _self;
};
class C : public P { $C\; <=\; P$
public:
C() : P(this) { }
C* self() { // ANSI/ISO
return _self?_self>self():this;
}
void attach(P* p) { // rejected
p>attach(self());
}
void redirect(C* c) { _self = c; }
private:
C* _self;
};
slide: Subtyping in C++
Suppose we have a parent class P which offers
the member functions self and attach,
as in slide [9ccsub].
The meaning of the function self is that
it dereferences the _self variable if
it is nonzero and delivers this otherwise.
(See section [hush] for an example of its use.)
The function attach may be used to connect an
instance of C to the _self variable.
The class C in its turn inherits from P
and redefines self and attach.
Syntactically, both refinements are allowed,
due to the function subtype refinements rules.
The function self is redefined to deliver
a more tightly specified result,
and the attach function is allowed to take a wider
range of arguments.
In a number of compilers for C++,
both redefinitions are considered illegal.
However, in the ANSI/ISO standard of C++,
redefining a member function to deliver
a subtype (that is, derived class) pointer will be allowed.
Redefining attach, as has been done for C
is probably not a wise thing to do,
since it changes the semantics of attach
as defined for the parent class P.
In effect, it allows us to write
$c>attach(p)$ instead of
$p>attach(c>self())$, for $P\backslash !*\; p$ and $C\backslash !*\; c$.
Nevertheless, from a type theoretical perspective,
there seem to be no grounds for forbidding it.
Intersection types
We define our second version of the typed lambda calculus
($\%l\_\{\; /\backslash \; \}$) as an extension of the first version ($\%l\_\{\; <=\; \}$),
an extension which provides facilities for
(ad hoc) overloading polymorphism.
Our extension consists of adding a type expression
$\backslash bigwedge\; [\; \%t\_1,...,\%t\_n\; ]$ which denotes
a finite conjunction of types.
Such a conjunction of types, that we will
also write as $\%t\_1\; /\backslash \; ...\; /\backslash \; \%t\_n$ is called
an intersection type.
The idea is that an expression e of type
$\backslash bigwedge\; [\; \%t\_1,...,\%t\_n\; ]$ is correctly typed
if $e\; :\; \%t\_i$ for some i in $1..n$.
This is expressed in the type assignment rule given
in slide 9cintersection.
Intersection types  overloading
$\%l\_\{\; /\backslash \; \}$
 $\%t\; ::=\; \%r\; \; \%t\_1\; >\; \%t\_2\; \; \backslash bigwedge\; [\; \%t\_1\; ..\; \%t\_n\; ]$
Type assignment
 \ffrac{$\%G\; \; e\; :\; \%t\_i$ $(i\; \backslash e\; 1..n)$}{
$\%G\; \; e\; :\; \backslash bigwedge\; [\; \%t\_1\; ..\; \%t\_n\; ]$
}
Refinement
 \ffrac{ $\%G\; \; \%s\; <=\; \%t\_i$ $(i\; \backslash e\; 1..n\; )$}{
$\%G\; \; \%s\; <=\; \backslash bigwedge\; [\; \%t\_1\; ..\; \%t\_n\; ]$
}
 $\backslash bigwedge\; [\; \%t\_1\; ..\; \%t\_n\; ]\; <=\; \%t\_i$
 $\%G\; \; \backslash bigwedge\; [\; \%s\; >\; \%t\_1\; ..\; \%s\; >\; \%t\_n\; ]\; <=\; \%s\; >\; \backslash bigwedge\; [\; \%t\_1\; ..\; \%t\_n\; ]$
slide: The intersection type calculus
The subtyping rule for intersection types states
that any subtype of a type occurring in the
intersection type $\backslash bigwedge\; [\; \%t\_1,...,\; \%t\_n\; ]$
is itself a subtype of the intersection type.
In addition we have two subtyping rules without premises,
the first of which says
that the intersection type itself
may be regarded as a subtype of any of its components.
In other words, from a typing perspective
an intersection type is equal (hence may be replaced by)
any of its component types.
Also, we may refine a function, with domain $\%s$, which
has an intersection type $\backslash bigwedge\; [\; \%t\_1,...,\; \%t\_n\; ]$ as its
range into an intersection type consisting of functions
$\%s\; >\; \%t\_i$ for $i\; =\; 1..n$.
Intersection types allow us to express
a limited form of overloading, by enumerating a finite
collection of possible types.
Since the collection of types comprising an
intersection type is finite, we do not need a higher
order calculus here, although we might have used type
abstraction to characterize intersection types.
Examples
 $+\; :\; \backslash bigwedge\; [\; Int\; \backslash *\; Int\; >\; Int,\; Real\; \backslash *\; Real\; >\; Real]$
 $Int\; >\; Int\; <=\; \backslash bigwedge\; [\; Int\; >\; Int,\; Real\; >\; Real\; ]$
 $Msg\; >\; Obj1\; /\backslash \; Msg\; >\; Obj2\; <=\; Msg\; >\; \backslash bigwedge\; [\; Obj1,\; Obj2\; ]$
slide: Intersection types  examples
A typical example of an intersection type is presented
by the addition operator, overloaded for integers and reals,
which we may define as
$+\; :\; \backslash bigwedge\; [\; Int\; \backslash *\; Int\; >\; Int,\; Real\; \backslash *\; Real\; >\; Real\; ]$
According to our refinement rule, we may specialize
an intersection type into any of its components.
For example, when we have an intersection type defining
a mapping for integers and a mapping for reals, we may choose
the one that fits our purposes best.
This example illustrates that intersection types may
be an important tool for realizing optimizations
that depend upon (dynamic) typing.
Similarly, we may refine a generic function working on
objects into a collection of (specialized) functions
by dividing out the range type.
See slide [9exintersection].
The resulting intersection type itself may subsequently
be specialized into one of the component
functions.
In [CGL93], a similar kind of type is used
to model the overloading of methods in objects,
that may but need not necessarily be related by inheritance.
The idea is to regard message passing to objects
as calling a polymorphic function
that dispatches on its first argument.
When the type of the first argument is compatible
with multiple functions (which may happen for
methods that are refined in the inheritance hierarchy) the most
specific function component is chosen,
that is the method with the minimal object type.
A similar idea is encountered in CLOS,
which allows for the definition of multimethods
for which dynamic dispatching takes place
for all arguments.
(A problem that occurs in modeling methods as overloaded
functions is that the subtyping relation between
methods no longer holds, due to the domain contravariance requirement.
See [CGL93] for a possible solution.)
Overloading in C++
Although C++ does not provide
support for subtyping, it does provide
extensive support for function overloading.
Given a collection of functions
(overloading a particular function name)
C++ employs a system of matches
to select the function that is most
appropriate for a particular call.
Overloaded function selection rules
C++
 [1] no or unavoidable conversions
 $array>pointer$, $T\; >\; const\; T$
 [2] integral promotion
 $char>int$, $short>int$, $float>double$
 [3] standard conversions
 $int>double$, $double>int$, $derived*\; >\; base*$
 [4] userdefined conversions
 constructors and operators
 [5] ellipsis in function declaration
 ...
Multiple arguments  intersect rule
 better match for at least one argument
and at least as good a match for every other
argument
slide: Overloading in C++
Matches may involve builtin or userdefined conversions.
The general rule underlying the application of
conversions is that {\em conversions that are considered
less errorprone and surprising are to be preferred
over the others}.
This rule is reflected in the ordering of the
C++ overloading selection rules depicted
in slide [9ccover].
According to the rules, the absence of conversions
is to be preferred.
For compatibility, with C, array to pointer
conversions are applied automatically,
and also T to $const\; T$ conversions
are considered as unproblematic.
Next, we have the integral promotion rules,
allowing for the conversion of char to int
and short to int, for example.
These conversions are also directly inherited
from C, and are safe in the sense that no information
loss occurs.
Further, we have the standard conversions
such as int to double and $derived*$
to $base*$,
userdefined conversions
(as determined by the definition of oneargument
constructors and conversion operators),
and the ... ellipsis notation, which allows us
to avoid
typechecking in an arbitrary manner.
For selecting the proper function from a collection
of overloaded functions with multiple arguments,
the socalled intersect rule is used,
which states that the function is selected
with a better match for at least one argument
and at least as good a match for every other
argument.
In the case that no winner can be found
because there are multiple candidate functions
with an equally good match,
the compiler issues an error, as in the example
below:
void f(int, double);
void f(double, int);
f(1,2.0); // f(int, double);
f(2.0,1); // f(double,int);
f(1,1); // error: ambiguous
slide: example
The reason that C++ employs a system of matches
based on declarations and actual parameters
of functions is that
the graph of builtin conversions
(as inherited from C)
contains cycles.
For example, implicit conversions exist
from int to double and
double to int
(although in the latter case the C++
compiler gives a warning).
Theoretically, however, the selection of
the best function according to the subtype
relation would be preferable.
However, the notion of best is not unproblematic
in itself.
For example, consider the definition of
the overloaded function f and the classes
P and C in slide [9ccbest].
class P;
class C;
void f(P* p) { cout << "f(P*)"; } // (1)
void f(C* c) { cout << "f(C*)"; } // (2)
class P {
public:
virtual void f() { cout << "P::f"; }// (3)
};
class C : public P {
public:
virtual void f() { cout << "C::f"; } // (4)
};
slide: Static versus dynamic selection
What must be considered the best function f,
given a choice between (1), (2), (3) and (4)?
P* p = new P; // static and dynamic P*
C* c = new C; // static and dynamic C*
P* pc = new C; // static P*, dynamic C*
f(p); // f(P*)
f(c); // f(C*)
f(pc); // f(P*)
p>f(); // P::f
c>f(); // C::f
pc>f(); // C::f
In the example given above,
we see that for the functions f
(corresponding to (1) and (2)) the choice
is determined by the static type of the argument,
whereas for the member functions f
(corresponding to (3) and (4))
the choice is determined by the dynamic type.
We have a dilemma.
When we base the choice of functions on
the dynamic type of the argument,
the function subtype refinement rule is violated.
On the other hand, adhering to
the domain contravariance property
seems to lead to ignoring
the potentially useful information captured
by the dynamic type of the argument.
Bounded polymorphism
Our next extension, which we call $F\_\{\; <=\; \}$, involves
(bounded) universal quantification.
For technical reasons we need to introduce a
primitive type Top, which may be considered as
the supertype of all types (including itself).
Also we need type abstraction variables, that we will
write as $\%a$ and $\%b$.
Our notation for a universally quantified (bounded) type
is $\backslash A\; \%a\; <=\; \%s\; .\; \%t$, which denotes the type $\%t$
with the type variable $\%a$ replaced by any subtype $\%s\text{'}$ of $\%s$.
In a number of cases, we will simply write $\backslash A\; \%a.\; \%t$,
which must be read as $\backslash A\; \%a\; <=\; Top.\; \%t$.
Recall that any type is a subtype of Top.
Observe that, in contrast to $\%l\_\{\; <=\; \}$ and $\%l\_\{\; /\backslash \; \}$,
the calculus $F\_\{\; <=\; \}$ is second order (due to the quantification
over types).
In addition to the (value) expressions found in the two
previous calculi, $F\_\{\; <=\; \}$ introduces a type abstraction
expression of the form $\%L\; \%a\; <=\; \%t.e$ and a type instantiation
expression of the form $e[\%t]$.
The type abstraction expression $\%L\; \%a\; <=\; \%t.e$
is used in a similar way as the function abstraction expression,
although the abstraction involves types and not values.
Similar to the corresponding type expression,
we write $\%L\; \%a.e$ as an abbreviation for $\%L\; \%a\; <=\; Top.e$.
The (complementary) type instantiation statement is written
as $e[\%t]$, which denotes the expression e in which
the type identifier $\%t$ is substituted for the type variable
bound by the first type abstractor.
Bounded polymorphism  abstraction
$F\_\{\; <=\; \}$
 $\%t\; ::=\; Top\; \; \%a\; \; \%r\; \; \%t\_1\; >\; \%t\_2\; \; \backslash A\; \%a\; <=\; \%t\_1.\; \%t\_2$
 $e\; ::=\; x\; \; \%l\; x:\%t.e\; \; e\_1\; e\_2\; \; \%L\; \%a\; <=\; \%t.e\; \; e\; [\; \%t\; ]$
Type assignment
 \ffrac{$\%G,\; \%a\; <=\; \%s\; \; e\; :\; \%t$ }{
$\%G\; \; \%L\; \%a\; <=\; \%s.\; e\; \backslash e\; \backslash A\; \%a\; <=\; \%s\; .\; \%t$
}
 \ffrac{$\%G,\; e\; :\; \backslash A\; \%a\; <=\; \%s\; .\; \%t$ \hspace{1cm} $\%G\; \; \%s\text{'}\; <=\; \%s$ }{
$\%G\; \; e\; [\; \%s\text{'}\; ]\; \backslash e\; \%t\; [\; \%a\; :=\; \%s\text{'}\; ]$
}
Refinement
 \ffrac{ $\%G\; \; \%s\; <=\; \%s\text{'}$ \hspace{1cm} $\%G\; \; \%t\text{'}\; <=\; \%t$}{
$\%G\; \; \backslash A\; \%a\; <=\; \%s\text{'}.\%t\text{'}\; <=\; \backslash A\; \%a\; <=\; \%s.\%t$
}
slide: The bounded type calculus
The type assignment rule for type abstraction states
that, when we may type an expression e as being of
type $\%t$ (under the assumption that $\%a\; <=\; \%s$),
then we may type $\%L\; \%a\; <=\; \%s.e$ as being of type $\backslash A\; \%a\; <=\; \%s.\%t$.
The type assignment rule for type instantiation
characterizes the relation between type instantiation
and substitution (which is notationally very similar).
When we have an expression e of type $\backslash A\; \%a\; <=\; \%s.\%t$
and we have that $\%s\text{'}\; <=\; \%s$, then $e[\%s\text{'}]$ is of type
$\%t\; [\; \%a\; :=\; \%s\text{'}\; ]$, which is $\%t$ with $\%s\text{'}$ substituted for
$\%a$.
See slide [9cbounded].
The refinement rule for bounded types states
the subtyping relation between two bounded types.
We have that $\backslash A\; \%a\; <=\; \%s\text{'}\; .\; \%t\text{'}$ is
a subtype of $\backslash A\; \%a\; <=\; \%s.\%t$ whenever
$\%s\; <=\; \%s\text{'}$ and $\%t\text{'}\; <=\; \%t$.
Notice that the relation is contravariant with respect
to the types bounding the abstraction, similar
as for the domains of function subtypes in
the function subtyping rule.
In contrast to the polymorphism due to object type
extensions and overloading, bounded polymorphism
(employing type quantifiers) is an example
of what we have called parametric polymorphism.
In effect, this means that we must explicitly give a type
parameter to instantiate an object or function of
a bounded (parametric) type, similar to when we use
a template in C++.
The examples given in
slide [9exparameters]
illustrate how we may define and subsequently
type parametric functions.
In these examples, we employ the convention
that in the absence of a bounding type we assume Top
as an upper limit.
The examples are taken from [CW85].
Examples
 $id\; =\; \%L\; \%a.\; \%l\; x:\%a.x$
$id\; :\; \backslash A\; \%a.\; \%a\; >\; \%a$
 $twice1\; =\; \%L\; \%a.\%l\; f:\; \%L\; \%b.\; \%b\; >\; \%b.\; \%l\; x:\%a.\; f[\%a](f[\%a](x))$
$twice1\; :\; \backslash A\; \%a.\; \backslash A\; \%b.\; (\%b\; >\; \%b)\; >\; \%a\; >\; \%b$
 $twice2\; =\; \%L\; \%a.\%l\; f:\; \%a\; >\; \%a.\; \%l\; x:\%a.\; f(f(x))$
$twice2\; :\; \backslash A\; \%a.\; (\%a\; >\; \%a)\; >\; \%a\; >\; \%a$
Applications
 $id\; [\; Int\; ]\; (\; 3\; )\; =\; 3$
 $twice1\; [\; Int\; ]\; (\; id\; )(\; 3\; )\; =\; 3$
 $twice1\; [\; Int\; ]\; (\; S\; )\; =\; illegal$
 $twice2\; [\; Int\; ]\; (\; S\; )(\; 3\; )\; =\; 5$
slide: Parametrized types  examples
The (generic) identity function id
is defined as $\%L\; \%a.\%l\; x:\%a.x$, which states
that when we supply a particular type, say Int,
then we obtain the function $\%l\; x:Int.\; x$.
Since the actual type used to instantiate id is not important,
we may type id as being of type $\backslash A\; \%a.\%a\; >\; \%a$.
In a similar way, we may define and type the two
(generic) variants of the function twice.
Notice the difference between the two definitions of twice.
The first variant requires the function argument itself
to be of a generic type, and fails (is incorrectly typed)
for the successor function S which is (non generic)
of type $Int\; >\; Int$.
In contrast, the second variant accepts S, and we may
rely on the automatic conversion
of $id\; :\; \backslash A\; \%a.\; \%a\; >\; \%a$ to $id\; [\; Int\; ]\; :\; Int\; >\; Int$
(based on the second type assignment rule) to accept id
as well.
The interplay between parametric and inclusion
polymorphism is illustrated in the examples presented
in slide [9exquantification].
Recall that inclusion polymorphism is based
on the subtyping relation between records
(which states that refinement of a record type involves the addition
of components and/or refinement of components that
already belong to the super type).
Bounded quantification
 $g\; =\; \%L\; \%a\; <=\; \{\; one\; :\; Int\; \}.\; \%l\; x:\; \%a.\; (x.one)$
$g\; :\; \backslash A\; \%a\; <=\; \{\; one\; :\; int\; \}.\; \%a\; >\; Int$
 $g\text{'}\; =\; \%L\; \%b\; .\; \%L\; \%a\; <=\; \{\; one\; :\; \%b\; \}.\; \%l\; x:\; \%a.\; (x.one)$
$g\text{'}\; :\; \backslash A\; \%b\; .\; \backslash A\; \%a\; <=\; \{\; one\; :\; \%b\; \}.\; \%a\; >\; \%b$
 $move\; =\; \%L\; \%a\; <=\; Point.\; \%l\; p:\%a.\; \%l\; d\; :\; Int\; .(p.x\; :=\; p.x\; +\; d);\; p$
$move\; :\; \backslash A\; \%a\; <=\; Point.\; \%a\; >\; Int\; >\; \%a$
Application
 $g\text{'}\; [\; Int\; ][\; \{\; one:Int,\; two\; :\; Bool\; \}](\{\; one\; =\; 3,\; two\; =\; true\; \})\; =\; 3$
 $move\; [\{\; x\; :\; Int,\; y\; :\; Int\; \}](\; \{\; x\; =\; 0,\; y\; =\; 0\; \}\; )(1)\; =\; \{\; x\; =\; 1,\; y\; =\; 0\; \}$
slide: Bounded quantification  examples
The first example defines a function g that works on a record
with at least one component one and delivers as a result
the value of the component one of the argument record.
The function $g\text{'}$ is a generalized version of g
that abstracts from the particular type of the one
component.
Notice that both g and $g\text{'}$ may be applied to any record
that conforms to the requirement stated in the bound,
such as the record $\{\; one\; =\; 3,\; two\; =\; true\; \}$.
As another example of employing bounds to impose requirements,
look at the function move that is defined for subtypes of Point
(which we assume to be a record containing x and y coordinates).
It expects a record (that is similar to or extends Point)
and an (integer) distance, and as a result delivers the modified
record.
Discussion
Parametric polymorphism is an important means to incorporate
subtyping in a coherent fashion.
Apart from [Pierce93], from which we have taken most of the
material presented here, we may mention
[PA93] as a reference for further study.
In [Pierce93] a calculus $F\_\{\; /\backslash \; \}$ is also introduced
in which intersection polymorphism is expressed by
means of an explicit type variable.
The resulting type may be written as $\backslash A\; \%a\; \backslash e\; \{\; ...\; \}$,
where $\{\; ...\; \}$ denotes a finite collection of types.
As already mentioned, intersection types may also be used
to model inclusion polymorphism
(see Castagna {\it et al.}, 1993).\index{Castagna {\it et al.} (1993)}
It is an interesting research issue to explore
the relation between parametric polymorphism and
inclusion polymorphism further along this line.
However, we will not pursue this line here.
Instead, in the next section we will look
at another application
of parametric polymorphism, namely existential types
that allow us to abstract from hidden component types.
This treatment is based on [CW85].
In the last section of this chapter, we will look in
more detail at the role of selfreference
in defining (recursive) object types,
following [CoHC90].
We will conclude this chapter with some
observations concerning the relevance of
such type theories for actual programming languages.
In particular, we will show that Eiffel is
not type consistent.
Type abstraction in C++
Type abstraction in C++ may occur in various
guises.
One important means of type abstraction
is to employ
what we have called polymorphic base class hierarchies.
For example, the function move,
which was somewhat loosely characterized in
slide [9exquantification],
may be defined in C++ as follows:
Point* move(Point* p, int d); // require int Point::x
Point* move(Point* p, int d) { p.x += d; return p; }
slide: example move
In effect, the function move accepts a pointer
to an instance of Point, or
any class derived from Point, satisfying the requirement
that it has a public integer data member x.
Similar restrictions generally hold when
instantiating a template class,
but in contrast to base class subtyping requirements,
these restrictions will only be verified at link time.
template< class T > // requires T::value()
class P {
public:
P(T& r) : t(r) {}
int operator==( P& p) {
return t.value() == p.t.value();
}
private:
T& t;
};
slide: Type abstraction in C++
Consider the template class definition given
in slide [9ccabs].
Evidently, for the comparison function to
operate properly, each instantiation type
substituted for the type parameter T
must satisfy the requirement that it has a public member function
value.
template< class T >
class A { A<T>
public:
virtual T value() = 0;
};
class Int : public A<int> { // Int $<=$ A<int>
public:
Int(int n = 0) : _n(n) {}
int value() { return _n; }
private:
int _n;
};
slide: Type instantiation
Such a requirement may also be expressed by defining
an abstract class A defining a pure
virtual member function value.
See slide [9ccabs2].
The restrictions on instantiating P
may then be stated informally as
the requirement that each instantiation type
T must be a subtype of $A$ for arbitrary type X.
The class Int is an example of a type complying with
the implicit requirements imposed by the definition of P.
An example of using P is given below
Int i1, i2;
P<Int> p1(i1), p2(i2);
if ( p1 == p2 ) cout << "OK" << endl; OK
slide: Example P
Note, however, that
the derivation of A<int> is by no means
necessary or in any way enforced by C++.
objectoriented programming
Existential types  hiding
Existential types were introduced in [CW85] to model
aspects of data abstraction and hiding.
The language introduced in [CW85] is essentially
a variant of the typed lambda calculi we have looked
at previously.
Our new calculus, that we call $F\_\{\; \backslash E\; \}$, is an
extension of $F\_\{\; <=\; \}$ with type expressions of the form
$\backslash E\; \%a\; <=\; \%s.\; \%t$ (to denote existential types)
and expressions of the form $pack[\; \%a\; =\; \%s\; in\; \%t\; ]$
(to denote values with hidden types).
Intuitively, the meaning of the expression $pack[\; \%a\; =\; \%s\; in\; \%t\; ]$
is that we represent the abstract type $\%a$ occurring
in the type expression $\%t$ by the actual type $\%s$
(in order to realize the value e).
Following the type assignment rule, we may actually provide
an instance of a subtype of the bounding type
as the realization of a hidden type.
See slide [9existential].
Existential types  hiding
$F\_\{\; \backslash E\; \}$
 $\%t\; ::=\; ...\; \; \backslash E\; \%a\; <=\; \%t\_1.\; \%t\_2$
 $e\; ::=\; ...\; \; pack[\; \%a\; =\; \%s\; in\; \%t\; ].\; e$
Type assignment
 \ffrac{$\%G\; \; \%s\text{'}\; <=\; \%s$ \hspace{1cm} $\%G\; \; e\; :\; \%t$}{
$pack[\; \%a\; =\; \%s\text{'}\; in\; \%t\; ].e\; \backslash e\; \backslash E\; \%a\; <=\; \%s.\; \%t$
}
Refinement
 \ffrac{$\%G\; \; \%s\; <=\; \%s\text{'}$ \hspace{1cm} $\%G\; \; \%t\text{'}\; <=\; \%t$}{
$\%G\; \; \backslash E\; \%a\; <=\; \%s\text{'}\; .\; \%t\text{'}\; <=\; \backslash E\; \%a\; <=\; \%s.\; \%t$
}
slide: The existential type calculus
The subtyping refinement rule is similar to the refinement
rule for universally quantified types.
Notice also here the contravariance relation
between the bounding types.
More interesting is what bounding types allow
us to express.
(As before, we will write $\backslash E\; \%a\; .\; \%t$ to denote
$\backslash E\; \%a\; <=\; Top.\; \%t$.)
First, existential types allow us to
indicate that the realization of a particular type exists,
even if we do not indicate how.
The declaration $e\; :\; \backslash E\; \%a\; .\; \%t$ tells us that
there must be some type $\%s$ such that e of type $\%t$
can be realized.
Apart from claiming that a particular
type exists, we may also provide information
concerning its structure, while leaving its actual type
undetermined.
Structure  indeterminacy
 $Top\; =\; \backslash E\; \%a.\%a$ \zline{the biggest type}
 $AnyPair\; =\; \backslash E\; \%a\; \backslash E\; \%b.\%a\; \backslash *\; \%b$ \zline{any pair}
 $(3,4):\E %a.%a$\{\backslash em\; \; does\; not\; provide\; sufficient\; structure!\}$
 $(3,4):\E %a.%a \* %a
Information hiding
 $\backslash E\; \%a.\%a\; \backslash *\; (\; \%a>Int\; )$ \zline{object, operation}
 $x\; :\; \backslash E\; \%a.\; \%a\; \backslash *\; (\; \%a>Int\; )$ \zline{ \( \leadsto \) $snd\; (\; x\; )(\; fst(\; x\; ))$ }
slide: Existential types  examples
For example, the type $\backslash E\; \%a.\%a$ (which may clearly be realized
by any type) carries no information whatsoever, hence it may
be considered to be equal
to the type Top.
More information, for example, is provided by the type
$\backslash E\; \%a\; \backslash E\; \%b.\; \%a\; \backslash *\; \%b$ which defines the product type
consisting of two (possibly distinct) types.
(A product may be regarded as an unlabeled record.)
The type $\backslash E\; \%a.\; \%a\; \backslash *\; \%a$ gives even more information
concerning the structure of a product type,
namely that the two components are of the same type.
Hence, for the actual product $(3,4)$ the latter is the best choice.
See slide [9exexistential].
Existential types may be used to impose structure on the
contents of a value,
while hiding its actual representation.
For example, when we have a variable x
of which we know that it has type $\backslash E\; \%a.\; \%a\; \backslash *\; (\; \%a\; >\; Int\; )$
then we may use the second component of x
to produce an integer value from its first component,
by $snd(x)(\; fst(x)\; )$, where fst extracts the first
and snd the second component of a product.
Clearly, we do not need to know the actual
representation type for $\%a$.
A similar idea may be employed for (labeled) records.
For example, when we have a record x of type
$\backslash E\; \%a.\{\; val\; :\; \%a,\; op\; :\; \%a\; >\; Int\; \}$ then we may
use the expression $x.op(x.val)$ to apply the
operation op to the value val.
Again, no knowledge of the type of val is required in this case.
However, to be able to use an element of an existential type
we must provide an actual representation type,
by instantiating the type parameter in a pack
statement.
Abstract data types  packages
 $x:\backslash E\; \%a.\{\; val\; :\; \%a,\; op\; :\; \%a\; >\; Int\; \}$
 $x\; =\; pack[\%a\; =\; Int\; in\; \{\; val:\%a,\; op:\%a\; >\; Int\; \}\; ]((3,S))$
 $x.op(x.val)\; =\; 4$
Encapsulation
$pack\; [\; representation\; in\; interface\; ](\; contents\; )$
 interface  type $\backslash E\; \%a.\; \{\; val\; :\; \%a,\; op\; :\; \%a\; >\; Int\; \}$
 representation  $\%a\; =\; Int$ \zline{(hidden data type)}
 contents  $(3,S)$
slide: Packages  examples
The pack statement may be regarded as an encapsulation
construct, allowing us to protect the inner parts
of an abstract data type.
When we look more closely at the pack statement,
we can see three components.
First, we have an interface specification corresponding
to the existential type associated with the pack expression.
Secondly, we need to provide an actual representation of
the hidden type, Int in the example above.
And finally, we need to provide the actual
contents of the structure.
See slide [9ADT].
In combination with the notion of objects as records,
existential types provide us with a model of abstract data types.
Real objects, however, require a notion of selfreference
that we have not captured yet.
In the next section we will conclude our exploration
of type theories by discussing the $F\_\{\%m\}$ calculus
that supports recursive (object) types and inheritance.
Hiding in C++
Naturally, the classical way of data hiding in C++
is to employ private or protected access protection.
Nevertheless, an equally important means
is to employ an abstract interface class
in combination with forwarding.
class event { event
protected:
event(event* x) : ev(x) {}
public:
int type() { return ev>type(); }
void* rawevent() { return ev; }
private:
event* ev;
};
class xevent : public event { X
public:
int type() { return X>type(); }
private:
struct XEvent* X;
};
slide: Hiding in C++
For example, as depicted in
slide [9cchide],
we may offer the user a class event
which records information concerning
events occurring in a window environment,
while hiding completely the underlying
implementation.
The actual xevent class realizing the type
event may itself need access to other
structures,
as for example those provided by the X window
environment.
Yet, the xevent class itself may remain entirely
hidden from the user, since events
are not something created directly
(note the protected constructor)
but only indirectly,
generally by the system in response
to some action by the user.
objectoriented programming
Selfreference
Recursive types are compound types in which the type
itself occurs as the type of one of its components.
Selfreference in objects clearly involves
recursive types since the expression self
denotes the object itself, and hence has the type
of the object.
In $F\_\{\%m\}$, our extension of $F\_\{<=\}$ taken from [CoHC90],
recursive types are written as $\%m\; \%a.\; \%t[\%a]$,
where $\%m$ is the recursion abstractor
and $\%a$ a type variable.
The dependence of $\%t$ on $\%a$ is made explicit
by writing $\%t[\%a]$.
We will use the type expressions $\%m\; \%a.\%t[\%a]$ to
type object specifications of the form
$\%l(self).\{\; a\_1\; =\; e\_1,\; ...,\; a\_n\; =\; e\_n\; \}$
as indicated by the type assignment rule below.
Object specifications may be regarded as class descriptions
in C++ or Eiffel.
Selfreference  recursive types
$F\_\{\; \%m\; \}$
 $\%t\; ::=\; ...\; \; \%m\; \%a.\; \%t\; [\%a]$
 $e\; ::=\; ...\; \; \%l(\; self\; ).\{\; a1\; =\; e\_1,\; ...,\; a\_n\; =\; e\_n\; \}$
Type assignment
 \ffrac{ $\%G\; \; e\_i\; :\; \%t\_i$ \hspace{1cm} $(i\; =\; 1..n)$ }{
$\%G\; \; \%l(\; self\; ).\{\; a1\; =\; \%t\_1,..,\; a\_n\; =\; \%t\_n\; \}\; \backslash e\; \%m\%a.\{\; a1:\%t\_1,..,\; a\_n\; :\; \%t\_n\; \}[\%a]$
}
Refinement
 \ffrac{ $\%G,\; \%a\; <=\; \%b\; \; \%s\; <=\; \%t$ }{
$\%G\; \; \%m\; \%a.\%s[\%a]\; <=\; \%m\; \%b.\%t\; [\%b]$
}
slide: A calculus for recursive types
The subtype refinement rule for recursive types states
that $\%m\; \%a.\; \%s\; [\%a]\; <=\; \%m\; \%b\; .\; \%t[\%b]$ if we can prove that
$\%s\; <=\; \%t$ assuming that $\%a\; <=\; \%b$.
An object specification $\%l(self).\{\; ...\; \}$ is a function
with the type of the actual object as its domain and (naturally)
also as its range.
For convenience we will write an object specification
as $\%l(self).F$, where F denotes the object record,
and the type of an object specification as $\%m\; \%a.F[\%a]$,
where $F[\%a]$ denotes the (abstract) type of the record F.
To obtain from an object specification $\%l(self).F$
the object that it specifies,
we need to find some type $\%s$ that types the record
specification F as being of type $\%s$ precisely
when we assign the expression self in F
the type $\%s$.
Technically, this means that the object of type $\%s$
is a fixed point of the object specification
$\%l(self).F(self)$ which is of type $\%s\; >\; \%s$.
We write this as $\backslash Y(\; \%l(self).F(self)\; )\; :\; \%s$,
which says that the object corresponding to the object
specification is of type $\%s$.
See slide [9recursion].
Object semantics  fixed point $ %s = F[%s] $
 $\backslash Y\; (\; \%l(\; self\; ).F(\; self\; )\; )\; :\; \%s$
Unrolling  unraveling a type
 $\%m\; \%a.F[\%a]\; =\; F[\; \%m\; \%a.F[\%a]\; ]$
Example
$T\; =$\%m \%a.{ a:int, c:\%a, b:\%a>\%a }
$T\_1\; =\; \{\; a:int,\; c:T,\; b:T>T,\; d:bool\; \}$
$T\_2\; =$\%m \%a.{ a:int, c:\%a, b:T>T, d:bool }
$T\_3\; =$\%m \%a.{ a:int, c:\%a, b:\%a>\%a, d:bool }
$T\_1,\; T\_2\; <=\; T$, $T\_3\; \backslash not<=\; T$ \zline{(contravariance)}
slide: Recursive types  examples
Finding the fixed point of a specification involves
technically a procedure known as unrolling,
which allows us to rewrite the type $\%m\; \%a.F[\%a]$
as $F[\%m\; \%a.F[\%a]\; ]$.
Notice that unrolling is valid, precisely because of
the fixed point property.
Namely, the object type $\%s$ is equal to $\%m\; \%a.F[\%a]$,
due to the type assignment rule, and we have that
$\%s\; =\; F[\%s]$.
See slide [9exrecursive].
Unrolling allows us to reason on the level of types
and to determine the subtyping relation between recursive
subtypes.
Consider, for example, the type declarations T and $T\_i$ $(i\; =\; 1..3)$
above.
Based on the refinement rules for object records, functions
and recursive types, we may establish that $T\_1\; <=\; T$,
$T\_2\; <=\; T$ but $T\_3\; \backslash not<=\; T$.
To see that $T\_1\; <=\; T$, it suffices to substitute T
for $\%a$ in F, where $F\; =\; \{\; a:Int,\; c:\%a,\; b:\%a>\%a\; \}$.
Since $F[T]=\; \{\; a:Int,\; c:T,\; b:T>T\; \}$
we immediately see that $T\_1$ only extends T with the field $d:Bool$,
hence $T\_1\; <=\; T$.
A similar line of reasoning is involved to determine that
$T\_2\; <=\; T$, only we need to unroll $T\_2$ as well.
We must then establish that $c:T\_2\; <=\; c:T$, which follows
from an application of the refinement rule.
To show that $T\_3\; \backslash not<=\; T$, let
$G[\%b]\; =\; \{\; a:Int,\; c:\%b,\; b:\%b>\%b,\; d:Bool\; \}$
and $T\_3\; =\; \%m\; \%b.G[\%b]$.
Then, by unrolling,
$T\_3\; =\; G[T\_3]\; =\; \{\; a:Int,\; c:T\_3,\; b:T\_3\; >\; T\_3,\; d:Bool\; \}$.
Now, suppose that $T\_3\; <=\; T$, then $G[T\_3]\; <=\; F[T\_3]$
and consequently $b:T\_3\; >\; T\_3$ must refine $b:T\; >\; T$.
But from the latter requirement it follows that $T\_3\; <=\; T$
and that $T\; <=\; T\_3$ (by the contravariance rule for function
subtyping).
However, this leads to a contradiction since T is clearly
not equal to $T\_3$ because $T\_3$ contains a field
$d:Bool$ that does not occur in T.
Although analyses of this kind are to some extent
satisfactory in themselves, the reader may wonder
where this all leads to.
In the following we will apply these techniques
to show the necessity of dynamic binding
and to illustrate that inheritance may easily violate
the subtyping requirements.
Inheritance
In section [flavors] we have characterized inheritance
as an incremental modification mechanism,
which involves a dynamic interpretation of the expression self.
In the recursive type calculus $F\_\{\%m\}$ we may characterize this
more precisely, by regarding a derived object specification
C as the result of applying the modifier M
to the object specification P.
We employ
the notation $C\; =\; \%l(self).P(self)\; \backslash with\; \{\; a\_1\text{'}\; =\; e\_1\text{'},...,a\_k\text{'}\; =\; e\_k\text{'}\; \}$
to characterize derivation by inheritance,
and we assume the modifier M corresponding with
$\{\; a\_1\text{'}\; =\; e\_1\text{'},\; ...,\; a\_k\text{'}\; =\; e\_k\text{'}\; \}$ to extend the record
associated with P in the usual sense.
See slide [9selfinheritance].
Inheritance  C = P + M
 $P\; =\; \%l(\; self\; ).\{\; a1\; =\; e1,...,a\_n\; =\; e\_n\; \}$
 $C\; =\; \%l(\; self\; ).P(\; self\; )$ $\backslash with$ \ifsli{\n}{} $\{\; a1\text{'}\; =\; e1\text{'},...,a\_k\text{'}\; =\; e\_k\text{'}\; \}$
Semantics  $\Y(C) = \Y(%l( self ).M( self )(P( self )))$
 $P\; :\; \%s\; >\; \%s$ $=>$ $\backslash Y(P):\%s$
 $C\; =\; \%l(s).M(s)(P(s))\; :\; \%t\; >\; \%t$ $=>$ $\backslash Y(C):\%t$
slide: Inheritance semantics  selfreference
The meaning of an object specification C is again a fixed
point $\backslash Y(C)$, that is
$\backslash Y(\%l(self).M(self)(P(self)))$.
Now when we assume that the object specification is of type
$\%t\; >\; \%t$ (and hence $\backslash Y(P)$ of type $\%t$),
and that C is of type $\%s\; >\; \%s$ (and hence $\backslash Y(C)$ of type
$\%s$), then we must require that $\%s\; <=\; \%t$ to obtain
a properly typed derivation.
We write $C\; <=\; P$ whenever $\%s\; <=\; \%t$.
A first question that arises when we characterize inheritance
as incremental modification is how we obtain the meaning
of the composition of two object specifications.
Object inheritance  dynamic binding
$P\; =\; \%l(\; self\; ).\{\; i\; =\; 5,\; id\; =\; self\; \}$
$C\; =\; \%l(\; self\; ).P(\; self\; )\; \backslash with\; \{\; b\; =\; true\; \}$
$\backslash Y(P):\%t$ where $\%t\; =\; \%m\; \%a.\{\; i:int,\; id:\%a\; \}$ and $P:\%t>\%t$
Simple typing  $\backslash Y(C):\%s\; =\; \{\; i:int,\; id:\%t,\; b:bool\; \}$
Delayed  $\backslash Y(C):\%s\text{'}\; =\; \%m\; \%a.\{\; i:int,\; id:\%a,\; b:bool\; \}$
We have $\%s\text{'}\; <=\; \%s$ \zline{(more information)}
slide: Object inheritance  dynamic binding
Let (parent) P and (child) C be defined as above.
Now, if we know that the type of $\backslash Y(P)$ is $\%t$
then we may simply characterize $\backslash Y(C)$ as being
of type $\%s\; =\; \{\; i:Bool,\; id:\%t,\; b:Bool\; \}$.
However, when we delay the typing of the P
component (by first composing the record specifications
before abstracting from self)
then we may obtain $\%s\text{'}\; =\; \%m\; \%a.\{\; i:Int,\; id:\%a,\; b:Bool\; \}$
as the type of $\backslash Y(C)$.
By employing the refinement rule and unrolling we can
show that $\%s\text{'}\; <=\; \%s$.
Hence, delayed typing clearly provides more information
and must be considered as the best choice.
Note, however, that both $\%s\text{'}\; <=\; \%t$ and $\%s\; <=\; \%t$ hold.
See slide [9selfdynamic].
A second, important question that emerges
with respect to inheritance is how
selfreference affects the subtyping relation between
object specifications related by inheritance.
Consider the object specifications P and C given
in slide [9selfcontravariance].
In the (derived) specification C, the method eq
is redefined to include an equality test for the b
component.
However, when we determine the object types corresponding
to the specifications P and C
we observe that $C\; \backslash not<=\; P$.
Contravariance
 $P\; =\; \%l(\; self\; ).\{\; i\; =\; 5,\; eq\; =\; \%l(o).(o.i\; =\; self.i)\; \}$
$C\; =$\%l( self ).P( self ) \with { b = true,
$eq\; =$\%l(o).(o.i = self.i and
$o.b\; =\; self.b)$
$\}$
$\backslash Y(P)\; :\; \%t$ where
$\%t\; =\; \%m\; \%a.\{\; i:int,\; eq:\%a\; >\; bool\; \}$
$\backslash Y(C):\%s$ where
$\%s\; =\; \%m\; \%a.\{\; i:int,\; id:\%a\; >\; bool,\; b:\; bool\; \}$
However $\%s\; \backslash not<=\; \%t$ \zline{(subtyping error)}
slide: Object inheritance  contravariance
The reasoning is as follows.
For $\backslash Y(P)\; :\; \%t$ and $\backslash Y(C)\; :\; \%s$, we have
that $\%s\; =\; \%m\; \%b.\{\; i:Int,\; id:\%b\; >\; Bool,\; b:Bool\; \}$
which is (by unrolling) equal to $\{\; i:Int,\; id:\; \%s>\; Bool,\; b:Bool\; \}$.
Now suppose that $\%s\; <=\; \%t$, then we have that
$\{\; i:Int,\; eq:\%s>Bool,\; b:Bool\; \}$ is a subtype of
$\{\; i:Int,\; eq:\%t>Bool\; \}$
which is true when $eq:\%s>Bool\; <=\; eq:\%t>Bool$
and hence (by contravariance) when $\%s\; <=\; \%t$.
Clearly, this is impossible. Hence $\%s\; \backslash not<=\; \%t$.
We have a problem here,
since the fact that $C\; \backslash not<=\; P$ means that the type checker
will not be able to accept the derivation of C from P,
although C is clearly dependent on P.
The solution to our problem
lies in making the type dependency involved in deriving
C from P explicit.
Notice, in this respect, that in the example above we
have omitted the type of the abstraction variable
in the definition of eq,
which would have to be written as $\%l\; x:\backslash Y(P).x.i\; =\; self.i$
(and in a similar way for C ) to do it properly.
Type dependency
The expression self is essentially of a polymorphic nature.
To make the dependency of object specification on self
explicit, we will employ an explicit type variable
similar as in $F\_\{<=\}$.
Let $F[\%a]$ stand for $\{\; a\_1\; :\; \%t\_1,...,a\_n:\%t\; \}$
as before.
We may regard $F[\%a]$ as a type function, in the sense
that for some type $\%t$ the expression $F[\%t]$
results in a type.
To determine the type of an object specification
we must find a type $\%s$ that satisfies both
$\%s\; <=\; F[\%s]$ and $F[\%s]\; <=\; \%s$.
Type dependency  is polymorphic
 Let $F[\%a]\; =\; \{\; m\_1:\%s\_1,...,m\_j:\%s\_j\; \}$ \zline{(type function)}
 $P:\backslash A\; \%a\; <=\; F[\%a].t\; >\; F[\%a]$
 $P\; =\; \%L\; \%a\; <=\; F[\%a].\%l(\; self:\%a\; ).\{\; m\_1:e1,...,m\_j:e\_j\; \}$
Fbounded constraint $\%a\; <=\; F[\%a]$\n
Object instantiation:
$\backslash Y(P[\%s])$ for $\%s\; =\; \%m\; t.F[t]$\n
We have $P[\%s]:\%s\; >\; F[\%s]$ because $F[\%s]\; =\; \%s$
slide: Bounded type constraints
We may write an object specification as
$\%L\; \%a\; <=\; F[\%a].\%l(self:\%a).\{\; a\_1\; =\; e\_1,...,a\_n$ $=\; e\_n\; \}$,
which is typed as $\backslash A\; \%a\; <=\; F[\%a].\; \%a\; >\; F[\%a]$.
The constraint that $\%a\; <=\; F[\%a]$, which is called
an Fbounded constraint, requires
that the subtype substituted for $\%a$ is
a (structural) refinement of the record type $F[\%a]$.
As before, we have that $\backslash Y(P[\%s])\; =\; \%s$ with $\%s\; =\; \%m\; \%a.F[\%a]$,
which differs from our previous definition only
by making the type dependency in P explicit.
See slide [9dependency].
Now, when applying this extended notion of object
specification to the characterization of inheritance,
we may relax our requirement that $\backslash Y(C)$ must be a subtype
of $\backslash Y(P)$ into the requirement that $G[\%a]\; <=\; F[\%a]$
for any $\%a$, where F is the record specification
of P and G the record specification of C.
Inheritance
$P\; =$\%L \%a <= F[\%a].\%l( self: \%a).{ ... }
$C\; =$\%L \%a <= G[\%a].\%l( self:\%a).P[\%a]( self ) \with { ... }
with recursive types
$F[\%a]\; =\; \{\; i:int,\; id:\%a\; >\; bool\; \}$
$G[\%a]\; =\; \{\; i:int,\; id:\%a\; >\; bool,\; b\; :\; bool\; \}$
Valid, because $G[\%a]\; <=\; F[\%a]$
However $\backslash Y(C[\%s])\; \backslash not<=\_\{subtype\}\; \backslash Y(P[\%t])$
slide: Inheritance and constraints
For example, when we declare $F[\%a]$
and $G[\%a]$ as in slide [9selfconstraint],
we have that $G[\%a]\; <=\; F[\%a]$
for every value for $\%a$.
However, when we find types $\%s$ and $\%t$
such that $\backslash Y(C[\%s])\; :\; \%s$ and $\backslash Y(P[\%t])\; :\; \%t$
we (still) have that $\%s\; \backslash not<=\; \%t$.
Conclusion, inheritance allows more than subtyping.
In other words, our type checker may guard
the structural application of inheritance, yet will
not guarantee that the resulting object types
behaviorally satisfy the subtype relation.
Discussion  Eiffel is not type consistent
We have limited our exploration of the recursive structure
of objects to (polymorphic) object variables.
Selfreference, however, may also occur to class variables.
The interested reader is referred to [CoHC90].
The question that interests us more at this particular
point is what benefits we may have from the techniques employed
here and what lessons we may draw from applying them.
One lesson, which should not come as a surprise,
is that a language may allow us to write programs
that are accepted by the compiler yet are behaviorally incorrect.
However, if we can determine syntactically that the
subtyping relations between classes is violated we may at
least expect a warning from the compiler.
So one benefit, possibly, is that we may improve our compilers
on the basis of the type theory presented in this chapter.
Another potential benefit is that we may better understand the tradeoffs
between the particular forms of polymorphism offered by our
language of choice.
The analysis given in [CoHC90] indeed leads to a
rather surprising result.
Contrary to the claims made by its developer,
[CoHC90] demonstrate that Eiffel is not type consistent.
The argument runs as follows.
Suppose we define a class C with a method eq
that takes an argument of a type similar
to the type of the object itself
(which may be written in Eiffel as like Current).
We further assume that the class P is defined
in a similar way, but with an integer field i
and a method eq that tests only on i.
See slide [9selfeiffel].
Inheritance != subtyping
Eiffel
class C inherit P redefine eq
feature
b : Boolean is true;
eq( other : like Current ) : Boolean is
begin
Result := (other.i = Current.i) and
(other.b = Current.b)
end
end C
slide: Inheritance and subtyping in Eiffel
We may then declare variables v and p of type P.
Now suppose that we have an object c of type C,
then we may assign c to v and invoke the method
eq for v, asking whether p is equal to v, as in
p,v:P, c:C
v:=c;
v.eq(p); // error p has no b
slide: Example
Since v is associated with an instance of C,
but syntactically declared as being of type P,
the compiler accepts the call.
Nevertheless, when p is associated with an instance of
P trouble will arise, since (due to dynamic binding)
the method eq defined for C will be invoked while
p not necessarily has a field b.
When we compare the definition of C in Eiffel
with how we may define C in C++,
then we are immediately confronted with
the restriction that we do not have such a dynamic typing mechanism
as like Current in C++.
Instead, we may use overloading, as shown
in slide [9selfcc].
class C : public P { C++
int b;
public:
C() { ... }
bool eq(C& other) { return other.i == i && other.b == b; }
bool eq(P& other) { return other.i == i; }
};
slide: Inheritance and subtyping in C++
When we would have omitted the P variant
of eq, the compiler complains about hiding a virtual
function.
However, the same problem arises when we define eq
to be virtual in P, unless we take care to
explicitly cast p into either a C or P reference.
(Overloading is also used in [Liskov93]
to solve a similar problem.)
In the case we choose for a nonvirtual definition
of eq, it is determined statically which variant
is chosen and (obviously) no problem occurs.
Considering that determining equality between
two objects is somehow orthogonal to
the functionality of the object proper,
we may perhaps better employ externally defined
overloaded functions to express relations
between objects.
This observation could be an argument to
have overloaded functions apart from
objects, not as a means
to support a hybrid approach but as a means
to characterize relations between objects
in a type consistent (polymorphic) fashion.
objectoriented programming
Summary
objectoriented programming
This chapter has treated polymorphism
from a foundational perspective.
In section 1,
we looked at abstract inheritance as
employed in knowledge representation.
1
 abstract inheritance  declarative relation
 inheritance networks  nonmonotonic reasoning
 taxonomic structure  predicate calculus
slide: Section 9.1: Abstract inheritance
We discussed the nonmonotonic aspects
of inheritance networks
and looked at a first order logic
interpretation of taxonomic
structures.
2
 types  sets of values
 the subtype relation  refinement rules
 functions  contravariance
 objects  as records
slide: Section 9.2: The subtype relation
In section 2,
a characterization of types as sets of values
was given.
We looked at a formal definition of the
subtype relation and discussed
the refinement rules for functions and objects.
3
 typing  protection against errors
 flavors  parametric, inclusion, overloading, coercion
 inheritance  incremental modification mechanism
slide: Section 9.3: Flavors of polymorphism
In section 3,
we discussed types as a means to prevent errors,
and distinguished between various flavors
of polymorphism,
including parametric polymorphism,
inclusion polymorphism, overloading and
coercion.
Inheritance was characterized as an incremental
modification mechanism, resulting in
inclusion polymorphism.
4
 subtypes  typed lambda calculus
 overloading  intersection types
 bounded polymorphism  generics and inheritance
slide: Section 9.4: Type abstraction
In section 4,
some formal type calculi were presented,
based on the typed lambda calculus.
These included a calculus for simple subtyping,
a calculus for overloading,
employing intersection types,
and a calculus for bounded polymorphism,
employing type abstraction.
Examples were discussed illustrating the (lack of) features
of the C++ type system.
5
 hiding  existential types
 packages  abstract data types
slide: Section 9.5: Existential types
In section 5,
we looked at a calculus employing
existential types, modeling abstract
data types
and hiding by means of packages
and type abstraction.
6
 selfreference  recursive types
 object semantics  unrolling
 inheritance  dynamic binding
 subtyping  inconsistencies
slide: Section 9.6: Selfreference
Finally, in section 6, we discussed selfreference
and looked at a calculus employing recursive
types.
It was shown how object semantics may be determined
by unrolling, and we studied the semantic
interpretation of dynamic binding.
Concluding this chapter, an example was given
showing an inconsistency in the
Eiffel type system.
objectoriented programming
 How would you characterize inheritance
as applied in knowledge representation?
Discuss the problems that arise
due to nonmonotony.
 How would you render the meaning of
an inheritance lattice?
Give some examples.
 What is the meaning of a type?
How would you characterize the relation between
a type and its subtypes?
 Characterize the subtyping rules for ranges,
functions, records and variant records.
Give some examples.
 What is the intuition underlying the
function subtyping rule?
 What is understood by the notion
of objects as records?
Explain the subtyping rule for objects.
 Discuss the relative merits of typed
formalisms and untyped formalisms.
 What flavors of polymorphism
can you think of?
Explain how the various flavors are
related to programming language constructs.
 Discuss how inheritance may be understood
as an incremental modification mechanism.
 Characterize the simple type calculus
$\%l\_\{<=\}$, that is the syntax, type
assignment and refinement rules.
Do the same for $F\_\{\; /\backslash \; \}$
and $F\_\{<=\}$.
 Type the following expressions:
(a) $\{\; a\; =\; 1,\; f\; =\; \%l\; x:Int.\; x\; +\; 1\; \}$,
(b) $\%l\; x:Int\; .\; x\; *\; x$,
and
(c) $\%l\; x:\{\; b:Bool,\; f:\{\; a:Bool\; \}\; \}\; >\; Int.x.f(x)$.
 Verify whether:
(a) $f\text{'}\; :\; 2..5\; >\; Int\; <=\; f:1..4\; >\; Int$,
(b) $\{\; a:Bool,\; f:Bool\; >\; Int\; \}\; <=\; \{\; a:Int,\; f:\; Int\; >\; Int\; \}$, and
(c) $\%l\; x:\; \{\; a:Bool\; \}\; >\; Int\; <=\; \%l\; x:\; \{\; a:Bool,\; f:Bool\; >\; Int\; \}\; >\; Int$.
 Explain how you may model abstract
data types as existential types.
 What realizations of
the type
$\backslash E\; \%a.\; \{\; a:\%a,\; f:\%a\; >\; Bool\; \}$
can you think of?
Give at least two examples.
 Prove that
$\%m\; \%a\; .\; \{\; c:\%a,\; b:\%a\; >\; \%a\; \}\; \backslash not<=\; \%m\; \%a\; .\; \{\; b\; :\; \%a\; >\; \%a\; \}$.
 Prove that
$\%m\; \%a\; .\; \{\; c\; :\; \%a,\; b:\; \%t\; >\; \%a\; \}\; <=\; \%t$, for $\%t\; =\; \%m\; \%a.\{\; b:\; \%a\; >\; \%a\; \}$.
slide: Questions
objectoriented programming
As further reading I recommend
[CW85] and [Pierce93].
As another source of material
and exercises consult [Palsberg94].
[BG93] contains a number of relevant papers.
An exhaustive overview of the semantics of object systems,
in both first order and second order calculi, is further
given in [ObjectCalculus].
(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.