Haskell有一个名为seq
的神奇函数,它接受任何类型的参数,并将其简化为 * 弱头范式 *(WHNF)。
我读过一些资料[我现在不记得他们是谁了 *...],他们声称“多态seq
是坏的”。
类似地,有一个rnf
函数,它将一个参数简化为 * 范式 *(NF)。它不适用于任意类型。在我看来,“很明显”可以修改语言规范,将其作为内置原语提供,类似于seq
。据推测,这将比仅仅使用seq
“甚至更糟糕”。这是怎么回事呢?
最后,有人建议给seq
、rnf
、par
和类似的函数赋予与id
相同的类型,而不是现在的const
函数,这将是一种改进。为什么呢?
3条答案
按热度按时间rjee0c151#
就我所知,多态
seq
函数是不好的,因为它削弱了自由定理,或者换句话说,一些在没有seq
时有效的等式在有seq
时不再有效。对于所有函数
g :: tau -> tau'
、所有列表xs :: [tau]
和所有多态函数f :: [a] -> [a]
都成立。基本上,这个等式表明f
只能重新排序其参数列表的元素或删除或复制元素,但不能发明新元素。老实说,它可以发明元素,就像它可以在列表中“插入”一个非终止计算/运行时错误一样,因为错误的类型是多态的。也就是说,在没有
seq
的编程语言中,这种等式已经被打破了。下面的函数定义提供了一个反例。基本上,在左手边的g
“隐藏”了错误。为了修正方程,
g
必须是严格的,也就是说,它必须将一个错误Map到另一个错误,在这种情况下,等式再次成立。如果添加多态
seq
运算符,则等式再次中断,例如,下面的示例化是一个反例。如果我们考虑列表
xs = [False, True]
,我们有但另一方面
也就是说,你可以使用
seq
使列表中某个位置的元素依赖于列表中另一个元素的定义性。如果g
是total,等式仍然成立。如果你对自由定理感兴趣,请查看free theorem generator。它允许您指定是考虑一种有错误的语言,还是考虑一种有seq
的语言,尽管这看起来没有什么实际意义,seq
破坏了一些用来提高函数式程序性能的转换,例如,foldr
/build
融合在seq
存在的情况下失败。如果你对seq
存在的情况下的自由定理的更多细节感兴趣,请看一下Free Theorems in the Presence of seq。据我所知,当多态
seq
被添加到语言中时,它会破坏某些转换。然而,其他的方法也有缺点。如果你添加一个基于seq
的类型类,那么如果你在程序的深处添加一个seq
,你可能不得不添加很多类型类约束。此外,省略X1 M23 N1 X不是一个选择,因为已经知道存在可以使用X1 M24 N1 X来修复的空间泄漏。最后,我可能遗漏了一些东西,但我不知道
a -> a
类型的seq
操作符是如何工作的。seq
的线索是它计算表达式的头部范式,如果另一个表达式的计算结果为头范式。如果seq
的类型为a -> a
,则无法使一个表达式的计算依赖于另一个表达式的计算。mbjcgjjk2#
在this answer中给出了另一个反例--单子不能满足
seq
和undefined
的单子定律。由于undefined
在图灵完备语言中是不可避免的,因此要受责备的是seq
。nzrxty8p3#
对
Prelude.seq
的焦虑(通常与⊥
有关)主要归因于以下几个原因:1.它削弱了“外延性”
1.它削弱了参数性
1.它使各种定律无效,例如用于一元接口的定律
然而:
1.参数性同样被GADT和满足函子定律的Map函数as shown by的组合所削弱,帕特丽夏·约翰(Patricia Johann)、恩里科·吉奥齐(Enrico Ghiorzi)和丹尼尔·杰弗里斯(Daniel Jeffries)。
1.多态定点运算符的存在:
也对参数性施加了限制,as specified by Philip Wadler。
1.运算符和值的某些组合可以使基本的逻辑或数学规则无效,这并不新鲜,例如除法和零。像除法一样,selective strictness是必要的--用于确定严格性(一个重要属性)的算法受Rice's theorem的约束:它们并不总是成功的,这会导致程序中意外的过多内存使用(即空间泄漏)。至于选择使用原语运算符或注解(对于patterns或types),这通常不会改变对重要定理和定律的不利影响。
另一种选择是使用按值调用语义的augmented form,但这假定所使用的扩充方法足够 “表现良好”。
在未来的某个时候,也许计算科学会有一个或多个进步来解决这个问题。在那之前,最实际的选择是管理有用的定律和定理之间的尴尬的交互,这与其他real-world programming features沿着。