Æliens

Polymorphism

9

• abstract inheritance
• subtypes
• type abstraction
• self-reference

Additional keywords and phrases: exceptions, type calculi, parametric types, coercion, ad hoc polymorphism, universal types, existential types, unfolding, intersection types

Taxonomic structure

  $\backslash A\; x\; .\; Elephant(x)\; ->\; Mammal(x)$
  $\backslash A\; x\; .\; Elephant(x)\; ->\; color(x)\; =\; gray$
  $\backslash A\; x\; .\; Penguin(x)\; ->\; Bird(x)\; /\backslash \; \backslash neg\; CanFly(x)$
  

Types as sets of values

• $V\; \backslash approx\; Int\; \backslash cup\; ...\; \backslash cup\; V\; \backslash times\; V\; \backslash cup\; V\; ->\; V$

Ideals -- over $V$

• subtypes -- ordered by set inclusion
• lattice -- $Top\; =\; V$, $Bottom\; =\; \backslash emptyset$

Type system

subtypes correspond to subsets

• a collection of ideals of V

subtyping

Function refinement

contravariance

• domain -- restrictions for the client
• range -- obligations for server

Subtyping in Emerald -- S conforms to T

• S provides at least the operations of T
• for each operation in T, the corresponding operation in S has the same number of arguments
• the type of the result of operations of S conform to those of the operations of T
• the types of arguments of operations of T conform to those of the operations of S

• static -- type checking at compile time
• strong -- all expressions are type consistent

• bitstrings, sets, $\%l$-calculus

• overloading, coercion, subranging, value-sharing (nil)

Flavors of polymorphism

• inclusion polymorphism -- to model subtypes and inheritance
• parametric polymorphism -- uniformly on a range of types
• intersection types -- coherent overloading

Inheritance -- incremental modification

• Result = Parent + Modifier

Example: $R\; =\; \{\; a1,\; a2\; \}\; +\; \{\; a2,\; a3\; \}\; =\; \{\; a1,\; a2,\; a3\; \}$

Independent attributes: M disjoint from P
Overlapping attributes: M overrules P

Dynamic binding

• $R\; =\; \{...,P\_i:\; self\; !\; A,...\}\; +\; \{\; ...,M\_j:\; self\; !\; B,\; ...\; \}$

Lambda calculus -- very informal

$\%l$

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

Lambda terms -- $ %L $

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

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

• $\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\; =\; ($\%l x.F ( xx ) ) W = F ( WW ) = FX
  

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

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

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

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

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

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

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

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

1

• abstract inheritance -- declarative relation
• inheritance networks -- non-monotonic reasoning
• taxonomic structure -- predicate calculus

1. How would you characterize inheritance as applied in knowledge representation? Discuss the problems that arise due to non-monotony.
2. How would you render the meaning of an inheritance lattice? Give some examples.
3. What is the meaning of a type? How would you characterize the relation between a type and its subtypes?
4. Characterize the subtyping rules for ranges, functions, records and variant records. Give some examples.
5. What is the intuition underlying the function subtyping rule?
6. What is understood by the notion of objects as records? Explain the subtyping rule for objects.
7. Discuss the relative merits of typed formalisms and untyped formalisms.
8. What flavors of polymorphism can you think of? Explain how the various flavors are related to programming language constructs.
9. Discuss how inheritance may be understood as an incremental modification mechanism.
10. Characterize the simple type calculus , that is the syntax, type assignment and refinement rules. Do the same for $F\_\{\; /\backslash \; \}$ and .
11. Type the following expressions: (a) $\{\; a\; =\; 1,\; f\; =\; \%l\; x:Int.\; x\; +\; 1\; \}$, (b) $\%l\; x:Int\; .\; x\; *\; x$, and (c) $\%l\; x:\{\; b:Bool,\; f:\{\; a:Bool\; \}\; \}\; ->\; Int.x.f(x)$.
12. Verify whether: (a) , (b) , and (c) .
13. Explain how you may model abstract data types as existential types.
14. What realizations of the type $\backslash E\; \%a.\; \{\; a:\%a,\; f:\%a\; ->\; Bool\; \}$ can you think of? Give at least two examples.
15. Prove that .
16. Prove that , for $\%t\; =\; \%m\; \%a.\{\; b:\; \%a\; ->\; \%a\; \}$.