Haskell 模式匹配 "diverge"和 ⊥

Question

我试图理解 Haskell 2010 Report section 3.17.2 “模式匹配的非正式语义”。其中大部分与模式匹配成功或失败相关似乎很简单，但是我很难理解被描述为模式匹配“发散”的情况。

我半信半疑，这意味着匹配算法不会“收敛”到答案(因此匹配函数永远不会返回)。但如果不返回，那么它如何返回一个值，如括号中的“即返回⊥”所示？无论如何，“返回 ⊥”是什么意思？如何处理这一结果？

第 5 项(对我来说)特别令人困惑，“如果值为 ⊥，则匹配发散”。这是否只是说 ⊥ 的值会产生 ⊥ 的匹配结果？ (先不说我不知道​​这个结果意味着什么!)

任何说明，可能有一个例子，将不胜感激!

<小时/>

几个冗长答案后的附录:感谢 Tikhon 和所有人的努力。

看来我的困惑来自于两个不同的解释领域:Haskell 特征和行为的领域，以及数学/语义学的领域，而在 Haskell 文献中，这两个领域被混合在一起，试图用术语解释前者。对于后者，(对我来说)没有足够的路标来说明哪些元素属于哪个元素。

显然“bottom”⊥在语义域中，并且在Haskell中不作为值存在(即:你不能输入它，你永远不会得到打印出来的结果“⊥”)。

因此，当解释中说函数“返回 ⊥”时，这是指执行许多不方便的操作的函数，例如不终止、抛出异常或返回“未定义” ”。是这样吗？

此外，那些评论 ⊥ 实际上是一个可以传递的值的人实际上正在考虑绑定(bind)到尚未实际调用的普通函数来评估(可以说是“未爆炸的炸弹”)，但由于懒惰，可能永远不会，对吧？

Answer 1

该值为 ⊥，通常发音为“bottom”。它是一个语义意义上的值——它本身不是一个正常的 Haskell 值。它表示不产生正常 Haskell 值的计算:例如异常和无限循环。

语义是关于定义程序的“含义”。在 Haskell 中，我们通常谈论指称语义，其中值是某种数学对象。最简单的例子是表达式 10(还有表达式 9 + 1)具有数字 10 的表示(而不是Haskell 值 10)。我们通常写成⟦9 + 1⟧ = 10，意思是Haskell表达式9 + 1的表示是数字10。

但是，我们如何处理像 let x = x in x 这样的表达式呢？该表达式没有 Haskell 值。如果你试图评估它，它根本就永远不会完成。而且，这对应于什么数学对象并不明显。然而，为了对程序进行推理，我们需要给它一些定义。因此，本质上，我们只是为所有这些计算创建一个值，我们将该值称为 ⊥(底部)。

所以 ⊥ 只是定义不返回“含义”的计算的一种方法。

我们还将其他计算(如 undefined 和 error "some message" )定义为 ⊥，因为它们也没有明显的正常值。所以抛出异常对应于⊥。这正是模式匹配失败时发生的情况。

通常的思考方式是，每个 Haskell 类型都是“提升的”——它包含 ⊥。也就是说，Bool 对应于 {⊥, True, False} 而不仅仅是 {True, False}。这表明 Haskell 程序不能保证终止并且可能有异常。当您定义自己的类型时也是如此 - 该类型包含您为其定义的每个值以及 ⊥。

有趣的是，由于 Haskell 是非严格的，⊥ 可以存在于普通代码中。所以你可以有一个像 Just ⊥ 这样的值，如果你从不评估它，一切都会正常工作。 const 就是一个很好的例子:const 1 ⊥ 的计算结果为 1。这也适用于失败的模式匹配:

const 1 (let Just x = Nothing in x) -- 1

您应该阅读有关 denotational semantics 的部分在 Haskell WikiBook 中。这是对这个主题的非常平易近人的介绍，我个人觉得非常有趣。