rseq/seq 的存在是否会破坏参照透明性？是否有一些替代方法没有？

Question

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

(更新：我在这件事上的推理来自自然演绎规则。单元类型对应于真（⊤），我们有一个扩展规则“如果x : ⊤然后() : ⊤” . 例如，参见this text 第 20 页。我认为用扩展或收缩替换表达式是安全的。）

这种优化的一个结果是undefined :: () 将被() :: () 取代，但我不认为这是一个问题——它只会让程序变得更懒惰（并且依赖undefined :: () 肯定是一种糟糕的编程习惯）。

但是今天我意识到这样的优化会完全破坏Control.Seq。 Strategy 定义为

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 的存在是否会破坏引用透明度（即使我们只考虑终止表达式）？
• 或者这是 Strategy 的设计缺陷，我们可以设计一种更好的方法来强制表达式与此类优化兼容的 WHNF？

Answer 1

引用透明性是关于等式声明和变量引用。当您说 x = y 并且您的语言在引用上是透明的，那么您可以用 y （模范围）替换每次出现的 x。

如果您没有指定x = ()，那么您不能安全地将x 替换为()，例如您的情况。这是因为你对() 的居民有误，因为在Haskell 中有两个：一个是() 的唯一构造函数，即()。另一个是从未计算过的值。你可以称它为 bottom 或 undefined：

x :: ()
x = x

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

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

Answer 2

您对引用透明度的定义不正确。引用透明并不意味着您可以将x :: () 替换为() :: () 并且一切都保持不变；这意味着您可以用其定义替换所有出现的变量，并且一切都保持不变。如果使用此定义，seq 和 rseq 不会与引用透明性冲突。

Answer 3

seq 在这里是一个红鲱鱼。

unitseq :: () -> a -> a
unitseq x y = case x of () -> y

这与单元上的seq 具有相同的语义，并且不需要魔法。事实上，seq 仅在处理无法进行模式匹配的事物（即函数）时才具有“魔力”。

用() 替换undefined :: () 与unitseq 和更神奇的seq 具有相同的不良影响。

一般来说，我们认为值不仅是它们的“什么”，而是它们是如何定义的。从这个角度来看，应该很清楚为什么我们不能任性地实施改变定义的转换。

Answer 4

感谢所有鼓舞人心的答案。再想一想，得出以下观点：

视图 1：仅考虑终止表达式

如果我们将自己限制为规范化系统，那么seq（或rseq 等）对程序的结果没有影响。它可以改变程序使用的内存量并增加 CPU 时间（通过评估我们实际上不需要的表达式），但结果是一样的。所以在这种情况下，规则x :: () --> () :: () 是可以接受的——不会丢失任何东西，可以节省CPU 时间和内存。

观点 2：Curry-Howard 同构

由于 Haskell 是图灵完备的，因此任何类型都包含一个无限循环，因此 C-H 对应的逻辑系统是不一致的（正如 Vitus 所指出的）——任何事情都可以证明。所以实际上任何规则在这样的系统中都是可以接受的。这可能是我最初的想法中最大的问题。

视图3：扩展规则

自然演绎规则为我们提供了不同类型运算符的缩减和扩展。例如-> 是 β-reduction 和 η-expansion，对于 (,) 它是

fst (x, y) --reduce--> x（snd 也是如此）

x : (a,b) --expand--> (fst x, snd x)

等等。由于底部的存在，减少规则仍然可以接受（我相信），但扩展规则不可以！特别是对于->：

rseq (undefined :: Int -> Int) = undefined

但它是 η-展开

rseq (\x -> (undefined :: Int -> Int) x) = ()

或(,)：

case undefined of (a,b) -> ()

但是

case (fst undefined, snd undefined) of (a,b) -> ()

等等。所以同理，() 的扩展规则是不可接受的。

视图 4：惰性模式匹配

允许x :: () 扩展为() :: () 可以被视为强制对单构造函数数据类型的所有模式匹配为lazy 的特殊情况。我从未见过在多构造函数数据类型上使用惰性模式匹配，所以我相信这种更改将使我们能够完全摆脱 ~ 惰性模式匹配符号。但是，它会将语言的语义更改为更加懒惰（另请参阅 Daniel Fischer 对该问题的评论）。此外（如问题中所述）打破Strategy。