一句话：提出两类 No-Go 定理，判定两个 monad 间不存在 Beck 分配律，统一并扩展已有结果。
Monad 在计算机科学中广泛使用，并可通过 Beck 分配律进行复合，但寻找分配律十分困难且易错；此前文献只有构造分配律的原则，缺乏证明其不存在的一般技术。本文提出两族定理，用于证明两个 monad 之间不存在分配律。第一族大幅推广了归功于 Plotkin 的反例，覆盖所有已知针对特定 monad 对的 No-Go 结果，并给出许多新结论；第二族完全新颖，可处理多种新的实际情形，例如否定性地解决了 list monad 是否可分配于自身的开放问题，并揭示了文献中一个此前未被注意的错误。
Monads are commonplace in computer science, and can be composed using Beck's distributive laws. Unfortunately, finding distributive laws can be extremely difficult and error-prone. The literature contains some principles for constructing distributive laws. However, until now there have been no general techniques for establishing when no such law exists. We present two families of theorems for showing when there can be no distributive law for two monads. The first widely generalizes a counterexample attributed to Plotkin. It covers all the previous known no-go results for specific pairs of monads, and includes many new results. The second family is entirely novel, encompassing various new practical situations. For example, it negatively resolves the open question of whether the list monad distributes over itself, and also reveals a previously unobserved error in the literature.
DOI 原文 ·
@inproceedings{paperbot4993,
title = {No-Go Theorems for Distributive Laws},
author = {Maaike Zwart and Dan Marsden},
booktitle = {LICS},
year = {2019},
doi = {10.1109/lics.2019.8785707}
}