#### Polymorphism

9

• abstract inheritance
• subtypes
• type abstraction
• self-reference

Additional keywords and phrases: exceptions, type calculi, parametric types, coercion, ad hoc polymorphism, universal types, existential types, unfolding, intersection types

slide: Polymorphism

#### Abstract inheritance

• declarative relation among entities

#### Inheritance networks

• isa-trees -- partial ordering
• isa/is-not -- bipolar, is-not inference

#### Non-monotonic reasoning


Nixon is-a Quaker
Nixon is-a Republican
Quakers are Pacifists
Republicans are not Pacifists


Incremental system evolution is in practice non-monotonic!

slide: Knowledge representation and inheritance

#### Taxonomic structure


$\A x . Elephant\left(x\right) -> Mammal\left(x\right)$
$\A x . Elephant\left(x\right) -> color\left(x\right) = gray$
$\A x . Penguin\left(x\right) -> Bird\left(x\right) /\ \neg CanFly\left(x\right)$


slide: Taxonomies and predicate logic

#### Types as sets of values

• $V \approx Int \cup ... \cup V \times V \cup V -> V$

#### Ideals -- over $V$

• subtypes -- ordered by set inclusion
• lattice -- $Top = V$, $Bottom = \emptyset$

#### Type system

subtypes correspond to subsets

• a collection of ideals of V

slide: The interpretation of types as sets

#### Sub-range 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$) }{ $\left\{a_1: %s_1, ... , a_n: %s_n\right\} <= \left\{a_1: %t_1 , ... , a_m: %t_m\right\}$ }

#### Variants

• \ffrac{$%s_i <= %t_i$ for $i = 1..m$ ($m <= n$) }{ $\left[a_1:%s_1 \/ ... \/ a_m:%s_m\right] <= \left[a_1:%t_1 \/ ... \/ a_n:%t_n\right]$ }

slide: The subtype refinement relation

#### Examples

subtyping

• $8..12 -> 3..5 <= 9..11 -> 2..6$
• $\left\{ age : int, speed : int, fuel : int \right\} <= \left\{ age : int, speed : int \right\}$
• $\left[ yellow \/ blue \right] < \left[ yellow \/ blue \/ green \right]$

slide: Examples of subtyping

#### Function refinement

• $f\text{'} : Nat -> Nat \not<= f : Int -> Int$

#### Functions -- as a service

contravariance

• domain -- restrictions for the client
• range -- obligations for server

slide: The function subtype relation

#### Objects as records

• record = finite association of values to labels

#### Field selection -- basic operation

• $\left(a = 3, b = true \right).a == 3$

#### Typing rule

• \ffrac{ $e_1 : %t_1$ and ... and $e_n : %t_n$ }{ $\left\{ a_1 = e1,..., a_n = e_n \right\} : \left\{ a_1 : %t_1, ..., a_n : %t_n \right\}$ }

slide: The object subtype relation

#### 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$ }{ $\left\{ a_1 : %s_1, ..., a_\left\{n + m\right\} : %s_\left\{n + m\right\} \right\} <= \left\{ a_1 : %t_1 , ..., a_n : %t_n \right\}$ }

slide: Examples of object subtyping

#### 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

#### 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:

slide: The nature of types

#### Flavors of polymorphism

• inclusion polymorphism -- to model subtypes and inheritance
• parametric polymorphism -- uniformly on a range of types

slide: Flavors of polymorphism

#### Inheritance -- incremental modification

• Result = Parent + Modifier

Example: $R = \left\{ a1, a2 \right\} + \left\{ a2, a3 \right\} = \left\{ a1, a2, a3 \right\}$

Independent attributes: M disjoint from P
Overlapping attributes: M overrules P

#### Dynamic binding

• $R = \left\{...,P_i: self ! A,...\right\} + \left\{ ...,M_j: self ! B, ... \right\}$

slide: Inheritance as incremental modification

#### Lambda calculus -- very informal

$%l$

• variables, abstractor $%l$, punctuation $\left(,\right)$

#### Lambda terms -- $%L$

• $x \e %L$ \zline{variables}
• $M \e %L => %l x. M \e %L$ \zline{abstraction}
• $M \e %L$ and $N \e %L => M N \e %L$ \zline{application}

slide: The lambda calculus -- terms

#### Laws

• $\left( %l x.M\right) N = M \left[ x := N \right]$ \zline{conversion}
• $M = N => MZ = NZ$ and $ZM = ZN$
• $M = N => %l x.M = %l x.N$

slide: The lambda calculus -- laws

#### Substitution

• $x\left[x:=N\right] == N$
• $y\left[x:=N\right] == y$ if $x != y$
• $\left(%l y.M\right)\left[x:=N\right] == %l y.\left(M\left[x:=N\right]\right)$
• $\left(M_1 M_2 \right) \left[x:=N\right]$ $==$ $\left(M_1 \left[x:=N\right]\right) \left(M_2\left[x:=N\right]\right)$

slide: The lambda calculus -- substitution

#### Examples


$\left($\%l x.x) 1 = x[x:=1] = 1
$\left($\%l x.x+1) 2 = (x+1)[x:=2] = 2 + 1
$\left($\%l x.x+y+1) 3 = (x+y+1)[x:=3] = 3+y+1
$\left($\%l y.(\%l x.x+y+1) 3) 4) =
$\left(\left($\%l x.x+y+1) 3)[y:=4] = 3 + 4 + 1


