`<*>`和`<$>`之间的关系

Question

根据Haskell Wikibook,以下关系<$>并<*>保持:

f <$> x = pure f <*> x

他们声称,人们可以证明这个定理是算子和适用法则的结果.

我不知道如何证明这一点.任何帮助表示赞赏.

Answer 1

函子和应用定律

让我们从函子和应用定律开始。让我们看一下 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 相同。从某种意义上说，这意味着纯粹保留了函数应用。

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

复合定律规定，pure (.)复合态射的方式与复合函数的方式类似(.)：将复合态射pure (.) <*> u <*> v应用于所得到的结果与应用于所得到的结果w相同。uvw

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

每@benjamin-hodgson

它足以表明fmap f x = pure f <*> x遵守fmap id = id法律是适用法律的结果。

我们之所以只需要证明 服从fmap f x = pure f <*> x定律fmap id = id，是因为可以证明第二函子定律遵循第一定律。我已经简要介绍了这个证明，但爱德华·克梅特（Edward Kmett）在这里有一个更详细的版本

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

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

给定函数f、g、k等，则h是给定函子的“自然”映射函数。该定理的完整证明有点冗长，但 Bartosz Milewski对其提供了很好的概述。g . h = k . f$map g . fmap h = fmap k . $map' f$map

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

引理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

f . g = id . (f . g)这是显而易见的id . v = v

把它们放在一起

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遵守第一函子法则。