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

Question

根据Haskell Wikibook ，<$> 之间的关系如下和 <*>捕获:

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

他们声称可以证明这一定理是仿函数和应用定律的结果。

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

Answer 1

仿函数和应用法则

让我们从仿函数和应用定律开始。 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

The identity law says that applying the pure id morphism does nothing, exactly like with the plain id function.

The homomorphism law says that applying a "pure" function to a "pure" value is the same as applying the function to the value in the normal way and then using pure on the result. In a sense, that means pure preserves function application.

The interchange law says that applying a morphism to a "pure" value pure y is the same as applying pure ($ y) to the morphism. No surprises there - as we have seen in the higher order functions chapter, ($ y) is the function that supplies y as argument to another function.

The composition law says that pure (.) composes morphisms similarly to how (.) composes functions: applying the composed morphism pure (.) <*> u <*> v to w gives the same result as applying u to the result of applying v to w.

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

每@benjamin-hodgson

it suffices to show that fmap f x = pure f <*> x obeys the fmap id = id law as a consequence of the Applicative laws.

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

Wadler 的 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这样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
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通过应用应用定律遵守第一仿函数定律。