Не могу доказать :-(

[lomeo]

Небольшое вступление.

Есть такой модуль Control.Applicative, в котором определён класс Applicative

class Functor a => Applicative a where
    pure :: a -> f a
    <*> :: f (a -> b) -> f a -> f b

т.е. он чуть шире Functor (за счёт pure), и чуть уже Monad. Золотая середина - полезно, когда нам от монад нужен только return.


Так вот есть такой метод: <**> :: f a -> f (a -> b) -> f b, который по сути представляет собой перевёрнутый <*>.
Однако его реализация в исходниках такая:

(<**>) = liftA2 (flip ($))

Я попытался привести это выражение к flip (*) и вот что у меня получилось:

liftA2 (flip ($))
\a b -> (flip ($)) <$> a <*> b -- definition of liftA2
\a b -> (fmap (flip ($)) a) <*> b -- definition of l<$>
\a b -> (pure (flip ($)) <*> a) <*> b -- Functor instance rule: f `fmap` a = pure f <*> a

В это месте у меня затык. Предположив, что a = pure a' можно получить

\a' b -> (pure (flip ($)) <*> pure a') <*> b -- a = pure a'
\a' b -> pure (flip ($) a') <*> b -- homomorphism rule: pure f <*> pure x = pure (f x)
\a' b -> pure ($ a') <*> b -- flip ($) x = ($ x)
\a' b -> b <*> pure a' -- interchange rule: u <*> pure y = pure ($ y) <*> u

Ну и возвращая a на место вместо a'

\a b -> b <*> a
flip (<*>)

ЧТД. Но! Я совершенно не уверен, что могу делать допущение подобное a = pure a'.
Кто нибудь подскажет, как выровнять доказательство?

Comments

[thesz.livejournal.com]

Подумал, подумал, и пришел к выводу, что можно делать допущение, подобное a = pure a'.

Таким образом ты просто конструируешь значение a :: Applicative f => f a. То есть, вкладываешь вычисление значения a' внутрь f, а это по другому сделать нельзя.

[lomeo.livejournal.com]

Видимо, надо знать ТК, чтобы можно было делать подобные допущения :-/

[thesz.livejournal.com]

Я посмотрел сюда: http://www.soi.city.ac.uk/~ross/papers/Applicative.pdf

По этому тексту получается вот, что:

...
\a b -> (flip ($)) <$> a <*> b -- definition of liftA2
\a b -> (pure (flip ($)) <*> a) <*> b -- definition of l<$>

Скобки можно переставлять и раскрывать? По статье - можно.

\a b -> pure (flip ($)) <*> a <*> b

Тут дальше лог с выводом типов, не то, чтобы это было доказательством, но, может, на что натолкнет:

*Main Control.Applicative> :t \ a b -> pure (flip ($)) <*> a <*> b
\ a b -> pure (flip ($)) <*> a <*> b :: (Applicative f) =>
                                        f a -> f (a -> b) -> f b
*Main Control.Applicative> :t \ a b -> pure (($)) <*> a <*> b
\ a b -> pure (($)) <*> a <*> b :: (Applicative f) => f (a -> b) -> f a -> f b
*Main Control.Applicative> :t pure (flip ($))
pure (flip ($)) :: (Applicative f) => f (a -> (a -> b) -> b)
*Main Control.Applicative> :t (<*>)
(<*>) :: (Applicative f) => f (a -> b) -> f a -> f b
*Main Control.Applicative> :t (pure (flip ($) <*>)
:1:20: parse error (possibly incorrect indentation)
*Main Control.Applicative> :t (pure (flip ($)) <*>)
(pure (flip ($)) <*>) :: (Applicative f) => f a -> f ((a -> b) -> b)
*Main Control.Applicative>

Первым параметром мы можем подставить f a, получим Applicative f => f ((a->b)->b). Если обединить (pure (flip ($)) <*> a) с (b :: f (a->b)) путем применения <*>, то и получим f b.

Как-то так.

Порядок применения эффектов в Applicative f сохраняется.

[lomeo.livejournal.com]

> Скобки можно переставлять и раскрывать? По статье - можно.
Раскрывать можно - ассоциация левая, а вот переставлять нельзя:

Есть composition rule:

pure (.) <*> u <*> v <*> w = u <*> (v <*> w)

Но мне не удалось свести к нему.

Насчёт вывода типов, я им активно пользовался в доказательстве, в посте я просто перевод с него сделал :-)

