haskell - P. Wadler 论文中的 “⊥” 中的 “The Strictness Monad” 是什么意思？

Question

有人可以帮我理解 Wadler 题为“Comprehending Monads”的论文中的以下定义吗？ (摘自第 3.2 节/第 9 页，即“Strictness Monad”小节。)

Sometimes it is necessary to control order of evaluation in a lazy functional program. This is usually achieved with the computable function strict, defined by

strict f x = if x ≠ ⊥ then f x else ⊥.

Operationally, strict f x is reduced by first reducing x to weak head normal form (WHNF) and then reducing the application f x. Alternatively, it is safe to reduce x and f x in parallel, but not allow access to the result until x is in WHNF.

在论文中，我们还没有看到使用由两条垂直线组成的符号(不确定它叫什么)，所以它有点不知从何而来。
鉴于 Wadler 继续说“我们将使用 [严格] 推导来控制惰性程序的评估”，这似乎是一个需要理解的非常重要的概念。

Answer 1

您描述的符号是“底部”。它来自有序理论(尤其是格理论)。部分有序集合的“底部”元素(如果存在)是所有其他元素之前的元素。在编程语言语义中，它指的是一个比任何其他值“定义较少”的值。将“底部”值分配给每个产生错误或未能终止的计算是很常见的，因为试图区分这些条件会大大削弱数学并使程序分析复杂化。

为了将事情与另一个答案联系起来，逻辑“假”值是真值网格的底部元素，而“真”是顶部元素。在经典逻辑中，只有这两种，但也可以考虑具有无限多个真实值的逻辑，例如直觉主义和各种形式的建构主义。这些将概念引向了一个完全不同的方向。