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.
When the bottom type is empty, 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 or never type. In the Curry–Howard correspondence, an empty type corresponds to falsity.
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 terms[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 a language with exceptions, a natural type for the raise construct is raise ∈ exception -> Bot, and similarly for other control structures. Intuitively, Bot here is the type of computations that do not return an answer.
- Bot is useful in typing the "leaf nodes" of polymorphic data structures. For example, List(Bot) is a good type for nil.
- Bot is a natural type for the "null pointer" value (a pointer which does not point to any object) of languages like Java: in Java, the null type is the universal subtype of reference types.
nullis the only value of the null type; and it can be cast to any reference type. However, the null type is not a bottom type as described above, it is not a subtype of
intand other primitive types.
- A type system including both Top and Bot seems to be a natural target for type inference, allowing the constraints on an omitted type parameter to be captured by a pair of bounds: we write S<:X<:T to mean "the value of X must lie somewhere between S and T." In such a scheme, a completely unconstrained parameter is bounded below by Bot and above by Top.
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
undefined constant or terms created with the
error constructor may be assigned any type. Attempting to evaluate such an expression causes the code to abort unrecoverably.
In Common Lisp the type
NIL, contains no values and is a subtype of every type. The type named
NIL is sometimes confused with the type named
NULL, which has one value, namely the symbol
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
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
panic!() or looping forever. It is also the type of certain control-flow keywords, such as
return, which do not produce a value but are nonetheless usable as expressions.
In Ceylon, the bottom type is
Nothing. It is comparable to
Nothing 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
!Null (literally, a non-null member of the
Null unit type).
In PHP, the bottom type is
In Python, the bottom type is
typing.Never since version 3.11).
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
Never type was introduced as the bottom type. Before that, the bottom type used to be
- ^ a b c Pierce, Benjamin C. (1997). "Bounded Quantification with Bottom". Indiana University CSCI Technical Report (492): 1.
- ^ "Section 4.1: The Kinds of Types and Values". Java Language Specification (3rd ed.).
- ^ "Chapter 3 Expressions". Haskell 2010 Language Report. Retrieved 25 October 2022.
- ^ "Type NIL". Common Lisp HyperSpec. Retrieved 25 October 2022.
- ^ "Primitive Type never". The Rust Standard Library Documentation. Retrieved 2020-09-24.
- ^ "Chapter 3. Type system — 3.2.5. The bottom type". The Ceylon Language. Red Hat, Inc. Retrieved 2017-02-19.
- ^ "Essentials - The Julia Language", The Julia Programming Language Documentation, retrieved 2021-08-13
- ^ The never type, TypeScript 2.0 release notes, Microsoft, 2016-10-06, retrieved 2019-11-01
- ^ The never type, TypeScript 2.0 release notes, source code, Microsoft, 2016-10-06, retrieved 2019-11-01
- ^ typing.NoReturn, typing — Support for type hints, Python documentation, Python Software Foundation, retrieved 2020-02-25
- ^ "typing — Support for type hints — Python 3.12.0a0 documentation". docs.python.org. Retrieved 2022-07-04.
- ^ Nothing, retrieved 2020-05-15
- ^ "Types - D Programming Language". dlang.org. Retrieved 2022-10-20.
- ^ Understanding null safety - top and bottom, retrieved 2022-04-13
- ^ Understanding null safety - never for unreachable code, retrieved 2022-04-13