在Haskell函数定义中，“bottom”（⊥）的作用是什么？

Question

在Haskell函数定义中，“bottom”（⊥）的作用是什么？

26

我不明白在Haskell函数定义中bottom (⊥或_|_)所起的作用。

例如，zip的定义被描述为“右惰性”，因为

zip [] _|_ = []

但我不清楚这与之有何不同

zip [] _ = []

在上述函数定义中，_|_ 所扮演的角色是什么？特别地，它与使用 _ 有何不同之处？

更新和说明：阅读优秀答案的读者会自行发现，这些答案中的一个关键部分（值得在此提出）是，⊥实际上不会（也不能）出现在Haskell函数定义中。继续阅读。

- orome

1

相关：Haskell 中的 bottom 概念 - dfeuer

1

还相关的是：Haskell中这个语法 ⊥ 或 (⊥) 代表什么意思？ - dfeuer

4个回答

8

我认为OP已经意识到这一点，但是为了其他有同样困惑的人的利益：zip [] _|_ = []不是实际的代码！符号|_|（这只是数学符号⊥的ASCII图形呈现）表示bottom¹，但仅当我们讨论Haskell时才具有此含义²。在Haskell代码中，它没有这个意思。 zip [] _|_ = []是实际的zip代码的属性描述；如果您使用第一个参数[]调用它，并将任何bottom值作为第二个参数传递，则结果等于[]。他们想要明确说明这一点的原因是因为函数f被非严格定义的技术定义是当f ⊥不是⊥时。但是，在定义Haskell函数（在代码中）时，没有|_|（或⊥或未定义或bottom概念）的作用。出于许多原因，必须不可能对参数进行模式匹配以查看它是否为⊥，因此在Haskell代码中不存在实际的⊥符号³。zip [] _|_ = []是一个属性的文档，该属性是zip定义的结果，而不是它的一部分。作为对这个属性的描述，zip [] _ = []是一个更不具体的声明；它将表明您调用zip []的任何内容，它都返回[]。它等同于完全相同的事情，因为只有当它根本不检查第二个参数时，zip [] ⊥才能返回非bottom的东西。但是，它对非严格性的定义说话的效果较弱。作为函数zip [] _ = []定义的一部分的代码不能与zip [] _|_ = []进行比较和对比。它们不是替代方案，第一个是有效的代码，第二个则无效。

¹这是一个永远运行，抛出异常或以其他方式无法计算为正常值的表达式的“值”。² 它甚至不是一个有效的Haskell标识符，因为它包含“名称”字符（_）和“运算符”字符（|）。因此，在Haskell代码中，它实际上不能成为表示任何东西的符号！

³ undefined 经常用于表示 ⊥，但它更像是指向一个 ⊥ 值的变量，而不是实际的值本身。就像如果你有 let xs = [1, 2, 3]，你可以使用 xs 来引用列表 [1, 2, 3]，但你不能将其用作与其他列表匹配的模式; 尝试的模式匹配将被视为引入一个名为 undefined 或 xs 的新变量，覆盖旧变量。

- Ben

6

参考AJFarmar的答案，我认为这一关键点并没有被明确说明：

_|_不是Haskell代码中有效的文字或标识符！
因此，zip [] _|_ = []也不是有效的代码！

这就是AJFarmar引用中隐含的意思：

[T]he line zip [] _|_ = [] does not act as a pattern match but an equation, stating the equality of zip [] _|_ and [].

为了让它非常清楚明白，zip [] _|_ = []出现在zip的文档注释中。它不是Haskell代码 - 它是用类似Haskell代码的非正式技术符号编写的英语注释。换句话说，它是伪代码。

- Luis Casillas

在代码中，_bs 是什么意思？它和 _ 一样吗？而且，模式 zip [] _bs = ... 是否确保如果第一个参数是[]（且右侧没有提到第二个参数），则第二个参数不会被评估？ - orome

1

在标准的 Haskell 中，像 x 这样的模式和特殊模式 _ 之间唯一的区别是 _ 永远不会出现在右侧。你可以写 f x = x 但不能写 f _ = _。在 GHC 中，有一个警告可用，通过 -Wall 等启用，它会警告未使用的绑定。在 GHC 中，以下划线开头的名称绑定会抑制该警告。因此，您可以编写 f _x = 3 来建议传入的是 x，但告诉编译器和人类读者您确实不打算使用它。 - dfeuer

1

@raxacoricofallapatorius，特别是绑定变量本身并不强制任何评估。强制评估的唯一方法是模式匹配、seq和evaluate函数，以及调用这些函数的函数，if-then-else（强制条件）和各种数字操作。（还有一个GHC扩展名为bang patterns） - dfeuer

所以如果我在右侧不引用它，它就不会被评估。正确吗？顺便问一下，为什么要特别指出⊥，当zip [] b对于任何 b都将是[]并且会使b未评估。⊥的情况是否满足某些重要的数学属性（另一个被忽略/未评估的值不会）？ - orome

