Bottom type

In type theory, the bottom type is the subtype of all types. It is the return type of a function that does not return normally. As an example, a certain program function may promise to return an integer but in a Turing-complete language the function might get stuck in an infinite loop or encounter an error/exception. In order to theoretically account for the fact that the function might not return an integer in spite of the promise, the bottom type is considered a subtype of integer (and, indeed, all types) even in languages that don't otherwise have subtypes.

Because the bottom type is used to indicate the lack of a normal return, it typically has no values. It contrasts with the top type, which spans all possible values in a system, and a unit type, which has only one value. The bottom type is sometimes confused with the so-called "void type", which is actually a unit type. In the Curry-Howard correspondence, the bottom type is associated with the false formula in logic proofs.

The bottom type is frequently used for the following purposes:
* To signal that a function or computation "diverges"; in other words, does not return a result to the caller. (This does not necessarily mean that the program fails to terminate; a subroutine may terminate without returning to its caller, or exit via some other means such as a continuation.)
* As an indication of error; this usage primarily occurs in theoretical languages where distinguishing between errors is unimportant. Production programming languages typically use other methods, such as option types (including tagged pointers) or exception handling.

Common abbreviations include bot, the "up tack" symbol (⊥) or the ASCII approximation _|_. It is also called the zero or empty type.

In programming languages

Even though the bottom type is an important theoretical aspect to all Turing-complete languages, most commonly used languages don't have a way to explicitly denote it. There are a few notable exceptions.

In Haskell, the keyword undefined represents a computation for which the result has the bottom type. Attempting to evaluate the computation undefined at runtime aborts the program.

In Common Lisp the symbol NIL, amongst its other uses, is also the name of a type that has no values. It is the complement of T which is the top type. The type named NIL is sometimes confused with the type named NULL, which has one value, namely the symbol NIL itself.

In Scala, the bottom type is denoted as Nothing. Besides its use for functions that just throw exceptions or otherwise don't return normally, it's also used for covariant parameterized types. For example, Scala's List is a covariant type constructor, so List [Nothing] is a subtype of List [A] for all types A. So Scala's Nil, the object for marking the end of a list of any type, belongs to the type List [Nothing] .

ee also

*NaN

References

*