一句话:构造出一对无法用分配律赋予语义的效果实例,并将其与严格性/惰性对偶联系起来。
论文关注可分别用 monad 和 comonad 刻画语义的两类效果。现有同时包含这两类效果的程序通常依赖分配律(distributive law)来组合语义,但已知并非任意 monad-comonad 对都有分配律;此前尚不清楚是否存在现实的效果对无法用该方式语义化。作者构造了一对这样的效果,说明分配律方法并不普遍适用,并指出该例子与严格性和惰性的对偶紧密相关。论文进一步从效果视角解释这一对偶,为 monad 与 comonad 的分层语义提供了边界与洞见。
Two particularly important classes of effects are those that can be given semantics using a monad and those that can be given semantics using a comonad. Currently, programs with both kinds of effects are usually given semantics using a technique that relies on a distributive law. While it is known that not every pair of a monad and a comonad has a distributive law, it was previously unknown if there were any realistic pairs of effects that could not be given semantics in this manner. This paper answers that question by giving an example of a pair of effects that cannot be given semantics using a distributive law. Our example furthermore is intimately tied to the duality of strictness and laziness. We discuss how to view this duality through the lens of effects.
@article{paperbot273,
title = {Strict and lazy semantics for effects: layering monads and comonads},
author = {Andrew K. Hirsch and Ross Tate},
journal = {Proceedings of the ACM on Programming Languages},
volume = {2},
number = {ICFP},
year = {2018},
doi = {10.1145/3236783}
}