Does any language need to have a bottom type?

Question

From wikipedia:

In type theory, a theory within mathematical logic, the bottom type is the type that has no values. It is also called the zero or empty type, and is sometimes denoted with the up tack (⊥) symbol.

The "bottomest" types I can think of in js are undefined and null, both unity types.

Notice how in TypeScript there is the explicit never bottom type for function that are not supposed to return anything, or to always throw an exception.

The question is/are:

1. does JavaScript have no bottom type?
2. if so, does that mean that languages do not need to have a bottom type?

Answer 1

Javascript has no bottom type. It does not even really have types in the sense of type theory. Instead, values are tagged with information that is called "dynamic type".

Programming languages typically do not have the bottom type (it is also called the empty type) because they allow defintion by general recursion, which implies that all types are non-empty. For example, to define a value v of any type T in Java, we can do this:

static T f() { return f(); }
static T v = f();

Answer 2

In actual programming languages, a function is not forced to deal explicity with input is not meant to. For a function f(x) you can say something like:

// x must satisfy x != 0, otherwise inv(x) results in undefined behaviour.
double inv(double x) { return 1/x; }

In computer since though, using $\bot$ is a very useful symbolic tool to express such indefinitions in piecewise-defined functions:

$$ f(x):\Bbb R\rightarrow\Bbb R = \begin{cases} \frac{1}{x} & \quad x\neq 0\\ \bot & \quad\text{otherwise} \end{cases} $$

So in short no, a programming language doesn't require to have any equivalent symbol. A language is only required of course of having tools for implementing well-defined cases. Any other precondition could be expressed in comments, documentation, etc, so the responsability of checking the input is transfered to the caller (this strategy is called design by contract).

NOTE: Some languages also have exceptions, but exceptions are more of a helper tool for error handling methods and not so much for expressing undefinition.