Haskell 模式匹配 "diverge" 和 ⊥答案

【问题标题】：Haskell pattern match "diverge" and ⊥Haskell 模式匹配 "diverge" 和 ⊥
【发布时间】：2013-02-05 00:53:44
【问题描述】：

我正在尝试理解Haskell 2010 Report section 3.17.2“模式匹配的非正式语义”。大多数情况下，与模式匹配成功或失败有关的情况似乎很简单，但是我很难理解被描述为模式匹配“发散”的情况。

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

第 5 项有一个特别令人困惑的（对我来说）点“如果值为 ⊥，则匹配发散”。这只是说⊥ 的值会产生⊥ 的匹配结果吗？（撇开我不知道那个结果意味着什么！）

任何照明，可能带有示例，将不胜感激！

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

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

显然“底部”⊥ 在语义域中，并且在 Haskell 中不作为值存在（即：您无法输入它，您永远不会得到打印为“⊥”的结果）。

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

此外，那些评论 ⊥ 实际上是可以传递的值的人，实际上是在考虑绑定到尚未实际调用评估的普通函数 ("未爆炸的炸弹”可以这么说）而且可能永远不会，因为懒惰，对吧？

【问题讨论】：

返回 undefined 就像抛出异常一样——undefined 就是这样定义的。是的，传递底部是可能的，只是因为 Haskell 并不严格，而这些值确实类似于未爆炸的炸弹。
但是在 Haskell 中，程序中没有任何东西实际上知道（或可以测试）一个值“是”一个底部，直到/除非它被实际调用并产生效果，此时它是一个实际的异常，未定义或非终止，对吗？（仍在尝试确定“底部”是否是 Haskell 中的实际值，而不是语义概念，对思考有用但不是实际值）。
是的，你不能测试它。考虑不终止的情况：你怎么知道评估不会终止？一般情况下是无法确定的。如果您手上有一个无限循环，那么您实际上并没有正常值，但您确实有⊥。我希望能澄清一些事情——正如我回答中的 cmets 所示，我想不出一个好的方式来描述它。
好的，谢谢。我认为对我的大脑来说，这意味着底部不是实际的 Haskell 值或类型。这是一个词/符号，用来讨论可能返回未定义、可能不返回或可能异常的函数。至于您答案中的 cmets，它们本身就有助于展示讨论和思考的各种方式。再次感谢。
了解⊥ 的“不可测试性”（在 Haskell 中）的一个非常重要的方法是了解单调性。有很长的路要走（这解释了 Haskell 语义的 CPO 域）或很短的路：⊥ 的完整语义是您无法对其进行模式匹配。任何“最终”构造函数可以匹配它（False、True、3、[]），但一旦你这样做，匹配的语义就会被感染，也只是⊥。因此，任何匹配无限循环的函数都是无限循环。与undefined 相同，错误也几乎相同（请注意，spoon 之类的库违反了这一点）。

标签： haskell pattern-matching

【解决方案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

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

【讨论】：

为了扩展这个答案，请注意，在 haskell 中，非正式地说，我们可以返回_|_，因为我们处于非严格设置中。这就是说，即使一个值具有 _|_ 的表示，我们仍然可以传递它，但需要注意的是，如果我们戳它，那么戳它的表达式 also 将采用外延_|_.
我认为⊥ 是一个非常真实的 Haskell 值，因为它可以被传递并在内存中具有表示，它可以被评估等等。
在不同的⊥s（例如undefined、error "undefined"和let x = x in x）之间也存在令人困惑的明显差异。每个都有不同的 Haskell 技术值，但它们被合并到指称语义中只是因为。
可以说，“Haskell”是一种语法，是对赋予其意义的语义域的映射。 ⊥ 是语义域中的值，就像 2 一样。 let x = x in x 和 1 + 1 都是表达式。碰巧⊥-the-value 是一个具有属性的值，该属性导致在该参数中严格的语义域中的表达式也为⊥。
@tel 作为运行程序的人，您可以观察到undefined、error 和非终止之间的区别。但是从程序内部看，它们之间没有明显的区别；它们都代表着无法恢复的灾难性事件。这就是它们在语义上相同的意义。

【解决方案2】：

指称语义

因此，简而言之，⊥ 所在的指称语义是从 Haskell 值到一些其他值空间的映射。你这样做是为了以更正式的方式赋予程序意义，而不仅仅是谈论程序应该做什么——你说它们必须尊重它们的指称语义。

所以对于 Haskell，您经常会想到 Haskell 表达式如何表示数学值。您经常看到 Strachey 括号 ⟦·⟧ 表示从 Haskell 到 Math 的“语义映射”。最后，我们希望我们的语义括号与语义操作兼容。比如

⟦x + y⟧ = ⟦x⟧ + ⟦y⟧

左侧+ 是Haskell 函数(+) :: Num a => a -> a -> a，右侧是交换群中的二元运算。虽然很酷，因为我们知道我们可以使用语义映射中的属性来了解我们的 Haskell 函数应该如何工作。也就是说，让我们在“数学”中写出交换性质

  ⟦x⟧ + ⟦y⟧ == ⟦y⟧ + ⟦x⟧ 
= ⟦x + y⟧ == ⟦y + x⟧ 
= ⟦x + y == y + x⟧

其中第三步还表明 Haskell (==) :: Eq a => a -> a -> a 应该具有数学等价关系的属性。

嗯，除了……

不管怎样，这一切都很好，直到我们记住计算机是有限的东西并且数学不太关心这一点（除非你使用直觉逻辑，然后你得到 Coq）。所以，我们必须注意我们的语义不完全正确地遵循数学的地方。以下是三个例子

⟦undefined⟧         = ??
⟦error "undefined"⟧ = ??
⟦let x = x in x⟧    = ??

这就是⊥ 发挥作用的地方。我们只是断言，就 Haskell 的指称语义而言，这些示例中的每一个都可能意味着（新引入的数学/语义概念）⊥。 ⊥ 的数学性质是什么？好吧，这就是我们开始真正深入研究语义域并开始讨论函数和 CPO 等的单调性的地方。不过，从本质上讲，⊥ 是一个数学对象，它玩的游戏与非终止游戏大致相同。从语义模型的角度来看，⊥ 是有毒的，它会以其有毒的不确定性感染表达式。

但这不是 Haskell 语言的概念，只是 Haskell 语言的语义域。在 Haskell 中，我们有 undefined、error 和无限循环。这很重要。

超语义行为（旁注）

因此，一旦我们理解了⊥ 的数学含义，⟦undefined⟧ = ⟦error "undefined"⟧ = ⟦let x = x in x⟧ = ⊥ 的语义就很清楚了，但也很清楚，它们各自在“现实”中具有不同的效果。这有点像 C 的“未定义行为”......就语义域而言，它是未定义的行为。你可以称它为语义上不可观察的。

那么模式匹配如何返回`⊥`？

那么返回⊥ 的“语义”是什么意思？好吧，⊥ 是一个完全有效的语义值，它具有模拟非确定性（或异步错误抛出）的感染属性。从语义的角度来看，它是一个完全有效的值，可以按原样返回。

从实现的角度来看，您有多种选择，每一种都映射到相同的语义值。 undefined 不太对，也不是进入无限循环，所以如果你要选择一个语义上未定义的行为，你不妨选择一个有用的并抛出错误

*** Exception: <interactive>:2:5-14: Non-exhaustive patterns in function cheers

【讨论】：

电话：感谢您在这里的辛勤工作。您将我的注意力引导到 Haskell 解释通常需要将 Haskell 行为与某些语义域相关联的程度，这很有帮助。也就是说，我的问题实际上是关于实际 Haskell 中发生的事情，而不是与发生的事情相对应的语义概念。我认为您在最后的“模式匹配如何返回⊥”部分中已经接近了，但是我并没有真正理解您要说的“您有很多选择”等。我在哪里有这些选择?
您作为 Haskell 用户没有这些选择，如果您正在实施 Haskell，那么您可以。实现可以选择做任何它喜欢在顶层评估 ⊥ 的事情。事实上，如果⊥ 真的代表无限循环，它可能除了挂起之外什么都做不了。但是像模式匹配失败这样的事情可以提供更多信息，这就是你得到“选择”的地方。

指称语义

嗯，除了……

超语义行为（旁注）

那么模式匹配如何返回⊥？

那么模式匹配如何返回`⊥`？