haskell - 仿函数定律是否证明了结构的完全保存？

Question

在 Data.Functor 的文档中以下两个被称为仿函数定律，所有仿函数都应遵守。

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

我的直觉告诉我仿函数应该起作用的方式是它们应该是“结构保持”，或者换句话说，如果你有一个函数 f :: a -> b它是相反的g :: b -> a然后

fmap f . fmap g  ==  id

我还没有想出 fmap 的实现这将遵守前两条法律并违反第二条，但这很难证明。有人可以启发我吗？

Answer 1

实际上，您的“第三”仿函数定律直接来自实际的仿函数定律以及 f . g ≡ id 的事实。 :

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

还有更多:Haskell 确保如果第一定律适用于 Functor例如，那么第二个也成立(这是 fmap 类型的自由定理)。 IE。你只需要证明fmap id ≡ id您的法律Functor实例以确保它是有效的。