Моноид в аппликативном функторе - моноид?

[_Ivana]

При решении одной задачки возникло такое предположение, и частично я вроде даже провел некоторые правдоподобные рассуждения, чтобы попытаться его доказать. Собственно, утверждение:
Мы имеем некоторый моноид. Применяем к нему аппликативный функтор. Получаем структуру, которая предположительно также является моноидом, с нейтральным элементом - нейтральным элементом исходного моноида при применении к нему этого функтора, и бинарной операцией - операцией исходного моноида, погруженной в контекст этого функтора, то есть:

Используется синтаксис Haskell

1) mempty' = pure mempty
2) mappend' a b = fmap mappend a <*> b (или mappend' = liftA2 mappend)

Таким образом можно неограниченно оборачивать моноиды в любое количество любых аппликативных функторов, сохраняя моноидальность результата. Я попробовал доказать выполнение условий левой и правой единиц образованного таким образом моноида, ассоциативность бинарной операции пока не осилил. Выкладки (после знаков равенства записаны номера тождеств, которые применялись при преобразованиях, тождества выписаны не все, а только которые потребовались для доказательства):

Используется синтаксис Haskell

Моноид:
m1) mappend mempty = id

Функтор:
f1) fmap id = id
f2) fmap (f . g) = fmap f . fmap g

Аппликативный функтор:
a1) pure f <*> pure x = pure (f x)
a2) u <*> pure y = pure ($ y) <*> u
a3) pure f <*> x = fmap f x

Новый моноид:
1) mempty' = pure mempty
2) mappend' a b = fmap mappend a <*> b (mappend' = liftA2 mappend)

Левая единица:
mappend' mempty' x = (1,2)
fmap mappend (pure mempty) <*> x = (a3)
(pure mappend) <*> (pure mempty) <*> x = (a1)
pure (mappend mempty) <*> x = (a3)
fmap (mappend mempty) x = (m1)
fmap id x = (f1)
x

Правая единица:
mappend' x mempty' = (1,2)
fmap mappend x <*> (pure mempty) = (a2)
pure ($ mempty) <*> (fmap mappend x) = (a3)
fmap ($ mempty) (fmap mappend x) = (f2)
fmap ($ mempty . mappend) x =
fmap (mappend mempty) x = (m1)
fmap id x = (f1)
x

Собственно, у меня несколько вопросов:
1) Не ошибся ли я в своих выкладках?
2) Натолкнёте на идею доказательства/опровержения последнего закона моноида - ассоциативности новой бинарной операции?
3) Справедливо ли вообще мое предположение о том, что это моноид?

ЗЫ пишу в этот раздел, т.к. вопрос теоретический, а не практического программирования.

[arseniiv]

Я щас предложу ерунду, так что не бейте. По непроверенному ощущению, если взять свободный моноид на трёх образующих $a, b, c$ и обработать подобным образом, то если в «функторном моноиде» $a'(b'c') = (a'b')c'$, всё в порядке. Это выглядит как какая-то ересь, но если верно, можно просто взять немного кода и напрямую это проверить. В качестве образующих можно взять "1", "2", "3" (а моноид, соответственно, String). Буду рад опровержению, а сам что-то не додумаюсь.

[_Ivana]

Вот немного кода и проверка ассоциативности напрямую - на примере трех аппликативных функторов: Maybe, [] и их композиции:

Используется синтаксис Haskell

import Data.Monoid
import Data.Functor
import Control.Applicative

newtype NT m a = NT (m a) deriving (Eq,Show)

instance (Monoid a, Applicative m) => Monoid (NT m a) where
    mempty = NT $ pure mempty
    mappend (NT a) (NT b) = NT $ mappend <$> a <*> b

