存在一个在范畴M上自然的、非恒等单子态射M~>M吗？

Question

存在一个在范畴M上自然的、非恒等单子态射M~>M吗？

7

已知类型为 a -> a 的自然变换必须是恒同函数。这来自于 Yoneda 引理，也可以直接导出。这个问题要求证明单子范畴中单子态射也具有相同的性质。

考虑单子之间 M ~> N 的单子态射（保持两边单子操作的自然变换 M a -> N a）。我们可以询问是否存在一个单子态射 e :: (Monad m) => m a -> m a，它在每个单子上都能够以相同的方式工作。换句话说，单子态射 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

这两个尝试具有正确的类型签名，但未通过单子态映射定律。

似乎无法将Yoneda引理应用于此情况，因为没有单子态映射Unit ~> M，其中Unit是单位单子态。我也找不到任何直接证明。

- winitzki

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- duplode · Accepted Answer

我认为你已经尝试过所有有趣的可能性。我们可能定义的任何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本身之外，我们还有以下可能性：

join (return v)，它是v，因此没有告诉我们任何新信息；
join (fmap return v)，它也是v；以及
join (fmap (\x -> fmap (f x) w) v)，对于某些其他根据规则构建的w :: m a和一些f :: a -> a -> a。（将f的类型添加m层，如a -> a -> m a，并添加额外的join以删除它们将无法得出任何结论，因为我们随后必须显示这些层的来源，而事情最终会归结为其他情况。）

唯一有趣的情况是第三种情况。此时，我将采取捷径：

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。然而，这种应用表达式有一个规范形式，通过使用applicative定律将所有(<*>)的使用重新关联到左边来获得，在这种情况下必须像这样...

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)

我们现在有一个明确的反例路径。如果我们使用应用定律将两边转换为规范形式，我们仍然会在左侧得到交错的u和v，并且在右侧所有u之后得到所有v。这意味着该属性不适用于像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