函子法律是否证明结构的完整保存？ [英] Do the functor laws prove complete preservation of structure?

问题描述

在 Data.Functor 的文档中，以下两个是所有仿函数应该遵守的仿函数法则。

In the documenation for Data.Functor the following two are stated as the functor laws, which all functors should adhere to.

fmap id  ==  id
fmap (f . g)  ==  fmap f . fmap g

我的直觉告诉我仿函数应该工作的是它们应该是结构保存，换句话说，如果你有一个函数 f :: a - > b ，它是相反的 g :: b - > a 然后

The way my intuition tells me functors should work is that they should be "structure preserving", or in other words, if you have a function f :: a -> b and it's inverse g :: b -> a then

fmap f . fmap g  ==  id

我无法想出 fmap 将遵守前两条法律并违反第二条法律，但这很难证明。其实，你的第三函子定律直接来自实际的函子定律，而且事实上，<$ $>

I have not been able to come up with an implementation of fmap that would adhere to the first two laws and violate the second, but that's hardly proof. Can someone enlighten me?

推荐答案

c $ c> f。 g≡id ：

Actually, your "third" functor law follows directly from actual functor laws and the fact that f . g ≡ id:

fmap f . fmap g ≡ fmap (f . g) ≡ fmap id ≡ id

还有更多：Haskell确保如果第一定律适用于 Functor 实例，那么第二个定律也成立（这是 fmap ）。即你必须证明你的 Functor 实例只有 fmap id≡id law，以确保它是有效的。

And there's more: Haskell ensures that if first law holds for Functor instance, then the second one also holds (this is a free theorem for the type of fmap). I.e. you have to prove only fmap id ≡ id law for your Functor instance to ensure that it is valid.

这篇关于函子法律是否证明结构的完整保存？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！