slide: Beta conversion -- examples

#### Properties

• $\A M \left(%l x.x\right) M = M$ \zline{identity}
• $\A F \E X. F X = X$ \zline{fixed point}

Proof: take $W = %l x.F \left( xx \right)$ and $X = WW$, then


$X = WW = \left($\%l x.F ( xx ) ) W = F ( WW ) = FX


slide: The lambda calculus -- properties

#### A simple type calculus -- subtypes

$%l_\left\{ <= \right\}$

• $%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 \e %s -> %t$ }
• \ffrac{$%G |- e_1 : %s -> %t, e_2 : %s$}{ $%G |- e_1 e_2 \e %t$ }

#### Refinement

• \ffrac{ $%G |- e : %s$ \hspace{1cm} $%G |- %s <= %t$}{ $%G |- e : %t$ }

slide: The subtype calculus

#### Examples

• $S = %l x:Int. x + 1$
$S : Int -> Int$
• $twice = %l f:Int -> Int. %l y : Int . f \left( f \left( y \right) \right)$ $twice : \left( Int -> Int \right) -> Int -> Int$

#### Application

• $S 0 = 1 \e Int$
• $twice \left( S \right) = %l x. S S x \e Int -> Int$

slide: Subtypes -- examples


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++


int SD(double x) { return x+1; } // twice(SD) rejected


slide: SD example


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++

$%l_\left\{ /\ \right\}$

• $%t ::= %r | %t_1 -> %t_2 | \bigwedge \left[ %t_1 .. %t_n \right]$

#### Type assignment

• \ffrac{$%G |- e : %t_i$ $\left(i \e 1..n\right)$}{ $%G |- e : \bigwedge \left[ %t_1 .. %t_n \right]$ }

#### Refinement

• \ffrac{ $%G |- %s <= %t_i$ $\left(i \e 1..n \right)$}{ $%G |- %s <= \bigwedge \left[ %t_1 .. %t_n \right]$ }
• $\bigwedge \left[ %t_1 .. %t_n \right] <= %t_i$
• $%G |- \bigwedge \left[ %s -> %t_1 .. %s -> %t_n \right] <= %s -> \bigwedge \left[ %t_1 .. %t_n \right]$

slide: The intersection type calculus

#### Examples

• $+ : \bigwedge \left[ Int \* Int -> Int, Real \* Real -> Real\right]$
• $Int -> Int <= \bigwedge \left[ Int -> Int, Real -> Real \right]$
• $Msg -> Obj1 /\ Msg -> Obj2 <= Msg -> \bigwedge \left[ Obj1, Obj2 \right]$

slide: Intersection types -- examples

C++

•  no or unavoidable conversions -- $array->pointer$, $T -> const T$
•  integral promotion -- $char->int$, $short->int$, $float->double$
•  standard conversions -- $int->double$, $double->int$, $derived* -> base*$
•  user-defined conversions -- constructors and operators
•  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


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


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


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


#### Bounded polymorphism -- abstraction

$F_\left\{ <= \right\}$

• $%t ::= Top | %a | %r | %t_1 -> %t_2 | \A %a <= %t_1. %t_2$
• $e ::= x | %l x:%t.e | e_1 e_2 | %L %a <= %t.e | e \left[ %t \right]$

