Mitchell's notion of representation independence is a particularly useful application of Reynolds' relational parametricity --- two different implementations of an abstract data type can be shown contextually equivalent so long as there exists a relation between their type representations that is preserved by their operations. There have been a number of methods proposed for proving representation independence in pure extensions of System F, as well as in impure Java-like languages. However, none of the existing work on representation independence addresses the interaction of existential type abstraction and mutable state. Specifically, none shows how to prove equivalence of generative ADTs, for which each instance of the ADT must introduce a distinct abstract type because the relational interpretation of that type depends on some local instance-specific state.
In this work, we present a method for proving state-dependent representation independence. Our method extends Ahmed's previous work on step-indexed logical relations for recursive and quantified types in order to handle ML-style unrestricted state.We use this method to prove a number of interesting contextual equivalences, some drawn from the literature on type generativity, that involve a close interaction between existentials and state. In these examples, the relational interpretations of the abstract types may be initially empty and then grow over time in a manner that is tightly coupled with changes to some local state. We encode such state-dependent type representations using a novel possible-worlds model that is inspired by several recent approaches but relies on step-indexing to enable a well-founded quasi-circular definition of possible worlds.