Representing layered monads
Representing layered monads
复制标题
表示分层单子
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
Andrzej Filinski
中科院分区：
文献类型：
--
作者：
Andrzej Filinski
已经有相当多的研究在构建模块化的，基于单子的计算效果规范（状态，异常，非确定性等）。在编程语言中。我们提出了一个简单的框架，在这个传统的基础上，教堂式的效果类型系统ML类语言。这种语言的语义是由一系列一元翻译正式定义的，每一个翻译都扩展了一层效果。这样的分层规范很容易推理，但是它的直接实现（无论是通过参数化解释还是通过实际翻译）通常都是非常低效的。然而，通过利用monad的更深层次的语义属性，也可以得到一个更高效的实现：我们表明，每一层的影响，可以统一模拟连续通过，并且进一步地，多个这样的层本身可以通过用于call/cc和可变状态的标准语义来模拟。因此，即使是多效果程序也可以在Scheme或SML/NJ中以完全的本地速度执行，从而推广了早期的单效果结果。作为一个例子，我们展示了如何一个简单的基于并行的语义，使我们能够直接模拟一个共享状态的程序在所有可能的动态交织的执行线程。
There has already been considerable research on constructing modular, monad-based specifications of computational effects (state, exceptions, nondeterminism, etc.) in programming languages. We present a simple framework in this tradition, based on a Church-style effect-typing system for an ML-like language. The semantics of this language is formally defined by a series of monadic translations, each one expanding away a layer of effects. Such a layered specification is easy to reason about, but its direct implementation (whether by parameterized interpretation or by actual translation) is often prohibitively inefficient.By exploiting deeper semantic properties of monads, however, it is also possible to derive a vastly more efficient implementation: we show that each layer of effects can be uniformly simulated by continuation-passing, and further that multiple such layers can themselves be simulated by a standard semantics for call/cc and mutable state. Thus, even multi-effect programs can be executed in Scheme or SML/NJ at full native speed, generalizing an earlier single-effect result. As an example, we show how a simple resumption-based semantics of concurrency allows us to directly simulate a shared-state program across all possible dynamic interleavings of execution threads.