@raxacoricofallapatorius，请查看我的答案，了解整个 ⊥ 事物的来源。如果您不使用它，它就不会被评估。评估的主要驱动程序是模式匹配。f x = let z = x + 3 in 7 不会评估 x，因为 x 只用于定义 z，而且没有人会查看 z。将其更改为 f x = let z = x + 3 in if z > 4 then 12 else 13，突然间 f 对 x 是严格的。 - dfeuer

1

@raxacoricofallapatorius：_bs只是一个变量，但它有一个小技巧：GHC的warn-unused-binds功能会警告未使用的变量，但跳过以下划线开头的变量。所以问题中发生的情况是，编译该选项的代码，并且使用该名称关闭了警告。为什么不直接使用_呢？我不知道作者的动机，但几乎肯定是出于风格考虑。 - Luis Casillas

6

⊥源自数学序理论。如果一个偏序集合有一个底部元素，表示为⊥，则该元素在其他所有元素之前。这如何出现在Haskell文档中？在某个时刻，计算机科学家意识到思考计算机程序（无论使用哪种语言）的“含义”将非常有用。其中一种方法称为指示语义。在指示语义中，编程语言中的每个术语都被分配了一个“指示”，或者说是某个数学含义的意思。例如，能够说出以下内容将是很棒的：

meaningInteger :: Integer -> 数学整数
meaningList :: [a] -> 可能是无限类型为a的元素序列

不幸的是，在Haskell中这并不完全适用，因为我可以这样写：

oops :: Integer
oops = oops

这给了我一个类型为整数(Integer)的术语，但是没有明显的方法将其赋予数学整数的含义。更有趣的是，我可以这样写：

undefined
undefined : undefined
3 : undefined
[undefined]
let foo = undefined : 3 : undefined : foo

这些都可以拥有相同的类型，但是存在各种不同程度的未定义性。因此，我们需要添加各种未定义事物的含义到我们的集合中。然而，我们可以基于它们的定义程度对它们强制实施“偏序”。例如，3：4：[]比3：4：undefined更加定义，并且比3：undefined：4更加定义，但是后面两个无法比较。每种类型的底部元素，即其最少定义的元素，称为⊥。

- dfeuer

如何才能有超过两个级别的定义（即已定义和未定义）？ - Praxeolitic

在第一组未定义实体示例之后，您说它们具有不同级别的未定义，这一点我不理解。难道某些东西不是已定义或未定义吗？然后，“例如，3:4: []比3:4:undefined更明确定义，并且也比3:undefined:4更明确定义，但后两者不可比较。” 我理解为3:4:undefined和3:undefined:4都是未定义的，两者都没有比另一个更未定义，因为“未定义”中没有区别，这显然与我对先前示例的理解相矛盾。 - Praxeolitic

1

@Praxeolitic，“undefined”比那些部分定义的值更不确定。将两个结构对齐。如果一个结构中已定义的部分与另一个结构中已定义的部分不同，则它们是不可比较的。否则，如果一个结构中未定义的部分位于另一个结构中未定义的部分之内，则第一个结构更为确定。如果两者都不在彼此之内，则它们再次是不可比较的。 - dfeuer

3 : undefined : 4 不是良好类型化的。为了保存您的示例，您可以将其替换为 3 : undefined : []。（3 : undefined : 4 : [] 与 3 : 4 : [] 不可比较，而 3 : undefined 没有 3 : 4 : undefined 定义得清楚。） - peter pun

更好的“不完全定义”偏序关系的定义可能是：当且仅当x为_|_或原子且等于y，或者可以与y对齐并且其所有组件都比y中对应的组件不完全定义时，则x比y不完全定义。当然，“原子”，“组件”和“对齐”之类的东西需要定义（这似乎不太难制定）。 - peter pun

显示剩余2条评论

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- AJF · Accepted Answer

底部本质上是一种高级的代数方式来表示undefined。

如果你尝试这样做，你会发现为什么zip对于它的右侧参数是惰性的：

λ> zip [] undefined
[]
λ> zip undefined []
*** Exception: Prelude.undefined

这是因为undefined只有在试图求值时才会失败。

你可能会因为它的呈现方式而将_|_与_混淆。我会让它变得更清晰：行zip [] _|_ = []不是一个模式匹配，而是一个等式，说明了 zip [] _|_和[]的相等性。也就是说，这不是有效的 Haskell 代码，而是一种符号、抽象代数方式来表示“我不关心第二个参数”。

在zip的定义中，你当然可以使用_，但这并不重要。你可以使用任何名称，只要它不是构造函数匹配模式，例如(Just x)或(a,b)。在纯代码中，值将保持为未求值状态，直到必须进行模式匹配。

你可以在这里了解更多关于惰性求值的信息。

你可以在这里和这里了解关于bottom的更多信息。