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

** $F\_\{\; \%m\; \}$**

- $\%t\; ::=\; ...\; |\; \%m\; \%a.\; \%t\; [\%a]$
- $e\; ::=\; ...\; |\; \%l(\; self\; ).\{\; a1\; =\; e\_1,\; ...,\; a\_n\; =\; e\_n\; \}$

- \ffrac{ $\%G\; |-\; e\_i\; :\; \%t\_i$ \hspace{1cm} $(i\; =\; 1..n)$ }{ $\%G\; |-\; \%l(\; self\; ).\{\; a1\; =\; \%t\_1,..,\; a\_n\; =\; \%t\_n\; \}\; \backslash e\; \%m\%a.\{\; a1:\%t\_1,..,\; a\_n\; :\; \%t\_n\; \}[\%a]$ }

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

- $\backslash Y\; (\; \%l(\; self\; ).F(\; self\; )\; )\; :\; \%s$

- $\%m\; \%a.F[\%a]\; =\; F[\; \%m\; \%a.F[\%a]\; ]$

$T\; =$\ %m.{ a:int, c:\ %a, b:\ %a->\ %a} $T\_1\; =\; \{\; a:int,\; c:T,\; b:T->T,\; d:bool\; \}$ $T\_2\; =$\ %a\ %m.{ a:int, c:\ %a, b:T->T, d:bool } $T\_3\; =$\ %a\ %m.{ a:int, c:\ %a, b:\ %a->\ %a, d:bool }\ %a

$T\_1,\; T\_2\; <=\; T$, $T\_3\; \backslash not<=\; T$ \zline{(contravariance)}

Finding the fixed point of a specification involves technically a procedure known as

- $P\; =\; \%l(\; self\; ).\{\; a1\; =\; e1,...,a\_n\; =\; e\_n\; \}$
- $C\; =\; \%l(\; self\; ).P(\; self\; )$ $\backslash with$ \ifsli{\n}{} $\{\; a1\text{'}\; =\; e1\text{'},...,a\_k\text{'}\; =\; e\_k\text{'}\; \}$

- $P\; :\; \%s\; ->\; \%s$ $=>$ $\backslash Y(P):\%s$
- $C\; =\; \%l(s).M(s)(P(s))\; :\; \%t\; ->\; \%t$ $=>$ $\backslash Y(C):\%t$

$P\; =\; \%l(\; self\; ).\{\; i\; =\; 5,\; id\; =\; self\; \}$

$C\; =\; \%l(\; self\; ).P(\; self\; )\; \backslash with\; \{\; b\; =\; true\; \}$

$\backslash Y(P):\%t$ where $\%t\; =\; \%m\; \%a.\{\; i:int,\; id:\%a\; \}$ and $P:\%t->\%t$

Simple typing -- $\backslash Y(C):\%s\; =\; \{\; i:int,\; id:\%t,\; b:bool\; \}$

Delayed -- $\backslash Y(C):\%s\text{'}\; =\; \%m\; \%a.\{\; i:int,\; id:\%a,\; b:bool\; \}$

We have $\%s\text{'}\; <=\; \%s$ \zline{(more information)}

Let (parent)

- $P\; =\; \%l(\; self\; ).\{\; i\; =\; 5,\; eq\; =\; \%l(o).(o.i\; =\; self.i)\; \}$

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

$\backslash Y(P)\; :\; \%t$ where
$\%t\; =\; \%m\; \%a.\{\; i:int,\; eq:\%a\; ->\; bool\; \}$

$\backslash Y(C):\%s$ where
$\%s\; =\; \%m\; \%a.\{\; i:int,\; id:\%a\; ->\; bool,\; b:\; bool\; \}$

However $\%s\; \backslash not<=\; \%t$ \zline{(subtyping error)}

The reasoning is as follows. For $\backslash Y(P)\; :\; \%t$ and $\backslash Y(C)\; :\; \%s$, we have that $\%s\; =\; \%m\; \%b.\{\; i:Int,\; id:\%b\; ->\; Bool,\; b:Bool\; \}$ which is (by unrolling) equal to $\{\; i:Int,\; id:\; \%s->\; Bool,\; b:Bool\; \}$. Now suppose that $\%s\; <=\; \%t$, then we have that $\{\; i:Int,\; eq:\%s->Bool,\; b:Bool\; \}$ is a subtype of $\{\; i:Int,\; eq:\%t->Bool\; \}$ which is true when $eq:\%s->Bool\; <=\; eq:\%t->Bool$ and hence (by contravariance) when $\%s\; <=\; \%t$. Clearly, this is impossible. Hence $\%s\; \backslash not<=\; \%t$. We have a problem here, since the fact that $C\; \backslash not<=\; P$ means that the type checker will not be able to accept the derivation of

- Let $F[\%a]\; =\; \{\; m\_1:\%s\_1,...,m\_j:\%s\_j\; \}$ \zline{(type function)}
- $P:\backslash A\; \%a\; <=\; F[\%a].t\; ->\; F[\%a]$
- $P\; =\; \%L\; \%a\; <=\; F[\%a].\%l(\; self:\%a\; ).\{\; m\_1:e1,...,m\_j:e\_j\; \}$

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

We may write an object specification as $\%L\; \%a\; <=\; F[\%a].\%l(self:\%a).\{\; a\_1\; =\; e\_1,...,a\_n$ $=\; e\_n\; \}$, which is typed as $\backslash A\; \%a\; <=\; F[\%a].\; \%a\; ->\; F[\%a]$. The constraint that $\%a\; <=\; F[\%a]$, which is called an

$P\; =$\ %L<= F[\ %a].\ %a( self:\ %l).{ ... } $C\; =$\ %a\ %L<= G[\ %a].\ %a( self:\ %l).P[\ %a]( self ) \with { ... }\ %a

with recursive types

$F[\%a]\; =\; \{\; i:int,\; id:\%a\; ->\; bool\; \}$

$G[\%a]\; =\; \{\; i:int,\; id:\%a\; ->\; bool,\; b\; :\; bool\; \}$

Valid, because $G[\%a]\; <=\; F[\%a]$

However $\backslash Y(C[\%s])\; \backslash not<=\_\{subtype\}\; \backslash Y(P[\%t])$

For example, when we declare $F[\%a]$ and $G[\%a]$ as in slide 9-self-constraint, we have that $G[\%a]\; <=\; F[\%a]$ for every value for $\%a$. However, when we find types $\%s$ and $\%t$ such that $\backslash Y(C[\%s])\; :\; \%s$ and $\backslash Y(P[\%t])\; :\; \%t$ we (still) have that $\%s\; \backslash not<=\; \%t$. Conclusion, inheritance allows more than subtyping. In other words, our type checker may guard the structural application of inheritance, yet will not guarantee that the resulting object types behaviorally satisfy the subtype relation.

** Eiffel**

class CinheritPredefineeqfeatureb : Booleanistrue; eq( other :likeCurrent ) : BooleanisbeginResult := (other.i = Current.i) and (other.b = Current.b)endendC

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

class C : public P {## int b; public: C() { ... } bool eq(C& other) { return other.i == i && other.b == b; } bool eq(P& other) { return other.i == i; } };

C++

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