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

[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, а это по другому сделать нельзя.

[deni-ok.livejournal.com]

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

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

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

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

offtop

[nealar.livejournal.com]

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

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