"底部"(⊥)在Haskell函数定义中的作用是什么？

Question

我不理解bottom(?或_|_)在Haskell函数定义中所起的作用.

zip例如,定义将其描述为"正确的懒惰",因为

zip [] _|_ = []

但我不清楚这有何不同

zip [] _ = []

_|_在上面的函数定义中扮演什么角色？特别是,它与使用_有何不同？

---

更新和注意:作为优秀答案的读者将自己发现,这些答案的一个关键部分,值得提拔,实际上,? 它不会(也不能)出现在Haskell函数定义中.继续阅读.

Answer 1

底层本质上是一种奇特的代数方式undefined.

如果你试试这个,你可以看到为什么zip它的右手参数是懒惰的:

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

这是因为undefined只有在您尝试评估它时才会失败.

你可能会混淆_|_与_因为它的方式提出.我会清楚:该行zip [] _|_ = []并没有作为一个模式匹配而公式,说明平等zip [] _|_和[].也就是说,这不是有效的Haskell代码,而是一种表示"我不关心第二个参数"的符号,抽象代数方式.

在zip你的定义当然可以使用_,但这是无关紧要的.您可以使用任何名称,只要它不是构造函数匹配模式,如(Just x)或(a,b).在纯代码中必须进行模式匹配之前,值仍将保持未评估状态.

您可以在此处阅读有关延迟评估的更多信息.

你可以阅读更多关于底部在这里和这里.

Answer 2

我认为OP已经意识到了这一点,但是为了其他来到这里同样困惑的人的利益:zip [] _|_ = []不是真正的代码!

符号_|_(这仅仅是一个数学符号的ASCII艺术渲染?)是指底部¹,但只有当我们谈论关于哈斯克尔.在Haskell代码中它没有这个含义².

该行zip [] _|_ = []是对实际代码的属性的描述zip; 如果你用第一个参数调用它[]并将任何底值作为第二个参数传递,则结果等于[].他们想要准确说明这一点的原因是因为对于函数f非严格意义的技术定义是什么时候f ?不是?.

但是在定义Haskell函数(代码中)中没有_|_(或者?,或者undefined底层的概念)的作用.它是不可能的模式匹配上的参数,看看它是否是?,对于一些原因,所以有是因为没有实际的符号?在Haskell代码³.zip [] _|_ = []是,是一个属性的文档后果的定义zip,其定义的不一部分.

由于此属性的描述zip [] _ = []是一个不太具体的声明; 它会说无论你怎么称呼zip []它都会回来[].它完全相同,因为唯一的方法zip [] ?可以返回非底部的东西,如果它从来没有检查它的第二个参数.但它对非严格定义的定义不那么直接.

由于代码构成了函数定义的一部分,zip [] _ = []因此无法进行比较和对比zip [] _|_ = [].它们不是替代品,第一个是有效代码,第二个不是.

¹哪个是永远运行的表达式的"值",抛出异常,或以其他方式降低以评估为正常值.

²它甚至不是有效的Haskell标识符,因为它包含"namey"字符(_)和"operator"字符(|).所以在Haskell代码中它实际上并不是一个符号意味着任何东西!

³ undefined通常用于?,但它更多的是一个变量,指的是一个?值,而不是实际的东西本身.就像你有let xs = [1, 2, 3]可以xs用来引用列表一样[1, 2, 3],但你不能将它用作匹配其他列表的模式; 尝试的模式匹配只会被视为引入一个名为undefined或xs隐藏旧变量的新变量.

Answer 3

重复 AJFarmar 的回答，我认为这个关键点没有明确表达：

\n\n

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

\n\n

AJFarmar 的这句话隐含了这一点：

\n\n

\n

[T]该行zip [] _|_ = []并不充当模式匹配，而是充当方程，说明zip [] _|_和的相等性[]。

\n

\n\n

为了使其非常清晰，zip [] _|_ = []出现在的定义的文档注释zip中。它不是 Haskell 代码\xe2\x80\x94，它是用非正式技术符号编写的英语注释，看起来有点像 Haskell 代码。或者，换句话说，伪代码。

\n

Answer 4

⊥来自数学秩序理论.如果该元素在每个其他元素之前,则部分有序集合具有底部元素,表示为⊥.这如何进入Haskell文档？在某些时候,计算机科学家意识到,思考计算机程序,无论用什么语言,"意味着什么"都是有用的.一种方法称为指称语义.在指称语义中,编程语言中的每个术语在某些数学意义的世界中被赋予"外延"或意义.例如,能够说出这样的话会很棒

1. meaningInteger :: Integer -> mathematical integer
2. meaningList :: [a] -> possibly-infinite sequence of elements of type 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,但后两者不具有可比性.每种类型的底部元素,其定义最少的元素,称为⊥.