Насчёт доказательства:

1. Ни в одном из законов нет вывода аргумента из под pure, значит трюк с гомоморфизмом не применишь (всё равно вытаскивать придётся a и b)
2. Ни в одном из законов, кроме interchange нельзя обернуть параметры (флип), а interchange использует pure, из под которого уже не выведешь аргмент

Это меня убеждает в том, что с помощью законов и определений участвующих в уравнении функций, нельзя построить доказательство.

Т.е. можно построить доказательство, что

liftA2 (flip ($)) (pure a) (pure b) = pure b <*> pure a

Но вот с a и b никак - их с трубы не снимешь :-(

[thesz.livejournal.com]

Ну, а если с другой стороны? Если параллельно рассматривать "эффекты" и типы?

pure (выраженное через fmap, или так) производит некий "нулевой эффект," E0. Он устроен так, что E0 <*> E0 = E0, E <*> E0 = E и E0 <*> E = E0. Это можно вывести из законов, что в книжке, как я понимаю.

Как-то так:

f (a -> (a -> b) -> b) ->  f a ->   f (a -> b) -> f b
pure (flip ($))        <*> a   <*>  b
      E0                   Ea       Eb

Вроде, последовательность эффектов соблюдена.

Кстати, <*> - это символ последовательного разбора в Utrecht University parsers library. А <$>, по-моему, там был в начале последовательного разбора.

Типа такого:

pList1 pItem = (:) <$> pItem <*> pList pItem
pList pItem = pList1 <|> pure []

Но это уже оффтопик. ;)

[lomeo.livejournal.com]

Честно говоря, совсем не понял про эффекты. Что ты под ними понимаешь?
Почему

E <*> E0 = E

а

E0 <*> E = E0?

Насчёт библиотеки парсеров интересно - может быть это экземпляр парсера для Control.Applicative?

Ну и напоследок: почитай ниже коммент migmit. Мы доказываем то, что доказать нельзя, так как это неверно :-)

[thesz.livejournal.com]

Опечатался.

E0 - правый и левый нуль-эффект. E0 <*> E = E и E <*> E0 = E. Но, как показал migmit, это неверно.

Парсеры были раньше, они появились году в 2002-ом. ;)

[deni-ok.livejournal.com]

> Я совершенно не уверен, что могу делать допущение подобное a = pure a'

С точки зрения бананов и линз тип

pure :: (Functor f) => a -> f a

задаёт f-коалгебру (pure там - это psi в анаморфизме). Ну и для функторов есть изоморфизм между f a и a. Так что вроде можно, но я не настолько крут в бананах, чтобы поставить тут ЧТД :)

[lomeo.livejournal.com]

Короче, как ниже показал migmit они ни фига не равны :-)

[deni-ok.livejournal.com]

Ага, видел :)) migmit - голова!

[lomeo.livejournal.com]

Точна! Только вот надо править либо описание функции, либо её реализацию.

[deni-ok.livejournal.com]

В кафе может запостить?

[lomeo.livejournal.com]

У меня туда письма не ходят :((

[deni-ok.livejournal.com]

Тебя там забанили ?!
:)

[migmit.livejournal.com]

Почему никто до сих пор не сказал о моей потрясающей скромности?!

[deni-ok.livejournal.com]

Виноваты, Ваше Мигмитство! Обещаем исправиться!

offtop

[nealar.livejournal.com]

читал
http://okmij.org/ftp/Haskell/types.html#restricted-datatypes
?

Re: offtop

[lomeo.livejournal.com]

Не читал, почитаю :-)

[migmit.livejournal.com]

Перед тем, как что-то доказывать, убедить, что оно верно.

Prelude Control.Applicative> [1,2] <**> [(+ 1),(+ 3)]
[2,4,3,5]
Prelude Control.Applicative> [(+ 1),(+ 3)] <*> [1,2]
[2,3,4,5]

[lomeo.livejournal.com]

Опа! Самый неожиданный коммент, спасибо!

[lomeo.livejournal.com]

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

"A variant of <*> with the arguments reversed."

Поверил, понимаешь, на слово!