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 the up tack (⊥) symbol.
A function whose return type is bottom cannot return any value, not even the zero size unit type. Therefore a function whose return type is the bottom type cannot return. In the Curry–Howard correspondence, the bottom type corresponds to falsity.
Computer science applications.
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 frequently used for the following purposes:
In "Bounded Quantification with Bottom", Pierce says that "Bot" has many uses:
In programming languages.
Most commonly used languages don't have a way to explicitly denote the empty type. There are a few notable exceptions.
Since Haskell2010, Haskell supports empty data types. Thus, it allows the definition codice_3 (with no constructors). The type codice_4 is not quite empty, as it contains non-terminating programs and the codice_5 constant. The codice_5 constant is often used when you want something to have the empty type, because codice_5 matches any type (so is kind of a "subtype" of all types), and attempting to evaluate codice_5 will cause the program to abort, therefore it never returns an answer.
In Common Lisp the symbol codice_9, amongst its other uses, is also the name of a type that has no values. It is the complement of codice_10 which is the top type. The type named codice_9 is sometimes confused with the type named codice_12, which has one value, namely the symbol codice_9 itself.
In Scala, the bottom type is denoted as codice_14. 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 codice_15 is a subtype of codice_16 for all types A. So Scala's codice_17, the object for marking the end of a list of any type, belongs to the type codice_15.
In Rust, the bottom type is called the never type and is denoted by codice_19. It is present in the type signature of functions guaranteed to never return, for example by calling codice_20 or looping forever. It is also the type of certain control-flow keywords, such as codice_21 and codice_22, which do not produce a value but are nonetheless usable as expressions.
In Ceylon, the bottom type is codice_14. It is comparable to codice_14 in Scala and represents the intersection of all other types as well as an empty set.
In Julia, the bottom type is codice_25.
In TypeScript, the bottom type is codice_26.
In JavaScript with Closure Compiler annotations, the bottom type is codice_27 (literally, a non-null member of the codice_28 unit type).
In Python, the bottom type is codice_29.
In Kotlin, the bottom type is codice_14.
In Elm, the bottom type is codice_31.