haskell - 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)

强制我们满足属性(property)。

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

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

最后一种形式表明，本质上，原始表达式“运行” Action 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

在最后一步中，我们利用了 (??) 的关联性.

(哇。)