26.5 Bounded Existential Types

< Free Open Study >

We can add bounds to existential types (Chapter 24) just as we have done for universal types, obtaining bounded existentials as shown in Figure 26-3. As with bounded universals, the subtyping rule S-SOME comes in two flavors, one where the bounds of the two quantifiers being compared must be identical, and one where they may be different.

Figure 26-3: Bounded Existential Quantification (Kernel Variant)

26.5.1 Exercise [⋆]

What is the full variant of S-SOME?

26.5.2 Exercise [⋆]

In pure System F with records and existential types (but no subtyping), how many different ways can you find of choosing T to make

   {*Nat, {a=5,b=7}} as T;

well typed? If we add subtyping and bounded existentials, do we get more?

We saw in §24.2 how ordinary existentials can be used to implement abstract data types. When we add bounds to existential quantifiers, we obtain a corresponding refinement at the level of ADTs, dubbed partially abstract types by Cardelli and Wegner (1985). The key intuition is that a bounded existential reveals some of the structure of its representation type to the outside world, while keeping the exact identity of the representation type hidden.

For example, suppose we implement an ADT of counters as in §24.2, but add the bound Counter<:Nat to the type annotation.

   counterADT =      {*Nat, {new = 1, get = λi:Nat. i, inc = λi:Nat. succ(i)}}      as {$Counter<:Nat,          {new: Counter, get: Counter→Nat, inc: Counter→Counter}}; ▸ counterADT : {$Counter<:Nat,                        {new:Counter,get:Counter→Nat, inc:Counter→Counter}}

We can use this counter ADT exactly as we did before, binding its type and term components to the variables Counter and counter and then using the fields of counter to perform operations on counters

   let {Counter,counter} = counterADT in   counter.get (counter.inc (counter.inc counter.new)); ▸ 3 : Nat

Moreover, we are now permitted to use Counter values directly as numbers:

   let {Counter,counter} = counterADT in   succ (succ (counter.inc counter.new)); ▸ 4 : Nat

On the other hand, we are still not able to use numbers as Counters:

   let {Counter,counter} = counterADT in   counter.inc 3; ▸ Error: parameter type mismatch

In effect, in this version of the counter abstraction, we have chosen to make it easier for the outside world to use counters by revealing their representation, while retaining control over how counters can be created.

26.5.3 Exercise [⋆⋆⋆]

Suppose we want to define two abstract data types, Counter and ResetCounter, such that (1) both ADTs provide operations new, get, and inc, (2) ResetCounter additionally provides a reset operation that takes a counter and returns a new counter set to some fixed value, say 1, (3) clients of the two ADTs are allowed to use a ResetCounter in place of a Counter (i.e., we have ResetCounter <: Counter), and (4) nothing more is revealed to clients about how counters and reset counters are represented. Can this be accomplished using bounded existential packages?

We can make a similar refinement of our encodings of objects in terms of existentials from §24.2. There, the witness types of existential packages were used to represent the types of the internal states of objects, which were records of instance variables. By using a bounded existential in place of an unbounded one, we can reveal the names and types of some, but not all, of an object's instance variables to the outside world. For example, here is a counter object with a partially visible internal state that shows just its x field while restricting the visibility of its (not very interesting) private field:

   c = {*{x:Nat, private:Bool},        {state = {x=5, private=false},         methods = {get = λs:{x:Nat}. s.x,                    inc = λs:{x:Nat,private:Bool}.                            {x=succ(s.x), private=s.private}}}}       as {$X<:{x:Nat}, {state:X, methods: {get:X→Nat, inc:X→X}}}; ▸ c : {$X<:{x:Nat}, {state:X,methods:{get:X→Nat, inc:X→X}}}

As with our partially abstract counter ADT above, such a counter object gives us the choice of accessing its value either by invoking its get method or by directly reaching inside and looking at the x field of its state.

26.5.4 Exercise [⋆⋆]

Show how to extend the encoding of existentials in terms of universals from §24.3 to an encoding of bounded existentials in terms of bounded universals. Check that the subtyping rule S-SOME follows from the encoding and the subtyping rules for bounded universals.

< Free Open Study >