单子提升M和函子fmap是否必须相等? [英] Do the monadic liftM and the functorial fmap have to be equivalent?

问题描述

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

(Note: I'm phrasing the question using Haskell terminology; answers are welcome to use the same terminology and/or the mathematical language of category theory, including proper mathematical definitions and axioms where I speak of functor and monad laws.)

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

It is well known that every monad is also a functor, with the functor's fmap equivalent to the monad's liftM. This makes sense, and of course holds for all common/reasonable monad instances.

我的问题是fmap和liftM的等价性是否可证明是根据函子和莫纳德定律得出的.如果是这样，很高兴看到如何做，如果不是，那么很高兴看到一个反例.

My question is whether this equivalence of fmap and liftM provably follows from the functor and monad laws. If so it will be nice to see how, and if not it will be nice to see a counterexample.

为澄清起见，我知道的函子和monad法则如下:

To clarify, the functor and monad laws I know are the following:

• 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 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)与单子功能(return和>>=)相关联的内容，因此，我很难看到和liftM(定义为liftM f x = x >>= (return . f))可以从它们派生.也许有一个论点还不够直接让我发现?或者也许我错过了一些法律?

I don't see anything in these laws which relates the functor functionality (fmap) to the monad functionality (return and >>=), and so I find it hard to see how the equivalence of fmap and liftM (defined as liftM f x = x >>= (return . f)) can be derived from them. Maybe there is an argument for it which is just not straightforward enough for me to spot? Or maybe I'm missing some laws?

推荐答案

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

What you have missed is the parametericity law, otherwise known as the free theorem. One of the consequences of parametricity is that all polymorphic functions are natural transformations. Naturality says that any polymorphic function of the form

t :: F a -> G a

其中F和G是仿函数，与fmap换向:

where F and G are functors, commutes with fmap:

t . fmap f = fmap f . t

如果我们可以使涉及liftM的事物具有自然变换的形式，那么我们将有一个与liftM和fmap相关的方程式. liftM本身不会产生自然转换:

If we can make something involving liftM that has the form of a natural transformation, then we will have an equation relating liftM and fmap. liftM itself doesn't produce a natural transformation:

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

但这是个主意，因为(a ->)是函子:

But here's an idea, since (a ->) is a functor:

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

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

Let's try using parametericity on flip liftM m:

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

前一个fmap在(a ->)函子上，在fmap = (.)上，所以

The former fmap is on the (a ->) functor, where fmap = (.), so

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

Eta扩展

(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就足够了.可能来自其定义:

It would suffice to show liftM id = id. That probably follows from its definition:

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

是的！ Qed.

这篇关于单子提升M和函子fmap是否必须相等?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！