monadic liftM和functorial fmap必须是等价的吗？

Question

(注意:我正在使用Haskell术语来表达这个问题;欢迎使用相同的术语和/或类别理论的数学语言,包括正确的数学定义和公理,其中我提到了仿函数和monad定律.)

众所周知,每个monad也是一个仿函数,仿函数与fmapmonad相当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)).也许有一个争论,这对我来说不够简单？或许我错过了一些法律？

Answer 1

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

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

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.这可能源于其定义:

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

是的!QED.

Answer 2

在本练习中,我发现使用它join比使用它更容易>>=.monad可以通过return并且join满足来等效地定义

1) join . join = join . fmap join
2) join . return = join . fmap return = id

确实,join并且>>=是可以相互定义的:

x >>= f = join (fmap f x)
join x = x >>= id

你提到的法律与上述法律相对应(我不会证明这一点).

然后,我们有:

liftM f x
= { def liftM }
x >>= return . f 
= { def >>= }
join (fmap (return . f) x)
= { def . and $ }
join . fmap (return . f) $ x
= { fmap law }
join . fmap return . fmap f $ x
= { join law 2 }
id . fmap f $ x
= { def id, ., $ }
fmap f x