A type, in type theory, which has the property that it is the subtype of all other types in the universe. As it is impossible for an instance to be a member of all types (there is no instance which is a record, AND a boolean, AND a function, for instance); this type is empty or "uninhabited"; no instances of this type exist.
Called Bot (_|_) in Haskell; called Void (VoidType?) in EiffelLanguage. C/C++ void has some properties similar to a bottom type; however neither language makes the claim that it is a universal subtype. (Of course, C doesn't HAVE a notion of subtypes and supertypes to begin with). Nil in CommonLisp is also the BottomType.
Unlike the universal supertype TopType, which is found in most OO languages (CeePlusPlus being an exception, although "void *" is often used to emulate it), BottomType causes problems with strong type systems; as virtually everything needs to be checked if it is a BottomType or not. (In addition, there is the problem of casting something to BottomType, and then casting it back to something else.)
Is this right? If there can be no instance of the bottom type, then it is impossible for you to ever receive an instance of it where you were expecting something else. And if you did somehow, then by definition it would be valid (as it would be a subtype of whatever it is you were expecting). Notably, 'null' as implemented in many (most?) languages is not the member of the bottom type; it is a singleton value of another class hierarchy which is special cased to allow it to be used in place of a normal value. Lastly, casting anything to the bottom type is a type error (again, by definition), and would be flagged as such at runtime if not at compile type. -- WilliamUnderwood
- Well, it's an exaggerated phrasing. Consider naive set theory. The null set is a subset of all sets, it is always an empty set (the empty set), it is the result of intersecting sets with no members in common. But it certainly exists. BottomType is precisely the same thing, there's no contradiction.
- You are correct that fiddling with BottomType is a type error, because essentially, BottomType is precisely that, the type that indicates type error, so it's not an issue that it "would be flagged as such at runtime if not at compile type", that is in fact a tautology. Any operation involving BottomType yields BottomType. On the other hand, rather than propagating errors, they can instead cause the computation to halt. The IEEE floating point standard supports either propagation of BottomType (NaN, not a number) or signalling upon encounter of BottomType. The difference between a computation that runs to completion and yields the result "error", and one that abruptly ceases and yields the result "error", is often not significant other than the convenience of waiting a shorter period of time.
- Despite the phrasing above, BottomType almost always "exists" in some sense, in any language in which type errors are possible; it just may or may not have an explicit representation in any particular language, since it's a mathematical entity. Formally, only completely polymorphic languages (those in which all functions accept TopType as a parameter) can avoid having at least an implicit BottomType, since that's the only way to avoid the possibility of type error across all possible programs. -- DougMerritt
Despite not existing; it is often used for several things:
- As the "return type" of FirstClassContinuations. Since continuations do not return, the fact that there are no values of BottomType is not a problem, and this approach allows the usual subtyping rules for function types to work for continuations.
- As type of the NullPointer (see WhatIsNull). Eiffel does this; CeeLanguage kinda does this. (NULL is ((void *)0) in C). CeePlusPlus undid this (redefining NULL to simply be 0); though BjarneStroustrup has proposed (http://www.cuj.com/documents/s=8009/cuj0209stroustr/) making NULL a void * once again.
- As an exception type. Useful in this context if you only want to have one type of exception; if you want to have exceptions that have information; using BottomType for this purpose doesn't work as well.
- As an indication of divergence (in other words, a function that doesn't return). Absent a stack overflow, a function that doesn't return won't return Bot, so not returning something that doesn't exist sort of works. HaskellLanguage does this.
--
ScottJohnson
See also MeetsAndJoins, LatticeStructure
CategoryLanguageTyping