我们首先使用适用的法律重写左侧。回想一下<$>
和<*>
都是左关联的,因此我们有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,c)
{-fIdnt,fComm-} ≡ g . (g***id) <$> fzip (fzip (a,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))
本文链接:https://www.f2er.com/2264603.html