haskell - rseq/seq 的存在是否会破坏引用透明度？是否有一些替代方法不可以？

Question

我一直认为用 ()::() 替换表达式 x::() 是编译 Haskell 程序时最基本的优化之一。由于()只有一个居民，无论x是什么，它的结果都是()。在我看来，这种优化是引用透明性的重要结果。我们可以对任何类型的单一居民进行这样的优化。

(更新:我在这件事上的推理来自自然演绎规则。其中单位类型对应于真值(⊤)，并且我们有一个扩展规则“if x : ⊤ then () : ⊤"。例如，请参阅 this text 第 20 页。我认为用其扩展或收缩替换表达式是安全的。)

此优化的一个结果是 undefined::() 将被 ()::() 替换，但我不认为这是一个问题 - 它只会使程序变得更加懒惰(并且依赖 undefined::() 肯定是一种糟糕的编程实践)。

然而今天我意识到这样的优化会完全破坏Control.Seq。 策略定义为

type Strategy a = a -> ()

我们有

-- | 'rseq' evaluates its argument to weak head normal form.
rseq :: Strategy a
rseq x = x `seq` ()

但是 rseq x::() 因此优化会简单地丢弃 x 到 WHNF 所需的评估。

那么问题出在哪里呢？

• rseq 和 seq 的存在是否会破坏引用透明度(即使我们只考虑终止表达式)？
• 或者这是策略设计的一个缺陷，我们可以设计一种更好的方法来强制表达式与此类优化兼容的 WHNF？

Answer 1

引用透明度涉及相等语句和变量引用。当您说x = y并且您的语言是引用透明的时，您可以将每次出现的x替换为y(模范围)。

如果您没有指定 x = ()，则无法安全地将 x 替换为 ()，例如你的情况。这是因为你对 () 的居民的理解是错误的，因为在 Haskell 中有两个:一个是 () 的唯一构造函数，即 ( )。另一个是从未计算过的值。您可以将其称为底部或未定义:

x :: ()
x = x

您当然不能在这里用 () 替换任何出现的 x，因为这会影响语义。语言语义中 bottom 的存在允许一些尴尬的边缘情况，特别是当你有一个 seq 组合器时，你甚至可以证明每个 monad 都是错误的。这就是为什么在许多正式讨论中我们忽略底部的存在。

但是，引用透明度并不会因此受到影响。 Haskell 仍然是引用透明的，因此是一种纯粹的函数式语言。