非平凡的共形体长什么样？

Question

例如在 Haskell 的 distributive library docs 中提到了 Comonoids：

由于 Haskell 中缺乏非平凡的 comonoid，我们可以将自己限制为需要 Functor 而不是一些 Coapplicative 类。

经过一番搜索，我找到了一个StackOverflow answer，它用共模类必须满足的定律来解释这一点。所以我想我理解为什么在 Haskell 中只有一个假设的 Comonoid 类型类的可能实例。

因此，要找到一个非平凡的类群，我想我们必须寻找其他类别。当然，如果范畴理论家有一个名称为类黑素，那么就会有一些有趣的名称。该页面上的其他答案似乎暗示了一个涉及Supply 的示例，但我想不出一个仍然符合法律规定的答案。

我也求助于 Wikipedia：有一个关于 monoids 的页面没有引用类别理论，在我看来这足以描述 Haskell 的 Monoid 类型类，但“comonoid”重定向到对 monoids 的类别理论描述和comonoids放在一起我看不懂，而且似乎还没有什么有趣的例子。

所以我的问题是：

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

编辑：我不确定这是否真的在类别理论上是正确的，但我在问题 2 的括号中想象的是 delete :: a -> m () 和 split :: a -> m (a, a) 的一些重要定义 特定 Haskell 类型 a 和 Haskell monad m 在链接答案中满足 Kleisli-arrow 版本的 comonoid 定律。仍然欢迎使用其他类黄酮的例子。

Answer 1

正如 Phillip JF 所提到的，在子结构逻辑中谈论类共体很有趣。让我们谈谈线性 lambda 演算。这很像普通类型的 lambda 演算，只是每个变量都必须只使用一次。

感受一下，让我们count linear functions of given types，即

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)

但前两个要求我们使用其中一个参数两次，同时丢弃另一个。这正是线性 lambda 演算的本质——不允许使用这些函数。

---

顺便说一句，线性 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 monad——所有的秘密都存在于 IO 的实现中，因此用户可以在“纯粹”的世界中工作。

这就是Comonoid 的用武之地。

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

在线性 lambda 演算中实例化 Comonoid 的类型是具有携带破坏和复制规则的类型。换句话说，它是一种完全不受线性 lambda 演算约束的类型。

由于 Haskell 根本没有实现线性 lambda 演算规则，我们总是可以实例化 Comonoid

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

或者，也许换一种方式认为，Haskell 是一个线性液相色谱系统，它恰好为每种类型实例化 Comonoid，并自动为您应用 destroy 和 split。

Answer 2

1. 通常意义上的幺半群与集合范畴中的分类幺半群相同。人们会期望通常意义上的可模类与集合类别中的分类可模类相同。但是集合范畴中的每个集合都是一个普通的类群，因此显然没有与类群相似的类群的非分类描述。
2. 就像单子是内函子类别中的幺半群（有什么问题？），共单子是内函子类别中的类单胞（有什么共同问题？）所以是的，Haskell 中的任何单子都是一个comonoid。

Answer 3

我们可以想到一个幺半群的一种方式是与我们正在使用的任何特定产品构造挂钩，所以在 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

这会为我们生成一个类同类型的流！我在为这些系统制定法律时遇到了很多麻烦，但我认为它们一定在某个地方，所以今晚我会继续寻找。如果有人能告诉我他们或我在某些方面对这些事情有错误，也对此感兴趣。

Answer 4

作为一名物理学家，我处理的最常见的例子是余代数，它是向量空间范畴中的共多边形对象，具有通常由张量积给出的幺半群结构。

在这种情况下，幺半群和共模对象之间存在双射，因为您可以通过乘积和单位映射的伴随或转置来获得满足共模公理的联积和共单元。

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

---

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

此外，弱指针是comonoid action 的一个很好的例子。您可以使用协同操作从共享指针生成弱指针。这可以通过注意从共享指针创建一个并立即删除它是一个单元操作来轻松检查，创建一个并克隆它相当于从共享指针创建两个。

这是您在非平凡的副产品及其共同作用中看到的普遍现象：当它们不简化为复制操作时，它们直观地暗示在两半之间的距离处进行某种形式的操作，同时还添加了操作抹去一半，让另一半独立。