paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Strict and lazy semantics for effects: layering monads and comonads

效果的严格与惰性语义:层叠 monad 与 comonad
ICFP 2(ICFP)2018匹配度 2/10 · 论文研究函数式语言中 monad/comonad 效果的形式语义与严格性/惰性对偶,属于 PL 理论基础,但与用户核心关注的静态分析、Agentic/LLM 程序分析、浮点程序分析、贝叶斯程序分析及其与 LLM 的交叉均无直接关联。引用 1 inbox
Andrew K. Hirsch, Ross Tate
crossref: 2026-09-10

AI 速览

一句话:构造出一对无法用分配律赋予语义的效果实例,并将其与严格性/惰性对偶联系起来。

论文关注可分别用 monad 和 comonad 刻画语义的两类效果。现有同时包含这两类效果的程序通常依赖分配律(distributive law)来组合语义,但已知并非任意 monad-comonad 对都有分配律;此前尚不清楚是否存在现实的效果对无法用该方式语义化。作者构造了一对这样的效果,说明分配律方法并不普遍适用,并指出该例子与严格性和惰性的对偶紧密相关。论文进一步从效果视角解释这一对偶,为 monad 与 comonad 的分层语义提供了边界与洞见。

问题
同时包含 monad 型效果与 comonad 型效果的程序应如何组合语义;是否存在现实中无法通过分配律语义化的效果对。
方法
通过范畴论语义分析,构造一对不存在分配律的 monad-comonad 效果实例,并将其与严格性/惰性对偶建立联系。
评估
以理论构造与语义论证为主:给出反例回答开放问题,并从效果视角讨论严格性与惰性的对偶。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@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}
}