liftA2是否保留结合性？

Question

假设有一个操作(??)，使得

(a ?? b) ?? c = a ?? (b ?? c)

也就是说，(??) 是可结合的

必须满足这种情况吗？

liftA2 (??) (liftA2 (??) a b) c = liftA2 (??) a (liftA2 (??) b c)

也就是说，liftA2 (??) 是可结合的。

如果我们愿意的话，可以将其重写为：

fmap (??) (fmap (??) a <*> b) <*> c = fmap (??) a <*> (fmap (??) b <*> c)

---

我花了一点时间研究应用定律，但我无法证明这是正确的。所以我开始尝试反驳它。我尝试过所有开箱即用的应用（Maybe、[]、Either等），都遵循这个定律，所以我想我会创建自己的。

我最好的想法是创建一个带有额外信息的空应用。

data Vacuous a = Vac Alg

其中Alg是我稍后会自行定义的某种代数，以使属性失败但适用法则成功。

现在我们将实例定义为：

instance Functor Vacuous where
  fmap f = id

instance Applicative Vacuous where
  pure x = Vac i
  liftA2 f (Vac a) (Vac b) = Vac (comb a b)
  (Vac a) <*> (Vac b) = Vac (comb a b)

在这里，i 是待确定的 Alg 元素，comb 是待确定的 Alg 二元组合器。实际上，我们没有其他方式来定义它。

如果我们想要满足 恒等律，那么 i 就必须是在 comb 上的一个恒等元素。这时我们就可以免费得到 同态 和 交换。但是此时，由于 组成 要求 comb 在 Alg 上具有结合性。

((pure (.) <*> Vac u) <*> Vac v) <*> Vac w = Vac u <*> (Vac v <*> Vac w)
   ((Vac i <*> Vac u) <*> Vac v) <*> Vac w = Vac u <*> (Vac v <*> Vac w)
               (Vac u <*> Vac v) <*> Vac w = Vac u <*> (Vac v <*> Vac w)
                (Vac (comb u v)) <*> Vac w = Vac u <*> (Vac (comb v w))
                   Vac (comb (comb u v) w) = Vac (comb u (comb v w))
                         comb (comb u v) w = comb u (comb v w)

强制我们满足该属性。

有反例吗？如果没有，我们如何证明这个属性？

- Wheat Wizard

---

请注意，base的instance (Applicative f, Semigroup a) => Semigroup (Ap f a)依赖于此属性为真。 - Joseph Sible-Reinstate Monica

Answer 1

我们从应用定律入手重写左边，需要注意的是<$> 和 <*> 都是左结合的。例如： x <*> y <*> z = (x <*> y) <*> z 以及 x <$> y <*> z = (x <$> y) <*> z。

(??) <$> ((??) <$> a <*> b) <*> c
= fmap/pure law
pure (??) <*> (pure (??) <*> a <*> b) <*> c
= composition law
pure (.) <*> pure (??) <*> (pure (??) <*> a) <*> b <*> c
= homomorphism law
pure ((.) (??)) <*> (pure (??) <*> a) <*> b <*> c
= composition law
pure (.) <*> pure ((.) (??)) <*> pure (??) <*> a <*> b <*> c
= homomorphism law
pure ((.) ((.) (??)) (??)) <*> a <*> b <*> c
= definition (.)
pure (\x -> (.) (??) ((??) x)) <*> a <*> b <*> c
= definition (.), eta expansion
pure (\x y z -> (??) ((??) x y) z) <*> a <*> b <*> c
= associativity (??)
pure (\x y z -> x ?? y ?? z) <*> a <*> b <*> c

最后的形式揭示了本质上原始表达式以该顺序运行动作a、b和c，按照这种方式排序其影响，然后使用(??)纯粹地合并三个结果。

然后我们可以证明右边的形式等同于上述形式。