#### Type assignment

• \ffrac{$%G, %a <= %s |- e : %t$ }{ $%G |- %L %a <= %s. e \e \A %a <= %s . %t$ }
• \ffrac{$%G, e : \A %a <= %s . %t$ \hspace{1cm} $%G |- %s\text{'} <= %s$ }{ $%G |- e \left[ %s\text{'} \right] \e %t \left[ %a := %s\text{'} \right]$ }

#### Refinement

• \ffrac{ $%G |- %s <= %s\text{'}$ \hspace{1cm} $%G |- %t\text{'} <= %t$}{ $%G |- \A %a <= %s\text{'}.%t\text{'} <= \A %a <= %s.%t$ }

slide: The bounded type calculus

#### Examples

• $id = %L %a. %l x:%a.x$ $id : \A %a. %a -> %a$
• $twice1 = %L %a.%l f: %L %b. %b -> %b. %l x:%a. f\left[%a\right]\left(f\left[%a\right]\left(x\right)\right)$
$twice1 : \A %a. \A %b. \left(%b -> %b\right) -> %a -> %b$
• $twice2 = %L %a.%l f: %a -> %a. %l x:%a. f\left(f\left(x\right)\right)$
$twice2 : \A %a. \left(%a -> %a\right) -> %a -> %a$

#### Applications

• $id \left[ Int \right] \left( 3 \right) = 3$
• $twice1 \left[ Int \right] \left( id \right)\left( 3 \right) = 3$
• $twice1 \left[ Int \right] \left( S \right) = illegal$
• $twice2 \left[ Int \right] \left( S \right)\left( 3 \right) = 5$

slide: Parametrized types -- examples

#### Bounded quantification

• $g = %L %a <= \left\{ one : Int \right\}. %l x: %a. \left(x.one\right)$
$g : \A %a <= \left\{ one : int \right\}. %a -> Int$
• $g\text{'} = %L %b . %L %a <= \left\{ one : %b \right\}. %l x: %a. \left(x.one\right)$
$g\text{'} : \A %b . \A %a <= \left\{ one : %b \right\}. %a -> %b$
• $move = %L %a <= Point. %l p:%a. %l d : Int .\left(p.x := p.x + d\right); p$
$move : \A %a <= Point. %a -> Int -> %a$

#### Application

• $g\text{'} \left[ Int \right]\left[ \left\{ one:Int, two : Bool \right\}\right]\left(\left\{ one = 3, two = true \right\}\right) = 3$
• $move \left[\left\{ x : Int, y : Int \right\}\right]\left( \left\{ x = 0, y = 0 \right\} \right)\left(1\right) = \left\{ x = 1, y = 0 \right\}$

slide: Bounded quantification -- examples


Point* move(Point* p, int d); // require int Point::x
Point* move(Point* p, int d) { p.x += d; return p; }


slide: example move


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++


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


Int i1, i2;
P<Int> p1(i1), p2(i2);
if ( p1 == p2 ) cout << "OK" << endl;  OK


slide: Example P

#### Existential types -- hiding

$F_\left\{ \E \right\}$

• $%t ::= ... | \E %a <= %t_1. %t_2$
• $e ::= ... | pack\left[ %a = %s in %t \right]. e$

#### Type assignment

• \ffrac{$%G |- %s\text{'} <= %s$ \hspace{1cm} $%G |- e : %t$}{ $pack\left[ %a = %s\text{'} in %t \right].e \e \E %a <= %s. %t$ }

#### Refinement

• \ffrac{$%G |- %s <= %s\text{'}$ \hspace{1cm} $%G |- %t\text{'} <= %t$}{ $%G |- \E %a <= %s\text{'} . %t\text{'} <= \E %a <= %s. %t$ }

slide: The existential type calculus

#### Structure -- indeterminacy

• $Top = \E %a.%a$ \zline{the biggest type}
• $AnyPair = \E %a \E %b.%a \* %b$ \zline{any pair}
• $(3,4):\E %a.%a$\left\{\em -- does not provide sufficient structure!\right\}$ •$(3,4):\E %a.%a \* %a

#### Information hiding

• $\E %a.%a \* \left( %a->Int \right)$ \zline{object, operation}
• $x : \E %a. %a \* \left( %a->Int \right)$ \zline{ $$\leadsto$$ $snd \left( x \right)\left( fst\left( x \right)\right)$ }

slide: Existential types -- examples

#### Abstract data types -- packages

• $x:\E %a.\left\{ val : %a, op : %a -> Int \right\}$
• $x = pack\left[%a = Int in \left\{ val:%a, op:%a -> Int \right\} \right]\left(\left(3,S\right)\right)$
• $x.op\left(x.val\right) = 4$

#### Encapsulation

$pack \left[ representation in interface \right]\left( contents \right)$

• interface -- type $\E %a. \left\{ val : %a, op : %a -> Int \right\}$
• representation -- $%a = Int$ \zline{(hidden data type)}
• contents -- $\left(3,S\right)$

slide: Packages -- examples


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++

#### Self-reference -- recursive types

$F_\left\{ %m \right\}$

• $%t ::= ... | %m %a. %t \left[%a\right]$
• $e ::= ... | %l\left( self \right).\left\{ a1 = e_1, ..., a_n = e_n \right\}$

#### Type assignment

• \ffrac{ $%G |- e_i : %t_i$ \hspace{1cm} $\left(i = 1..n\right)$ }{ $%G |- %l\left( self \right).\left\{ a1 = %t_1,.., a_n = %t_n \right\} \e %m%a.\left\{ a1:%t_1,.., a_n : %t_n \right\}\left[%a\right]$ }

#### Refinement

• \ffrac{ $%G, %a <= %b |- %s <= %t$ }{ $%G |- %m %a.%s\left[%a\right] <= %m %b.%t \left[%b\right]$ }

slide: A calculus for recursive types

#### Object semantics -- fixed point $%s = F[%s]$

• $\Y \left( %l\left( self \right).F\left( self \right) \right) : %s$

#### Unrolling -- unraveling a type

• $%m %a.F\left[%a\right] = F\left[ %m %a.F\left[%a\right] \right]$

#### Example


$T =$\%m \%a.{ a:int, c:\%a, b:\%a->\%a }
$T_1 = \left\{ a:int, c:T, b:T->T, d:bool \right\}$
$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 \not<= T$ \zline{(contravariance)}

slide: Recursive types -- examples

#### Inheritance -- C = P + M

• $P = %l\left( self \right).\left\{ a1 = e1,...,a_n = e_n \right\}$
• $C = %l\left( self \right).P\left( self \right)$ $\with$ \ifsli{\n}{} $\left\{ a1\text{'} = e1\text{'},...,a_k\text{'} = e_k\text{'} \right\}$

#### Semantics -- $\Y(C) = \Y(%l( self ).M( self )(P( self )))$

• $P : %s -> %s$ $=>$ $\Y\left(P\right):%s$
• $C = %l\left(s\right).M\left(s\right)\left(P\left(s\right)\right) : %t -> %t$ $=>$ $\Y\left(C\right):%t$

slide: Inheritance semantics -- self-reference

#### Object inheritance -- dynamic binding

$P = %l\left( self \right).\left\{ i = 5, id = self \right\}$
$C = %l\left( self \right).P\left( self \right) \with \left\{ b = true \right\}$
$\Y\left(P\right):%t$ where $%t = %m %a.\left\{ i:int, id:%a \right\}$ and $P:%t->%t$

Simple typing -- $\Y\left(C\right):%s = \left\{ i:int, id:%t, b:bool \right\}$
Delayed -- $\Y\left(C\right):%s\text{'} = %m %a.\left\{ i:int, id:%a, b:bool \right\}$
We have $%s\text{'} <= %s$ \zline{(more information)}

slide: Object inheritance -- dynamic binding

#### Contravariance

• $P = %l\left( self \right).\left\{ i = 5, eq = %l\left(o\right).\left(o.i = self.i\right) \right\}$


$C =$\%l( self ).P( self )  \with { b = true,
$eq =$\%l(o).(o.i = self.i    and
$o.b = self.b\right)$
$\right\}$


$\Y\left(P\right) : %t$ where $%t = %m %a.\left\{ i:int, eq:%a -> bool \right\}$
$\Y\left(C\right):%s$ where $%s = %m %a.\left\{ i:int, id:%a -> bool, b: bool \right\}$
However $%s \not<= %t$ \zline{(subtyping error)}

slide: Object inheritance -- contravariance

#### Type dependency -- is polymorphic

• Let $F\left[%a\right] = \left\{ m_1:%s_1,...,m_j:%s_j \right\}$ \zline{(type function)}
• $P:\A %a <= F\left[%a\right].t -> F\left[%a\right]$
• $P = %L %a <= F\left[%a\right].%l\left( self:%a \right).\left\{ m_1:e1,...,m_j:e_j \right\}$

F-bounded constraint $%a <= F\left[%a\right]$\n Object instantiation: $\Y\left(P\left[%s\right]\right)$ for $%s = %m t.F\left[t\right]$\n We have $P\left[%s\right]:%s -> F\left[%s\right]$ because $F\left[%s\right] = %s$

slide: Bounded type constraints

#### 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\left[%a\right] = \left\{ i:int, id:%a -> bool \right\}$
$G\left[%a\right] = \left\{ i:int, id:%a -> bool, b : bool \right\}$
Valid, because $G\left[%a\right] <= F\left[%a\right]$
However $\Y\left(C\left[%s\right]\right) \not<=_\left\{subtype\right\} \Y\left(P\left[%t\right]\right)$

slide: Inheritance and constraints

#### 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


p,v:P, c:C

v:=c;
v.eq(p);   // error p has no b


slide: Example


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++

#### Abstract inheritance

1

• abstract inheritance -- declarative relation
• inheritance networks -- non-monotonic reasoning
• taxonomic structure -- predicate calculus

slide: Section 9.1: Abstract inheritance

#### The subtype relation

2

• types -- sets of values
• the subtype relation -- refinement rules
• functions -- contravariance
• objects -- as records

slide: Section 9.2: The subtype relation

#### Flavors of polymorphism

3

• typing -- protection against errors
• inheritance -- incremental modification mechanism

slide: Section 9.3: Flavors of polymorphism

#### Type abstraction

4

• subtypes -- typed lambda calculus
• bounded polymorphism -- generics and inheritance

slide: Section 9.4: Type abstraction

#### Existential types

5

• hiding -- existential types
• packages -- abstract data types

slide: Section 9.5: Existential types

#### Self-reference

6

• self-reference -- recursive types
• object semantics -- unrolling
• inheritance -- dynamic binding
• subtyping -- inconsistencies

slide: Section 9.6: Self-reference

1. How would you characterize inheritance as applied in knowledge representation? Discuss the problems that arise due to non-monotony.
2. How would you render the meaning of an inheritance lattice? Give some examples.
3. What is the meaning of a type? How would you characterize the relation between a type and its subtypes?
4. Characterize the subtyping rules for ranges, functions, records and variant records. Give some examples.
5. What is the intuition underlying the function subtyping rule?
6. What is understood by the notion of objects as records? Explain the subtyping rule for objects.
7. Discuss the relative merits of typed formalisms and untyped formalisms.
8. What flavors of polymorphism can you think of? Explain how the various flavors are related to programming language constructs.
9. Discuss how inheritance may be understood as an incremental modification mechanism.
10. Characterize the simple type calculus $%l_\left\{<=\right\}$, that is the syntax, type assignment and refinement rules. Do the same for $F_\left\{ /\ \right\}$ and $F_\left\{<=\right\}$.
11. Type the following expressions: (a) $\left\{ a = 1, f = %l x:Int. x + 1 \right\}$, (b) $%l x:Int . x * x$, and (c) $%l x:\left\{ b:Bool, f:\left\{ a:Bool \right\} \right\} -> Int.x.f\left(x\right)$.
12. Verify whether: (a) $f\text{'} : 2..5 -> Int <= f:1..4 -> Int$, (b) $\left\{ a:Bool, f:Bool -> Int \right\} <= \left\{ a:Int, f: Int -> Int \right\}$, and (c) $%l x: \left\{ a:Bool \right\} -> Int <= %l x: \left\{ a:Bool, f:Bool -> Int \right\} -> Int$.
13. Explain how you may model abstract data types as existential types.
14. What realizations of the type $\E %a. \left\{ a:%a, f:%a -> Bool \right\}$ can you think of? Give at least two examples.
15. Prove that $%m %a . \left\{ c:%a, b:%a -> %a \right\} \not<= %m %a . \left\{ b : %a -> %a \right\}$.
16. Prove that $%m %a . \left\{ c : %a, b: %t -> %a \right\} <= %t$, for $%t = %m %a.\left\{ b: %a -> %a \right\}$.

slide: Questions

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].