`x >> pure y` 是否等同于 `liftM (const y) x`

Question

两种表达方式

y >> pure x
liftM (const x) y

在 Haskell 中具有相同的类型签名。 我很好奇它们是否等价，但我既无法证明这一事实，也无法举出反例。

如果我们重写这两个表达式，从而消除x和y，那么问题就变成了以下两个函数是否等价

flip (>>) . pure
liftM . const

请注意，这两个函数的类型均为 Monad m => a -> m b -> m a。

我使用 Haskell 为 monad、applicatives 和 functors 提供的定律将这两个语句转换为各种等价形式，但我无法在两者之间产生一系列等价。

比如我发现y >> pure x可以改写如下

y >>= const (pure x)
y *> pure x
(id <$ y) <*> pure x
fmap (const id) y <*> pure x

和liftM (const x) y可以改写如下

fmap (const x) y
pure (const x) <*> y

在我看来，这些都不是必然等价的，但我想不出它们不等价的任何情况。

Answer 1

是的，它们是一样的

让我们从flip (>>) . pure开始，这是您提供的x >> pure y的免积分版本：

flip (>>) . pure

flip (>>) 就是 (=<<) . const，所以我们可以重写为：

((=<<) . const) . pure

由于函数组合 ((.)) 是关联的，我们可以这样写：

(=<<) . (const . pure)

现在我们想重写const . pure。我们可以注意到const 只是pure 在(a ->) 上，这意味着因为pure . pure 是fmap pure . pure，const . pure 是(.) pure . const，（(.) 是fmap 对于函子@987634 )。

(=<<) . ((.) pure . const)

现在我们再次关联：

((=<<) . (.) pure) . const

((=<<) . (.) pure) 是 liftM¹ 的定义，所以我们可以替换：

liftM . const

这就是目标。两者是一样的。

---

^{1：liftM的定义是liftM f m1 = do { x1 <- m1; return (f x1) }，我们可以将do脱糖成liftM f m1 = m1 >>= return . f。我们可以将(>>=) 翻转为liftM f m1 = return . f =<< m1 并省略m1 以得到liftM f = (return . f =<<) 一点无点魔法，我们得到liftM = (=<<) . (.) return}

Answer 2

另一个答案最终会到达那里，但它需要一个漫长的路线。真正需要的只是liftM、const 的定义和一个单子定律：m1 >> m2 和m1 >>= \_ -> m2 必须在语义上相同。 （确实，这是(>>)的默认实现，很少被覆盖。）然后：

liftM (const x) y
= { definition of liftM* }
y >>= \z -> pure (const x z)
= { definition of const }
y >>= \z -> pure x
= { monad law }
y >> pure x

* 好的，好的，所以liftM 的实际定义使用return 而不是pure。随便。

Answer 3

另一种可能的途径，利用适用法则：

例如我发现y >> pure x可以改写如下[...]

fmap (const id) y <*> pure x

这相当于……

fmap (const id) y <*> pure x
pure ($ x) <*> fmap (const id) y -- interchange law of applicatives
fmap ($ x) (fmap (const id) y) -- fmap in terms of <*>
fmap (($ x) . const id) y -- composition law of functors
fmap (const x) y

...正如您所指出的，它与liftM (const x) y 相同。

这条路线只需要应用法则而不是单子法则反映了(*>)（(>>) 的另一个名称）是一个Applicative 方法。