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)

返回 False？

- Kiuhnm

---

“懒惰”并不意味着“尽可能少地工作”，它的含义是“在需要时才计算值”。 - that other guy

...并且需要确保第一个案例不匹配。 - rampion

把这两个参数想象成“神秘盒子”。Haskell 想要知道它们中是否有一个包含 False，就必须打开盒子，也就是对这些参数进行求值。Haskell 不可能“猜测”应该先处理哪个盒子！ - Lynn

从操作上来看，Haskell的定义需要按顺序检查定义。 - rampion

你应该研究一下unamb，它是一个并行计算运算符，可以执行两个计算并使用第一个计算的结果终止而不出错。但基本上，惰性求值是一种特定的求值策略-还有其他可能更适合你目的的策略。 - dfeuer

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）中，上述函数是不可能的。这是由Plotkin于1977年提出的。在Winskel关于指称语义的笔记第8章“完全抽象”中可以找到讨论。

即使证明更加复杂，关键思想在于lambda演算是一种顺序的、确定性的语言。因此，一旦惰性二元函数被喂入两个布尔值（可能是底部值），它需要决定先评估哪一个，从而固定了一个评估顺序。这将打破或和与的对称性，因为如果选择的参数发散，则或/与也会发散。

正如其他人所提到的，在Haskell中，有一个通过非顺序手段定义unamb的库，即利用了一些并发技术，从而超出了PCF的能力范围。有了它，您就可以定义自己的并行或或与。

- chi

---

我点赞了你的回答，因为我很欣赏你的理论解释。但是我选择了另一个答案，因为他提供了具体实现。 - Kiuhnm

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

- rampion

---

如果我理解正确的话，那只适用于非常特定的非终结符表达式。因此，对于我的问题来说，答案是一个坚定的“不”。 - Kiuhnm

使用“unamb”代码，即使在ghci中运行“und False（non_term 1）”，我仍然无法终止。我怀疑是因为“non_term 1”正在一个线程中运行，该线程正在锁定尝试杀死它的线程：https://downloads.haskell.org/~ghc/latest/docs/html/libraries/base/Control-Concurrent.html#g:13 - xnyhps

Answer 3

Haskell确实是一种惰性的语言。惰性意味着表达式只有在需要时才会被计算。但是，惰性并不意味着两个表达式可以以任意顺序计算。在Haskell中，表达式的计算顺序很重要。例如，考虑你的und函数：

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

首先，我想指出这个函数是不完整的。完整的函数如下：

und :: Bool -> Bool -> Bool
und False y = False
und y False = False
und y True  = True          -- you forgot this case

实际上，und函数可以更加简洁（和懒惰）地编写如下：

-- if the first argument is False then the result is False
-- otherwise the result is the second argument
-- note that the second argument is never inspected

und :: Bool -> Bool -> Bool
und False _ = False
und _     x = x

无论如何，在Haskell中的模式匹配语法只是case表达式的语法糖。例如，你原始（不完整）的函数将被转换为（最多到α等价）：

und :: Bool -> Bool -> Bool
und x y = case x of False -> False
                    True  -> case y of False -> False
                                       True  -> undefined

我们可以看到：

1. 你的函数不完整，因为最后一个情况是undefined。
2. 即使第一个参数不需要，如果第一个参数是True，你的函数也会评估第二个参数。请记住，case表达式总是强制评估正在检查的表达式。
3. 你的函数首先检查x，然后检查y，如果x评估为True。因此，在这里确实有明确的评估顺序。请注意，如果x评估为False，则永远不会评估y（证明und确实是惰性的）。

正是由于这种评估顺序，你的表达式und (non_term 1) False会发散：

  und (non_term 1) False
= case non_term 1 of False -> False
                     True  -> case False of False -> False
                                            True  -> undefined
= case non_term 2 of False -> False
                     True  -> case False of False -> False
                                            True  -> undefined
= case non_term 3 of False -> False
                     True  -> case False of False -> False
                                            True  -> undefined
                .
                .
                .
                .

如果您愿意，可以创建一个具有不同评估顺序的函数：

und :: Bool -> Bool -> Bool
und x y = case y of False -> False
                    True  -> x     -- note that x is never inspected

现在，表达式 und (non_term 1) False 的评估结果为False。然而，表达式und False (non_term 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?

短答案是不行。您总是需要特定的评估顺序；并且根据评估顺序，und (non_term 1) False或und False (non_term 1)将会出现分歧。

这是否意味着Haskell是错误/有问题的？不。Haskell做了正确的事情，并且只是没有产生任何答案。对于人类（可以同时评估两个表达式的人），und (non_term 1) False的结果必须是False。然而，计算机必须始终具有评估顺序。

那么，实际问题是什么？在我看来，实际问题是二者之一：

1. Parallel evaluation. Haskell should evaluate the expression both ways in parallel and choose the one that terminates first:

   import Data.Unamb (unamb)
   
   type Endo a = a -> a
   
   bidirectional :: Endo (a -> a -> b)
   bidirectional = unamb <*> flip
   
   und :: Bool -> Bool -> Bool
   und = bidirectional (&&)
   

2. General recursion. In my humble opinion, general recursion is too powerful for most use cases: it allows you to write absurd functions like non_term x = non_term (x + 1). Such functions are quite useless. If we don't consider such useless functions as inputs then your original und function is a perfectly good function to use (just implement the last case or use &&).

希望这能有所帮助。

- Aadit M Shah

---

然而，计算机必须始终具有评估顺序。如果我能做到，计算机也可以。正如我已经说过的那样，Haskell可以检查所有具有相同右侧手边的相邻定义以获得简单匹配，然后必要时按常规方式进行。 - Kiuhnm

@Kiuhnm，定义“容易”是什么意思？如果我将第二个等式右侧的False替换为not True，它仍然是一个“容易匹配”吗？如果不是，那么我不能再用相等替换相等而不改变程序的含义。我认为你会发现很难定义一个具有明确定义、确定性语义的语言，包括像你想编写的函数。无论如何，Haskell不是那种语言，执行您建议的评估的编译器不是正确的Haskell编译器。 - Reid Barton

@ReidBarton 我的意思是左边很容易匹配。无论如何，我们必须定义右边相等的含义。我们可以明确告诉 Haskell 一些定义可以按任意顺序考虑。Haskell 将尝试以轮换方式进行匹配，每次只进行一次替换后放弃。这应该能够起到作用。 - Kiuhnm