Bounded polymorphism

Instructor's Guide

intro, inheritance, subtypes, polymorphism, types, hiding, self-reference, summary, Q/A, literature
Our next extension, which we call F \leqslant , involves (bounded) universal quantification. For technical reasons we need to introduce a primitive type Top, which may be considered as the supertype of all types (including itself). Also we need type abstraction variables, that we will write as F \leqslant and F \leqslant . Our notation for a universally quantified (bounded) type is F \leqslant , which denotes the type F \leqslant with the type variable α replaced by any subtype α of σ. In a number of cases, we will simply write σ, which must be read as \A α\leqslant Top. τ. Recall that any type is a subtype of Top. Observe that, in contrast to λ \leqslant and λ \leqslant , the calculus F \leqslant is second order (due to the quantification over types). In addition to the (value) expressions found in the two previous calculi, F \leqslant introduces a type abstraction expression of the form Λ α\leqslant τ.e and a type instantiation expression of the form e[τ]. The type abstraction expression e[τ] is used in a similar way as the function abstraction expression, although the abstraction involves types and not values. Similar to the corresponding type expression, we write Λ α.e as an abbreviation for Λ α.e. The (complementary) type instantiation statement is written as e[τ], which denotes the expression e in which the type identifier τ is substituted for the type variable bound by the first type abstractor.
τ
slide: The bounded type calculus
 The type assignment rule for type abstraction states that, when we may type an expression e as being of type τ (under the assumption that τ), then we may type Λ α\leqslant σ.e as being of type \A α\leqslant σ.τ. The type assignment rule for type instantiation characterizes the relation between type instantiation and substitution (which is notationally very similar). When we have an expression e of type \A α\leqslant σ.τ and we have that σ′\leqslant σ, then σ′\leqslant σ is of type τ[ α: = σ′], which is τ[ α: = σ′] with τ[ α: = σ′] substituted for τ[ α: = σ′]. See slide 9-c-bounded. The refinement rule for bounded types states the subtyping relation between two bounded types. We have that τ[ α: = σ′] is a subtype of τ[ α: = σ′] whenever σ\leqslant σ′ and σ\leqslant σ′. Notice that the relation is contravariant with respect to the types bounding the abstraction, similar as for the domains of function subtypes in the function subtyping rule. In contrast to the polymorphism due to object type extensions and overloading, bounded polymorphism (employing type quantifiers) is an example of what we have called parametric polymorphism. In effect, this means that we must explicitly give a type parameter to instantiate an object or function of a bounded (parametric) type, similar to when we use a template in C++. The examples given in slide 9-ex-parameters illustrate how we may define and subsequently type parametric functions. In these examples, we employ the convention that in the absence of a bounding type we assume Top as an upper limit. The examples are taken from  [CW85].
  
  
slide: Parametrized types -- examples
 The (generic) identity function id is defined as   
   , which states that when we supply a particular type, say Int, then we obtain the function   
   . Since the actual type used to instantiate id is not important, we may type id as being of type   
   . In a similar way, we may define and type the two (generic) variants of the function twice. Notice the difference between the two definitions of twice. The first variant requires the function argument itself to be of a generic type, and fails (is incorrectly typed) for the successor function S which is (non generic) of type   
   . In contrast, the second variant accepts S, and we may rely on the automatic conversion of   
   to id [ Int ] : Int → Int (based on the second type assignment rule) to accept id as well. The interplay between parametric and inclusion polymorphism is illustrated in the examples presented in slide 9-ex-quantification. Recall that inclusion polymorphism is based on the subtyping relation between records (which states that refinement of a record type involves the addition of components and/or refinement of components that already belong to the super type).
  
  • g = Λ α\leqslant {one : Int}. λx: α. (x.one) g : \A α\leqslant {one : int}. α→ Int

  • g′ = Λ β. Λ α\leqslant {one : β}. λx: α. (x.one) g′: \A β. \A α\leqslant {one : β}. α→ β
  • move = Λ α\leqslant Point. λp:α. λd : Int .(p.x : = p.x + d); p move : \A α\leqslant Point.  α→ Int → α
  
  • g′[ Int ][ {one:Int, two : Bool}]({one = 3, two = true}) = 3

  • move [{x : Int, y : Int}]( {x = 0, y = 0} )(1) = {x = 1, y = 0}

slide: Bounded quantification -- examples
 The first example defines a function g that works on a record with at least one component one and delivers as a result the value of the component one of the argument record. The function   
  • g = Λ α\leqslant {one : Int}. λx: α. (x.one) g : \A α\leqslant {one : int}. α→ Int

  • g′ = Λ β. Λ α\leqslant {one : β}. λx: α. (x.one) g′: \A β. \A α\leqslant {one : β}. α→ β
  • move = Λ α\leqslant Point. λp:α. λd : Int .(p.x : = p.x + d); p move : \A α\leqslant Point.  α→ Int → α
  
  • g′[ Int ][ {one:Int, two : Bool}]({one = 3, two = true}) = 3

  • move [{x : Int, y : Int}]( {x = 0, y = 0} )(1) = {x = 1, y = 0}

