论文标题
无针对分配法的定理
No-Go Theorems for Distributive Laws
论文作者
论文摘要
在计算机科学中很普遍,可以使用Beck的分配法则组成。不幸的是,查找分配定律可能非常困难且容易出错。文献包含一些构建分布定律的一般原则。但是,到目前为止,当没有分配法律存在时,还没有这样的技术来建立。 我们介绍了三个定理家族,以显示何时在两个单子之间没有分配法律。第一个广泛概括了归因于plotkin的反例。它涵盖了以前的所有已知的NO-GO结果,用于特定的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 general principles for constructing distributive laws. However, until now there have been no such techniques for establishing when no distributive law exists. We present three families of theorems for showing when there can be no distributive law between 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 and third families are entirely novel, encompassing various new practical situations. For example, they negatively resolve the open question of whether the list monad distributes over itself, reveal a previously unobserved error in the literature, and confirm a conjecture made by Beck himself in his first paper on distributive laws. In addition, we establish conditions under which there can be at most one possible distributive law between two monads, proving various known distributive laws to be unique.