main = do
    print $ (NT (Just "a") <>  NT (Just "b")) <> NT (Just "c")
    print $  NT (Just "a") <> (NT (Just "b")  <> NT (Just "c"))
    print $ (NT ["a"] <>  NT ["b"]) <> NT ["c"]
    print $  NT ["a"] <> (NT ["b"]  <> NT ["c"])
    print $ (NT (Just $ NT ["a"]) <>  NT (Just $ NT ["b"])) <> NT (Just $ NT ["c"])
    print $  NT (Just $ NT ["a"]) <> (NT (Just $ NT ["b"])  <> NT (Just $ NT ["c"]))
 

Используется синтаксис Haskell

NT (Just "abc")
NT (Just "abc")
NT ["abc"]
NT ["abc"]
NT (Just (NT ["abc"]))
NT (Just (NT ["abc"]))

https://ideone.com/OXkl6d

И я это конечно же проверял, как и условия нейтральных элементов. Но одно дело - проверить на нескольких конкретных аппликативных функторах, а совсем другое - строго доказать для любых. В первом посте корректность нейтральных элементов я именно доказываю теоретически для любого функтора. И ассоциативность операции мне в по-хорошему хотелось бы доказать так же.

[arseniiv]

_Ivana в сообщении #1063543 писал(а):

Но одно дело - проверить на нескольких конкретных аппликативных функторах, а совсем другое - строго доказать для любых.

Так если теперь применить equational reasoning? (то проблема сводится в точности к исходной, вижу свой ляп).

-- Сб окт 17, 2015 02:39:17 --

Кажется, соотношения

Используется синтаксис Haskell

pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
fmap f x = pure f <*> x

приводят обе штуки к

Используется синтаксис Haskell

pc <*> pc <*> pc <*> pma <*> pma <*> a <*> b <*> c where
    pc = pure (.)
    pma = pure mappend

Одну из них (левоассоциативную) — точно, а другую стало лень доделывать.

P. S. Вот первая, если вдруг что (app = mappend) — перепроверьте:

Используется синтаксис Haskell

[1] = pure app <*> (pure app <*> a <*> b) <*> c
[1] = pure (.) <*> pure app <*> (pure app <*> a) <*> b <*> c
[1] = pure (.) <*> (pure (.) <*> pure app) <*> pure app <*> a <*> b <*> c
[1] = pure (.) <*> pure (.) <*> pure (.) <*> pure app <*> pure app <*> a <*> b <*> c

[_Ivana]

arseniiv, большое спасибо, вы мне показали очевидные вещи, которые я до сего момента почему-то не замечал - левоассоциативность <*> приводит к очевидному

Используется синтаксис Haskell

a<*>b<*>c<*>d == (a<*>b)<*>c<*>d

из чего с применение упомянутого вами закона аппликативного функтора я получил тот же результат при раскрытии скобок. Второй вариант пока не раскрывал, но очень сильно подозреваю, что он раскроется в то же самое! Спасибо вам! Это именно то, что было надо!

-- 17.10.2015, 01:28 --

UPD мой первоначальный оптимизм немножко поутих, т.к. раскрытие выражения с правой скобкой пока приводит к несколько другому, более громоздкому, выражению, которое, впрочем, может быть эквивалентно требуемому. На первый взгляд выглядит очень похоже на трюк с

Используется синтаксис Haskell

($ a) . b == b a

, который потребовался для доказательства правой единицы.

-- 17.10.2015, 01:45 --

Второе выражение раскрывается в

Используется синтаксис Haskell

pc <*> pc <*> pc <*> pc <*> pc <*> pc <*> pc <*> pa <*> a <*> pa <*> b <*> c
app = mappend
pc = pure (.)
pa = pure app
 

, которое компилируется и выдает правильный результат Осталось его немножко редуцировать до удобоваримой формы

[arseniiv]

_Ivana в сообщении #1063572 писал(а):

Спасибо вам! Это именно то, что было надо!

Не за что! Надеюсь, оно действительно эквивалентно!

А попробуйте собрать px <*> py <*> pz = pure (x y z), чего-то я зря не собрал у себя:

Используется синтаксис Haskell

