Does any language need to have a bottom type?

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?

2 Answers

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();

• Do you mean f()? – András Kovács Jan 11 at 19:42
• Yes, thanks, fixed. – Andrej Bauer Jan 12 at 12:37
• "Programming languages typically do not have the bottom type" -- citation needed. Seems to be catching on in modern languages. For example, in Kotlin your can't write a similar snippet because a function with "return" type Nothing may never return. – Raphael Jan 12 at 23:59
• @Raphael: Really? How about this: pl.kotl.in/IdDjW2fUt it seems to work. (And if you're worried about the "unreachable code" warning, we should be able to trick the analyzer into giving up.) With general recursion in hand, every type will have a closed expression but not necessarily a value. (So Nothing does not have any values, but there are expressions in the language that have that type.) – Andrej Bauer Jan 13 at 7:53

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.

• You are confusing the empty type and the undefined value $\bot$. – Andrej Bauer Jan 11 at 17:19
• @AndrejBauer Yes you are totally right. I never used $\bot$ as synonym of empty type but only as undefined value. I should have read the question better. – Peregring-lk Jan 11 at 23:01