问`<*>`与`<$>`的关系

EN

函数式及其应用规律

让我们从函数式和应用法则开始。Let's take a look at these laws presented in the Haskell Wikibook。

fmap id = id                   -- 1st functor law
fmap (g . f) = fmap g . fmap f -- 2nd functor law

现在我们应该看看适用的法律。

pure id <*> v = v                            -- Identity
pure f <*> pure x = pure (f x)               -- Homomorphism
u <*> pure y = pure ($ y) <*> u              -- Interchange
pure (.) <*> u <*> v <*> w = u <*> (v <*> w) -- Composition

恒等式定律说，应用pure id态射什么也不做，这与普通的id函数完全一样。

同态定律指出，对“纯”值应用“纯”函数与以正常方式将函数应用于该值，然后对结果使用纯函数是相同的。从某种意义上说，这意味着纯保留函数的应用。

交换法则指出，对“纯”值pure y应用态射与对态射应用pure ($ y)是相同的。这并不奇怪-正如我们在高阶函数一章中看到的那样，($ y)是一个将y作为参数提供给另一个函数的函数。

合成法则说，pure (.)合成态射的方式类似于(.)合成函数的方式:将合成的态射pure (.) <*> u <*> v应用于w，与将u应用于v的结果应用于w的结果相同。

为了证明这种关系，我们需要证明什么

Per @benjamin hodgson

它足以表明，作为应用定律的结果，fmap f x = pure f <*> x遵守fmap id = id定律。

我们只需要证明fmap f x = pure f <*> x遵守fmap id = id定律的原因是因为第二函子定律可以证明是从第一定律开始的。我已经简要介绍了这个证明，但是Edward Kmett有一个更详细的here版本

Wadler的Theorems for Free的3.5节提供了一些关于map函数的工作。基于自由定理的思想，为一个函数所显示的任何内容都适用于相同类型签名的任何其他函数。因为我们知道list是一个函数式的函数，所以map :: (a -> b) -> [a] -> [b]的类型类似于fmap :: Functor f => (a -> b) -> [a] -> [b]的类型，这意味着Wadler对map的所有工作也同样适用于fmap。

Wadler关于map的结论引出了关于fmap的这个定理：

给定函数f、g、k和h，使得g . h = k . f然后是$map g . fmap h = fmap k . $map' f，其中$map是给定函数器的“自然”映射函数。这个定理的完整证明有点冗长，但Bartosz Milewski提供了它的一个很好的overview。

我们需要两个引理来证明第二个函数律是第一个引理的结果。

引理1

给定fmap id = id --the first functor law，然后是fmap f = $map f

fmap f = $map id . fmap f   --Because $map id = id
= fmap id . $map f          --Because of the free theorem with g = k = id and h = f
= $map f                    --Because of the first functor law

所以fmap f = $map f和扩展fmap = $map

引理2

在给定id . v = v的情况下，f . g = id . (f . g)是显而易见的

把所有这些放在一起

给定fmap id = id，然后是fmap f . fmap g = fmap (f . g)

fmap f . fmap g = $map f . fmap g  --Because of lemma 1
= fmap id . $map (f . g)           --Because of the free theorem for fmap and lemma 2
= $map (f . g)                     --Because of the first functor law
= fmap (f . g)                     --Because $map = fmap

因此，如果我们可以证明第一函子定律成立，那么第二个定律也将成立。

证明关系

来证明我们需要适用的身份法则。从定律上看，我们有pure id <*> v = v，从等价性出发，我们试图证明f <$> x = pure f <*> x。如果我们设为x = id，那么应用恒等式告诉我们，等价的右侧是id x，而第一函子定律告诉我们，左侧是id x。

f <$> x = pure f <*> x
id <$> x = pure id <*> x  -- Substitute id into the general form
id <$> x = x              -- Apply the applicative identity law
id x = x                  -- Apply the first functor law
x = x                     -- simplify id x to x

在那里，我们已经通过应用应用定律证明了fmap f x = pure f <*> x遵守第一函子定律。