is a generalized version of g that abstracts from the particular type of the one component. Notice that both g and   
  • g = Λ α\leqslant {one : Int}. λx: α. (x.one) g : \A α\leqslant {one : int}. α→ Int

  • g′ = Λ β. Λ α\leqslant {one : β}. λx: α. (x.one) g′: \A β. \A α\leqslant {one : β}. α→ β
  • move = Λ α\leqslant Point. λp:α. λd : Int .(p.x : = p.x + d); p move : \A α\leqslant Point.  α→ Int → α
  
  • g′[ Int ][ {one:Int, two : Bool}]({one = 3, two = true}) = 3

  • move [{x : Int, y : Int}]( {x = 0, y = 0} )(1) = {x = 1, y = 0}

may be applied to any record that conforms to the requirement stated in the bound, such as the record   
  • g = Λ α\leqslant {one : Int}. λx: α. (x.one) g : \A α\leqslant {one : int}. α→ Int

  • g′ = Λ β. Λ α\leqslant {one : β}. λx: α. (x.one) g′: \A β. \A α\leqslant {one : β}. α→ β
  • move = Λ α\leqslant Point. λp:α. λd : Int .(p.x : = p.x + d); p move : \A α\leqslant Point.  α→ Int → α
  
  • g′[ Int ][ {one:Int, two : Bool}]({one = 3, two = true}) = 3

  • move [{x : Int, y : Int}]( {x = 0, y = 0} )(1) = {x = 1, y = 0}

. As another example of employing bounds to impose requirements, look at the function move that is defined for subtypes of Point (which we assume to be a record containing x and y coordinates). It expects a record (that is similar to or extends Point) and an (integer) distance, and as a result delivers the modified record.

Discussion

 Parametric polymorphism is an important means to incorporate subtyping in a coherent fashion. Apart from  [Pierce93], from which we have taken most of the material presented here, we may mention  [PA93] as a reference for further study. In  [Pierce93] a calculus   
  • g = Λ α\leqslant {one : Int}. λx: α. (x.one) g : \A α\leqslant {one : int}. α→ Int

  • g′ = Λ β. Λ α\leqslant {one : β}. λx: α. (x.one) g′: \A β. \A α\leqslant {one : β}. α→ β
  • move = Λ α\leqslant Point. λp:α. λd : Int .(p.x : = p.x + d); p move : \A α\leqslant Point.  α→ Int → α
  
  • g′[ Int ][ {one:Int, two : Bool}]({one = 3, two = true}) = 3

  • move [{x : Int, y : Int}]( {x = 0, y = 0} )(1) = {x = 1, y = 0}

is also introduced in which intersection polymorphism is expressed by means of an explicit type variable. The resulting type may be written as \A α  ∈  {…}, where \A α  ∈  {…} denotes a finite collection of types. As already mentioned, intersection types may also be used to model inclusion polymorphism (see Castagna {\it et al.}, 1993).\index{Castagna {\it et al.} (1993)} It is an interesting research issue to explore the relation between parametric polymorphism and inclusion polymorphism further along this line. However, we will not pursue this line here. Instead, in the next section we will look at another application of parametric polymorphism, namely existential types that allow us to abstract from hidden component types. This treatment is based on  [CW85]. In the last section of this chapter, we will look in more detail at the role of self-reference in defining (recursive) object types, following  [CoHC90]. We will conclude this chapter with some observations concerning the relevance of such type theories for actual programming languages. In particular, we will show that Eiffel is not type consistent.

Type abstraction in C++

 Type abstraction in C++ may occur in various guises. One important means of type abstraction is to employ what we have called polymorphic base class hierarchies. For example, the function move, which was somewhat loosely characterized in slide 9-ex-quantification, may be defined in C++ as follows: 
  Point* move(Point* p, int d); 
 require int Point::x

  Point* move(Point* p, int d) { p.x += d; return p; }
slide: example move
 In effect, the function move accepts a pointer to an instance of Point, or any class derived from Point, satisfying the requirement that it has a public integer data member x. Similar restrictions generally hold when instantiating a template class, but in contrast to base class subtyping requirements, these restrictions will only be verified at link time. 
  template< class T > 
 requires T::value()

  class P {
  public:
  P(T& r) : t(r) {}
  int operator==( P<T>& p) {
  	return t.value() == p.t.value();
  	}
  private:
  T& t;
  };
slide: Type abstraction in C++
 Consider the template class definition given in slide 9-cc-abs. Evidently, for the comparison function to operate properly, each instantiation type substituted for the type parameter T must satisfy the requirement that it has a public member function value. 
  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;
  };
slide: Type instantiation
 Such a requirement may also be expressed by defining an abstract class A defining a pure virtual member function value. See slide 9-cc-abs-2. The restrictions on instantiating P may then be stated informally as the requirement that each instantiation type T must be a subtype of A for arbitrary type X. The class Int is an example of a type complying with the implicit requirements imposed by the definition of P. An example of using P is given below 
  Int i1, i2;
  P<Int> p1(i1), p2(i2);
  if ( p1 == p2 ) cout << "OK" << endl; 
 OK
slide: Example P
 Note, however, that the derivation of A<int> is by no means necessary or in any way enforced by C++.