haskell - `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 和 functor 给出的定律将这两个语句转换为各种等价形式，但我无法生成两者之间的等价序列。

例如，我发现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

另一个答案最终会到达那里，但它需要一个漫长的过程。实际需要的只是 liftM 的定义。 , const ，以及单个单子(monad)定律: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 。无论如何。