在 M 中是否存在单子自然的非同一性单子态射 M ~> M？

Question

众所周知，类型签名a -> a 的自然变换必须是恒等函数。这来自米田引理，但也可以直接推导出来。这个问题要求相同的属性，但要求单子态射而不是自然变换。

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

单子自然法则规定，对于任意两个单子 M 和 N 之间的任何单子态射 f: M a -> N a，我们必须有 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

这两种尝试都有正确的类型签名，但不符合单子态射定律。

似乎米田引理不能应用于这种情况，因为没有单子态射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 选择的单子态射。既然如此，monad中唯一完全多态的monad态射是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，因此不会告诉我们任何新信息；

2. join (fmap return v)，也就是v；和

3. join (fmap (\x -> fmap (f x) w) v)，还有一些根据我们的规则构建的w :: m a，还有一些f :: a -> a -> a。 （将m 层添加到f 的类型中，如a -> a -> m a 和额外的joins 以删除它们不会导致任何地方，因为我们必须显示这些层的出处，以及最终会减少到其他情况。）

唯一有趣的案例是#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，要么是这种模式的进一步迭代，最终达到u s 在叶子上。然而，这类应用表达式具有规范形式，通过使用应用法则将(<*>) 的所有用法重新关联到左侧，在这种情况下必须看起来像这样......

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

... 省略号代表零次或多次出现的u，由<*> 分隔，c 是适当数量的a -> ... -> a -> a 函数。由于a 是完全多态的，所以c 必须通过参数化，成为一些类似于const 的函数，它选择它的一个参数。既然如此，任何这样的表达式都可以重写为(<*) 和(*>)...

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，而所有vs 毕竟是@987654390 @s 在右侧。这意味着该属性不适用于 IO、State 或 Writer 之类的单子，无论 (*>) 和 (<*) 中有多少 e，或者究竟是哪些值被 @ 987654397@-like 功能在任一侧。快速演示：

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