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.
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.