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.
Additional keywords and phrases:
exceptions, type calculi,
parametric types, coercion, ad hoc polymorphism,
universal types, existential types,
unfolding, intersection types
Incremental system evolution is in practice non-monotonic!
The meaning of is-a and is-not relations in a knowledge representation inheritance graph may equivalently be expressed as predicate logic statements. For example, the statements
In Inheritance as incremental modification
Example:
Independent attributes: M disjoint from P
Overlapping attributes: M overrules P
Proof: take and , then
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 ) and function types (written
, where stands for the domain
and for the range or codomain).
This version of the typed lambda calculus
(with subtyping) is called in
, \zline{(contravariance)}
Simple typing --
where
F-bounded constraint \n
Object instantiation:
for \n
We have because
with recursive types
2 3 4 5 6
As further reading I recommend
draft version 0.1 (15/7/2001) Bounded polymorphism
Our next extension, which we call , 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 and .
Our notation for a universally quantified (bounded) type
is , which denotes the type
with the type variable replaced by any subtype of .
In a number of cases, we will simply write ,
which must be read as .
Recall that any type is a subtype of Top.
Observe that, in contrast to and ,
the calculus is second order (due to the quantification
over types).
In addition to the (value) expressions found in the two
previous calculi, introduces a type abstraction
expression of the form and a type instantiation
expression of the form .
The type abstraction expression
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 as an abbreviation for .
The (complementary) type instantiation statement is written
as , which denotes the expression e in which
the type identifier is substituted for the type variable
bound by the first type abstractor.
Bounded polymorphism -- abstraction
Type assignment
Refinement
Examples
Applications
Bounded quantification
Application
Discussion
Type abstraction in C++
public:
virtual T value() = 0;
};
class Int : public A<int> { // OK
Existential types -- hiding
Existential types were introduced in Existential types -- hiding
Type assignment
Refinement
Structure -- indeterminacy
Information hiding
Abstract data types -- packages
Encapsulation
Hiding in C++
protected:
event(event* x) : ev(x) {}
public:
int type() { return ev->type(); }
void* rawevent() { return ev; }
private:
event* ev;
};
class xevent : public event {
public:
int type() { return X->type(); }
private:
struct XEvent* X;
};
Self-reference
Recursive types are compound types in which the type
itself occurs as the type of one of its components.
Self-reference in objects clearly involves
recursive types since the expression self
denotes the object itself, and hence has the type
of the object.
In , our extension of taken from Self-reference -- recursive types
Type assignment
Refinement
Object semantics -- fixed point $ %s = F[%s] $
Unrolling -- unraveling a type
Example
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 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
to characterize derivation by inheritance,
and we assume the modifier M corresponding with
to extend the record
associated with P in the usual sense.
See slide 9-self-inheritance.
Inheritance -- C = P + M
Semantics -- $\Y(C) = \Y(%l( self ).M( self )(P( self )))$
Object inheritance -- dynamic binding
where and
Delayed --
We have \zline{(more information)}
Contravariance
where
However \zline{(subtyping error)}
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 .
Let stand for
as before.
We may regard as a type function, in the sense
that for some type the expression
results in a type.
To determine the type of an object specification
we must find a type that satisfies both
and .
Type dependency -- is polymorphic
Inheritance
Valid, because
However
Discussion -- Eiffel is not type consistent
Inheritance != subtyping
int b;
public:
C() { ... }
bool eq(C& other) { return other.i == i && other.b == b; }
bool eq(P& other) { return other.i == i; }
};
Summary
Abstract inheritance
The subtype relation
Flavors of polymorphism
Type abstraction
Existential types
Self-reference
Questions
Further reading
[]
readme
course
preface
1
2
3
4
5
6
7
8
9
10
11
12
appendix
lectures
resources
eliens@cs.vu.nl