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'.
Кто нибудь подскажет, как выровнять доказательство?

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

no subject

no subject

no subject

no subject