Principles of Object-Oriented Software Development

[] readme course preface 1 2 3 4 5 6 7 8 9 10 11 12 appendix lectures resources

Existential types -- hiding

Existential types were introduced in [CW85] to model aspects of data abstraction and hiding. The language introduced in [CW85] is essentially a variant of the typed lambda calculi we have looked at previously. Our new calculus, that we call

F_{ \E }

, is an extension of

F_{ <= }

with type expressions of the form

\E %a <= %s. %t

(to denote existential types) and expressions of the form

pack[ %a = %s   in   %t ]

(to denote values with hidden types). Intuitively, the meaning of the expression

pack[ %a = %s   in   %t ]

is that we represent the abstract type

%a

occurring in the type expression

%t

by the actual type

%s

(in order to realize the value e). Following the type assignment rule, we may actually provide an instance of a subtype of the bounding type as the realization of a hidden type. See slide 9-existential.

Existential types -- hiding

$F_{ \E }$

$%t ::= ... | \E %a <= %t_1. %t_2$
$e ::= ... | pack[ %a = %s in %t ]. e$

Type assignment

\ffrac{ $%G |- %s' <= %s$ \hspace{1cm} $%G |- e : %t$ }{ $pack[ %a = %s' in %t ].e \e \E %a <= %s. %t$ }

Refinement

\ffrac{ $%G |- %s <= %s'$ \hspace{1cm} $%G |- %t' <= %t$ }{ $%G |- \E %a <= %s' . %t' <= \E %a <= %s. %t$ }

slide: The existential type calculus

The subtyping refinement rule is similar to the refinement rule for universally quantified types. Notice also here the contravariance relation between the bounding types. More interesting is what bounding types allow us to express. (As before, we will write

\E %a . %t

to denote

\E %a <= Top. %t

.) First, existential types allow us to indicate that the realization of a particular type exists, even if we do not indicate how. The declaration

e : \E %a . %t

tells us that there must be some type

%s

such that e of type

%t

can be realized. Apart from claiming that a particular type exists, we may also provide information concerning its structure, while leaving its actual type undetermined.

Structure -- indeterminacy

$Top = \E %a.%a$ \zline{the biggest type}
$AnyPair = \E %a \E %b.%a \* %b$ \zline{any pair}
$(3,4):\E %a.%a ${\em -- does not provide sufficient structure!}$
$(3,4):\E %a.%a \* %a

Information hiding

$\E %a.%a \* ( %a->Int )$ \zline{object, operation}
$x : \E %a. %a \* ( %a->Int )$ \zline{ $ \leadsto $ $snd ( x )( fst( x ))$ }

slide: Existential types -- examples

For example, the type

\E %a.%a

(which may clearly be realized by any type) carries no information whatsoever, hence it may be considered to be equal to the type Top. More information, for example, is provided by the type

\E %a \E %b. %a \* %b

which defines the product type consisting of two (possibly distinct) types. (A product may be regarded as an unlabeled record.) The type

\E %a. %a \* %a

gives even more information concerning the structure of a product type, namely that the two components are of the same type. Hence, for the actual product

(3,4)

the latter is the best choice. See slide 9-ex-existential. Existential types may be used to impose structure on the contents of a value, while hiding its actual representation. For example, when we have a variable x of which we know that it has type

\E %a. %a \* ( %a -> Int )

then we may use the second component of x to produce an integer value from its first component, by

snd(x)( fst(x) )

, where fst extracts the first and snd the second component of a product. Clearly, we do not need to know the actual representation type for

%a

. A similar idea may be employed for (labeled) records. For example, when we have a record x of type

\E %a.{ val : %a, op : %a -> Int }

then we may use the expression

x.op(x.val)

to apply the operation op to the value val. Again, no knowledge of the type of val is required in this case. However, to be able to use an element of an existential type we must provide an actual representation type, by instantiating the type parameter in a pack statement.

Abstract data types -- packages

$x:\E %a.{ val : %a, op : %a -> Int }$
$x = pack[%a = Int in { val:%a, op:%a -> Int } ]((3,S))$
$x.op(x.val) = 4$

Encapsulation

$pack [ representation in interface ]( contents )$

interface -- type $\E %a. { val : %a, op : %a -> Int }$
representation -- $%a = Int$ \zline{(hidden data type)}
contents -- $(3,S)$

slide: Packages -- examples

The pack statement may be regarded as an encapsulation construct, allowing us to protect the inner parts of an abstract data type. When we look more closely at the pack statement, we can see three components. First, we have an interface specification corresponding to the existential type associated with the pack expression. Secondly, we need to provide an actual representation of the hidden type, Int in the example above. And finally, we need to provide the actual contents of the structure. See slide 9-ADT. In combination with the notion of objects as records, existential types provide us with a model of abstract data types. Real objects, however, require a notion of self-reference that we have not captured yet. In the next section we will conclude our exploration of type theories by discussing the

F_{%m}

calculus that supports recursive (object) types and inheritance.

Hiding in C++

Naturally, the classical way of data hiding in C++ is to employ private or protected access protection. Nevertheless, an equally important means is to employ an abstract interface class in combination with forwarding.


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

slide: Hiding in C++

For example, as depicted in slide 9-cc-hide, we may offer the user a class event which records information concerning events occurring in a window environment, while hiding completely the underlying implementation. The actual xevent class realizing the type event may itself need access to other structures, as for example those provided by the X window environment. Yet, the xevent class itself may remain entirely hidden from the user, since events are not something created directly (note the protected constructor) but only indirectly, generally by the system in response to some action by the user.

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