pure 和 liftA2 的应用函子定律是什么？

Question

我正在研究根据 pure 和 liftA2 制定 Applicative（以便 (<*>) = liftA2 id 成为派生组合器）。

我能想到一堆候选定律，但我不确定最小集合是什么。

f <$> pure x = pure (f x)
f <$> liftA2 g x y = liftA2 ((f .) . g) x y
liftA2 f (pure x) y = f x <$> y
liftA2 f x (pure y) = liftA2 (flip f) (pure y) x
liftA2 f (g <$> x) (h <$> y) = liftA2 (\x y -> f (g x) (h y)) x y
...

Answer 1

根据 McBride 和 Paterson 的 laws for Monoidal（第 7 节），我建议 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

此时我们已经根据 liftA2、pure 和任何 y 编写了 fmap； fmap完全由以上规律决定。尚未证明的其余证明由优柔寡断的作者留下，作为对已确定 reader.

的练习

Answer 2

根据在线书籍 Learn You A Haskell:Functors, Applicative Functors and Monoids，Applicative Functor 法则如下所示，但出于格式原因进行了重组；但是，我正在使这个 post 社区可编辑，因为如果有人可以嵌入推导，它会很有用：

    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]  (.) = (b->c) -> (a->b) -> (a->c)
application operator]    $ = (a->b) -> a -> b

Found a treatment on Reddit

pure 和 liftA2 的应用函子定律是什么？

What are the applicative functor laws in terms of pure and liftA2?

haskell

applicative