From dynamic binding to state via modal possibility
From dynamic binding to state via modal possibility
复制标题
通过模态可能性从动态绑定到状态
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Aleksandar Nanevski
中科院分区：
文献类型：
--
作者：
Aleksandar Nanevski
在本文中，我们为状态(具有第二类位置)提出了一种类型化的纯函数演算，其中类型反映了从全局存储读取和写入全局存储之间的二分法。这与通常通过Monad表示状态的方式不同，在Monad中，用于读取和写入的原语引入了相同的一元类型构造函数。我们的类型系统基于构造性模态逻辑S4的证明项演算，它有两个模态类型运算符：␣表示必然性，◊表示可能性。我们使用名称(代表位置)的概念来扩展这个演算，并将其推广到模运算符的索引族(由名称集索引)。然后，模式类型␣CA对从集合C中列出的商店位置读取的类型A的计算进行分类。双重类型␣CA对首先从$C$写入位置并随后使用改变的商店来获得类型A的值的计算进行分类。首先，该语言的必需性片段本身很有趣：它形成了一个动态绑定演算。其次，可能性操作符◊是单线程，因此强制内存写入的单线程，但不强制内存读取的单线程(因为这些与␣相关联)。最后，读取和写入的不同状态提供了一种自然的方式来表示未初始化内存的分配，同时还提供了仅取消引用初始化位置的保证。
In this paper we propose a typed, purely functional calculus for state (with second-class locations) in which types reflect the dichotomy between reading from and writing into the global store. This is in contrast to the usual formulation of state via monads, where the primitives for reading and writing introduce the same monadic type constructor. We hope to argue that making this distinction is useful, simple, and has strong logical foundations.Our type system is based on the proof-term calculus for constructive modal logic S4, which has two modal type operators: ␣ for necessity and ◊ for possibility. We extend this calculus with the notion of names (which stand for locations) and generalize to indexed families of modal operators (indexed by sets of names). Then, the modal type ␣CA classifies computations of type A which read from store locations listed in the set C. The dual type ␣CA classifies computations which first write into the locations from $C$ and than use the changed store to obtain a value of type A.There are several benefits to this development. First, the necessitation fragment of the language is interesting in its own: it formulates a calculus of dynamic binding. Second, the possibility operator ◊ is a monad, thus forcing the single-threading of memory writes, but not of memory reads (as these are associated with ␣). Finally, the different status of reads and writes gives rise to a natural way of expressing the allocation of uninitialized memory while also providing guarantees that only initialized locations are dereferenced.