Principles of Object-Oriented Software Development
[] readme course preface 1 2 3 4 5 6 7 8 9 10 11 12 appendix lectures resources

talk show tell print

Self-reference

Recursive types are compound types in which the type itself occurs as the type of one of its components. Self-reference in objects clearly involves recursive types since the expression self denotes the object itself, and hence has the type of the object. In F_{%m}, our extension of F_{<=} taken from  [CoHC90], recursive types are written as %m %a. %t[%a], where %m is the recursion abstractor and %a a type variable. The dependence of %t on %a is made explicit by writing %t[%a]. We will use the type expressions %m %a.%t[%a] to type object specifications of the form %l(self).{ a_1 = e_1, ..., a_n = e_n } as indicated by the type assignment rule below. Object specifications may be regarded as class descriptions in C++ or Eiffel.

Self-reference -- recursive types

F_{ %m }


  • %t ::= ... | %m %a. %t [%a]
  • e ::= ... | %l( self ).{ a1 = e_1, ..., a_n = e_n }

Type assignment

  • \ffrac{ %G |- e_i : %t_i \hspace{1cm} (i = 1..n) }{ %G |- %l( self ).{ a1 = %t_1,.., a_n = %t_n } \e %m%a.{ a1:%t_1,.., a_n : %t_n }[%a] }

Refinement

  • \ffrac{ %G, %a <= %b |- %s <= %t }{ %G |- %m %a.%s[%a] <= %m %b.%t [%b] }
slide: A calculus for recursive types
The subtype refinement rule for recursive types states that %m %a. %s [%a] <= %m %b . %t[%b] if we can prove that %s <= %t assuming that %a <= %b. An object specification %l(self).{ ... } is a function with the type of the actual object as its domain and (naturally) also as its range. For convenience we will write an object specification as %l(self).F, where F denotes the object record, and the type of an object specification as %m %a.F[%a], where F[%a] denotes the (abstract) type of the record F. To obtain from an object specification %l(self).F the object that it specifies, we need to find some type %s that types the record specification F as being of type %s precisely when we assign the expression self in F the type %s. Technically, this means that the object of type %s is a fixed point of the object specification %l(self).F(self) which is of type %s -> %s. We write this as \Y( %l(self).F(self) ) : %s, which says that the object corresponding to the object specification is of type %s. See slide 9-recursion.

Object semantics -- fixed point $ %s = F[%s] $

  • \Y ( %l( self ).F( self ) ) : %s

Unrolling -- unraveling a type

  • %m %a.F[%a] = F[ %m %a.F[%a] ]

Example

 

  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 }

T_1, T_2 <= T, T_3 \not<= T \zline{(contravariance)}

slide: Recursive types -- examples
Finding the fixed point of a specification involves technically a procedure known as unrolling, which allows us to rewrite the type %m %a.F[%a] as F[%m %a.F[%a] ] . Notice that unrolling is valid, precisely because of the fixed point property. Namely, the object type %s is equal to %m %a.F[%a] , due to the type assignment rule, and we have that %s = F[%s] . See slide 9-ex-recursive. Unrolling allows us to reason on the level of types and to determine the subtyping relation between recursive subtypes. Consider, for example, the type declarations T and T_i (i = 1..3) above. Based on the refinement rules for object records, functions and recursive types, we may establish that T_1 <= T, T_2 <= T but T_3 \not<= T. To see that T_1 <= T, it suffices to substitute T for %a in F, where F = { a:Int, c:%a, b:%a->%a }. Since F[T] = { a:Int, c:T, b:T->T } we immediately see that T_1 only extends T with the field d:Bool, hence T_1 <= T. A similar line of reasoning is involved to determine that T_2 <= T, only we need to unroll T_2 as well. We must then establish that c:T_2 <= c:T, which follows from an application of the refinement rule. To show that T_3 \not<= T, let G[%b] = { a:Int, c:%b, b:%b->%b, d:Bool } and T_3 = %m %b.G[%b]. Then, by unrolling, T_3 = G[T_3] = { a:Int, c:T_3, b:T_3 -> T_3, d:Bool }. Now, suppose that T_3 <= T, then G[T_3] <= F[T_3] and consequently b:T_3 -> T_3 must refine b:T -> T. But from the latter requirement it follows that T_3 <= T and that T <= T_3 (by the contravariance rule for function subtyping). However, this leads to a contradiction since T is clearly not equal to T_3 because T_3 contains a field d:Bool that does not occur in T. Although analyses of this kind are to some extent satisfactory in themselves, the reader may wonder where this all leads to. In the following we will apply these techniques to show the necessity of dynamic binding and to illustrate that inheritance may easily violate the subtyping requirements.

