Applicative类型类的实例的要求与它们对Functor的实现有何关系

Question

根据Haskell的库文档，Applicative类的每个实例必须满足以下四个规则：

• 身份： pure id <*> v = v
• 组成： pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
• 同态： pure f <*> pure x = pure (f x)
• interchange： u <*> pure y = pure ($ y) <*> u

然后，由于这些规则，底层的Functor实例将满足fmap f x = pure f <*> x。但是由于方法fmap甚至没有出现在上述方程式中，因此该属性如何精确地从它们得出？

Answer 1

Update：我已经大大扩展了答案。希望对您有所帮助。

“简短”答案：

对于任何函子F，类型都有一个“自由定理”（见下文）：

(a -> b) -> F a -> F b

[该定理指出，对于具有这种类型的任何（全部）函数，例如foo，对于具有适当匹配的任何函数f，f'，g和h，以下条件均成立类型：

如果为f' . g = h . f，则为foo f' . fmap g = fmap h . foo f。

请注意，为什么这是正确的，一点也不明显。

无论如何，如果设置f = id和g = id并使用函子定律fmap id = id，则该定理简化为：

对于所有h，我们都有foo h = fmap h . foo id。

现在，如果F也是可应用的，则该函数：

foo :: (a -> b) -> F a -> F b
foo f x = pure f <*> x

具有正确的类型，因此它满足定理。因此，对于所有h，我们具有：

pure h <*> x
-- by definition of foo
= foo h x
-- by the specialized version of the theorem
= (fmap h . foo id) x
-- by definition of the operator (.)
= fmap h (foo id x)
-- by the definition of foo
= fmap h (pure id <*> x)
-- by the identity law for applicatives
= fmap h x

换句话说，申请人的身份法暗示了这种关系：

pure h <*> x = fmap h x

很遗憾，文档没有对此事实进行某些解释或至少承认。更长的答案：

[最初，文档列出了四个定律（同一性，组成，同态和互换），以及*>和<*的两个附加定律，然后简单说明：

Functor实例应满足

fmap f x = pure f <*> x

以上措词已被新文本替换：

由于这些法律，Functor的f实例将满足

fmap f x = pure f <*> x

作为2011年2月commit 92b562403的一部分，以回应Russell O'Connor在图书馆名单上的suggestion。

罗素指出，该规则实际上是函子法所隐含的。最初，他提供了以下证明（帖子中的链接已断开，但我在archive.org上找到了副本）。他指出该功能：

possibleFmap :: Applicative f => (a -> b) -> f a -> f b
possibleFmap f x = pure f <*> x

满足fmap的函子定律：

pure id <*> x = x {- Identity Law -}

pure (f . g) <*> x
= {- infix to prefix -}
pure ((.) f g) <*> x
= {- 2 applications of homomorphism law -}
pure (.) <*> pure f <*> pure g <*> x
= {- composition law -}
pure f <*> (pure g <*> x)

然后推理：

因此，\f x -> pure f <*> x满足函子的定律。由于每种数据类型最多有一个仿函数实例，(\f x -> pure f <*> x) = fmap。

此证明的关键部分是每种数据类型只有一个可能的函子实例（即，只有一种定义fmap的方式。

当被问到这一点时，他给出了fmap唯一性的以下证明。

假设我们有一个函子f和另一个函数

foo :: (a -> b) -> f a -> f b

然后是foo的自由定理的结果，对于任何f :: a -> b以及任何g :: b -> c。

foo (g . f) = fmap g . foo f

特别是foo id = id，则

foo g = foo (g . id) = fmap g . foo id = fmap g . id = fmap g

显然，这主要取决于“ foo的自由定理的结果”。后来，罗素意识到自由定理可以与应用程序的身分法一起直接用于证明所需的法则。这就是我在上面的“简短回答”中总结的内容。

自由定理...

那么这个“自由定理”业务呢？

自由定理的概念来自Wadler的论文“免费定理”。这是Stack Overflow question，可链接到本文和其他一些资源。很难理解“真实”的理论，但是您可以凭直觉思考它。让我们选择一个特定的函子，例如Maybe。假设我们有一个具有以下类型的函数；

foo :: (a -> b) -> Maybe a -> Maybe b
foo f x = ...

请注意，无论foo的实现多么复杂和复杂，对于所有类型a和b而言，相同的实现都需要工作。它对a一无所知，因此除了应用函数a之外，它不能
do

具有h类型值的任何东西，而只是给它一个b值。它也不了解b，因此它不能do具有b值的任何东西，除非返回Just someBvalue。至关重要的是，这意味着foo执行的计算结构-它对输入值x的处理方式，是否以及何时决定应用f等-完全取决于x ]为Nothing或Just ...。仔细考虑一下-foo可以检查x以查看是Nothing还是Just someA。但是，如果它是Just someA，就无法了解有关值someA的任何信息：它不能按原样使用它，因为它无法理解a的类型，并且不能对它进行任何操作h someA，因为它不了解类型b。因此，如果x为Just someA，则函数foo只能以其Just形式起作用，而不能以基础值someA起作用。这具有惊人的后果。如果要使用函数g通过以下方式从foo f x下更改输入值：

foo f' (fmap g x)

因为fmap g不会更改x的Nothing -ness或Just -ness，所以此更改不会影响foo的计算结构。它的行为方式相同，以相同的方式处理Nothing或Just ...值，并在与先前应用f'完全相同的条件和相同的时间应用f，等等。>
[这意味着，只要我们进行了排列，以使f'转换为g转换后的值，就可以得到与h转换后的f转换为原始值的版本相同的答案- -换句话说，如果我们有：

f' . g = h . f

然后我们可以诱骗foo以与处理原始输入完全相同的方式处理g转换后的输入，只要我们通过应用[ C0]到输出：
foo

我不知道这是否令人信​​服，但这就是我们得到自由定理的方式：
如果为h，则为foo f' (fmap g x) = fmap h (foo f x)
。

基本上说，因为我们可以以f' . g = h . f不会注意到的方式转换输入（由于其多态类型），所以无论是转换输入并运行foo f' . fmap g = fmap h . foo f还是运行[ C0]，然后转换其输出。

Answer 2

TL; DR] Applicative定律衍生自一种替代表达，其定律根据fmap明确定义。有人可能会说正确的pure和<*>遵守他们的定律因为