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

• [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] user-defined 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


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