In type theory, a theory within mathematical logic, the bottom type of a type system is the type that is a subtype of all other types. Where such a type exists, it is often represented with the up tack (⊥) symbol.

Relation with the empty type

When the bottom type is uninhabited, a function whose return type is bottom cannot return any value, not even the lone value of a unit type. In such a language, the bottom type may therefore be known as the zero, never or empty type which, in the Curry–Howard correspondence, corresponds to falsity. However, when the bottom type is inhabited, it is then different from the empty type.

Computer science applications

In subtyping systems, the bottom type is a subtype of all types. It is dual to the top type, which spans all possible values in a system. If a type system is sound, the bottom type is uninhabited and a term of bottom type represents a logical contradiction. In such systems, typically no distinction is drawn between the bottom type and the empty type, and the terms may be used interchangeably. If the bottom type is inhabited, its term(s) typically correspond to error conditions such as undefined behavior, infinite recursion, or unrecoverable errors. 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 denote the bottom type. There are a few notable exceptions. In Haskell, the bottom type is called. In Common Lisp the type, contains no values and is a subtype of every type. The type named is sometimes confused with the type named , which has one value, namely the symbol itself. In Scala, the bottom type is denoted as. 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 is a subtype of for all types A. So Scala's , the object for marking the end of a list of any type, belongs to the type. In Rust, the bottom type is called the never type and is denoted by. It is present in the type signature of functions guaranteed to never return, for example by calling or looping forever. It is also the type of certain control-flow keywords, such as and , which do not produce a value but are nonetheless usable as expressions. In Ceylon, the bottom type is. It is comparable to in Scala and represents the intersection of all other types as well as an empty set. In Julia, the bottom type is. In TypeScript, the bottom type is. In JavaScript with Closure Compiler annotations, the bottom type is (literally, a non-null member of the unit type). In PHP, the bottom type is. In Python's optional static type annotations, the general bottom type is (introduced in version 3.11), while (introduced in version 3.5) can be used as the return type of non-returning functions specifically (and doubled as the general bottom type prior to the introduction of ). In Kotlin, the bottom type is. In D, the bottom type is. In Dart, since version 2.12 with the sound null safety update, the type was introduced as the bottom type. Before that, the bottom type used to be.