我试图理解 Haskell 2010 Report section 3.17.2 “模式匹配的非正式语义”。其中大部分与模式匹配成功或失败相关似乎很简单,但是我很难理解被描述为模式匹配“发散”的情况。
我半信半疑,这意味着匹配算法不会“收敛”到答案(因此匹配函数永远不会返回)。但如果不返回,那么它如何返回一个值,如括号中的“即返回⊥
”所示?无论如何,“返回 ⊥
”是什么意思?如何处理这一结果?
第 5 项(对我来说)特别令人困惑,“如果值为 ⊥
,则匹配发散”。这是否只是说 ⊥
的值会产生 ⊥
的匹配结果? (先不说我不知道这个结果意味着什么!)
任何说明,可能有一个例子,将不胜感激!
<小时/>几个冗长答案后的附录: 感谢 Tikhon 和所有人的努力。
看来我的困惑来自于两个不同的解释领域:Haskell 特征和行为的领域,以及数学/语义学的领域,而在 Haskell 文献中,这两个领域被混合在一起,试图用术语解释前者。对于后者,(对我来说)没有足够的路标来说明哪些元素属于哪个元素。
显然“bottom”⊥
在语义域中,并且在Haskell中不作为值存在(即:你不能输入它,你永远不会得到打印出来的结果“⊥
”)。
因此,当解释中说函数“返回 ⊥
”时,这是指执行许多不方便的操作的函数,例如不终止、抛出异常或返回“未定义” ”。是这样吗?
此外,那些评论 ⊥
实际上是一个可以传递的值的人实际上正在考虑绑定(bind)到尚未实际调用的普通函数来评估(可以说是“未爆炸的炸弹”),但由于懒惰,可能永远不会,对吧?
最佳答案
该值为 ⊥,通常发音为“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 中。这是对这个主题的非常平易近人的介绍,我个人觉得非常有趣。
关于Haskell 模式匹配 "diverge"和 ⊥,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/14698414/