<s5>Æliens</s5> -- slide(s)

Lambda calculus -- very informal

$%l$

variables, abstractor $%l$ , punctuation $(,)$

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

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

slide: The lambda calculus -- laws

Substitution

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

slide: The lambda calculus -- substitution

Examples


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

slide: Beta conversion -- examples

Properties

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

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


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

slide: The lambda calculus -- properties

A simple type calculus -- subtypes

$%l_{ <= }$

$%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 ( f ( y ) )$ $twice : ( Int -> Int ) -> Int -> Int$

Application

$S 0 = 1 \e Int$
$twice ( S ) = %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++

Intersection types -- overloading

$%l_{ /\ }$

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

Type assignment

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

Refinement

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

slide: The intersection type calculus

Examples

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

slide: Intersection types -- examples

Overloaded function selection rules

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

slide: Overloading in C++


  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_{ <= }$

$%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 [ %t ]$

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' <= %s$ }{ $%G |- e [ %s' ] \e %t [ %a := %s' ]$ }

Refinement

\ffrac{ $%G |- %s <= %s'$ \hspace{1cm} $%G |- %t' <= %t$ }{ $%G |- \A %a <= %s'.%t' <= \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[%a](f[%a](x))$
$twice1 : \A %a. \A %b. (%b -> %b) -> %a -> %b$
$twice2 = %L %a.%l f: %a -> %a. %l x:%a. f(f(x))$
$twice2 : \A %a. (%a -> %a) -> %a -> %a$

Applications

$id [ Int ] ( 3 ) = 3$
$twice1 [ Int ] ( id )( 3 ) = 3$
$twice1 [ Int ] ( S ) = illegal$
$twice2 [ Int ] ( S )( 3 ) = 5$

slide: Parametrized types -- examples

Bounded quantification

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

Application

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

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

Æliens

2009

subsections:

Lambda calculus -- very informal

Lambda terms -- $ %L $

Laws

Substitution

Examples

Properties

A simple type calculus -- subtypes

Type assignment

Refinement

Examples

Application

P

$C <= P$

Intersection types -- overloading

Type assignment

Refinement

Examples

Overloaded function selection rules

Multiple arguments -- intersect rule

Bounded polymorphism -- abstraction

Type assignment

Refinement

Examples

Applications

Bounded quantification

Application

A<T>

OK