[1] = pure (.) <*> pure (.) <*> pure (.) <*> pure app <*> pure app <*> a <*> b <*> c
[1] = pure ((.) (.) (.) app app) <*> a <*> b <*> c
[1] = pure ((.) . (.) app app) <*> a <*> b <*> c
[1] = pure (\a b c -> (a `app` b) `app` c) <*> a <*> b <*> c

Это даже выглядит весьма знакомо…

[_Ivana]

Сборка трех точек и двух аппендов, когда все аргументы подряд и справа, действительно знакома. Я сейчас пытаюсь собрать свои 7 точек и 2 аппенда когда еще аргументы не подряд... Или не собирать а вашу первую форму привести к моей страшной или их обе привести к третьей еще более страшной, но одинаковой

-- 17.10.2015, 02:23 --

arseniiv у меня есть онлайн-лямбдабот - он например мне редуцировал сейчас

Используется синтаксис Haskell

(((((((.) (.)) (.)) (.)) (.)) (.)) (.))

в

Используется синтаксис Haskell

(((.) . (.)) .)

- щас с ним попробую поиграться...

[arseniiv]

Хм, а вот теперь мне уже во второй раз показалось, что может существовать функтор-контрпример такой, что образ моноида при нём хотя и будет моноидом (заменим a на pure a и ассоциативность получится сразу же), но все элементы — нет.

Как можно видеть, (c c c c c c c app) x f y z = app x (f y z), где c = (.), и чего-то я тоже не вижу, как x и f можно было бы поменять местами. Возможно, это нужное дополнительное ограничение на функтор. Или я плохо соображаю. (Ого, скоро утро. Конечно!)

-- Сб окт 17, 2015 04:35:55 --

_Ivana в сообщении #1063580 писал(а):

он например мне редуцировал сейчас

А ghci на что же? Я вот щас с TupleSections как летаю:

Используется синтаксис Haskell

> :t com com com com com com com (,)
com com com com com com com (,) :: a -> (a1 -> a2 -> b) -> a1 -> a2 -> (a, b)
> :set -XTupleSections
> com com com com com com com (1,,) '1' (2,,) '2' '3'
(1,'1',(2,'2','3'))

[_Ivana]

Мы с вами одновременно подобрались к одному и тому же. И я тоже пока не готов сказать, при каких условиях будет эквивалентность. Может всегда в теории, а может всегда в хаскеле, а может и там не всегда. Но мне интересен этот вопрос.

Либо уже ночь и я туплю, либо я таки поменял порядок и собрал все 3 аргумента подряд в конце Привел к виду

Используется синтаксис Haskell

pc <*> p ($ a) <*> p (((((((c c) c) c) c) c) c) a) <*> x <*> y <*> z

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

Последнее выражение (а значит и исходное с правой скобкой) привел к

Используется синтаксис Haskell

p ((. a) . (.) . a) <*> x <*> y <*> z

сейчас первое к нему если (надеюсь) приведу - то вроде пасьянс сойдется всегда в теории

Или я опять ошибся, и это просто бесточечная нотация правого применения апенда - что и было в самом начале )....

[arseniiv]

arseniiv в сообщении #1063582 писал(а):

функтор-контрпример

Никак не соображу, что от него требуется. Не перебирать же их. К тому же, не вижу никаких причин, почему он должен быть: какая разница, в каком порядке выполнять чистые действия? А порядок потенциально гразных a, …, c не меняется.

-- Сб окт 17, 2015 05:10:25 --

_Ivana в сообщении #1063583 писал(а):

сейчас первое к нему если (надеюсь) приведу - то вроде пасьянс сойдется всегда в теории

О, покажьте потом магию.

[_Ivana]

Моя магия оказалась шарлатанством - я с помощью законов функторов привел левую и правую порядки вычислений соответственно к

Используется синтаксис Haskell

p ((a .) . a) <*> x <*> y <*> z
p ((. a) . (.) . a) <*> x <*> y <*> z

