Haskell Functor 暗含法则

23

Typeclassopedia中说:

"类似的论证也表明,任何满足第一个定律(fmap id = id)的Functor实例都将自动满足第二个定律。从实际上讲,这意味着只需要检查第一个定律(通常通过非常简单的归纳法完成)即可确保Functor实例是有效的。"

如果是这样的话,为什么我们还要提到第二个Functor定律呢?

Law 1: fmap id = id
Law 2: fmap (g . h) = (fmap g) . (fmap h)
4个回答

21

虽然我无法提供证明,但我认为这句话的意思是,由于 参数多态性,只要第一条规则成立,类型系统就强制执行第二条规则。之所以指定两个规则,是因为在更一般的数学设置中,你可能有一些类别C,可以定义从C到其自身的“映射”(即Obj(C)Hom(C) 上的一对自函数),该映射遵循第一个规则但不遵循第二个规则,因此不能构成一个函子。

请记住,Haskell 中的FunctorHask类别上的自函子,并且甚至不能用Haskell来表达在数学上被认为是Hask上的自函子的所有东西......参数多态性的约束排除了能够为所有对象(类型)均按一致方式进行映射的函子的指定。

根据此线程,普遍共识是第二条规则对于HaskellFunctor实例来说是由第一条规则推导而来的。Edward Kmett 表示

鉴于 fmap id = idfmap (f . g) = fmap f . fmap g遵循 fmap 的自由定理。

这曾经在一篇论文中作为旁注发表过,但我忘记了具体位置。


1
这里有一个更详细的写作,介绍从自由定理到第二函子定律的过程,https://github.com/quchen/articles/blob/master/second_functor_law.md - David
@David 这里有个打字错误:"Fnuctor" -> "Functor" - fans656
幸运的是,总会有一个箭头... ;-) - petre

14

使用 seq,我们可以编写一个满足第一条规则但不满足第二条规则的实例。

data Foo a = Foo a
    deriving Show

instance Functor Foo where
    fmap f (Foo x) = f `seq` Foo (f x)
我们可以验证这满足第一定律:
fmap id (Foo x)
= id `seq` Foo (id x)
= Foo (id x)
= Foo x

然而,它违反了第二定律:

> fmap (const 42 . undefined) $ Foo 3
Foo 42
> fmap (const 42) . fmap undefined $ Foo 3
*** Exception: Prelude.undefined

话虽如此,我们通常会忽略这样的病态情况。


2
请注意,当您在涉及底部值时使用seq区分不同行为时,您正在“破坏”类型系统。 Haskell类型形成Hask类别,其中函数是态射,但如果您不包括底部,则是如此。如果您在图像中包含底部,则类似于您的操作显示,结果结构不是范畴(关联性失败),因此谈论函子也没有意义。 - gigabytes

3
我认为第二定律提及的并不是其有效性,而是其重要的属性:
第一定律表示将恒等函数映射到容器中的每个项目不会产生影响。第二定律表示在每个项目上映射两个函数的组合与首先映射一个函数,然后映射另一个函数相同。——《类型类百科全书》
(我无法理解第一定律为什么暗示了第二定律,但我不是一位熟练的Haskeller - 当你知道正在发生什么时,这可能是显而易见的)

2
不要对自己太苛刻——这并不是那么显而易见的。 - Daniel Wagner

2
似乎最近才意识到第二条法律是从第一条法律中推导出来的。因此,在最初编写文档时,可能认为它是一个独立的要求。(个人而言,我对这个论点并不完全信服,但由于我还没有时间自己研究细节,所以在这里给予怀疑的好处。)

你提供的链接似乎是关于Functor实例的唯一性,而不是第一个法则暗示第二个法则... 这个线程 是关于后者的。 - Tom Crockett

网页内容由stack overflow 提供, 点击上面的
可以查看英文原文,
原文链接