为什么 Haskell 中的 seq 必须对底部有特殊的规则？答案

【问题标题】：Why seq in Haskell has to have special rule for bottom?为什么 Haskell 中的 seq 必须对底部有特殊的规则？
【发布时间】：2014-10-31 07:59:19
【问题描述】：

Haskell 报告 2010 说 seq“削弱了 Haskell 的参数属性”，因为“⊥ 与 \x -> ⊥ 不同，因为 seq 可以用来区分它们”[1]。

这似乎完全是因为一个明确的规则：

seq ⊥ b  =  ⊥

我想知道为什么要引入这种特殊情况？一定是有原因的

seq a b  =  b

还不够，seq 需要针对这种特殊情况进行更复杂的定义：

seq ⊥ b  =  ⊥
seq a b  =  b, if a ≠ ⊥

[1]https://www.haskell.org/onlinereport/haskell2010/haskellch6.html#x13-1260006.2

[编辑] 它澄清了问题，这是另一个角度。为什么seq不能这样定义：

seq :: a -> b -> b
seq a b  =  b

seq 是一个特殊函数，它会“尽可能多地”评估其第一个参数。如果评估结果为 HNF，则该参数被完全评估。如果它会导致异常或底部值，则将它们存储起来，并在第一个参数实际用于评估第二个参数时抛出或返回。

这有点蹩脚，但我认为这应该让我的问题更清楚一些。这与seq 的工作方式无关。这是关于当前设计的意图。

从实施的角度来看，也许有一些明显的原因。或者它可能会产生一些后果，比如无法提供一些当前基于 seq 的有用属性，这些属性是用底部的特殊情况定义的。或者也许还有一些我不知道的其他联系。这就是我好奇的地方:)

【问题讨论】：

也许我在这里完全是愚蠢的，但第一个只是说明 seq 在第一个参数中是严格的，这就是首先使用 seq 的重点（它将 a 评估为 HNF）跨度>
（顺便说一句，⊥ 是否需要与\x -> ⊥ 区分开来实际上似乎是一个悬而未决的问题。cstheory.stackexchange.com/questions/19165/…）

标签： haskell

【解决方案1】：

seq x y 的全部意义在于评估x，然后返回y。 Haskell 是惰性的，所以定义如

seq x y = y

不会这样做，因为 x 未被评估。如果我们知道x :: Int，我们可以写

seq x y = case x of
          0 -> y
          _ -> y

强制x 被评估。我们可以对列表、树等使用相同的技巧，但有一个明显的例外：functions。如果x 是一个函数，我们不能case 覆盖它（除了琐碎的模式，它不会强制评估）。函数只在调用时评估，所以我们可能会尝试

seq x y = case x 12 of -- let's pretend it's an Int->Int function
          0 -> y
          _ -> y

这将强制评估x（好！），但也会评估x 12（坏！）。

事实证明，我们知道在 lambda 演算中写 seq 实际上是不可能：理论形式化了围绕“我们不能强制一个函数，除非我们应用，如果我们应用我们也在逼迫结果”。

因此，在 Haskell 中，seq 被添加为原始操作，无法根据其他所有内容进行定义。 seq 的实现对其第一个参数是严格的，即使不需要评估它来返回第二个参数。

由于seq 在 lambda 演算之外做了一些事情，它破坏了一些理论上的东西，例如参数性，但这种损失并没有大到破坏整个语言，它仍然享有许多不错的理论性质λ演算。

从历史上看，如果我没记错的话，早期的 Haskell 即将为 seq 添加一个类：

 class Seq a where
    seq :: a -> b -> b

并且这个类在每个类型除了函数上都被实例化了，所以参数性也被保留了。后来，决定在代码中添加所有Seq a 约束是不切实际的，因为单独使用seq 将需要在周围添加大量约束。所以，seq 被做成了一个原语，代价是稍微打破了理论。

【讨论】：

一个类需要实例化用户可以添加的任何新类型，不是吗？我还是Haskell的新手，所以我可能在这里遗漏了一些东西......简而言之，你是说第一条规则是允许“基于类”的实现？因为如果不是，并且seq 是“一个原始操作，不能根据其他所有内容定义”，我仍然看不到第一条规则的意义。
@IlyaBobyr 不，seq 被制成不需要类型类的原语。没有第一条规则seq 只是flip const，这是不一样的。尝试例如seq (error "evaluated!") 42 和 flip const (error "evaluated!") 42。或者将错误替换为需要很长时间的计算。
我了解seq 的作用。我不明白为什么需要特殊情况。如果它是“魔术”函数，为什么不能要求它，例如“尽可能”地评估它的第一个参数。如果它会引发异常，请在此之前停止。如果它是底部，则存储底部并继续第二个参数。然后，每当第二个参数实际使用第一个参数时 - 只有然后抛出异常，返回底部或返回计算的 HNF。这种方法有什么实施困难吗？还是理论上的？
我不认为flip const 是一样的。对论点的评估没有要求。它们仍会以 thunk 形式存储。
@IlyaBobyr 第一条规则只是表达“即使不需要第一个参数也有一个神奇的评估”的一种手段，因此seq /= \x y -> y = flip const。没有第一条规则，即没有任何魔法，seq = \x y -> y = flip const。你为 seq 提出了不同的行为——异常，错误可以被完成；甚至可以通过在一个单独的线程中计算它来处理非终止，并逐渐增加超时。为什么不这样做呢？也许选择了最简单的东西。

【解决方案2】：

上面的答案包含一个讨论，最终让我明白我错过了什么。我认为以下是它的要点。

如果我们将自己限制为仅一个线程，则建议的定义将需要解决停止问题。 ⊥ 表示 3 个不同的东西：异常、错误和不终止。前两个可以解决，第三个一般情况下是不可能解决的。

也许可以提供一个使用附加线程来运行a 评估的实现。但它看起来像一个更复杂的解决方案，可能有其自身的缺陷。

【讨论】：