Bottom 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.

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:

1. 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.
2. Bot is useful in typing the "leaf nodes" of polymorphic data structures. For example, List(Bot) is a good type for nil.
3. 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. null is the only value of the null type; and it can be cast to any reference type.{{cite book | chapter-url = http://docs.oracle.com/javase/specs/jls/se5.0/html/typesValues.html#4.1 | title = Java Language Specification | edition = 3rd | chapter = Section 4.1: The Kinds of Types and Values }} However, the null type is not a bottom type as described above, it is not a subtype of int and other primitive types.
4. 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.

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 Void.{{cite web

| url = https://hackage.haskell.org/package/base-4.18.0.0/docs/Data-Void.html

| title = Data.Void

| website = Hackage

| access-date = 2023-09-20

}}

In Common Lisp the type NIL, contains no values and is a subtype of every type.{{cite web |title=Type NIL |url=http://www.lispworks.com/documentation/HyperSpec/Body/t_nil.htm |website=Common Lisp HyperSpec |access-date=25 October 2022}} The type named NIL is sometimes confused with the type named NULL, which has one value, namely the symbol NIL itself.

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 List[Nothing].

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 break and return, which do not produce a value but are nonetheless usable as expressions.{{cite web

| url = https://doc.rust-lang.org/std/primitive.never.html

| title = Primitive Type never

| website = The Rust Standard Library Documentation

| access-date = 2020-09-24

}}

In Ceylon, the bottom type is Nothing.{{cite web

| url = https://ceylon-lang.org/documentation/spec/html/typesystem.html#bottomtype

| title = Chapter 3. Type system — 3.2.5. The bottom type

| website = The Ceylon Language

| publisher = Red Hat, Inc.

| access-date = 2017-02-19

}} 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 Union{}.{{Citation|title=Essentials - The Julia Language|website=The Julia Programming Language Documentation|url=https://docs.julialang.org/en/v1/base/base/#Union{}|access-date=2021-08-13}}

In TypeScript, the bottom type is never.{{Citation|title=The never type, TypeScript 2.0 release notes|date=2016-10-06|url=https://www.typescriptlang.org/docs/handbook/release-notes/typescript-2-0.html#the-never-type|publisher=Microsoft|access-date=2019-11-01}}{{Citation|title=The never type, TypeScript 2.0 release notes, source code|date=2016-10-06|url=https://github.com/microsoft/TypeScript-Handbook/blob/bb3564f4f06dd776d430198a137ae9058454d990/pages/release%20notes/TypeScript%202.0.md#the-never-type|publisher=Microsoft|access-date=2019-11-01}}

In JavaScript with Closure Compiler annotations, the bottom type is !Null (literally, a non-null member of the Null unit type).

In PHP, the bottom type is never.

In Python's optional static type annotations, the general bottom type is typing.Never (introduced in version 3.11),{{Cite web |title=typing — Support for type hints — Python 3.12.0a0 documentation |url=https://docs.python.org/3.12/library/typing.html#typing.Never |access-date=2024-03-02 |website=docs.python.org}} while typing.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 of Never).{{Citation|title=typing.NoReturn, typing — Support for type hints, Python documentation|url=https://docs.python.org/3/library/typing.html#typing.NoReturn|publisher=Python Software Foundation|access-date=2024-03-02}}

In Kotlin, the bottom type is Nothing.{{Citation|title=Nothing|url=https://kotlinlang.org/api/latest/jvm/stdlib/kotlin/-nothing.html|access-date=2020-05-15}}

In D, the bottom type is noreturn.{{Cite web |title=Types - D Programming Language |url=https://dlang.org/spec/type.html#noreturn |access-date=2022-10-20 |website=dlang.org}}

In Dart, since version 2.12 with the [https://medium.com/dartlang/announcing-dart-2-12-499a6e689c87 sound null safety update], the Never type was introduced as the bottom type. Before that, the bottom type used to be Null.{{Citation|title=Understanding null safety - top and bottom|url=https://dart.dev/null-safety/understanding-null-safety#top-and-bottom|access-date=2022-04-13}}{{Citation|title=Understanding null safety - never for unreachable code|url=https://dart.dev/null-safety/understanding-null-safety#never-for-unreachable-code|access-date=2022-04-13}}

• Contradiction
• Fail-stop
• NaN
• Top type
• Unit type

{{reflist}}

• {{cite book |last=Pierce |first=Benjamin C. |author-link=Benjamin C. Pierce |title=Types and Programming Languages |year=2002 |publisher=MIT Press |isbn=0-262-16209-1}}

{{data types}}

{{DEFAULTSORT:Bottom Type}}

Category:Data types

Category:Type theory