ch:existential-types: ch:existential-types

Problem and result. Extend the checker with packages, run two counter representations through two increments, compare their $\mathbb{N}$ observations, and reject leaking clients and fixed-record selection.

Representation. Keep the hidden constructor existential in the checker and use two concrete run-time package representations. Erasing packages early would simplify evaluation but lose the scope check on the unpacking result type.

First complete version. Add named existential formation, packing, unpacking, and the call-by-value package contraction. Check that the unpacking result is formed outside the hidden-constructor scope before evaluating.

Remaining cases. Implement unary and pair counters, execute two increments, and observe $2$. Then try returning the state, returning a hidden-typed function, and selecting $\mathsf{port}$ from a fixed record.

A failing version. Admitting the first leaking client changes the third line to FAIL. The mutation typechecks because it changes the modeled boundary, not Kappa’s own type system.

Acceptance test. Require equal natural-number observations, both leak rejections, fixed-record rejection, mutation failure, and an empty audit.

Mathematical boundary. The paired run compares one concrete representation-independence observation. It does not prove the logical relation or decide representation independence.