Haskell 和懒惰

Question

我刚开始学习 Haskell，有人告诉我 Haskell 是懒惰的，即它在评估表达式时所做的工作尽可能少，但我认为这不是真的。

考虑一下:

und :: Bool -> Bool -> Bool
und False y = False
und y False = False

non_term x = non_term (x+1)

评价 und (non_term 1) False永远不会终止，但很明显，如果为 False，则结果很明显。

有没有办法实现 und (即 and 德语)正确(不仅仅是部分如上)，因此两者

und (non_term 1) False

和

und False (non_term 1)

返回假？

Answer 1

Is there a way to implement und (i.e. and in German) correctly (not just partially as above) so that both

und (non_term 1) False

and

und False (non_term 1)

return False?

如果您对理论感兴趣，那么有一个经典的理论结果表明，上面的函数在具有递归的惰性 lambda 演算(称为 PCF)中是不可能的。这要归功于 1977 年的 Plotkin。您可以在 Winskel's notes on denotational demantics 中找到讨论。在第 8 章“完全抽象”中。

即使证明涉及更多，这里的关键思想是 lambda 演算是一种顺序的、确定性的语言。因此，一旦向惰性二进制函数提供了两个 bool 值(可能是底部值)，它需要决定先评估哪个值，从而确定评估顺序。这将破坏 or 的对称性和 and ，因为如果选择的参数发散，那么 or/ and也会发散。

正如其他人提到的，在 Haskell 中有一个定义 unamb 的库。通过非顺序方式，即利用底层的一些并发性，因此超出了 PCF 的能力。有了它，您可以定义您的并行 or或 and .