是否存在在 M 中自然单子的非恒等单子态射 M ~> M？

Question

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

考虑单子之间的单子态射 M ~> N。（这些是自然变换M a -> N a，保留了两侧的 monad 操作。这些变换是 monad 范畴中的态射。）我们可以问是否存在一个 monad 态射 e :: (Monad m) => m a -> m a 在相同的情况下起作用每个 monad 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

这两种尝试都具有正确的类型签名，但不符合 monad 态射法则。

似乎米田引理不能应用于这种情况，因为没有单子态射 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 本身，我们还有以下可能性：

join (return v)，即 v，因此没有告诉我们任何新信息；
join (fmap return v)，也就是v；和
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 的函数，该函数会选择其参数之一。既然如此，任何此类表达式都可以根据 (<*) 和 (*>)...

重写

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 毕竟 us 在右边。这意味着属性不适用于像 IO、State 或 Writer 这样的单子，无论有多少 (*>) 和 (<*)在 e 中，或者确切地说，哪些值是由任一侧的 const 类函数选择的。快速演示：

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

是否存在在 M 中自然单子的非恒等单子态射 M ~> M？

Is there a non-identity monad morphism M ~> M that is monadically natural in M?

monads

haskell

category-theory