haskell - 单子(monad) liftM 和仿函数 fmap 必须相等吗？

Question

(注意:我使用 Haskell 术语来表达问题；欢迎使用相同的术语和/或范畴论的数学语言来回答，包括我谈到仿函数和单子(monad)定律时的正确数学定义和公理。)

众所周知，每个 monad 也是一个仿函数，仿函数的 fmap 相当于 monad 的 liftM。这是有道理的，当然适用于所有常见/合理的 monad 实例。

我的问题是 fmap 和 liftM 的等价性是否可以证明遵循仿函数和单子(monad)定律。如果是这样，那么很高兴看到如何实现，如果没有，那么很高兴看到反例。

澄清一下，我所知道的仿函数和单子(monad)定律如下:

• fmap id == id
• fmap f 。 fmap g == fmap (f . g)
• 返回 x >>= f ≡ f x
• x >>= return ≡ x
• (x >>= f) >>= g ≡ x >>= (\x -> f x >>= g)

我在这些法律中没有看到任何将仿函数功能(fmap)与 monad 功能(return 和 >>=)，所以我发现很难看出 fmap 和 liftM 的等价性(定义为 liftM f x = x >>= (return . f) ) 可以从它们中派生出来。也许有一个论点对我来说还不够简单？或者也许我遗漏了一些法律？

Answer 1

您错过的是参数律，也称为自由定理。参数化的后果之一是所有多态函数都是自然变换。自然性说任何形式的多态函数

t :: F a -> G a

其中 F 和 G 是仿函数，与 fmap 进行通勤:

t . fmap f = fmap f . t

如果我们可以制作出具有自然变换形式的涉及 liftM 的东西，那么我们将得到一个与 liftM 和 fmap 相关的方程。 liftM 本身不会产生自然变换:

liftM :: (a -> b) -> m a -> m b
              --       ^______^
              -- these need to be the same

但是这里有一个想法，因为 (a ->) 是一个仿函数:

as :: m a
flip liftM as :: (a -> b) -> m b
              --  F    b  -> G b

让我们尝试在 flip liftM m 上使用参数性:

flip liftM m . fmap f = fmap f . flip liftM m

前一个 fmap 位于 (a ->) 仿函数上，其中 fmap = (.)，因此

flip liftM m . (.) f = fmap f . flip liftM m

埃塔展开

(flip liftM m . (.) f) g = (fmap f . flip liftM m) g
flip liftM m (f . g)     = fmap f (flip liftM m g)
liftM (f . g) m          = fmap f (liftM g m)

这是有希望的。取g = id:

liftM (f . id) m = fmap f (liftM id m)
liftM f m        = fmap f (liftM id m)

显示liftM id = id就足够了。这可能是从它的定义中得出的:

liftM id m
   = m >>= return . id
   = m >>= return
   = m

是的! Qed。