# How can we directly reaching inside and looking at the state of a partially existential object?

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 reﬁnement 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 ﬁeld while restricting the visibility of its (not very interesting) private ﬁeld:

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 ﬁeld of its state.

I was wondering how to "directly reaching inside and looking at the x ﬁeld 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.

Thanks.

• 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. – Andrej Bauer Sep 8 '19 at 21:07