What does “⊥” mean in “The Strictness Monad” from P. Wadler's paper?

Question

Can someone help me understand the following definition from Wadler's paper titled "Comprehending Monads"? (Excerpt is from section 3.2/page 9, i.e., the "Strictness Monad" subsection.)

---

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.

---

In the paper, we have yet to see use of the symbol made up of the two perpendicular lines (not sure what it's called) so it sort of comes out of nowhere.

Given that Wadler goes on to say that "we will use [strict] comprehensions to control the evaluation of lazy programs", it seems like a pretty important concept to understand.

Answer 1

The symbol you describe is "bottom". It comes from order theory (particularly lattice theory). The "bottom" element of a partially ordered set, if one exists, is the one that precedes all others. In programming language semantics, it refers to a value that is "less defined" than any other. It's common to assign the "bottom" value to every computation that either produces an error or fails to terminate, because trying to distinguish these conditions greatly weakens the mathematics and complicates program analysis.

To tie things into another answer, the logical "false" value is the bottom element of a lattice of truth values, and "true" is the top element. In classical logic, these are the only two, but one can also consider logics with infinitely many truthfulness values, such as intuitionism and various forms of constructivism. These take the notions in a rather different direction.

Answer 2

In standard Boolean logic, the symbol ⊥, read falsum or bottom, is simply a statement which is always false, the equivalent of the false constant in programming languages. The form is an inverted (upside-down) version of the symbol ⊤ (verum or top), which is the equivalent of true - and there's mnemonic value in the fact that the symbol looks like a capital letter T. (The names verum and falsum are Latin for "true" and "false"; the names "top" and "bottom" come from the use of the symbols in the theory of ordered sets, where they were chosen based on the location of the horizontal crossbar.)

In computability theory, ⊥ is also the value of an uncomputable computation, so you can also think of it as the undefined value. It doesn't matter why the computation is uncomputable - whether because it has undefined inputs, or never terminates, or whatever. Your snippet is a formalization of that first reason: it defines strict as a function that makes any computation (another function) undefined whenever its inputs (arguments) are undefined.