Bottom type

Last updated

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 the up tack (⊥) symbol.

Contents

A function whose return type is bottom cannot return any value, not even the zero size unit type. Therefore a function whose return type is the bottom type cannot return. In the Curry–Howard correspondence, the bottom type corresponds to falsity.

Computer science applications

In subtyping systems, the bottom type is the subtype of all types. [1] (However, the converse is not true—a subtype of all types is not necessarily the bottom type.) 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, which spans all possible values in a system, and a unit type, which has exactly one value.

The bottom type is frequently used for the following purposes:

In Bounded Quantification with Bottom, [1] 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. [3] 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 value null.
  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.

In programming languages

Most commonly used languages don't have a way to explicitly denote the empty type. There are a few notable exceptions.

Since Haskell2010, Haskell supports empty data types. Thus, it allows 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].

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. [4]

In Ceylon, the bottom type is Nothing. [5] 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{}. [6]

In TypeScript, the bottom type is never. [7] [8]

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, the bottom type is typing.NoReturn. [9]

In Kotlin, the bottom type is Nothing. [10]

In Elm, the bottom type is Never. [11]

See also

Related Research Articles

In object-oriented programming, the iterator pattern is a design pattern in which an iterator is used to traverse a container and access the container's elements. The iterator pattern decouples algorithms from containers; in some cases, algorithms are necessarily container-specific and thus cannot be decoupled.

In object-oriented and functional programming, an immutable object is an object whose state cannot be modified after it is created. This is in contrast to a mutable object, which can be modified after it is created. In some cases, an object is considered immutable even if some internally used attributes change, but the object's state appears unchanging from an external point of view. For example, an object that uses memoization to cache the results of expensive computations could still be considered an immutable object.

In computer science, primitive data type is either of the following:

In computer science, a NOP, no-op, or NOOP is an assembly language instruction, programming language statement, or computer protocol command that does nothing.

Pointer (computer programming) Object which stores memory addresses in a computer program

In computer science, a pointer is an object in many programming languages that stores a memory address. This can be that of another value located in computer memory, or in some cases, that of memory-mapped computer hardware. A pointer references a location in memory, and obtaining the value stored at that location is known as dereferencing the pointer. As an analogy, a page number in a book's index could be considered a pointer to the corresponding page; dereferencing such a pointer would be done by flipping to the page with the given page number and reading the text found on that page. The actual format and content of a pointer variable is dependent on the underlying computer architecture.

In computer programming, a return statement causes execution to leave the current subroutine and resume at the point in the code immediately after the instruction which called the subroutine, known as its return address. The return address is saved by the calling routine, today usually on the process's call stack or in a register. Return statements in many languages allow a function to specify a return value to be passed back to the code that called the function.

Many programming language type systems support subtyping. For instance, if the type Cat is a subtype of Animal, then an expression of type Cat should be substitutable wherever an expression of type Animal is used.

In computer science, the Boolean data type is a data type that has one of two possible values which is intended to represent the two truth values of logic and Boolean algebra. It is named after George Boole, who first defined an algebraic system of logic in the mid 19th century. The Boolean data type is primarily associated with conditional statements, which allow different actions by changing control flow depending on whether a programmer-specified Boolean condition evaluates to true or false. It is a special case of a more general logical data type —logic doesn't always need to be Boolean.

In computing, a null pointer or null reference is a value saved for indicating that the pointer or reference does not refer to a valid object. Programs routinely use null pointers to represent conditions such as the end of a list of unknown length or the failure to perform some action; this use of null pointers can be compared to nullable types and to the Nothing value in an option type.

In computer programming, an entry point is a point in a program where the execution of a program begins, and where the program has access to command line arguments.

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 ignore the details of its value. One may also regard the unit type as the type of 0-tuples, i.e. the product of no types.

The syntax of JavaScript is the set of rules that define a correctly structured JavaScript program.

In mathematical logic and computer science, some type theories and type systems include a top type that is commonly denoted with top or the symbol ⊤. The top type is sometimes called also universal type, or universal supertype as all other types in the type system of interest are subtypes of it, and in most cases, it contains every possible object of the type system. It is in contrast with the bottom type, or the universal subtype, which every other type is supertype of and it is often that the type contains no members at all.

Nullable types are a feature of some programming languages which allow the value to be set to the special value NULL instead of the usual possible values of the data type. In statically typed languages, a nullable type is an option type, while in dynamically typed languages, equivalent behavior is provided by having a single null value.

In object-oriented computer programming, a null object is an object with no referenced value or with defined neutral ("null") behavior. The null object design pattern describes the uses of such objects and their behavior. It was first published in the Pattern Languages of Program Design book series.

The null coalescing operator is a binary operator that is part of the syntax for a basic conditional expression in several programming languages, including C#, PowerShell as of version 7.0.0, Perl as of version 5.10, Swift, and PHP 7.0.0. While its behavior differs between implementations, the null coalescing operator generally returns the result of its left-most operand if it exists and is not null, and otherwise returns the right-most operand. This behavior allows a default value to be defined for cases where a more specific value is not available.

In computing, undefined value is a condition where an expression does not have a correct value, although it is syntactically correct. An undefined value must not be confused with empty string, boolean "false" or other "empty" values. Depending on circumstances, evaluation to an undefined value may lead to exception or undefined behaviour, but in some programming languages undefined values can occur during a normal, predictable course of program execution.

CoffeeScript is a programming language that compiles to JavaScript. It adds syntactic sugar inspired by Ruby, Python and Haskell in an effort to enhance JavaScript's brevity and readability. Specific additional features include list comprehension and destructuring assignment.

Gradual typing is a type system in which some variables and expressions may be given types and the correctness of the typing is checked at compile time and some expressions may be left untyped and eventual type errors are reported at runtime. Gradual typing allows software developers to choose either type paradigm as appropriate, from within a single language. In many cases gradual typing is added to an existing dynamic language, creating a derived language allowing but not requiring static typing to be used. In some cases a language uses gradual typing from the start.

In object-oriented programming, the safe navigation operator is a binary operator that returns null if its first argument is null; otherwise it performs a dereferencing operation as specified by the second argument.

References

  1. 1 2 Pierce, Benjamin C. (1997). "Bounded Quantification with Bottom". CiteSeerX   10.1.1.17.9230 .Cite journal requires |journal= (help)
  2. Griffin, Timothy G. (1990). "The Formulae-as-Types Notion of Control". Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, POPL '90, San Francisco, CA, USA, 17-19 Jan 1990. pp. 47–57.
  3. "Section 4.1: The Kinds of Types and Values". Java Language Specification (3rd ed.).
  4. "Primitive Type never". The Rust Standard Library Documentation. Retrieved 2020-09-24.
  5. "Chapter 3. Type system — 3.2.5. The bottom type". The Ceylon Language. Red Hat, Inc. Retrieved 2017-02-19.
  6. Essentials - The Julia Language
  7. The never type, TypeScript 2.0 release notes, Microsoft, 2016-10-06, retrieved 2019-11-01
  8. The never type, TypeScript 2.0 release notes, source code, Microsoft, 2016-10-06, retrieved 2019-11-01
  9. typing.NoReturn, typing — Support for type hints, Python documentation, Python Software Foundation, retrieved 2020-02-25
  10. Nothing , retrieved 2020-05-15
  11. Never , retrieved 2021-03-25

Further reading