, а это похоже те же наши левые/правые аппенды в бесточечной нотации...

-- 17.10.2015, 03:27 --

Я лохЪ! Это же свойства ВНУТРЕННЕГО моноида А он моноид и у него честная ассоциативность! И на нее мы опираемся, чтобы доказать ассоциативность внешнего - или я совсем отупел в пол-четвертого ночи Или магия сошлась.

[arseniiv]

https://wiki.haskell.org/Typeclassopedia#Laws_2 писал(а):

Considered as left-to-right rewrite rules, the homomorphism, interchange, and composition laws actually constitute an algorithm for transforming any expression using pure and (<*>) into a canonical form with only a single use of pure at the very beginning and only left-nested occurrences of (<*>). Composition allows reassociating (<*>); interchange allows moving occurrences of pure leftwards; and homomorphism allows collapsing multiple adjacent occurrences of pure into one.

Я сейчас потому проверю ваш вывод. [UPD: ага, не буду.]

-- Сб окт 17, 2015 05:50:40 --

_Ivana в сообщении #1063587 писал(а):

И на нее мы опираемся, чтобы доказать ассоциативность внешнего - или я совсем отупел в пол-четвертого ночи Или магия сошлась.

А, и правда, если левые штуки совпадают. Я тоже вам на слово поверил.

[_Ivana]

Я навскидку не понял что там написано, сейчас оформляю пошаговое доказательство аналогично первому посту... Как будет готово - выложу. Если в нем будут ошибки, интересно будет их увидеть

[arseniiv]

Надо просто вовремя применить zzz <*> pure g = pure ($ g) <*> zzz, если выдастся возможность. Это если вы будете повторять вывод с самого начала, с pa <*> a <*> (pa <*> b <*> c).

-- Сб окт 17, 2015 06:20:34 --

Всё сходится, подтверждаю!

Используется синтаксис Haskell

pa <*> a <*> (pa <*> b <*> c)
(pa <*> a) <*> ((pa <*> b) <*> c)
pc <*> (pa <*> a) <*> (pa <*> b) <*> c
pc <*> (pc <*> (pa <*> a)) <*> pa <*> b <*> c
pc <*> (pc <*> pc <*> pa <*> a) <*> pa <*> ...
pc <*> (p (c c app) <*> a) <*> pa <*> ...
pc <*> pc <*> p (c c app) <*> a <*> pa <*> ...
p (c c (c c app)) <*> a <*> pa <*> ...
p ($ app) <*> (p (c c (c c app)) <*> a) <*> ...
pc <*> p ($ app) <*> p (c c (c c app)) <*> a <*> ...
p (c ($ app)) <*> p (c c (c c app)) <*> ...
p ((c ($ app)) (c c (c c app))) <*> ...
[ghci] ((c ($ (,))) (c c (c c (,)))) 1 2 3 = (1,(2,3))
p (\a b c -> app a (app b c)) <*> ...
p (\a b c -> app (app a b) c) <*> ...

[_Ivana]

Не оптимизировал, просто аккуратно повторил весь путь преобразований полностью. Зато все сходится. Выдам себе шоколадную медаль И вам тоже

Используется синтаксис Haskell

Моноид:
m1) mappend mempty = id
m2) mappend (mappend x y) z = mappend x (mappend y z)

Функтор:
f1) fmap id = id
f2) fmap (f . g) = fmap f . fmap g

Аппликативный функтор:
a1) pure f <*> pure x = pure (f x)
a2) u <*> pure y = pure ($ y) <*> u
a3) pure f <*> x = fmap f x
a4) pure (.) <*> u <*> v <*> w = u <*> (v <*> w)

Новый моноид:
1) mempty' = pure mempty
2) mappend' a b = fmap mappend a <*> b (mappend' = liftA2 mappend)

Левая единица:

