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

Question

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

考虑 monadM ~> N之间的monad 态射。（这些是M a -> N a保留两边 monad 操作的自然变换。这些变换是 monad 范畴中的态射。）我们可以问是否存在e :: (Monad m) => m a -> m a对每个 monad 都以相同方式工作的 monad 态射m。换句话说，monad 态射e在 monad 类型参数中必须是单子自然的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 ~> Mwhere Unitis the unit monad。我也无法直接找到任何证据。

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无法成为 monad 的许多选择的 monad 态射m。既然如此，单子中唯一完全多态的单子态射是id。

让我们把论点说得更明确一些。

为了清楚起见，我将暂时切换到join//演示。我们想要实施：returnfmap

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和 extrajoin来删除它们不会导致任何结果，因为我们必须显示这些层的出处，并且事情最终会减少到其他情况。）

唯一有趣的案例是#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由*>或分隔的进一步出现， a 的右侧<*没有。*><*

回到开始，所有非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 和s，而在右侧得到所有s 之后的所有 s。这意味着该属性不适用于、或等单子，无论中有多少个和，或者两侧的类似函数选取了哪些值。一个快速演示：vvuIOStateWriter(*>)(<*)econst

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