Haskell Functor暗示着法律 [英] Haskell Functor implied law

问题描述

Typeclassopedia 说：

也有类似的论点表明任何满足第一定律的函子实例（fmap id = id）都会自动满足第二个定律，实际上，这意味着只需要检查第一个定律（通常通过非常简单的归纳），以确保函数

如果是这种情况，为什么我们还要提到第二个函数法？

<$法则1：fmap id = id
定律2：fmap（g。h）=（fmap g）。 （fmap h）

解决方案

虽然我无法给我相信这是说由于 parametricity ，只要第一定律成立，类型系统就执行第二定律。指定两个规则的原因是，在更一般的数学设置中，可能有一些类别 C ，完全可以从 C 自己定义一个映射 （即 Obj C ）和 Hom（ C ）分别遵守第一条规则但未遵守第二条规则，因此未能构成函子。

请记住<$在Haskell中，c $ c> Functor s是 Hask 类中的endofunctors，即使在数学上被认为是 Hask 在Haskell中表达...参数多态的约束排除了能够指定一个仿函数，它对于它所映射的所有对象（类型）不是一致的。

基于此主题 ，普遍的共识似乎是，第一条为Haskell Functor 实例的第二条法则。 Edward Kmett 表示，

给定 fmap id = id ， fmap（f。g）= fmap F 。 fmap g 遵循fmap的免费
定理。

在一篇长篇论文旁边，但我忘了在哪里。

Typeclassopedia says:

"A similar argument also shows that any Functor instance satisfying the first law (fmap id = id) will automatically satisfy the second law as well. Practically, this means that only the first law needs to be checked (usually by a very straightforward induction) to ensure that a Functor instance is valid."

If this is the case, why do we even mention the second functor law?

Law 1: fmap id = id
Law 2: fmap (g . h) = (fmap g) . (fmap h)

解决方案

While I can't give a proof, I believe what this is saying is that due to parametricity, the type system enforces the second law as long as the first law holds. The reason to specify both rules is that in the more general mathematical setting, you might have some category C where it is perfectly possible to define a "mapping" from C to itself (i.e. a pair of endofunctions on Obj(C) and Hom(C) respectively) which obeys the first rule but fails to obey the second rule, and therefore fails to constitute a functor.

Remember that Functors in Haskell are endofunctors on the category Hask, and not even everything that would mathematically be considered an endofunctor on Hask can be expressed in Haskell... the constraints of parametric polymorphism rule out being able to specify a functor which does not behave uniformly for all objects (types) which it maps.

Based on this thread, the general consensus seems to be that the second law follows from the first for Haskell Functor instances. Edward Kmett says,

Given fmap id = id, fmap (f . g) = fmap f . fmap g follows from the free theorem for fmap.

This was published as an aside in a paper a long time back, but I forget where.

这篇关于Haskell Functor暗示着法律的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！