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