(Added remark that _|_ is a member of any type)
m (spelling: thouhg -> though)
|(2 intermediate revisions by 2 users not shown)|
Revision as of 02:33, 6 January 2008
The term bottom refers to a computation which never completes successfully. That includes a computation that fails due to some kind of error, and a computation that just goes into an infinite loop (without returning any data).
The mathematical symbol for bottom is '⊥'. That's Unicode character 22A5 hex = 8869 decimal. Also available in HTML as '⊥' and in LaTeX as '\bot' (within math mode). In plain ASCII, it's often written as the extremely ugly character sequence '
Bottom is a member of any type, even the trivial type () or the equivalent simple type:
data Unary = Unary
If it were not, the compiler could solve the halting problem and statically determine whether any computation terminated (though note that some languages with dependent type systems, such as Epigram, can statically enforce termination, based on the type for particular programs, such as those using induction).
Bottom can be expressed in Haskell thus:
bottom = bottom
bottom = error "Non-terminating computation!"
Indeed, the Prelude exports a function
undefined = error "Prelude; undefined"
Other implementations of Haskell, such as Gofer, defined bottom as:
undefined | False = undefined
The type of bottom is arbitrary, and defaults to the most general type:
undefined :: a
As bottom is an inhabitant of every type (though with some caveats concerning types of unboxed kind), bottoms can be used wherever a value of that type would be. This can be useful in a number of circumstances:
-- For leaving a todo in your program to come back to later: foo = undefined -- When dispatching to a type class instance: print (sizeOf (undefined :: Int)) -- When using laziness: print (head (1 : undefined))