haskell - 适用:证明 `pure f <*> x = pure (flip ($)) <*> x <*> pure f`

Question

在我学习期间Typoclassopedia我遇到了这个证明，但我不确定我的证明是否正确。问题是:

One might imagine a variant of the interchange law that says something about applying a pure function to an effectful argument. Using the above laws, prove that:

pure f <*> x = pure (flip ($)) <*> x <*> pure f

“以上法律”指向 Applicative Laws , 简要地:

pure id <*> v = v -- identity law
pure f <*> pure x = pure (f x) -- homomorphism
u <*> pure y = pure ($ y) <*> u -- interchange
u <*> (v <*> w) = pure (.) <*> u <*> v <*> w -- composition

我的证明如下:

pure f <*> x = pure (($) f) <*> x -- identical
pure f <*> x = pure ($) <*> pure f <*> x -- homomorphism
pure f <*> x = pure (flip ($)) <*> x <*> pure f -- flip arguments

Answer 1

你的证明的前两步看起来不错，但最后一步不行。虽然 flip 的定义允许您使用如下定律:

f a b = flip f b a

这并不意味着:

pure f <*> a <*> b = pure (flip f) <*> b <*> a

事实上，这在一般情况下是错误的。比较这两行的输出:

pure (+) <*> [1,2,3] <*> [4,5]
pure (flip (+)) <*> [4,5] <*> [1,2,3]

如果你想要提示，你将需要在某个时候使用原始互换定律来证明这个变体。

事实上，我发现我必须使用同态、互换和组合定律来证明这一点，并且证明的一部分非常棘手，尤其是让部分正确——比如 ($ f)，它不同于(($) f)。打开 GHCi 以仔细检查我的证明类型的每个步骤是否已检查并给出了正确的结果，这很有帮助。 (你上面的类型检查没问题；只是最后一步不合理。)

> let f = sqrt
> let x = [1,4,9]
> pure f <*> x
[1.0,2.0,3.0]
> pure (flip ($)) <*> x <*> pure f
[1.0,2.0,3.0]
>