Types and Programming Languages by Pierce says in Section 26.5 Bounded Existential Types, about partial existential objects implemented in terms of bounded existential types:

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.

I was wondering how to "directly reaching inside and looking at the x field of its state"? For example?

Why can we do it? Although we know the bound of the type component is {x:Nat}, we still don't know the type component of a specific partial existential objects.


  • $\begingroup$ What? We can write c.state.x and know it's going to be a Nat. That's direct access to the x field of the state field of c. $\endgroup$ – Andrej Bauer Sep 8 '19 at 21:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.