【发布时间】：2020-10-12 00:58:47
【问题描述】：
在https://hackage.haskell.org/package/category-extras-0.53.0/docs/Control-Comonad-Reader.html 中，定义了共同阅读器monad，并且共同单子类型模态应用于类型a 并生成一对(r,a)。因此，comonadic 类型模态 w 是 a -> (r, a) 类型。
这与 reader monad 完全不同，其中 monadic 类型模态适用于类型 a 并为特定类型 r 生成类型为 r -> a 的函数。
我不清楚为什么联合单子模态没有以类似于阅读器模态的方式定义，因此，w 是相关的联合单子模态，我们有 w a := r -> a，然后函数extract :: w a -> a 和(<<=) :: (w a -> b) -> w a -> w b 只是分别重新排列return :: a -> m a 和绑定(=<<) :: (a -> m b) -> m a -> m b（其中m a : = r -> a）。
也就是说，co-reader monad 是否可以类似于 reader monad 的定义，只是我们改变箭头的方向？改变 bind 和 return 的箭头是否足以生成 (a (?)) co-reader monad？如果没有，那为什么不呢。
此外，是否可以将 w 与函数 extract :: w a -> a 和 (<<=) :: (w a -> b) -> w a -> w b 一起定义为 w a := r -> a 的共元模态？
编辑：这个问题已经完全重写，以回应不清楚的反对意见。
【问题讨论】：
-
多态类型
(e -> a) -> a没有终止实现，而(e, a) -> a（使用snd）及其咖喱变体a -> ( e -> a)（使用const）很容易实现。我们不能从单子中获取相同的函子并将其变成共单子。我们需要左伴随词，它由 (un)currying 提供。 -
这是一个有趣的话题，但由于目前还不清楚，我投票结束。如果您可以使问题准确，请这样做。 — 以下是关于读者和作者共生词的简短讨论：olivierverdier.com/posts/2014/12/31/reader-writer-monad-comonad
-
@leftaroundabout 我完全重写了问题
-
@chi 在这种情况下，终止实现是什么意思？为什么这很重要？为什么我们需要左伴奏？
-
@user65526 仅仅因为在某些模型中公式为真，并不意味着它可以被证明（在其他模型中可能为假）。对于最后一个问题：直观地说，如果我给你一个函数
r->e，但没有r，你就没有办法构造一个e。更一般地说，(A->B)->B命题不是直觉的重言式（也不是经典的），因此 Curry-Howard 无法实现它。