哈斯克尔和懒惰

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从不终止的评价,但很明显,结果如果是假的.

有没有一种方法可以正确实现und(即and德语)(不仅仅是部分如上),以便两者兼顾

und (non_term 1) False

和

und False (non_term 1)

返回False？

Answer 1

有没有办法正确实现und(即德语)(不仅仅是部分如上),以便两者兼顾

und (non_term 1) False

和

und False (non_term 1)

返回False？

如果你对理论感兴趣,那么有一个经典的理论结果表明上述函数在带递归的懒惰lambda演算中是不可能的(称为PCF).这是由Plotkin于1977年提出的.你可以在第8章"完全抽象"中的温斯克尔关于指称语义的注释中找到一个讨论.

即使证据涉及更多,这里的关键思想是lambda演算是一种顺序的,确定性的语言.因此,一旦惰性二元函数被馈送两个布尔值(可能是底部值),它需要决定在另一个之前评估哪一个,从而修复评估顺序.这将打破的对称性or和and,因为如果所选择的参数,则该发散or/ and还将发散.

正如其他人所提到的,在Haskell中,有一个unamb通过非顺序方式定义的库,即利用下面的一些并发性,因此超出了PCF的功能.有了它你可以定义你的并行or或and.

Answer 2

你可以写一个完整的定义und,它将适用于非终止表达式......等等

为了使这项工作,你需要你自己的定义Bool,明确任何计算的延迟:

import Prelude hiding (Bool(..))
data Bool = True | False | Delay Bool
  deriving (Show, Eq)

然后,无论何时定义类型的值Bool,您都必须将自己约束为共同递归,其中延迟是使用Delay构造函数显式的,而不是通过递归,您必须在其中评估子表达式以查找顶部的构造函数 - 级别返回值.

在这个世界中,非终止值可能如下所示:

nonTerm :: Bool
nonTerm = Delay nonTerm

然后und成为:

und :: Bool -> Bool -> Bool
und False y = False
und x False = False
und True y  = y
und x True  = x
und (Delay x) (Delay y) = Delay $ und x y

哪个工作得很好:

? und True False
False
? und False nonTerm
False
? und nonTerm False
False
? case und nonTerm nonTerm of Delay _ -> "delayed" ; _ -> "not delayed"
"delayed"

跟进dfeuer的评论,看起来你正在寻找的东西可以完成unamb

? :m +Data.Unamb 
? let undL False _ = False ; undL _ a = a
? let undR _ False = False ; undR a _ = a
? let und a b = undL a b `unamb` undR a b
? und True False
False
? und False False
False
? und False True
False
? und True True
True
? und undefined False
False
? und False undefined
False