haskell - 一个不平凡的共同类群是什么样子的？

Question

例如，Haskell 的 distributive library docs 中提到了 Comonoids :

Due to the lack of non-trivial comonoids in Haskell, we can restrict ourselves to requiring a Functor rather than some Coapplicative class.

经过一番搜索，我发现了 StackOverflow answer这用 comonoid 必须满足的定律更好地解释了这一点。所以我想我明白为什么 Haskell 中假设的 Comonoid 类型类只有一个可能的实例。

因此，为了找到一个不平凡的共类群，我想我们必须寻找其他类别。当然，如果范畴论学家给共谐函数起了一个名字，那么就会有一些有趣的名字。该页面上的其他答案似乎暗示了一个涉及 Supply 的示例，但我无法找出仍然满足法律的答案。

我还查阅了维基百科:有一个关于幺半群的页面没有引用范畴论，在我看来，这足以描述 Haskell 的 Monoid 类型类，但“comonoid”重定向到一个类别-我无法理解幺半群和共半群的理论描述，而且似乎仍然没有任何有趣的例子。

所以我的问题是:

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

编辑:我不确定这实际上在类别理论上是否正确，但我在问题 2 的括号中想象的是 delete::a -> m 的重要定义() 和 split::a -> m (a, a) 对于某些特定的 Haskell 类型 a 和 Haskell monad m 满足链接答案中科莫尼定律的 Kleisli 箭头版本。仍然欢迎其他 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 — 所有 secret 都存在于 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 是一个线性 LC 系统，它恰好为每种类型实例化 Comonoid 并应用 destroy 和 自动为您分割。