Factorisation Systems for Logical Relations and Monadic Lifting in Type-and-effect System Semantics
Factorisation Systems for Logical Relations and Monadic Lifting in Type-and-effect System Semantics
复制标题
类型与效果系统语义中逻辑关系和单子提升的因式分解系统
DOI：
10.1016/j.entcs.2018.11.012
复制
发表时间：
2018
影响因子：
--
通讯作者：
Kammar O
中科院分区：
文献类型：
--
作者：
Kammar O
类型和效果系统包含有关计算效果的信息，例如状态突变、概率选择或 I/O，程序短语可以与其返回值一起调用。类型和效果系统的语义涉及参数化的单子族，其大小与效果的数量呈指数关系。我们从一个类别上的单个单子、这个单子的代数运算的选择以及这个类别上合适的因式分解系统中导出如此精致的语义。我们使用逻辑关系的纤维化将派生语义与原始语义联系起来。我们的证明使用民间传说技术来通过操作提升单子。
Type-and-effect systems incorporate information about the computational effects, e.g., state mutation, probabilistic choice, or I/O, a program phrase may invoke alongside its return value. A semantics for type-and-effect systems involves a parameterised family of monads whose size is exponential in the number of effects. We derive such refined semantics from a single monad over a category, a choice of algebraic operations for this monad, and a suitable factorisation system over this category. We relate the derived semantics to the original semantics using fibrations for logical relations. Our proof uses a folklore technique for lifting monads with operations.