In  [CW85], a distinction is made between ad hoc polymorphism (which characterizes the mechanisms mentioned as common exceptions to monomorphic typing) and universal polymorphism (which allows for theoretically well-founded means of polymorphism). Universal polymorphism may take the form of inclusion polymorphism (which is a consequence of derivation by inheritance) or parametric polymorphism (which supports generic types, as the template mechanism offered by C++). See slide 9-flavors. The term inclusion polymorphism may be understood by regarding inheritance as a means to define the properties of a (sub)type incrementally, and thus (by adding information) delimiting a subset of the elements corresponding to the supertype. When overloading is done in a systematic fashion we may speak of intersection types, which allows for polymorphism based on a finite enumeration of types. See section calculi.

Inheritance as incremental modification

  $($\%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
  

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

    $$\%t ::= \%r | \%t_1 -> \%t_2
  

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


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

   $+\; :\; \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)
  };
  

  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
  

  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


  

  class event { 
   event  


  protected:
  event(event* x) : ev(x) {}
  public:
  int type() { return ev->type(); }
  void* rawevent() { return ev; }
  private:
  event* ev;
  };
  
  
  class xevent : public event { 
   X  


  public:
  int type() { return X->type(); }
  private:
  struct XEvent* X;
  };
  

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

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

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

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