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

Question

Haskell Report 2010表示seq"削弱了Haskell的参数性质",因为"⊥与\ x - > not不同,因为seq可以用来区分它们"[1].

它似乎完全是因为一个明确的规则:

seq ? b  =  ?

我想知道为什么会引入这个特例？必须有一个原因

seq a b  =  b

这还不够,seq需要一个更复杂的定义:

seq ? b  =  ?
seq a b  =  b, if a ? ?

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

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

使用规则seq是一个特殊的函数,可以"尽可能地"评估它的第一个参数.如果评估结果为HNF,则完全评估参数.如果它将导致异常或底部值,那么这些将被存储,并且只要第一个参数实际用于评估第二个参数,就会抛出或返回它们.

这有点蹩脚,但我认为这应该让我的问题更加明确.这不是关于如何seq工作.这是关于当前设计的意图.

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

Answer 1

整点seq x y是评估 x然后回归y.Haskell很懒,所以定义如

seq x y = y

不会做,因为x没有评估.如果我们知道x :: Int我们可以写

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

强迫x进行评估.我们可以为列表,树等播放相同的技巧,但有一个重要的例外:函数.如果x是一个函数,我们不能case超过它(除了琐碎的模式,没有力量评估).功能仅在通话时评估,因此我们可能会尝试

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

这将强制评估x(好!),但也会评估x 12(不好!).

事实证明,我们知道seq在lambda演算中写作实际上是不可能的:理论将直觉形式化为"我们不能强制执行函数,除非我们应用,如果我们应用,我们也强迫结果".

因此,在Haskell中,seq被添加为原始操作,而不是就其他所有内容而言都是可定义的.第seq一个参数的执行是严格的,即使没有必要对它进行评估以返回第二个参数.

由于seq在lambda演算之外做了一些事情,它在理论上打破了一些东西,例如参数化,但是这种损失并没有破坏整个语言,它仍然享有lambda演算的许多优秀理论属性.

从历史上看,如果我的记忆对我有用,早期的Haskell即将包括一个类seq:

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

并且这个类在每个类型上都被实例化但是函数,因此也保留了参数.后来,决定Seq a在代码中添加所有约束是不切实际的,因为单次使用seq会需要添加大量约束.因此,seq制造成一个原始,以牺牲理论为代价.

Answer 2

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

\n\n

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

\n\n

或许可以提供一种使用额外线程来运行a. 但它看起来是一个更复杂的解决方案，可能有其自身的陷阱。

\n