To install click the Add extension button. That's it.

The source code for the WIKI 2 extension is being checked by specialists of the Mozilla Foundation, Google, and Apple. You could also do it yourself at any point in time.

4,5
Kelly Slayton
Congratulations on this excellent venture… what a great idea!
Alexander Grigorievskiy
I use WIKI 2 every day and almost forgot how the original Wikipedia looks like.
Live Statistics
English Articles
Improved in 24 Hours
Languages
Recent
Show all languages
What we do. Every page goes through several hundred of perfecting techniques; in live mode. Quite the same Wikipedia. Just better.
.
Leo
Newton
Brights
Milds

# Bottom type

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.

A function whose return type is bottom (presumably) 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:

• 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 continuation.)
• 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 pointers) or exception handling.

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]

## References

1. ^ a b 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", The Julia Programming Language Documentation, retrieved 2021-08-13
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