是否存在一个非等式单子态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态射定律。

[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 m和k = flip fmap m . const等于您的两次尝试）。但是，在这种情况下，m效果将被复制，并且对于任何非幂等单子e，m都不会成为单子态。如此，单子中唯一完全多态的单子态是id。