haskell - 单子(monad)提升M和仿函数fmap是否必须相等？

(注意:我使用Haskell术语来表述问题；欢迎使用相同的术语和/或类别理论的数学语言来回答，包括适当的数学定义和公理，其中我涉及仿函数和莫纳德定律。)

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

我的问题是fmap和liftM的等效性是否可证明是根据仿函数和monad定律得出的。如果是这样，那么很高兴看到如何做，如果不是，那么很高兴看到一个反例。

需要澄清的是，我知道的仿函数和monad法则如下:

fmap id≡id

fmap f . fmap g≡fmap (f . g)

return 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))的等效项。从他们。也许有一个论点还不够直接让我发现？也许我错过了一些法律？

最佳答案

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

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。

关于haskell - 单子(monad)提升M和仿函数fmap是否必须相等？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/53022087/