haskell - 在pure和liftA2方面适用的仿函数定律是什么？

我正在按照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

...

最佳答案

基于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

至此，我们已经根据fmap，liftA2和任何pure编写了y； fmap完全由上述法律确定。尚未确定的证据的其余部分由不确定的作者留下，作为对确定的读者的练习。

关于haskell - 在pure和liftA2方面适用的仿函数定律是什么？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/29017633/