Каковы законы прикладного функтора в терминах чистого и поднятия А2?

Question

Я играю с формулировкой Аппликативный с точки зрения pure и liftA2 (так что (<*>) = liftA2 id становится производным комбинатором).

Я могу придумать кучу законов о кандидатах, но я не уверен, каким будет минимальный набор.

1. f <$> pure x = pure (f x)
2. f <$> liftA2 g x y = liftA2 ((f .) . g) x y
3. liftA2 f (pure x) y = f x <$> y
4. liftA2 f x (pure y) = liftA2 (flip f) (pure y) x
5. liftA2 f (g <$> x) (h <$> y) = liftA2 (\x y -> f (g x) (h y)) x y
6. ...

Answer 1

основе (раздел 7) laws for Monoidal Макбрайд и Патерсона я бы SuG gest следующие законы для liftA2 и pure.

левый и правый тождественное

liftA2 (\_ y -> y) (pure x) fy  = fy 
liftA2 (\x _ -> x) fx  (pure y) = fx 

ассоциативность

liftA2 id   (liftA2 (\x y z -> f x y z) fx fy) fz = 
liftA2 (flip id) fx (liftA2 (\y z x -> f x y z) fy fz) 

естественность

liftA2 (\x y -> o (f x) (g y)) fx fy = liftA2 o (fmap f fx) (fmap g fy) 

Это не сразу видно, что они являются достаточными для покрытия связи между fmap и Applicative «с pure и liftA2. Давайте посмотрим, если мы сможем доказать, из приведенных выше законов,

fmap f fx = liftA2 id (pure f) fx 

Мы начнем работать над fmap f fx. Все перечисленные ниже эквивалентны.

fmap f fx 
liftA2 (\x _ -> x) (fmap f fx) (  pure y)  -- by right identity 
liftA2 (\x _ -> x) (fmap f fx) ( id (pure y))  -- id x = x by definition 
liftA2 (\x _ -> x) (fmap f fx) (fmap id (pure y))  -- fmap id = id (Functor law) 
liftA2 (\x y -> (\x _ -> x) (f x) (id y)) fx (pure y) -- by naturality 
liftA2 (\x _ -> f x     ) fx (pure y) -- apply constant function 

На данный момент мы написали fmap с точки зрения liftA2, pure и любой y; fmap полностью определяется вышеуказанными законами. Остальная часть еще не доказанного доказательства остается нерешительным автором как упражнение для определенного читателя.

Answer 2

В соответствии с онлайн-книгой Learn You A Haskell:Functors, Applicative Functors and Monoids законы Применительного Functor ниже, но реорганизованы для форматирования; однако, я делаю это сообщение сообщества редактируемым, так как это было бы полезно, если бы кто-то мог вставлять выкладок:

identity]    v = pure id <*> v 
homomorphism]  pure (f x) = pure f <*> pure x 
interchange] u <*> pure y = pure ($ y) <*> u 
composition] u <*> (v <*> w) = pure (.) <*> u <*> v <*> w 

Примечание:

function composition] (.) = (a->b) -> (b->c) -> (a->c) 
application operator] $ = (a->b) -> a -> b 

Found a treatment on Reddit