Karl's answer is good. Here is an additional use that I don't think anyone else has mentioned. The type of
if E then A else B
should be a type that includes all the values in the type of A
and all the values in the type of B
. If the type of B
is Nothing
, then the type of the if
expression can be the type of A
. I'll often declare a routine
def unreachable( s:String ) : Nothing = throw new AssertionError("Unreachable "+s)
to say that code is not expected to be reached. Since its type is Nothing
, unreachable(s)
can now be used in any if
or (more often) switch
without affecting the type of result. For example
val colour : Colour := switch state of
BLACK_TO_MOVE: BLACK
WHITE_TO_MOVE: WHITE
default: unreachable("Bad state")
Scala has such a Nothing type.
Another use case for Nothing
(as mentioned in Karl's answer) is List[Nothing] is the type of lists each of whose members has type Nothing. Thus it can be the type of the empty list.
The key property of Nothing
that makes these use cases work is not that it has no values --although in Scala, for example, it does have no values-- it is that it is a subtype of every other type.
Suppose you have a language where every type contains the same value -- let's call it ()
. In such a language the unit type, which has ()
as its only value, could be a subtype of every type. That doesn't make it a bottom type in the sense that the OP meant; the OP was clear that a bottom type contains no values. However, as it is a type that is a subtype of every type, it can play much the same role as a bottom type.
Haskell does things a bit differently. In Haskell, an expression that never produces a value can have the type scheme forall a.a
. An instance of this type scheme will unify with any other type, so it effectively acts as a bottom type, even though (standard) Haskell has no notion of subtyping. For example, the error
function from the standard prelude has type scheme forall a. [Char] -> a
. So you can write
if E then A else error ""
and the type of the expression will be the same as the type of A
, for any expression A
.
The empty list in Haskell has the type scheme forall a. [a]
. If A
is an expression whose type is a list type, then
if E then A else []
is an expression with the same type as A
.
void
data...void
, and unit type must have one value. Also, as you pointed out, you cannot even declare a value of typevoid
, that means it's not even a type, just a special corner case in the language.void
in Java is nearly the same: not really a type & can't have values.nil
(a.k.a.,()
), which is a unit type.