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
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
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 abstraction in C++
(C) Æliens 04/09/2009You 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.