Æliens

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

Object inheritance -- dynamic binding

$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 \zline{(more information)}

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

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

$\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 \zline{(subtyping error)}

• Let $F[\%a]\; =\; \{\; m\_1:\%s\_1,...,m\_j:\%s\_j\; \}$ \zline{(type function)}

F-bounded constraint \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$

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
  

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

  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; }
  };