单子与效应的语义结合
编程语言
2014-01-22 v1
摘要
Wadler 和 Thiemann 通过语法对应以及关于操作语义的可靠性结果，将类型与效应系统（type-and-effect systems）与单子语义（monadic semantics）统一起来。他们推测，可以给出一种通用的、“连贯的”指称语义，以将效应系统与单子风格的语义统一起来。我们基于引入的索引单子（indexed monad）的新颖结构，提供了这样一种语义。我们用（强）索引单子重新定义了 Moggi 的计算 lambda 演算的语义，这在指称的索引与传统效应系统的效应标注之间建立了一一对应关系。对偶地，该方法产生了索引余单子（indexed comonads），为上下文效应概念（称为余效应，coeffects）提供了统一的语义和效应系统，我们此前已对此进行过描述。
引用
@article{arxiv.1401.5391,
title = {The semantic marriage of monads and effects},
author = {Dominic Orchard and Tomas Petricek and Alan Mycroft},
journal= {arXiv preprint arXiv:1401.5391},
year = {2014}
}
备注
extended abstract