3

情况如下（我改为更标准的 Haskell 表示法）：

class Functor f => MonoidallyCopointed f where
    copointAppend ::  (∀r.f(r)->r) -> (∀r.f(r)->r) -> (∀r.f(r)->r)
    copointEmpty  ::  ∀r.f(r)->r

使得对于所有的实例 FMonoidallyCopointed并且对于所有

x,y,z::∀r.F(r)->r

以下成立：

x `copointAppend` copointEmpty == copointEmpty `copointAppend` x == x
x `copointAppend` (y `copointAppend` z) == (x `copointAppend` y) `copointAppend` z

那么 F 有一个从和Comonad定义的自然实例是真的吗？copointAppendcopointEmpty

NB 反过来成立 (with copointEmpty = extractand copointAppend f g = f . g . duplicate.)

编辑

正如 Bartosz 在评论中指出的那样，这主要是使用 co-Kleisli 附加词来定义共胞。所以问题实际上是关于这个概念的建设性。因此，就实际应用而言，以下问题可能更有趣：

Comonadf 的可能实例集和 f 的可能实例集之间是否存在建设性同构MonoidallyCopointed？

这在实践中很有用，因为Comonad实例的直接定义可能涉及一些技术性的、难以阅读的代码，这些代码无法通过类型检查器进行验证。例如，

data W a = W (Maybe a) (Int -> a) (Either (String -> a) (a,a,a,a))

有一个 Comonad 实例，但直接定义（证明它确实是一个 Comonad！）可能并不那么容易。另一方面，提供一个MonoidallyCopointed实例可能会更容易一些（但我并不完全确定这一点）。

4

0 回答 0