Is there a reason to have a bottom type in a programming language?

I'll take a simple example: C++ vs Rust.

Here is a function used to throw an exception in C++11:

[[noreturn]] void ThrowException(char const* message,
                                 char const* file,
                                 int line,
                                 char const* function);

And here is the equivalent in Rust:

fn formatted_panic(message: &str, file: &str, line: isize, function: &str) -> !;

On a purely syntactic matter, the Rust construct is more sensible. Note that the C++ construct specifies a return type even though it also specifies it is not going to return. That's a bit weird.

On a standard note, the C++ syntax only appeared with C++11 (it was tacked on top), but various compilers had been providing various extensions for a while, so that third party analysis tools had to be programmed to recognize the various ways this attribute could be written. Having it standardized is obviously clearly superior.

Now, as for the benefit?

The fact that a function does not return can be useful for:

• optimization: one can prune any code after it (it won't return), there is no need to save the registers (as it won't be necessary to restore them), ...
• static analysis: it eliminates a number of potential execution paths
• maintainability: (see static analysis, but by humans)

Maybe it loops forever, or maybe it throws an exception.

Sounds like a useful type to have in those situations, rare though they may be.

Also, even though Nothing (Scala's name for the bottom type) can have no values, List[Nothing] does not have that restriction, which makes it useful as the type of an empty list. Most languages get around this by making an empty list of strings a different type than an empty list of integers, which kind of makes sense, but makes an empty list more verbose to write, which is a big drawback in a list-oriented language. Haskell's empty list is a type constructor, which is equally terse and kind of elegant, but hard to wrap your head around.

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.

Haskell does things a bit differently. In Haskell an expression that never produces a value can have the type 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 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 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. The type of [] is the same as the type [error ""], which goes to show that the empty list is not the only value of its type.

Types form a monoid in two ways, together making a semiring. That's what's called algebraic data types. For finite types, this semiring directly relates to the semiring of natural numbers (including zero), which means you count how many possible values the type has (excluding “nonterminating values”).

• The bottom type (I'll call it Void) has zero values.
• The unit type has one value. I'll call both the type and its single value ().
• Composition (which most programming languages support quite directly, through records / structs / classes with public fields) is a product operation. For instance, (Bool, Bool) has four possible values, namely (False,False), (False,True), (True,False) and (True,True).
  The unit type is the identity element of the composition operation. E.g. ((), False) and ((), True) are the only values of type ((), Bool), so this type is isomorphic to Bool itself.
• Alternative types are somewhat neglected in most languages (OO languages kind-of support them with inheritance), but they are no less useful. An alternative between two types A and B basically has all the values of A, plus all the values of B, hence sum type. For instance, Either () Bool has three values, I'll call them Left (), Right False and Right True.
  The bottom type is the identity element of the sum: Either Void A has only values of the form Right a, because Left ... doesn't make sense (Void has no values).

What's interesting about these monoids is that, when you introduce functions to your language, the category of these types with the functions as morphisms is a monoidal category. Amongst other things, this allows you to define applicative functors and monads, which turn out to be an excellent abstraction for general computations (possibly involving side-effects etc.) within otherwise purely functional terms.

Now, actually you can get quite far with worrying only one side of the issue (the composition monoid), then you don't really need the bottom type explicitly. For instance, even Haskell doesn't have a standard bottom type (though it's extremely popular in libraries).

But when you consider the full picture, as a bicartesian closed category, then the type system is actually equivalent to the whole lambda calculus, so basically you have the perfect abstraction over everything possible in a Turing-complete language. Great for embedded domain-specific languages, for instance there's a project about directly coding electronic circuits this way.

Of course, you may well say that this is all theoretists' general nonsense. You don't need to know about category theory at all to be a good programmer, but when you do, it gives you powerful and ridiculously general ways to reason about code, and proove invariants.

In some languages, null has the bottom type, since the subtype of all types nicely defines what languages use null for (despite the mild contradiction of having null be both itself and a function that returns itself, avoiding the common arguments about why bot should be uninhabited).

It can also be used as a catch-all in function types (any -> bot) to handle dispatch gone awry.

And some languages allow you to actually resolve bot as an error, which can be used to provide custom compiler errors.

It is useful for static analysis to document the fact that a particular code path is not reachable. For example if you write the following in C#:

int F(int arg) {
 if (arg != 0)
  return arg + 1; //some computation
 else
  Assert(false); //this throws but the compiler does not know that
}
void Assert(bool cond) { if (!cond) throw ...; }

The compiler will complain that F does not return anything in at least one code path. If Assert were to be marked as non-returning the compiler would not need to warn.

Yes this is a quite useful type; while its role would be mostly interior to the type system, there are some occasion where the bottom type would appear in openly.

Consider a statically typed language in which conditionals are expressions (so the if-then-else construction doubles as the ternary operator of C and friends, and there might be a similar multi-way case statement). Functional programming language have this, but it happens in certain imperative languages as well (ever since ALGOL 60). Then all branch expressions must ultimately produce the type of the whole conditional expression. One could simply require their types to be equal (and I think this is the case for the ternary operator in C) but this is overly restrictive especially when the conditional can also be used as conditional statement (not returning any useful value). In general one wants each branch expression to be (implicitly) convertible to a common type that will be the type of the full expression (possibly with more or less complicated restrictions to allow that common type to be effectively found by the complier, cf. C++, but I won't go into those details here).

There are two kinds of situations where a general kind of conversion will allow necessary flexibility of such conditional expressions. One is already mentioned, where the result type is the unit type void; this is naturally a super-type of all other types, and allowing any type to be (trivially) converted to it makes it possible to use the conditional expression as conditional statement. The other involves cases where the expression does return a useful value, but one or more branches are incapable of producing one. They will usually raise an exception or involve a jump, and requiring them to (also) produce a value of the type of the whole expression (from an unreachable point) would be pointless. It is this kind of situation that can be gracefully handled by giving exception-raising clauses, jumps, and calls that will have such an effect, the bottom type, the one type that can be (trivially) converted into any other type.

I would suggest writing such a bottom type as * to suggest its convertibility to arbitrary type. It may serve other useful purposes internally, for instance when trying to deduce a result type for a recursive function that does not declare any, the type inferencer could assign the type * to any recursive call to avoid a chicken-and-egg situation; the actual type will be determined by non-recursive branches, and the recursive ones will be converted to the common type of the non-recursive ones. If there are no non-recursive branches at all, the type will remain *, and correctly indicate that the function has no possible way of ever returning from the recursion. Other than this and as result type of exception throwing functions, one can use * as component type of sequences of length 0, for instance of the empty list; again if ever an element is selected from an expression of type [*] (necessarily empty list), then the resulting type * will correctly indicated that this can never return without an error.

If a function's return type is the bottom type, that means that it does not return. Period.

In theory there is nothing to return, so for this purpose we can say it does not return, but of course it does return because the program must continue.

Maybe it loops forever, or maybe it throws an exception.

This would be the programmer's issue, not the programming language's problem.

What is the point of having this weird type in a programming language?

To indicate that nothing is to be returned of course! It is not always necessary to include in Scala, but from time to time it is required by Scala's type system so it can infer possibilities elsewhere. It is after all Turing complete...