Inheritance

In section flavors we have characterized inheritance as an incremental modification mechanism, which involves a dynamic interpretation of the expression self. In the recursive type calculus F_{%m} we may characterize this more precisely, by regarding a derived object specification C as the result of applying the modifier M to the object specification P. We employ the notation C = %l(self).P(self) \with { a_1' = e_1',...,a_k' = e_k' } to characterize derivation by inheritance, and we assume the modifier M corresponding with { a_1' = e_1', ..., a_k' = e_k' } to extend the record associated with P in the usual sense. See slide 9-self-inheritance.

Inheritance -- C = P + M

  • P = %l( self ).{ a1 = e1,...,a_n = e_n }
  • C = %l( self ).P( self ) \with \ifsli{\n}{} { a1' = e1',...,a_k' = e_k' }

Semantics -- $\Y(C) = \Y(%l( self ).M( self )(P( self )))$

  • P : %s -> %s => \Y(P):%s
  • C = %l(s).M(s)(P(s)) : %t -> %t => \Y(C):%t
slide: Inheritance semantics -- self-reference
The meaning of an object specification C is again a fixed point \Y(C), that is \Y(%l(self).M(self)(P(self))). Now when we assume that the object specification is of type %t -> %t (and hence \Y(P) of type %t), and that C is of type %s -> %s (and hence \Y(C) of type %s), then we must require that %s <= %t to obtain a properly typed derivation. We write C <= P whenever %s <= %t. A first question that arises when we characterize inheritance as incremental modification is how we obtain the meaning of the composition of two object specifications.

Object inheritance -- dynamic binding

P = %l( self ).{ i = 5, id = self }
C = %l( self ).P( self ) \with { b = true }
\Y(P):%t where %t = %m %a.{ i:int, id:%a } and P:%t->%t

Simple typing -- \Y(C):%s = { i:int, id:%t, b:bool }
Delayed -- \Y(C):%s' = %m %a.{ i:int, id:%a, b:bool }
We have %s' <= %s \zline{(more information)}

slide: Object inheritance -- dynamic binding
Let (parent) P and (child) C be defined as above. Now, if we know that the type of \Y(P) is %t then we may simply characterize \Y(C) as being of type %s = { i:Bool, id:%t, b:Bool }. However, when we delay the typing of the P component (by first composing the record specifications before abstracting from self) then we may obtain %s' = %m %a.{ i:Int, id:%a, b:Bool } as the type of \Y(C). By employing the refinement rule and unrolling we can show that %s' <= %s. Hence, delayed typing clearly provides more information and must be considered as the best choice. Note, however, that both %s' <= %t and %s <= %t hold. See slide 9-self-dynamic. A second, important question that emerges with respect to inheritance is how self-reference affects the subtyping relation between object specifications related by inheritance. Consider the object specifications P and C given in slide 9-self-contravariance. In the (derived) specification C, the method eq is redefined to include an equality test for the b component. However, when we determine the object types corresponding to the specifications P and C we observe that C \not<= P.

Contravariance
  • 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)
   }

\Y(P) : %t where %t = %m %a.{ i:int, eq:%a -> bool }
\Y(C):%s where %s = %m %a.{ i:int, id:%a -> bool, b: bool }
However %s \not<= %t \zline{(subtyping error)}

slide: Object inheritance -- contravariance
The reasoning is as follows. For \Y(P) : %t and \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 \not<= %t. We have a problem here, since the fact that C \not<= P means that the type checker will not be able to accept the derivation of C from P, although C is clearly dependent on P. The solution to our problem lies in making the type dependency involved in deriving C from P explicit. Notice, in this respect, that in the example above we have omitted the type of the abstraction variable in the definition of eq, which would have to be written as %l x:\Y(P).x.i = self.i (and in a similar way for C ) to do it properly.

Type dependency

