[]
readme
course(s)
preface
I
1
2
II
3
4
III
5
6
7
IV
8
9
10
V
11
12
afterthought(s)
appendix
reference(s)
example(s)
resource(s)
_

object-oriented programming

In this section we will study type calculi that allow us to express the various forms of polymorphism, including

** $\%l$**

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

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

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

- $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])$

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

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

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

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

$$::=\ %t|\ %r_1 ->\ %t_2\ %t

** $\%l\_\{\; <=\; \}$ **

- $\%t\; ::=\; \%r\; |\; \%t\_1\; ->\; \%t\_2$
- $e\; ::=\; x\; |\; \%l\; x\; :\; \%t\; .\; e\; |\; e\_1\; e\_2$

- \ffrac{$\%G\; |-\; x\; :\; \%s$ \hspace{1cm} $\%G\; |-\; e\; :\; \%t$}{ $\%G\; |-\; \%l\; x\; :\; \%s\; .\; e\; \backslash e\; \%s\; ->\; \%t$ }
- \ffrac{$\%G\; |-\; e\_1\; :\; \%s\; ->\; \%t,\; e\_2\; :\; \%s$}{ $\%G\; |-\; e\_1\; e\_2\; \backslash e\; \%t$ }

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

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

- $S\; 0\; =\; 1\; \backslash e\; Int$
- $twice\; (\; S\; )\; =\; \%l\; x.\; S\; S\; x\; \backslash e\; Int\; ->\; Int$

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; }// twice(SD) rejected

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 {

P## public: C() : P(this) { } C* self() {

$C\; <=\; P$// ANSI/ISOreturn _self?_self->self():this; } void attach(P* p) {// rejectedp->attach(self()); } void redirect(C* c) { _self = c; } private: C* _self; };

** $\%l\_\{\; /\backslash \; \}$ **

- $\%t\; ::=\; \%r\; |\; \%t\_1\; ->\; \%t\_2\; |\; \backslash bigwedge\; [\; \%t\_1\; ..\; \%t\_n\; ]$

- \ffrac{$\%G\; |-\; e\; :\; \%t\_i$ $(i\; \backslash e\; 1..n)$}{ $\%G\; |-\; e\; :\; \backslash bigwedge\; [\; \%t\_1\; ..\; \%t\_n\; ]$ }

- \ffrac{ $\%G\; |-\; \%s\; <=\; \%t\_i$ $(i\; \backslash e\; 1..n\; )$}{ $\%G\; |-\; \%s\; <=\; \backslash bigwedge\; [\; \%t\_1\; ..\; \%t\_n\; ]$ }
- $\backslash bigwedge\; [\; \%t\_1\; ..\; \%t\_n\; ]\; <=\; \%t\_i$
- $\%G\; |-\; \backslash bigwedge\; [\; \%s\; ->\; \%t\_1\; ..\; \%s\; ->\; \%t\_n\; ]\; <=\; \%s\; ->\; \backslash bigwedge\; [\; \%t\_1\; ..\; \%t\_n\; ]$

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

$+\; :\; \backslash bigwedge\; [\; Int\; \backslash *\; Int\; ->\; Int,\; Real\; \backslash *\; Real\; ->\; Real\; ]$

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

- 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

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;// 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::fc->f();// C::fpc->f();// C::f

** $F\_\{\; <=\; \}$ **

- $\%t\; ::=\; Top\; |\; \%a\; |\; \%r\; |\; \%t\_1\; ->\; \%t\_2\; |\; \backslash A\; \%a\; <=\; \%t\_1.\; \%t\_2$
- $e\; ::=\; x\; |\; \%l\; x:\%t.e\; |\; e\_1\; e\_2\; |\; \%L\; \%a\; <=\; \%t.e\; |\; e\; [\; \%t\; ]$

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

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

- $id\; =\; \%L\; \%a.\; \%l\; x:\%a.x$ $id\; :\; \backslash A\; \%a.\; \%a\; ->\; \%a$
- $twice1\; =\; \%L\; \%a.\%l\; f:\; \%L\; \%b.\; \%b\; ->\; \%b.\; \%l\; x:\%a.\; f[\%a](f[\%a](x))$

$twice1\; :\; \backslash A\; \%a.\; \backslash A\; \%b.\; (\%b\; ->\; \%b)\; ->\; \%a\; ->\; \%b$ - $twice2\; =\; \%L\; \%a.\%l\; f:\; \%a\; ->\; \%a.\; \%l\; x:\%a.\; f(f(x))$

$twice2\; :\; \backslash A\; \%a.\; (\%a\; ->\; \%a)\; ->\; \%a\; ->\; \%a$

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

- $g\; =\; \%L\; \%a\; <=\; \{\; one\; :\; Int\; \}.\; \%l\; x:\; \%a.\; (x.one)$

$g\; :\; \backslash A\; \%a\; <=\; \{\; one\; :\; int\; \}.\; \%a\; ->\; Int$ - $g\text{'}\; =\; \%L\; \%b\; .\; \%L\; \%a\; <=\; \{\; one\; :\; \%b\; \}.\; \%l\; x:\; \%a.\; (x.one)$

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

$move\; :\; \backslash A\; \%a\; <=\; Point.\; \%a\; ->\; Int\; ->\; \%a$

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

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

template< class T >// requiresclass P { public: P(T& r) : t(r) {} int operator==( PT::value()& 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> {

A<T>//public: Int(int n = 0) : _n(n) {} int value() { return _n; } private: int _n; };Int $<=$ A<int>

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

OK

[]
readme
course(s)
preface
I
1
2
II
3
4
III
5
6
7
IV
8
9
10
V
11
12
afterthought(s)
appendix
reference(s)
example(s)
resource(s)
_

(C) Æliens 04/09/2009

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