一个非平凡的余单半群是什么样子？

Question

“Comonoids”在编程语言Haskell的distributive库文档中被提到：

由于Haskell中缺乏非平凡的共余子代数，我们可以将自己限制为要求一个Functor，而不是一些Coapplicative类。

经过一番搜索，我找到了一个StackOverflow答案，其中解释了共余子代数必须满足的定律。因此，我认为我明白了为什么在Haskell中假设Comonoid类型类只有一种可能的实例。

因此，要找到一个非平凡的comonoid，我想我们必须在其他类别中寻找。当然，如果范畴论者有一个共余子代数的名称，那么一定有一些有趣的例子。该页面上的其他答案似乎暗示了涉及Supply的一个例子，但我无法找到一个仍然符合定律的例子。

我还查阅了维基百科：有一个关于幺半群的页面，没有提及范畴论，这对于Haskell中的Monoid类型类来说似乎是一个足够描述，但是“余幺半群”会重定向到一个我无法理解的关于幺半群和余幺半群的范畴论描述，而且仍然没有任何有趣的例子。

所以我的问题是：

1. 能否像幺半群一样用非范畴论术语解释余幺半群？
2. 什么是一个简单的有趣的余幺半群示例，即使它不是Haskell类型？（可以在熟悉的Haskell单子上找到Kleisli类别中的一个吗？）

编辑： 我不确定这是否实际上是范畴论正确的，但我在问题2的括号里想象的是某个特定的Haskell类型a和Haskell单子m的非平凡定义，满足链接答案中的Kleisli箭头版本的余幺半群定律。其他余幺半群的例子仍然受欢迎。

- betaveros

---

Kleisli箭头版本的余单子律是什么？假设我有Z_n代表a，[]代表m，我的运算符是：delete _ = []; split x = [(0, x), (1, x+1), ... (n-1, x+n-1)]（所有加法都是模n的）。我如何检查是否满足这些定律？如果我想要检查idL $ first delete $ split x = x，我该如何将其提升到[]单子中？ - n. m.

再多考虑一下，如果你只是将定律提升到具有 return、fmap 和 bind 的单子上，那么这些提升后的定律会与普通的余半群定律完全等价，因此你仍然只有微不足道的实例。 - n. m.

Answer 1

正如Phillip JF提到的，对于半结构逻辑来说，共同体是一个有趣的讨论话题。让我们谈谈线性λ演算。这很像您平常使用的类型化lambda演算，只不过每个变量必须正好使用一次。

为了感受一下，让我们计算给定类型的线性函数，也就是说，

a -> a

具有唯一的一个元素 id。 而

(a,a) -> (a,a)

有两个变量，id 和 flip。请注意，在常规的 lambda 演算中，(a,a) -> (a,a) 有四个取值。

(a, b) ↦ (a, a)
(a, b) ↦ (b, b)
(a, b) ↦ (a, b)
(a, b) ↦ (b, a)

但前两种方法要求我们使用其中一个参数两次，而丢弃另一个参数。这正是线性λ演算的本质——不允许这些类型的函数。

---

顺便提一句，线性LC的目的是什么？嗯，我们可以用它来模拟线性效应或资源使用。例如，如果我们有一个文件类型和几个转换器，它可能看起来像

data File
open  :: String -> File
close :: File   -> ()      -- consumes a file, but we're ignoring purity right now
t1    :: File -> File
t2    :: File -> File

然后以下是有效的管道：

close . t1 . t2 . open
close . t2 . t1 . open
close . t1      . open
close . t2      . open

但是这种“分支”计算并不是。

let f1 = open "foo"
    f2 = t1 f1
    f3 = t2 f1
in close f3

由于我们两次使用了f1，你可能会有所疑惑。

---

现在，在这一点上，您可能会对哪些事情必须遵循线性规则产生疑问。例如，我决定某些管道不必包括t1和t2（与之前的枚举练习相比）。此外，我引入了open和close函数，它们可以愉快地创建和销毁File类型，尽管这违反了线性规则。

事实上，我们可能会假设存在一些违反线性规则的函数——但并非所有客户端都可能会这样假设。这就像IO单子—所有的秘密都存在于IO的实现中，以便用户在“纯粹”的世界中工作。

这就是Comonoid发挥作用的地方。

class Comonoid m where
  destroy :: m -> ()
  split   :: m -> (m, m)

在线性λ演算中实例化Comonoid的类型是具有带着销毁和复制规则的携带型。换句话说，这种类型并不是非常受限于线性λ演算。

由于Haskell根本不实现线性λ演算规则，因此我们总是可以实例化Comonoid。