The expression self is essentially of a polymorphic nature. To make the dependency of object specification on self explicit, we will employ an explicit type variable similar as in F_{<=} . Let F[%a] stand for { a_1 : %t_1,...,a_n:%t } as before. We may regard F[%a] as a type function, in the sense that for some type %t the expression F[%t] results in a type. To determine the type of an object specification we must find a type %s that satisfies both %s <= F[%s] and F[%s] <= %s.

Type dependency -- is polymorphic
  • Let F[%a] = { m_1:%s_1,...,m_j:%s_j } \zline{(type function)}
  • P:\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: \Y(P[%s]) for %s = %m t.F[t]\n We have P[%s]:%s -> F[%s] because F[%s] = %s

slide: Bounded type constraints
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 \A %a <= F[%a]. %a -> F[%a]. The constraint that %a <= F[%a], which is called an F-bounded constraint, requires that the subtype substituted for %a is a (structural) refinement of the record type F[%a]. As before, we have that \Y(P[%s]) = %s with %s = %m %a.F[%a], which differs from our previous definition only by making the type dependency in P explicit. See slide 9-dependency. Now, when applying this extended notion of object specification to the characterization of inheritance, we may relax our requirement that \Y(C) must be a subtype of \Y(P) into the requirement that G[%a] <= F[%a] for any %a, where F is the record specification of P and G the record specification of C.

Inheritance

 

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

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 \Y(C[%s]) \not<=_{subtype} \Y(P[%t])

slide: Inheritance and constraints
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 \Y(C[%s]) : %s and \Y(P[%t]) : %t we (still) have that %s \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.

Discussion -- Eiffel is not type consistent

 We have limited our exploration of the recursive structure of objects to (polymorphic) object variables. Self-reference, however, may also occur to class variables. The interested reader is referred to  [CoHC90]. The question that interests us more at this particular point is what benefits we may have from the techniques employed here and what lessons we may draw from applying them. One lesson, which should not come as a surprise, is that a language may allow us to write programs that are accepted by the compiler yet are behaviorally incorrect. However, if we can determine syntactically that the subtyping relations between classes is violated we may at least expect a warning from the compiler. So one benefit, possibly, is that we may improve our compilers on the basis of the type theory presented in this chapter. Another potential benefit is that we may better understand the trade-offs between the particular forms of polymorphism offered by our language of choice. The analysis given in  [CoHC90] indeed leads to a rather surprising result. Contrary to the claims made by its developer,  [CoHC90] demonstrate that Eiffel is not type consistent. The argument runs as follows. Suppose we define a class C with a method eq that takes an argument of a type similar to the type of the object itself (which may be written in Eiffel as like Current). We further assume that the class P is defined in a similar way, but with an integer field i and a method eq that tests only on i. See slide 9-self-eiffel.

Inheritance != subtyping

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
slide: Inheritance and subtyping in Eiffel
We may then declare variables v and p of type P. Now suppose that we have an object c of type C, then we may assign c to v and invoke the method eq for v, asking whether p is equal to v, as in 


  p,v:P, c:C 
  
  v:=c; 
  v.eq(p);   // error p has no b
slide: Example
Since v is associated with an instance of C, but syntactically declared as being of type P, the compiler accepts the call. Nevertheless, when p is associated with an instance of P trouble will arise, since (due to dynamic binding) the method eq defined for C will be invoked while p not necessarily has a field b. When we compare the definition of C in Eiffel with how we may define C in C++, then we are immediately confronted with the restriction that we do not have such a dynamic typing mechanism as like Current in C++. Instead, we may use overloading, as shown in slide 9-self-cc. 


  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; }
  };
slide: Inheritance and subtyping in C++
When we would have omitted the P variant of eq, the compiler complains about hiding a virtual function. However, the same problem arises when we define eq to be virtual in P, unless we take care to explicitly cast p into either a C or P reference. (Overloading is also used in  [Liskov93] to solve a similar problem.) In the case we choose for a non-virtual definition of eq, it is determined statically which variant is chosen and (obviously) no problem occurs. Considering that determining equality between two objects is somehow orthogonal to the functionality of the object proper, we may perhaps better employ externally defined overloaded functions to express relations between objects. This observation could be an argument to have overloaded functions apart from objects, not as a means to support a hybrid approach but as a means to characterize relations between objects in a type consistent (polymorphic) fashion.
[] readme course preface 1 2 3 4 5 6 7 8 9 10 11 12 appendix lectures resources
eliens@cs.vu.nl

draft version 0.1 (15/7/2001)