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)

---

Я потратил немного времени, глядя на аппликативный l aws, но я не смог найти доказательства, что это так. Поэтому я решил это опровергнуть. Все готовые приложения (Maybe, [], Either, и c.), Которые я пробовал, следуют закону, поэтому я подумал, что создам свой собственный.

Моя лучшая идея состояла в том, чтобы сделать бессодержательное аппликативное слово с дополнительной информацией.

data Vacuous a = Vac Alg

Где Alg - некоторая алгебра, которую я определил бы позже, когда мне будет удобно, чтобы сделать свойство неуспешно, но аппликативный l aws успешен.

Теперь мы определяем наши экземпляры как таковые:

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, который также подлежит определению. На самом деле нет другого способа go определить это.

Если мы хотим выполнить закон Идентификации , это заставляет 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)

Заставляет нас удовлетворять свойство.

Есть контрпример? Если нет, то как мы можем доказать это свойство?

Answer 1

Начнем с переписывания левой части, используя аппликатив l aws. Напомним, что и <$>, и <*> левоассоциативны, поэтому у нас есть, например, 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

, где на последнем шаге мы использовали ассоциативность (??).

(Уф.)

Answer 2

Он не только сохраняет ассоциативность, я бы сказал, что, возможно, основная идея за аппликативным l aws в первую очередь!

Вспомните математическую форму выражения class:

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

с l aws

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 href="https://hackage.haskell.org/package/base-4.14.0.0/docs/Control-Arrow.html#v:-42--42--42-" rel="nofollow noreferrer" title="(***) :: (a->α) -> (b->β) -> (a,b)->(α,β)">***</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

ie

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