(that is
used to bind variables in an expression), and punctuation
symbols.
Abstractors may be used to abstract a lambda term 
into
a function 
with parameter 
.
The expression 
must be read as denoting the
function with body 
and formal parameter 
.
The variable x is called the bound variable, since it
is bound by the abstractor 
.
In addition to function abstraction, we also
have (function) application, which is written
as the juxtaposition of two lambda terms.
See slide lambda-terms.
Behaviorally, lambda terms have a number of properties,
as expressed in the laws given in slide lambda-laws.
, results
in the function body M in which N is substituted
for x.
Two other laws are the so-called 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.
)
if y is x and remains y otherwise.
A substitution 
performed on an abstraction
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 lambda-substitution.
Some examples of beta conversion are given
in slide lambda-examples.
In the examples, for simplicity we employ
ordinary arithmetical values and operators.
This does not perturb the underlying 
-theory,
since both values and operations may be expressed
as proper 
-terms.
holds.
See slide lambda-properties.
As another example, consider the statement that each function F
has a fixed point, that is a value X for which 
.
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 self-reference)
we will write 
for the fixed
point of a function F.
In 
) 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
calculus is a first order calculus, since it
does not involve quantification over types.
See slide 9-c-subtypes.
The structure of type expressions is given by the
definition
as a type identifier and 
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
.
)
we need type assignment rules, as given above.
Typing is usually based on a collection
of assumptions 
, 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 
means that
the expression e has type 
, under the assumption that
the type assignments in 
are valid.
When 
is empty, as in 
, the type assignment
holds unconditionally.
Occasionally, we write 
instead of
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 
(x has type 
) and
(e has type 
)
then 
, in other words
the abstraction 
may be validly typed
as 
.
Similarly, the second type assignment rule
states that applying a function 
to an expression 
of type 
results
in an (application) expression 
of type 
.
We may assume the basic types denoted by 
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 
, with 
, as being
of type 
.
In slide 9-ex-subtypes, 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 
then we may type S
straightforwardly as being of type 
.
Similarly, we may type the (higher order) function
twice as being of type 
.
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 
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
as a subtype of
(according
to the contra-variant subtyping rule for functions).
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); }
int SD(double x) { return x+1; }
class 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 {
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;
};
) as an extension of the first version (
),
an extension which provides facilities for
(ad hoc) overloading polymorphism.
Our extension consists of adding a type expression
which denotes
a finite conjunction of types.
Such a conjunction of types, that we will
also write as 
is called
an intersection type.
The idea is that an expression e of type
is correctly typed
if 
for some i in 
.
This is expressed in the type assignment rule given
in slide 9-c-intersection.
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 
, which
has an intersection type 
as its
range into an intersection type consisting of functions
for 
.
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.
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
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)
};
P* p = new P;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.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
, 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.
(under the assumption that 
),
then we may type 
as being of type 
.
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 
and we have that 
, then 
is of type
, which is 
with 
substituted for
.
See slide 9-c-bounded.
The refinement rule for bounded types states
the subtyping relation between two bounded types.
We have that 
is
a subtype of 
whenever
and 
.
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 9-ex-parameters
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 
, which states
that when we supply a particular type, say Int,
then we obtain the function 
.
Since the actual type used to instantiate id is not important,
we may type id as being of type 
.
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 
.
In contrast, the second variant accepts S, and we may
rely on the automatic conversion
of 
to 
(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 9-ex-quantification.
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).
is a generalized version of g
that abstracts from the particular type of the one
component.
Notice that both g and 
may be applied to any record
that conforms to the requirement stated in the bound,
such as the record 
.
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.
is also introduced
in which intersection polymorphism is expressed by
means of an explicit type variable.
The resulting type may be written as 
,
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 Point* move(Point* p, int d);require int Point::x
Point* move(Point* p, int d) { p.x += d; return p; }
template< class T >requires T::value()
class P { public: P(T& r) : t(r) {} int operator==( P<T>& p) { return t.value() == p.t.value(); } private: T& t; };
template< class T >
class A {
public:
virtual T value() = 0;
};
class Int : public A<int> {
public:
Int(int n = 0) : _n(n) {}
int value() { return _n; }
private:
int _n;
};
Int i1, i2; P<Int> p1(i1), p2(i2); if ( p1 == p2 ) cout << "OK" << endl;OK
|
Hush Online Technology
hush@cs.vu.nl
12/29/99 |
|
|