Bottom type
Encyclopedia
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 falsum
(⊥).
A function whose return type is bottom cannot return any value. In the Curry–Howard correspondence, the bottom type corresponds to falsity.
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 sometimes confused with the so-called "void type
", which is actually a unit type, albeit one with no defined operations.
The bottom type is frequently used for the following purposes:
In Bounded Quantification with Bottom, Pierce says that "Bot" has many uses:
Haskell
does not support empty data types. However, in GHC
, there is a flag -XEmptyDataDecls to allow the definition data Empty (with no constructors). The type Empty is not quite empty, as it contains non-terminating programs and the undefined constant. The undefined constant is often used when you want something to have the empty type, because undefined matches any type (so is kind of a "subtype" of all types), and attempting to evaluate undefined will cause the program to abort, therefore it never returns an answer.
In Common Lisp
the symbol NIL, amongst its other uses, is also the name of a type that has no values. It is the complement of T which is the top type. 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].
Type theory
In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...
, a theory within mathematical logic
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, the bottom type is the type that has no values. It is also called the zero or empty type, and is sometimes denoted with falsum
Falsum
The up tack is a constant symbol used to represent:* Bottom element in lattice theory.* The bottom type in type theory.* A logical constant denoting contradiction in logic.It appears as the upside down tee symbol....
(⊥).
A function whose return type is bottom cannot return any value. In the Curry–Howard correspondence, the bottom type corresponds to falsity.
Computer science applications
The bottom type is a subtype of all types. 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
Top type
The top type in type theory, commonly abbreviated as top or by the down tack symbol , is the universal type—that type which contains every possible object in the type system of interest. The top type is sometimes called the universal supertype as all other types in any given type system are...
, which spans all possible values in a system, and a unit type
Unit type
In the area of mathematical logic, and computer science known as type theory, a unit type is a type that allows only one value . The carrier associated with a unit type can be any singleton set. There is an isomorphism between any two such sets, so it is customary to talk about the unit type and...
, which has exactly one value. The bottom type is sometimes confused with the so-called "void type
Void type
The void type, in several programming languages derived from C and Algol68, is the type for the result of a function that returns normally, but does not provide a result value to its caller. Usually such functions are called for their side effects, such as performing some task or writing to their...
", which is actually a unit type, albeit one with no defined operations.
The bottom type is frequently used for the following purposes:
- To signal that a function or computation diverges; in other words, does not return a result to the caller. (This does not necessarily mean that the program fails to terminate; a subroutine may terminate without returning to its caller, or exit via some other means such as a continuationContinuationIn computer science and programming, a continuation is an abstract representation of the control state of a computer program. A continuation reifies the program control state, i.e...
.)- When coupled with the Curry-Howard interpretation of bottom as "falsity", this yields a computational interpretation of non-constructive logic in terms of control flowControl flowIn computer science, control flow refers to the order in which the individual statements, instructions, or function calls of an imperative or a declarative program are executed or evaluated....
operators.
- When coupled with the Curry-Howard interpretation of bottom as "falsity", this yields a computational interpretation of non-constructive logic in terms of control flow
- As an indication of error; this usage primarily occurs in theoretical languages where distinguishing between errors is unimportant. Production programming languages typically use other methods, such as option types (including tagged pointerTagged pointerIn computer science, a tagged pointer is a common example of a tagged union, where the primary type of data to be stored in the union is a pointer...
s) or exception handlingException handlingException handling is a programming language construct or computer hardware mechanism designed to handle the occurrence of exceptions, special conditions that change the normal flow of program execution....
.
In Bounded Quantification with Bottom, Pierce says that "Bot" has many uses:
- In a language with exceptionsException handlingException handling is a programming language construct or computer hardware mechanism designed to handle the occurrence of exceptions, special conditions that change the normal flow of program execution....
, 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.
- List[Bot] is a natural type for the "null pointer" value (a pointer which does not point to any object) of languages like Java: in JavaJava (programming language)Java is a programming language originally developed by James Gosling at Sun Microsystems and released in 1995 as a core component of Sun Microsystems' Java platform. The language derives much of its syntax from C and C++ but has a simpler object model and fewer low-level facilities...
, 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 does not satisfy all the properties of a bottom type as described above, because bottom types cannot have any possible values, and the null type has the valuenull. - A type system including both Top and Bot seems to be a natural target for type inferenceType inferenceType inference refers to the automatic deduction of the type of an expression in a programming language. If some, but not all, type annotations are already present it is referred to as type reconstruction....
, 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 explicitly denote the empty type. There are a few notable exceptions.Haskell
Haskell (programming language)
Haskell is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a first-class citizen" of the programming language. As a functional programming language, the...
does not support empty data types. However, in GHC
Glasgow Haskell Compiler
The Glorious Glasgow Haskell Compilation System, more commonly known as the Glasgow Haskell Compiler or GHC, is an open source native code compiler for the functional programming language Haskell. The lead developers are Simon Peyton Jones and Simon Marlow...
, there is a flag -XEmptyDataDecls to allow the definition data Empty (with no constructors). The type Empty is not quite empty, as it contains non-terminating programs and the undefined constant. The undefined constant is often used when you want something to have the empty type, because undefined matches any type (so is kind of a "subtype" of all types), and attempting to evaluate undefined will cause the program to abort, therefore it never returns an answer.
In Common Lisp
Common Lisp
Common Lisp, commonly abbreviated CL, is a dialect of the Lisp programming language, published in ANSI standard document ANSI INCITS 226-1994 , . From the ANSI Common Lisp standard the Common Lisp HyperSpec has been derived for use with web browsers...
the symbol NIL, amongst its other uses, is also the name of a type that has no values. It is the complement of T which is the top type. 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
Covariance and contravariance (computer science)
Within the type system of a programming language, covariance and contravariance refers to the ordering of types from narrower to wider and their interchangeability or equivalence in certain situations ....
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].
See also
- Haskell's Denotational semantics (Discusses the role of Bottom in the denotational semantics of programming languages)
- Top typeTop typeThe top type in type theory, commonly abbreviated as top or by the down tack symbol , is the universal type—that type which contains every possible object in the type system of interest. The top type is sometimes called the universal supertype as all other types in any given type system are...
- NaNNaNIn computing, NaN is a value of the numeric data type representing an undefined or unrepresentable value, especially in floating-point calculations...
- Fail-stopFail-stopA fail-stop subset of a computer language is one that has the same semantics as the original, except in the case where an exceptional condition arises...