instance Comonoid a where
  destroy a = ()
  split a   = (a, a)

或者，另一种思考的方式是Haskell是一个线性LC系统，恰好为每种类型实例化 Comonoid，并自动应用destroy和split。

- J. Abrahamson

---

@dfeuer，我差点写成了 |->，但在ASCII中看起来太丑了。在你的坚持下，我完全赞同，我采取了一个折中的方法。 :) - J. Abrahamson

Answer 2

1. 在通常意义下，单子同范畴集合中的范畴单子是相同的。人们可能认为，在通常意义下的余单子与范畴集合中的范畴余单子是相同的。但是，范畴集合中的每个集合都以一种琐碎的方式成为余单子，因此似乎没有非范畴化的余单子描述方式可以平行于单子的描述方式。
2. 就像单子是函子自身范畴中的单子一样（有什么问题？），余单子是函子自身范畴中的余单子（有什么麻烦？）。因此，在Haskell中，任何余单子都是余单子的一个示例。

- n. m.

---

我花了一些时间才理解它，但我认为我懂了，并且这是一个有趣的例子。不过，那并不完全是我在我的第二个问题中想要探讨的方向。我编辑了我的问题。 - betaveros

为什么集合的所有共同体都是平凡的？你有来源或证明吗？ - PyRulez

@PyRulez 一个共单子（comonoid）具有共乘和余单位，类似于乘法和单位元，但箭头反向。在集合中，您可以使用comult :: a->（a，a）; comult a =（a，a）和counit :: a->（）; counit a =（）来进行计算。您能否写下共结合律和余恒等律，并验证它们是否成立？ - n. m.

哦，等等，我明白为什么它必须是微不足道的了。 因为余单位元强制两个参数都是输入。 - PyRulez

Answer 3

作为一名物理学家，我处理的最常见的例子是余代数，它们是向量空间范畴中的余单子对象，其蒙德纳尔结构通常由张量积给出。

在这种情况下，单子对象和余单子对象之间存在双射，因为您只需取乘积和单位映射的伴随或转置即可得到满足余单子公理的余积和余单位。

在某些物理学分支中，非常常见的是具有代数和余代数结构以及一些兼容性公理的对象。两种最常见的情况是Hopf代数和Frobenius代数。它们非常方便构造纠缠或相关的状态或解决方案。

---

在编程中，我能想到的最简单的非平凡示例是引用计数指针，例如C++中的shared_ptr和Rust中的Rc，以及它们的弱等效项。您可以复制它们，这是一个非平凡的操作，会增加引用计数（因此两个副本与初始状态不同）。您可以在其中一个上删除（调用析构函数），这是非平凡的，因为它会减少指向相同数据块的任何其他引用计数指针的引用计数。

此外，弱指针是余单子作用的一个很好的例子。您可以使用共作用来从共享指针生成弱指针。通过注意到从共享指针创建一个并立即将其删除是一个单位操作，并且创建一个并克隆它等效于从共享指针创建两个来轻松检查这一点。

这是非平凡余积及其共作用中通常看到的一般事情：当它们不归结为复制操作时，它们直观地暗示两个半之间的某种远程作用，同时添加了一种操作，以擦除一个半并使另一个独立。

- saolof

Answer 4

我们可以将单子视为与我们使用的任何特定产品构造相关联的一种方式，在Set中，我们会采用这个签名：

mul : A * A -> A
one : A

转换成这个：

dup : A -> A * A
one : A

但是二元性的想法是，你可以做出的所有逻辑语句都有对应的对偶可以应用于对偶对象，还有一种表达幺半群的方式就是不关心乘积结构的选择，然后在进行共构造时我们可以在输出中取一个余积，就像这样：

div : A -> A + A
one : A

其中 + 是一个标记求和。在这里，我们基本上可以看出该类型中的每个术语都准备好产生一个新位，这个新位是从用于表示 A 的左侧或右侧实例的标记中隐含地派生出来的。我个人认为这真的很酷。我认为人们谈论的事情的酷版本是当你不特别构建单子中的那些内容时，而是构建单子操作时。

如果有一个函数，一个单子 M 被称为对一个集合 A 进行作用。

act : M * A -> A

在这里，我们有以下规则

act identity a = a
act f (act g a) = act (f * g) a

如果我们想要协同作用，具体指什么呢？

act : A -> M * A

这会生成我们共同体类型的流！我在为这些系统制定规则时遇到了很多麻烦，但我认为它们一定存在于某个地方，所以今晚我会继续寻找。如果有人能告诉我这些规则，或者以某种方式告诉我我在某些方面是错误的，我也很感兴趣。

- Samuel Schlesinger