Bottom type

In type theory, a theory within mathematical logic, the bottom type is the type that has no values. It is also called the zero or empty type, and is sometimes denoted with falsum (⊥).

A function whose return type is bottom cannot return any value. In the Curry–Howard correspondence, the bottom type corresponds to falsity.

In subtyping systems, the bottom type is the subtype of all types. (However, the converse is not true—a subtype of all types is not necessarily the bottom type.) It is used to represent the return type of a function that does not return a value: for instance, one which loops forever, signals an exception, or exits.

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 exactly one value. The bottom type is sometimes confused with the so-called "void type", which is actually a unit type, albeit one with no defined operations.

The bottom type is frequently used for the following purposes:

In Bounded Quantification with Bottom, Pierce says that "Bot" has many uses:

Most commonly used languages don't have a way to explicitly denote the empty type. There are a few notable exceptions.

Haskell does not support empty data types. However, in GHC, there is a flag -XEmptyDataDecls to allow the definition data Empty (with no constructors). The type Empty is not quite empty, as it contains non-terminating programs and the undefined constant. The undefined constant is often used when you want something to have the empty type, because undefined matches any type (so is kind of a "subtype" of all types), and attempting to evaluate undefined will cause the program to abort, therefore it never returns an answer.

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.

...
Wikipedia