应用：证明`pure f <*> x = pure (flip ($)) <*> x <*> pure f`答案

【问题标题】：Applicative: Prove `pure f <*> x = pure (flip ($)) <*> x <*> pure f`应用：证明`pure f <*> x = pure (flip ($)) <*> x <*> pure f`
【发布时间】：2023-03-07 21:32:01
【问题描述】：

在我研究Typoclassopedia 的过程中，我遇到了这个证明，但我不确定我的证明是否正确。问题是：

人们可能会想象交换定律的一种变体，它说明了将纯函数应用于有效论证的内容。使用上述定律，证明：

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

【问题讨论】：

标签： haskell applicative category-theory

【解决方案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)，这与 @ 不同987654326@。让 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]
>

【讨论】：

非常感谢，我最终通过从右侧到左侧来证明它。我不接受您的回答，因为它实际上不包含证明，愿意分享您的证明吗？
我的证明和你的证明是一样的，最后有几个额外的步骤，类似于@leftroundabout 的 eta 扩展。请随意接受您自己的完整答案。

【解决方案2】：

我最终证明了这一点：

pure (flip ($)) <*> x <*> pure f
    = (pure (flip ($)) <*> x) <*> pure f -- <*> is left-associative
    = pure ($ f) <*> (pure (flip ($)) <*> x) -- interchange
    = pure (.) <*> pure ($ f) <*> pure (flip ($)) <*> x -- composition
    = pure (($ f) . (flip ($))) <*> x -- homomorphism
    = pure (flip ($) f . flip ($)) <*> x -- identical
    = pure f <*> x

上一次变换的解释：

flip ($) 的类型为a -> (a -> c) -> c，直观地说，它首先接受a 类型的参数，然后是一个接受该参数的函数，最后它用第一个参数调用函数。所以flip ($) 5 将一个函数作为参数，该函数以5 作为参数调用。如果我们将(+ 2) 传递给flip ($) 5，我们得到flip ($) 5 (+2)，它等价于表达式(+2) $ 5，计算结果为7。

flip ($) f等价于\x -> x $ f，也就是说，它接受一个函数作为输入，并以函数f作为参数调用它。

这些函数的组合是这样的：首先flip ($)将x作为它的第一个参数，并返回一个函数flip ($) x，这个函数正在等待一个函数作为它的最后一个参数，它将被@调用987654338@ 作为它的论点。现在这个函数flip ($) x 被传递给flip ($) f，或者写成它等价的(\x -> x $ f) (flip ($) x)，这导致表达式(flip ($) x) f，它等价于f $ x。

您可以检查flip ($) f . flip ($) 的类型是这样的（取决于您的功能f）：

λ: let f = sqrt
λ: :t (flip ($) f) . (flip ($))
(flip ($) f) . (flip ($)) :: Floating c => c -> c

【讨论】：

最后一步很简单，只需要一个 eta 扩展，不是吗？ ($f) . flip ($) ≡ \x -> ($f) $ ($x) ≡ \x -> ($x)$f ≡ \x -> f $ x ≡ f.
@leftaroundabout 是的，应该是，我实际上正在写一篇关于 Typoclassopedia 的文章，其中包含练习的解决方案，这个解释是针对那个帖子的，所以我试图为任何挣扎的人逐个解释首先要掌握它。顺便说一句，感谢您的编辑，看起来好多了。

【解决方案3】：

我要说的是，这些定理通常在以 monoidal functor 的数学风格而不是应用程序版本（即等效类）编写时涉及的内容要少得多 p>

class Functor f => Monoidal f where
  pure :: a -> f a
  (⑂) :: f a -> f b -> f (a,b)

那么法律就是

id <$> v = v
f <$> (g <$> v) = f . g <$> v
f <$> pure x = pure (f x)
x ⑂ pure y = fmap (,y) x
a⑂(b⑂c) = assoc <$> (a⑂b)⑂c

assoc ((x,y),z) = (x,(y,z)).

然后这个定理是

pure u ⑂ x = swap <$> x ⑂ pure u

证明：

swap <$> x ⑂ pure u
    = swap <$> fmap (,u) x
    = swap . (,u) <$> x
    = (u,) <$> x
    = pure u ⑂ x

□

【讨论】：