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

Question

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

• 身份： pure id <*> v = v
• 作品： pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
• 同态： pure f <*> pure x = pure (f x)
• 互换： u <*> pure y = pure ($ y) <*> u

然后它说作为这些规则的结果，底层的 Functor 实例将满足fmap f x = pure f <*> x。但是由于该方法fmap甚至没有出现在上述等式中，那么这个性质究竟是如何从它们得出的呢？

Answer 1

更新：我已经大大扩展了答案。我希望它有帮助。

“简短”答案：

对于任何 functor 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

不幸的是，文档没有包括一些解释或至少对这个极其不明显的事实的承认。

更长的答案：

最初，文档列出了四个定律（恒等式、组合式、同态性和互换性），再加上两个额外的关于*>and 的定律<*，然后简单地说：

该Functor实例应满足

fmap f x = pure f <*> x

上面的措辞被替换为新的案文：

作为这些定律的结果， 的Functor实例f将满足

fmap f x = pure f <*> x

作为2011 年 2 月提交 92b562403 的一部分，以响应Russell O'Connor 在库列表中提出的建议。

罗素指出，这条规则实际上是由其他适用法律所隐含的。最初，他提供了以下证明（帖子中的链接已损坏，但我在 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 的论文“Theorems for Free”。这是一个Stack Overflow 问题，链接到论文和其他一些资源。理解“真实”的理论很难，但你可以凭直觉思考。让我们选择一个特定的函子，比如Maybe. 假设我们有一个具有以下类型的函数；

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

请注意，无论 的实现多么复杂和复杂foo，相同的实现都需要适用于所有类型a和b. 它对 一无所知a，因此除了应用函数之外，它不能对 type 的值做任何事情，而这只会给它一个值。它对两者一无所知，因此它不能对值执行任何操作，除了 return 。重要的是，这意味着计算的结构进行由-它做什么与输入值，是否以及何时它决定应用等-是完全由是否确定是或afbbbJust someBvaluefooxfxNothingJust .... 想一想——foo可以检查x一下它是否是Nothing或Just someA。但是，如果是Just someA，它就无法了解有关该值的任何信息someA：它无法按原样使用它，因为它不了解类型a，并且无法使用 做任何事情f someA，因为它不了解类型b. 因此，如果x是Just someA，则该函数foo只能对其Just-ness起作用，而不能对基础值起作用someA。

这有一个惊人的后果。如果我们要使用一个函数通过编写以下内容g来改变输入值foo f x：

foo f' (fmap g x)

因为fmap g不会改变x的Nothing-ness 或Just-ness，所以这种改变对foo的计算结构没有影响。它的行为方式相同，以相同的方式处理NothingorJust ...值，f'在完全相同的情况下应用，并且与之前应用的时间完全相同f，等等。

这意味着，只要我们已经安排了一些事情，使得f'对g-transformed 值进行操作会给出与对原始值进行操作的h-transformed 版本相同的答案f——换句话说，如果我们有：

f' . g = h . f

然后我们可以用与处理原始输入完全相同的方式来foo处理我们的g-transformed 输入，只要我们foo通过应用h到输出来考虑在完成运行后的输入更改：

foo f' (fmap g x) = fmap h (foo f x)

我不知道这是否令人信​​服，但这就是我们得到自由定理的方式：

如果f' . g = h . f那么foo f' . fmap g = fmap h . foo f。

它基本上是说，因为我们可以以一种foo不会注意到的方式转换输入（因为它的多态类型），所以无论我们转换输入并运行foo，还是foo先运行并转换其输出，答案都是一样的。