haskell - 为什么 seq 不好？

Question

Haskell 有一个名为 seq 的神奇函数，它接受任何类型的参数并将其简化为弱头范式 (WHNF)。

我读过一些资料[但我现在不记得他们是谁了...]，它们声称“多态 seq 很糟糕”。他们在哪些方面“不好”？

类似地，还有 rnf 函数，它将参数简化为普通形式 (NF)。但是this是一个类方法；它不适用于任意类型。对我来说，“显而易见”的是，人们可以改变语言规范，将其作为内置原语提供，类似于 seq。据推测，这比仅仅拥有 seq“更糟糕”。这是什么情况？

最后，有人建议给 seq、rnf、par 和类似的类型与 id 相同的类型函数，而不是现在的 const 函数，将是一个改进。怎么会这样？

Answer 1

据我所知，多态 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 是总的，则等式再次成立。如果您对自由定理感兴趣，请查看 free theorem generator ，它允许您指定是否正在考虑一种有错误的语言，甚至是一种带有 seq 的语言。尽管这似乎不太实际，但 seq 破坏了一些用于提高函数程序性能的转换，例如 foldr/build 存在 seq 时融合失败。如果您对 seq 存在下的自由定理的更多细节感兴趣，请查看 Free Theorems in the Presence of seq .

据我所知，当多态 seq 添加到语言中时，它会破坏某些转换。然而，替代方案也有缺点。如果您添加基于类型类的 seq，如果您在深处的某处添加 seq，则可能需要向程序添加大量类型类约束。此外，省略 seq 并不是一个选择，因为我们已经知道存在可以使用 seq 修复的空间泄漏。

最后，我可能会错过一些东西，但我不明白 a -> a 类型的 seq 运算符如何工作。 seq 的线索是，如果另一个表达式被评估为 head 范式，它就会评估一个表达式为 head 范式。如果 seq 的类型为 a -> a，则无法使一个表达式的计算依赖于另一个表达式的计算。