一个非平凡的comonoid长什么样？

Question

经过稍加搜索，我找到了一个StackOverflow的答案，它用comonoids必须满足的定律更好地解释了这一点。所以我想我明白了为什么在Haskell中只有一个假设的Comonoid类型的可能实例。

因此，要找到一个非平凡的comonoide，我想我们必须从其他类别中寻找。当然，如果范畴理论家有一个comonoids的名字，那么有一些有趣的。该页上的其他答案似乎暗示了一个涉及supply的示例，但我找不出一个仍然满足这些规律的答案。

我还转到Wikipedia：有一个关于monoid的页面没有引用类别理论，在我看来，这是对Haskell的monoidtypeclass的充分描述，但“comonoid”重定向到对monoid和comonoid的类别理论描述，我无法理解，而且似乎仍然没有任何有趣的例子。

1. 同子类可以用类似单子类的非范畴理论术语来解释吗？
2. 有趣的comonoid的一个简单示例是什么，即使它不是Haskell类型？（在熟悉的Haskell Monad之上，还能在Kleisli类别中找到一个吗？）

编辑：我不确定这是否真的是类别理论上的正确，但我在问题2的括号中想象的是delete::a->m()和split::a->m(a，a)对于一些特定的Haskell类型a和Haskell单元体m的非平凡定义，它们满足链接答案中comonoid定律的Kleisli-arrow版本。comonoids的其他例子仍然是受欢迎的。

Answer 1

正如Phillip JF所提到的，在子结构逻辑中谈论comonoid是很有趣的。我们来谈谈线性λ微积分。这很像您的普通类型的λ演算，除了每个变量必须使用一次。

为了获得一种感觉，让我们数一下给定类型的线性函数，即。

a -> a

只有一个居民，ID。而

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

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

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和closehtml" target="_blank">函数，它们愉快地创建和销毁file类型，尽管这违反了线性。

实际上，我们可能会假设存在违反线性的函数--但并非所有客户机都可能。这很像io单子--所有的秘密都存在于io的实现中，因此用户可以在一个“纯粹”的世界中工作。

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

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

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

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

或者，从另一种角度来看，Haskell是一个线性LC系统，它只是碰巧为每个类型实例化comonoid，并自动为您应用destroy和split。