给定一个操作(??)
使得
(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)
迫使我们满足物业。
有反例吗? 如果不是,我们如何证明这个属性?
我们首先使用应用定律重写左侧。回想一下,<$>
和<*>
都是左结合的,因此我们有,例如,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
在最后一步中,我们利用了(??)
的结合性。
(呜。
它不仅保留了结合性,我想说这也许是应用法则背后的主要思想!
回想一下该类的数学风格形式:
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***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-} ≡g . (g***id)<$>fzip (fzip (a,b), c)
{-gAssc,zAssc-} ≡ g . (id***g)<$>fzip (a, fzip (b,c))
{-fComm,fIdnt-} ≡ g <$>fzip (a, g <$>fzip (b,c))
{-liftA2'-} ≡ liftZ2 g (a, liftZ2 g (b,c))