Bottom Type

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 Despite not existing; it is often used for several things:

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

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

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

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

EditText of this page (last edited November 8, 2013) or FindPage with title or text search