一个不平凡的共生体是什么样的？

Question

例如,在Haskell的distributive库文档中提到了Comonoids :

由于Haskell中缺少非平凡的共生,我们可以限制自己需要一个Functor而不是一些Coapplicative类.

经过一番搜索后,我发现了一个StackOverflow答案,它可以解释这一点,以及comonoids必须满足的规律.所以我想我理解为什么在Haskell中假设的Comonoid类型类只有一个可能的实例.

因此,为了找到一个非常重要的共生体,我想我们必须看一些其他类别.当然,如果类别理论家有共同体的名称,那么有一些有趣的.该页面上的其他答案似乎暗示了一个涉及的例子Supply,但我无法弄明白仍然满足法律.

我也转向维基百科:有一个Monoidmonoids 的页面没有引用类别理论,这在我看来是对Haskell的类型类的充分描述,但是"comonoid"重定向到一个类别理论描述的幺半群和共生组合,我可以不明白,似乎还没有任何有趣的例子.

所以我的问题是:

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

编辑:我不知道,如果这实际上是类,理论上是正确的,但我在问题2的括号被想象为的非平凡的定义delete :: a -> m ()和split :: a -> m (a, a)对一些特定 Haskell的类型a和Haskell单子m是满足的comonoid法律Kleisli箭头版本相关的答案.其他共生体的例子仍然受到欢迎.

Answer 1

正如Phillip JF所提到的,comonoids在子结构逻辑中很有趣.我们来谈谈线性lambda演算.这非常类似于普通类型的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)

但前两个要求我们使用其中一个参数而丢弃另一个.这正是线性lambda演算的本质 - 不允许这些函数.

简而言之,线性液晶显示器有什么意义？好吧,我们可以用它来模拟线性效应或资源使用.例如,如果我们有一个文件类型和一些变形金刚,它可能看起来像

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,尽管,作为一个违反线性类型.

实际上,我们可能会认为存在违反线性的函数 - 但并非所有客户都可以.它就像IOmonad一样 - 所有秘密都存在于实现中,IO以便用户在"纯粹"的世界中工作.

这就是Comonoid进来的地方.

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

Comonoid在线性lambda演算中实例化的类型是具有随身破坏和复制规则的类型.换句话说,它是一种根本不受线性lambda演算约束的类型.

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

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

或者,也许另一种思考方式是Haskell是一个线性LC系统,恰好可以Comonoid为每种类型实例化destroy并split自动应用.

Answer 2

1. 通常意义上的幺半群与集合类别中的分类幺半群相同.人们可以预期,通常意义上的共生体与集合类别中的分类共生体相同.但是,集合类别中的每一组都是一个微不足道的共生体,所以显然没有非类别的共生体描述与幺半群的平行.
2. 就像monad是endofunctor类别中的monoid一样(问题是什么？),comonad是endofunctors类别中的comonoid(什么是coproblem？)所以是的,Haskell中的任何comonad都是comonoid的一个例子.