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

根据Haskell Wikibook，<$>和<*>之间的以下关系成立:

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

他们声称，由于仿函数和适用法则的存在，可以证明这一定理。

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

最佳答案

仿函数和适用法

让我们从仿函数和适用法则开始。 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

我们需要证明什么才能证明这种关系

每个@ benjamin-hodgson



我们只需要证明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，而第一个Functor法则告诉我们该等价关系的左侧是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通过应用适用定律而服从了第一仿函数定律。

关于haskell - `<*>`和 `<$>`之间的关系，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/47277479/