Intype theory, a theory withinmathematical logic, thebottom type of a type system is the type that is asubtype of all other types.[1]
Where such a type exists, it is often represented with theup tack (⊥) symbol.
When the bottom type isuninhabited, a function whose return type is bottom cannot return any value, not even the lone value of aunit type.In such a language, the bottom type may therefore be known as thezero,never orempty type which, in theCurry–Howard correspondence, corresponds to falsity.
However, when the bottom type is inhabited, it is then different from the empty type.
If a type system issound, 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 theempty type, and the terms may be used interchangeably.
In subtyping systems, the bottom type is a subtype of all types.[1] It is dual to thetop type, which spans all possible values in a system.
If the bottom type is inhabited, its term(s) typically correspond to error conditions such as undefined behavior, infinite recursion, or unrecoverable errors.
InBounded Quantification with Bottom,[1] Pierce says that "Bot" has many uses:
null is the only value of the null type; and it can be cast to any reference type.[2] However, the null type is not a bottom type as described above, it is not a subtype ofint and other primitive types.Most commonly used languages don't have a way to denote the bottom type. There are a few notable exceptions.
InHaskell, the bottom type is calledVoid.[3]
InCommon Lisp the typeNIL, contains no values and is a subtype of every type.[4] The type namedNIL is sometimes confused with the type namedNULL, which has one value, namely the symbolNIL itself.
InScala, the bottom type is denoted asNothing. Besides its use for functions that just throw exceptions or otherwise don't return normally, it's also used forcovariantparameterized types. For example, Scala's List is a covariant type constructor, soList[Nothing] is a subtype ofList[A] for all types A. So Scala'sNil, the object for marking the end of a list of any type, belongs to the typeList[Nothing].
InRust, 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 callingpanic!() or looping forever. It is also the type of certain control-flow keywords, such asbreak andreturn, which do not produce a value but are nonetheless usable as expressions.[5]
InCeylon, the bottom type isNothing.[6] It is comparable toNothing in Scala and represents the intersection of all other types as well as an empty set.
InJulia, the bottom type isUnion{}.[7]
InTypeScript, the bottom type isnever.[8][9]
InJavaScript withClosure Compiler annotations, the bottom type is!Null (literally, a non-null member of theNullunit type).
InPHP, the bottom type isnever.
InPython's optional static type annotations, the general bottom type istyping.Never (introduced in version 3.11),[10] whiletyping.NoReturn (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 ofNever).[11]
InKotlin, the bottom type isNothing.[12]
InD, the bottom type isnoreturn.[13]
InDart, since version 2.12 with thesound null safety update, theNever type was introduced as the bottom type. Before that, the bottom type used to beNull.[14][15]