(??) <$> a <*> ((??) <$> b <*> c)
= fmap/pure law
pure (??) <*> a <*> (pure (??) <*> b <*> c)
= composition law
pure (.) <*> (pure (??) <*> a) <*> (pure (??) <*> b) <*> c
= composition law
pure (.) <*> pure (.) <*> pure (??) <*> a <*> (pure (??) <*> b) <*> c
= homomorphism law
pure ((.) (.) (??)) <*> a <*> (pure (??) <*> b) <*> c
= composition law
pure (.) <*> (pure ((.) (.) (??)) <*> a) <*> pure (??) <*> b <*> c
= composition law
pure (.) <*> pure (.) <*> pure ((.) (.) (??)) <*> a <*> pure (??) <*> b <*> c
= homomorphism law
pure ((.) (.) ((.) (.) (??))) <*> a <*> pure (??) <*> b <*> c
= interchange law
pure ($ (??)) <*> (pure ((.) (.) ((.) (.) (??))) <*> a) <*> b <*> c
= composition law
pure (.) <*> pure ($ (??)) <*> pure ((.) (.) ((.) (.) (??))) <*> a <*> b <*> c
= homomorphism law
pure ((.) ($ (??)) ((.) (.) ((.) (.) (??)))) <*> a <*> b <*> c

现在，我们只需要将无参函数表达式((.) ($ (??)) ((.) (.) ((.) (.) (??))))重写为更易读的有参函数形式，以便使它等于我们在证明的前半部分得到的表达式。这只是根据需要应用(.)和($)的问题。

((.) ($ (??)) ((.) (.) ((.) (.) (??))))
= \x -> (.) ($ (??)) ((.) (.) ((.) (.) (??))) x
= \x -> ($ (??)) ((.) (.) ((.) (.) (??)) x)
= \x -> (.) (.) ((.) (.) (??)) x (??)
= \x y -> (.) ((.) (.) (??) x) (??) y
= \x y -> (.) (.) (??) x ((??) y)
= \x y z -> (.) ((??) x) ((??) y) z
= \x y z -> (??) x ((??) y z)
= \x y z -> x ?? y ?? z

在最后一步中，我们利用了(??)的结合性。

(呼。)

- chi

---

哇，的确如此！我发现Haskell的柯里化风格对于那种证明工作并不是太有益。 - leftaroundabout

Answer 2

它不仅保留了结合性, 我认为这或许是应用法则背后的主要思想!

回忆一下类的数学式样式:

class Functor f => Monoidal f where
  funit ::    ()     -> f  ()
  fzip :: (f a, f b) -> f (a,b)

与法律相关

zAssc:  fzip (fzip (x,y), z) ≅ fzip (x, fzip (y,z))  -- modulo tuple re-bracketing
fComm:  fzip (fmap fx x, fmap fy y) ≡ fmap (fx<a title="(***) :: (a->α) -> (b->β) -> (a,b)->(α,β)" rel="nofollow noreferrer" href="https://hackage.haskell.org/package/base-4.14.0.0/docs/Control-Arrow.html#v:-42--42--42-">***</a>fy) (fzip (x,y))
fIdnt:  fmap id ≡ id                    -- ─╮
fCmpo:  fmap f . fmap g ≡ fmap (f . g)  -- ─┴ functor laws

在这种方法中，liftA2 会将一个元组值的函数映射到已经准备好的成对元素上，形成函数返回的新的元组。

liftZ2 :: ((a,b)->c) -> (f a,f b) -> f c
liftZ2 f = fmap f . fzip

即（即例如）

liftZ2 f (a,b) = f <$> fzip (a,b)

现在假设我们已经拥有

g :: (G,G) -> G
gAssc:  g (g (α,β), γ) ≡ g (α, g (β,γ))

或无点 (忽略元组括号交换)

gAssc:  g . (g***id) ≅ g . (id***g)

如果我们以这种方式编写所有内容，很容易看出关联性保持基本上只是使用 zAssc 实现的，而有关 g 的所有内容都在单独的 fmap 步骤中进行：

liftZ2 g (liftZ2 g (a,b), c)
    {-liftA2'-} ≡ g <$> fzip (g <$> fzip (a,b), c)
{-fIdnt,fComm-} ≡ <b>g . (g***id)</b> <$> <b>fzip (fzip (a,b), c)
{-gAssc,zAssc-} ≡ g . (id***g)</b> <$> <b>fzip (a, fzip (b,c))</b>
{-fComm,fIdnt-} ≡ g <$> fzip (a, g <$> fzip (b,c))
    {-liftA2'-} ≡ liftZ2 g (a, liftZ2 g (b,c))

- leftaroundabout

---

实际上，每当需要使用应用定律证明某些东西时，使用单调演示是一个明智的默认选择。 - duplode