应用：证明`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]
>

Answer 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作为第一个参数，returns一个函数flip ($) x，这个函数正在等待一个作为最后一个参数运行，将使用 x 作为参数调用。现在这个函数 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

Answer 3

我要说的是，通常，当以 幺半群函子 的数学风格而不是应用版本（即相当于 class

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

□

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

Applicative: Prove `pure f <> x = pure (flip ($)) <> x <*> pure f`

haskell

category-theory

applicative

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

Applicative: Prove `pure f <*> x = pure (flip ($)) <*> x <*> pure f`

haskell

category-theory

applicative

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

Applicative: Prove `pure f <> x = pure (flip ($)) <> x <*> pure f`