Bottom Type¶
The least type in a declared subtyping order, below every type and useful for typing paths that return no ordinary value.
Core Idea¶
A bottom type is the least type in a declared subtyping order: \(\bot<:T\) for every type \(T\) in that system's stated universe. This explains why a bottom-typed expression can fit many otherwise unrelated expected types. Kotlin calls its bottom type Nothing, Scala also uses Nothing, and TypeScript uses never with corresponding assignability behavior.[ref-956988672350][ref-03fe01e6ff7b][^ref-8e8f31ab9906]
These types have no ordinary runtime instances in the cited systems. A thrown exception or infinite loop can be assigned a bottom static type precisely because it does not return a value. The exception itself is not a value of Nothing, and a loop does not manufacture one.[ref-956988672350][ref-c13991ecda67]
Scope of Application¶
Kotlin's official example defines a fail function returning Nothing and uses it as the fallback of an expression assigned to String: person.name ?: fail("Name required"). If the name is present, the expression yields a string; otherwise it throws. Nothing is below String, so the nonreturning fallback fits the expected type without claiming it produces a string.[ref-956988672350][ref-c13991ecda67]
TypeScript uses never for another purpose. In an exhaustive switch over a Circle | Square union, the default branch has no remaining variant, so assigning it to never succeeds. Add Triangle without handling it, and the assignment fails: the unhandled variant is not never. This is a compile-time coverage check rather than a runtime never value.[^ref-8e8f31ab9906]
Scala illustrates a third use: its Nil has type List[Nothing], and covariance makes it usable as List[T] for any element type T. That consequence depends on the List variance rule as well as on Nothing being below all types.[^ref-03fe01e6ff7b]
Clarity¶
The bottom test is about position in a type order, not merely about having no values. A live Empty Type entry describes absent inhabitants and elimination from an impossible value. A concrete type can be both empty and bottom, but one must check the language's subtyping rule before equating the identities. Agda's empty datatype with an absurd pattern illustrates the empty-type side; Kotlin's specification explicitly supplies the universal subtype relation.[ref-a122d739ab93][ref-956988672350]
Bottom also differs from Unit or ordinary void-like completion, where a computation may finish normally. It differs from Scala Null, which has a null value and is lower only with respect to reference types; Scala's Nothing is the universal subtype with no instances.[^ref-03fe01e6ff7b]
Manages Complexity¶
One least type can account for many nonreturning paths that otherwise would need separate special typing rules for every possible expected type. The surrounding program can still retain a precise successful result type, as Kotlin's String example shows.[^ref-c13991ecda67]
Bottom can also mark a state that should be impossible after all cases of a union have been removed. TypeScript's never assignment converts that fact into an exhaustiveness check. The benefit has a cost: extending the union makes existing exhaustive consumers fail until they handle the new case, which may be desirable assurance or unwanted churn depending on the design.[^ref-8e8f31ab9906]
Abstract Reasoning¶
First state the type universe and its subtype or assignment relation. Then ask whether the proposed bottom \(B\) satisfies \(B<:T\) for every admissible \(T\). If it is lower only than some category of types, it is not universal bottom for a larger universe.[ref-956988672350][ref-03fe01e6ff7b]
Next separate typing from evaluation. A Nothing-typed throw can fit a String context because it never returns normally. An exhaustively narrowed never branch is unreachable. Neither case proves that a bottom value exists at runtime.[ref-c13991ecda67][ref-8e8f31ab9906]
Knowledge Transfer¶
The least-element test transfers across type systems with an appropriate order, but a language's precise nullability, variance, coercion and exhaustiveness rules do not transfer automatically. The broader pattern relates to live prime Order. The proposed DAG link is to live Subtyping as a prerequisite, not a claim that a type is a kind of subtyping relation.
The name remains domain-specific because a least element of an arbitrary order is not thereby a type, and an empty type without a declared subtype relation is not automatically a bottom type.
[^ref-956988672350]: Kotlin Language Specification, “Type System,” Built-in Types (kotlin.Nothing) and Upper and Lower Bounds. Official specification.
[^ref-c13991ecda67]: Kotlin Documentation, “Exception and Error Handling,” “The Nothing type.” Official documentation.
[^ref-8e8f31ab9906]: TypeScript Handbook, “Narrowing,” “The never type” and “Exhaustiveness checking.” Official handbook.
[^ref-03fe01e6ff7b]: Scala 3.2.2 API, scala.Nothing, definition and Nil covariance example. Official Scala API.
[^ref-a122d739ab93]: Agda 2.6.3 documentation, “Coverage Checking,” empty datatype and absurd-clause case. Official documentation.
Relationships to Other Abstractions¶
Current abstraction Bottom Type Domain-specific
Parents (1) — more general patterns this builds on
-
Bottom Type presupposes Subtyping Domain-specific
A bottom type requires a subtyping relation in which it is below every admissible type.
Hierarchy paths (2) — routes to 2 parentless roots
- Bottom Type → Subtyping → Type System → Classification
- Bottom Type → Subtyping → Type System → Constraint
Neighborhood in Abstraction Space¶
Bottom Type sits in a sparse region of the domain-specific corpus (82nd percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.
Family — Type Systems & Functional Constructs (18 abstractions)
Nearest neighbors
- Many-sorted logic — 0.83
- Principal type — 0.83
- Distributive Law Between Monads — 0.83
- Kind (Type Theory) — 0.82
- Subtyping — 0.82
Computed from structural-signature embeddings · 2026-10-08