在M中是否有一个非恒等单态射M ~> M是单自然的？

Question

众所周知，具有类型签名a -> a的自然转换必须是标识函数。这是从Yoneda引理中得到的，但也可以直接导出。这个问题要求相同的性质，但单态射，而不是自然转换。

考虑一下单模之间的单态射M ~> N。(这是自然转换M a -> N a，它保留双方的单一操作。这些变换是monads范畴中的态射。)我们可以问，是否存在一个单一的态射e :: (Monad m) => m a -> m a，它对每个单一的m都有相同的工作方式。换句话说，单模态射e必须在单模类型参数m中是单自然的。

一元自然性定律指出，对于任意两个单模M和N之间的任意单态射f: m a -> N，我们必须有具有适当类型参数的f . e = e . f。

问题是，我们能否证明任何这样的e都必须是一个恒等函数，或者是否有一个非恒等单态射e定义为反例？

  e :: (Monad m) => m a -> m a
  e ma = ...

定义此类e的一个失败尝试是：

 e ma = do
         _ <- ma
         x <- ma
         return x

另一次失败的尝试是

 e ma = do
         x <- ma
         _ <- ma
         return x

这两次尝试都有正确的类型签名，但都失败了单态射定律。

似乎Yoneda引理不能适用于这种情况，因为不存在单模态射Unit ~> M，其中Unit是单位单模。我也无法直接找到任何证据。

Answer 1

我想你已经用尽了所有有趣的可能性。我们可能定义的任何Monad m => m a -> m a函数都不可避免地如下所示：

e :: forall m a. Monad m => m a -> m a
e u = u >>= k
    where
    k :: a -> m a
    k = _

特别是，如果k = return，e = id。为了使e不是id，k必须以一种非平凡的方式使用u (例如，k = const u和k = flip fmap u . const相当于您的两次尝试)。然而，在这种情况下，u效应将被复制，导致e不能成为许多m选择的单一形式。既然如此，单模中唯一完全多态的是id。

让我们把论点说得更清楚些。

为了清晰起见，我将转到join/return/fmap演示文稿。我们要执行：

e :: forall m a. Monad m => m a -> m a
e u = _

我们能用什么填充右手边呢？最明显的选择是u。就其本身而言，这意味着e = id，这看起来并不有趣。然而，由于我们也有join，return和fmap，所以有归纳推理的选择，以u为基本案例。假设我们有一些v :: m a，它是用我们手头的方法构建的。除了v本身，我们还有以下可能性：

1. join (return v)，是v，因此没有告诉我们任何东西，也就是v；and
2. join (fmap (\x -> fmap (f x) w) v)，是根据我们的规则构建的其他w :: m a，还有一些f :: a -> a -> a。(将m层添加到f类型中，就像在a -> a -> m a中那样，而删除它们的额外join不会带来任何结果，因为这样我们就必须显示这些层的来源，而事情最终将减少到其他情况)。

唯一有趣的例子是#3。在这一点上，我要走一条捷径：

join (fmap (\x -> fmap (f x) w) v)
    = v >>= \x -> fmap (f x) w
    = f <$> v <*> w

因此，任何非u的右侧都可以用f <$> v <*> w形式表示，v和w要么是u，要么是该模式的进一步迭代，最终在叶子处到达us。然而，这类应用表达式有一个规范形式，它是通过使用应用律将(<*>)的所有用法重新组合到左边得到的，在这种情况下，这种用法必须如下所示.

c <$> u <*> ... <*> u

..。用省略号表示u的零或更多次，<*>隔开，c是一个合适的a -> ... -> a -> a函数。由于a是完全多态的，根据参数，c必须是一些const-like函数，它选择它的一个参数。既然如此，任何这样的表达式都可以用(<*)和(*>)重写.

u *> ... <* u

..。用省略号表示u的零次或更多次，用*>或<*分隔，<*的右边没有*>。

回到开始阶段，所有非id候选实现都必须如下所示：

e u = u *> ... <* u

我们还希望e是一个单态射。因此，它也必须是一种可应用的态射。特别是：

-- (*>) = (>>) = \u v -> u >>= \_ -> v
e (u *> v) = e u *> e v

这就是：

(u *> v) *> ... <* (u >* v) = (u *> ... <* u) *> (v *> ... <* v)

我们现在有了一条通往反例的明确道路。如果我们使用应用律将双方转换成规范形式，我们将(仍然)在左手侧以交错的us和vs结束，而在右手侧则以所有us之后的所有vs结束。这意味着无论在IO、State或Writer中有多少(*>)和(<*)，也不管在e中有多少(*>)和(<*)，或者无论哪一方的const-like函数都选择哪个值，该属性都不适用于(<*)、(*>)或Writer。一个简单的演示：

GHCi> e u = u *> u <* u  -- Canonical form: const const <$> u <*> u <*> u
GHCi> e (print 1 *> print 2)
1
2
1
2
1
2
GHCi> e (print 1) *> e (print 2)
1
1
1
2
2
2