mappend' mempty' x = (1,2)
fmap mappend (pure mempty) <*> x = (a3)
(pure mappend) <*> (pure mempty) <*> x = (a1)
pure (mappend mempty) <*> x = (a3)
fmap (mappend mempty) x = (m1)
fmap id x = (f1)
x

Правая единица:

mappend' x mempty' = (1,2)
fmap mappend x <*> (pure mempty) = (a2)
pure ($ mempty) <*> (fmap mappend x) = (a3)
fmap ($ mempty) (fmap mappend x) = (f2)
fmap ($ mempty . mappend) x =
fmap (mappend mempty) x = (m1)
fmap id x = (f1)
x

Ассоциативность бинарной операции:

Левый порядок:
mappend' (mappend' x y) z = (1,2)
fmap mappend (fmap mappend x <*> y) <*> z = (a3)
pure mappend <*> (pure mappend <*> x <*> y) <*> z = (a4)
pure (.) <*> pure mappend <*> (pure mappend <*> x) <*> y <*> z = (a4)
pure (.) <*> (pure (.) <*> pure mappend) <*> pure mappend <*> x <*> y <*> z = (a4)
pure (.) <*> pure (.) <*> pure (.) <*> pure mappend <*> pure mappend <*> x <*> y <*> z = (a1)
pure (((((.) (.)) (.)) mappend) mappend) <*> x <*> y <*> z = (lambdabot pl)
pure ((mappend .) . mappend) <*> x <*> y <*> z = (lambdabot unpl)
pure (\ x y z -> mappend (mappend x y) z) <*> x <*> y <*> z = 
pure f <*> x <*> y <*> z where f = \ x y z -> mappend (mappend x y) z

Правый порядок:
mappend' x (mappend' y z) = (1,2)
fmap mappend x <*> (fmap mappend y <*> z) = (a3)
pure mappend <*> x <*> (pure mappend <*> y <*> z) = (a4)
pure (.) <*> (pure mappend <*> x) <*> (pure mappend <*> y) <*> z = (a4)
pure (.) <*> (pure (.) <*> (pure mappend <*> x)) <*> pure mappend <*> y <*> z = (a4)
pure (.) <*> pure (.) <*> pure (.) <*> (pure mappend <*> x) <*> pure mappend <*> y <*> z = (a4)
pure (.) <*> (pure (.) <*> pure (.) <*> pure (.)) <*> pure mappend <*> x <*> pure mappend <*> y <*> z = (a4)
pure (.) <*> pure (.) <*> (pure (.) <*> pure (.)) <*> pure (.) <*> pure mappend <*> x <*> pure mappend <*> y <*> z = (a4)
pure (.) <*> (pure (.) <*> pure (.)) <*> pure (.) <*> pure (.) <*> pure (.) <*> pure mappend <*> x <*> pure mappend <*> y <*> z = (a4)
pure (.) <*> pure (.) <*> pure (.) <*> pure (.) <*> pure (.) <*> pure (.) <*> pure (.) <*> pure mappend <*> x <*> pure mappend <*> y <*> z = (a1)
pure ((((((((.) (.)) (.)) (.)) (.)) (.)) (.)) mappend) <*> x <*> pure mappend <*> y <*> z = (a2)
pure ($ mappend) <*> (pure ((((((((.) (.)) (.)) (.)) (.)) (.)) (.)) mappend) <*> x) <*> y <*> z = (lambdabot pl)
pure ($ mappend) <*> (pure ((((.) . (.)) .) mappend) <*> x) <*> y <*> z = (a4)
pure (.) <*> pure ($ mappend) <*> pure ((((.) . (.)) .) mappend) <*> x <*> y <*> z = (lambdabot pl)
pure ((. mappend) . (.) . mappend) <*> x <*> y <*> z = (lambdabot unpl)
pure (\ x y z -> mappend x (mappend y z)) <*> x <*> y <*> z =
pure g <*> x <*> y <*> z where g = \ x y z -> mappend x (mappend y z)

f = g (m2) => ч.т.д.