是否可以在 Haskell 中实现此功能？答案

【问题标题】：Is it possible to implement this function in Haskell?是否可以在 Haskell 中实现此功能？
【发布时间】：2020-03-24 09:43:02
【问题描述】：

在页面https://en.wikibooks.org/wiki/Haskell/Denotational_semantics#Pattern_Matching有以下练习：

考虑具有以下属性的两个布尔参数的函数or：

或⊥ ⊥ = ⊥

或真⊥ =真

或 ⊥ 真 = 真

或假 y = y

或 x 假 = x

这个函数是联合严格性的另一个例子，但更清晰：如果两个参数都是（至少当我们将参数限制为 True 和 ⊥ 时），结果只是 ⊥。 Haskell中可以实现这样的功能吗？

函数可以用下表表示：

      |   ⊥   | False | True
------|-----------------------
  ⊥   |   ⊥   |   ⊥   | True
False |   ⊥   | False | True
True  | True  | True  | True

根据https://en.wikibooks.org/wiki/Haskell/Denotational_semantics#Monotonicity 中给出的定义，这个函数是单调的，所以我看不出有理由排除在Haskell 中实现这个函数的可能性。尽管如此，我没有看到实现它的方法。

练习题的答案是什么？

PS：我知道答案是“不，你不能”。我正在寻找的是一个严格的证明。我觉得我错过了一些关于可以定义哪些功能的重要限制。绝对不是所有的单调函数。

【问题讨论】：

你不能实现这个，除非依赖并发来并行计算两个表达式（或者一些隐藏并行性的不安全函数）。它以por 的形式存在于库中，表示“并行或”。
@chi 你介意分享一个证明吗？
@Federico 这是停机问题。给定or x y，您必须至少评估其中的一个，以确定是返回True 还是False。无论您选择x 或y 中的哪一个，您都有可能将其视为发散计算，即使另一个不是。并发让您可以“一次一点”评估它们中的每一个，因此如果存在非底部值，您最终会找到它。
我没有快速参考，但您可以尝试在 lambda 演算中搜索“por”，以及与指称语义完全抽象相关的失败。我认为某处有一些 Winskel (?) 幻灯片。
@chepner 我不会将此与停机问题联系起来，因为它可以通过并发来解决。我认为这可能会产生误导——如果这个问题由于 HP 而无法确定，那么再多的并发也无济于事。幸运的是，我们不必决定x 或y 上的HP 来计算por x y，因为我们可以同时运行计算。在我看来，这与 lambda 演算中缺乏并发性有关。

标签： haskell lazy-evaluation strictness

【解决方案1】：

假设您要尝试评估or x y。为此，您必须选择一个或另一个参数来查看评估它是否会导致True 或False。如果你猜对了，你就会知道结果应该是True 还是False，而无需评估另一个参数（可能是⊥）。

如果你猜错了，那么你将永远无法完成对论证的评估；要么陷入无限循环，要么出现运行时错误。

并发让您可以并行评估两个参数[1]。假设两个参数之一的计算结果为正确的Boolean，则两个分支之一将成功找到它。另一个分支将引发错误（在这种情况下，您可以简单地丢弃该分支并忽略错误）或陷入循环（当另一个分支成功时您可以强制终止该循环）。不管怎样，你最终都能得到正确的答案。

如果两个参数都导致⊥，当然or的隐含结果仍然是⊥；你不能完全绕过停机问题。

[1] “并行”并不一定是指分叉另一个进程并同时评估它们。您可以评估 N 步骤的一个参数（对于某些值 N 和任何“步骤”的含义）；如果出现错误，放弃并尝试另一个参数，如果你还没有终止，暂停这个线程并尝试另一个N步骤。不断在两者之间来回切换，直到其中一个产生具体值。

【讨论】：

【解决方案2】：

The unamb package 使用 chepner 的回答中描述的并发（和 unsafePerformIO）来实现可以定义并行 or 的原语。

parOr :: Bool -> Bool -> Bool
parOr x y = (x || y) `unamb` (y || x)  -- unamb from Data.Unamb

【讨论】：