摘要
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 various pure extensions of System F (where data abstraction is achieved through existential typing), as well as in Algol- or Java-like languages (where data abstraction is achieved through the use of local mutable state). However, none of these approaches addresses the interaction of existential type abstraction and local state. In particular, none allows one to prove representation independence results for generative ADTs -- i.e. ADTs that both maintain some local state and define abstract types whose internal representations are dependent on that local state.
In this paper, we present a syntactic, logical-relations-based method for proving representation independence of generative ADTs in a language supporting polymorphic types, existential types, general recursive types, and unrestricted ML-style mutable references. We demonstrate the effectiveness of our method by using it to prove several interesting contextual equivalences that involve a close interaction between existential typing and local state, as well as some well-known equivalences from the literature (such as Pitts and Stark's "awkward" example) that have caused trouble for previous logical-relations-based methods.
The success of our method relies on two key technical innovations. First, in order to handle generative ADTs, we develop a possible-worlds model in which relational interpretations of types are allowed to grow over time in a manner that is tightly coupled with changes to some local state. Second, we employ a step-indexed stratification of possible worlds, which facilitates a simplified account of mutable references of higher type.
摘要译文
一个抽象数据类型的两个不同的实现可以在上下文中等同显示，只要它们的类型表示之间存在一个由它们的操作保留的关系。已经提出了许多用于证明系统F的各种纯粹扩展中的表示独立性（其中通过存在式键入来实现数据抽象）的方法，以及Algol或Java类语言（通过使用局部可变状态来实现数据抽象）。然而，这些方法都没有涉及存在型抽象和本地状态的交互。尤其是，没有人允许证明生成ADT的表示无关结果 - 即ADT既保持一些本地状态，又定义内部表示依赖于本地状态的抽象类型。在本文中，我们提出一个句法，基于逻辑关系的方法，以支持多态类型的语言证明生成ADT的表示独立性，存在类型，一般递归类型，和不受限制的ML风格的可变引用。我们证明了我们的方法的有效性，用它来证明几个有趣的上下文等价关系，它涉及存在性类型和本地状态之间的密切相互作用，以及文献中的一些众所周知的等价（比如Pitts和Stark的“尴尬”的例子），这些为以前的基于逻辑关系的方法造成了麻烦。我们的方法的成功取决于两个关键的技术创新。首先，为了处理生成的ADT，我们开发了一个可能的世界模型，在这个模型中，类型的关系解释可以随着时间的推移而增长，这种方式与某些地方国家的变化密切相关。第二，我们对可能的世界采用逐步索引的分层，这有助于简化对较高类型可变引用的说明。
Amal Ahmed[1];Derek Dreyer[2];Andreas Rossberg[2]. State-dependent representation independence[J]. ACM SIGPLAN Notices, 2009,44(1): 340-353