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.

Irony

It's commonly called bottom. – Qp

What does your question have to do with monads? – Ovariotomy

It's called bottom, or in Haskell specifically called undefined. This is only one form of it though Technically bottom is also a non-terminating computation, such as length [1..] – Renaterenato

See bottom type. Bottom basically means, this expression is not computable/runs forever/never returns a value/throws an exception/etc. The rule is saying: if x is computable, then strict f x evaluates to f x, but if x is not computable, then strict f x evaluates to "not computable". To put it differently: say f x = 2 * x. What is f (1 / 0)? You can't evaluate it because you can't evaluate (1 / 0). – Salep

@leftaroundabout: I probably should have made it more clear in my original post. The excerpt is from a paper titled "Comprehending Monads". The specific sub-section is called "The Strictness Monad". – Irony

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.

Godoy

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.

Haggle

Except that in a lazy functional language, f x can be defined even if x is undefined! e.g. if f = const 1. Wadler is not merely observing that a function's result is undefined if it's input is undefined (since that's not always true), he's defining the function strict that converts any function to have this property. – Mixologist