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

[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]

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

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-ом. ;)