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

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

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
 

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