Haskell 语义未定义值答案

【问题标题】：Haskell semantics undefined valueHaskell 语义未定义值
【发布时间】：2012-05-28 10:42:53
【问题描述】：

我不熟悉 Haskell 及其语义。我了解到并非每个函数都可以映射到一个对象。例如：

square :: Int -> Int 
square x = x*x

square 的值被映射到数学对象。然而，对于任何非终止函数，我们将其映射到一个特殊的数学值⊥。我想知道如果我必须用这个未定义的值进行计算会发生什么。例如，我有一组数字Z⊥ ={⊥, 1,0,-1}。如果我将⊥ 乘以 1，输出会是什么？因为⊥ 的类型是未定义的，我可以用定义明确的类型进行乘法运算吗？因为⊥ 在Z⊥ 的域中，所以我想我可以进行乘法运算。但是，那么它必须返回⊥！我想得到一些关于它的指导！

【问题讨论】：

标签： haskell undefined semantics

【解决方案1】：

乘法也将返回⊥。它的行为与您描述的完全一样；任何依赖于⊥ 值的计算也将产生⊥。

2 * undefined ~= undefined

底部值是每个类型的居民，因此是每个值集的隐含成员，不能被类型排除（使用 GHC 内部原语除外）。这个特殊值存在的原因是为了让讨论 Haskell 中的 Halting Problem 成为可能；如果没有这个值，编译器必须能够证明某个计算终止才能进行类型检查，而这通常是不可能的。

【讨论】：

进一步说明，当且仅当对于所有 x，f x = f ⊥，f ⊥ ≠ ⊥ 是允许的。
是的，这就是我所说的“任何依赖于⊥ 值的计算”的意思，这就是上面用外行术语表达的：如果f 不依赖于x，当应用于底部值时，该函数可能会产生一个具体的值。另一方面，⊥ ≠ ⊥，这就是为什么我在上面发明了模棱两可的“等价”运算符；）
@DietrichEpp：不正确；考虑f x = (x, x)。对于所有x，正确的规则是f ⊥ ⊑ f x。
Haskell 函数的好处在于，它们对于 提升离散 CPO 是单调的（关系为 ⊑ - 小于定义），即 x ⊑ y ⇒ fx ⊑ 是的。在语言方面，这是由 ⊥ 上无法进行模式匹配来保证的。
是什么让你说⊥≠⊥？对我来说，⊥ 只是我们描述纯 Haskell 程序的指称语义中的一个元素，并且由于我们的指称语义是根据普通逻辑定义的，因此必然遵循 ⊥ = ⊥。