为什么seq不好?
Haskell有一个名为seq
的神奇函数,它接受任何类型的参数并将其减少为弱头范式(WHNF)。
我读过几个消息来源[我不记得他们现在是谁......],声称“多态seq
不好”。 他们以什么方式“不好”?
类似地,还有rnf
函数,它将参数减少到Normal Form(NF)。 但这是一种类方法; 它不适用于任意类型。 对我来说,似乎“显而易见”的是,人们可以改变语言规范,将其作为内置原语提供,类似于seq
。 据推测,这可能比只有seq
更“糟糕”。 这是怎样的?
最后,有人建议给seq
, rnf
, par
和类似于id
函数的类型,而不是像现在这样的const
函数,这将是一种改进。 怎么会这样?
据我知道的多态seq
的功能是不好的,因为它削弱了免费的定理或者,换句话说,一些等式是有效的,而不seq
任何与不再有效seq
。 例如,平等
map g (f xs) = f (map g xs)
适用于所有函数g :: tau -> tau'
,所有列表xs :: [tau]
和所有多态函数f :: [a] -> [a]
。 基本上,这种平等说明f
只能重新排列其参数列表的元素,或删除或重复元素,但不能创造新的元素。
说实话,它可以发明元素,因为它可以将非终止计算/运行时错误“插入”列表中,因为错误类型是多态的。 也就是说,这种平等已经在像Haskell这样的编程语言中没有seq
。 下面的函数定义为这个方程提供了一个反例。 基本上,在左侧g
“隐藏”错误。
g _ = True
f _ = [undefined]
为了修正方程, g
必须严格,即必须将错误映射到错误。 在这种情况下,平等再次成立。
如果添加多态seq
运算符,则方程再次中断,例如,以下实例化就是一个反例。
g True = True
f (x:y:_) = [seq x y]
如果我们考虑列表xs = [False, True]
,我们有
map g (f [False, True]) = map g [True] = [True]
但另一方面
f (map g [False, True]) = f [undefined, True] = [undefined]
也就是说,您可以使用seq
使列表中某个位置的元素取决于列表中另一个元素的定义。 如果g
是总数,那么等式再次成立。 如果你在自由定理中进行了讨论,请查看免费的定理生成器,它允许你指定你是在考虑一个有错误的语言,甚至是一个带有seq
的语言。 尽管这似乎不太实际,但seq
打破了一些用于提高功能程序性能的转换,例如,在seq
存在下, foldr
/ build
融合失败。 如果在seq
存在的情况下对自由定理的更多细节进行了详细讨论,请查看seq
中存在的自由定理。
据我所知,已经知道一个多态seq
打破了一定的转换,当它被添加到语言。 但是,别名也有缺点。 如果你添加一个基于类型的seq
,你可能需要为你的程序添加大量的类型约束,如果你在内部深处添加一个seq
。 此外,它不是一个可以省略seq
的选择,因为它已经知道可以使用seq
来修复空间泄漏。
最后,我可能会错过一些东西,但我不明白类型a -> a
的seq
运算符是如何工作的。 seq
的线索是,如果另一个表达式被评估为标准形式,它将评估表达式以标准形式。 如果seq
已经键入a -> a
,则无法使一个表达式的评估取决于另一个表达式的评估。
在这个答案中给出了另一个反例 - monad不能满足seq
和undefined
单子法则。 而且由于undefined
在图灵完全语言中是不可避免的,所以应该指责的是seq
。
上一篇: Why is seq bad?