Bottom Type¶

The least type in a declared subtyping order, below every type and useful for typing paths that return no ordinary value.

Version: v1 · 2026-10-03 · History
Domain-specific #: 13022
Domain group: Applied Sciences & Engineering
Origin domain: Computer Science & Software Engineering
Subdomains: Type Theory, Programming Language Semantics → Computer Science & Software Engineering
Aliases: Least Type, Universal Subtype

Core Idea¶

A bottom type is the least type in a specified subtyping order. If \(\bot\) is bottom and \(T\) ranges over the types in the declared universe, then \(\bot<:T\) for every \(T\). This universal-lower-bound property explains why a bottom-typed expression can fit a position whose expected type is otherwise unrelated. Kotlin's language specification identifies Nothing as the unified subtype of every well-formed Kotlin type; Scala identifies Nothing as a subtype of every type; TypeScript documents never as assignable to every type.^[1]^[2]^[3]

The type-order relation is the identity, not the spelling of a language feature. Nothing, never, and similar names are implementations with different typing and control-flow details. The result is especially useful for an expression that does not return an ordinary value: throwing, exiting, or looping forever can be assigned a bottom static type without requiring the enclosing expression to pretend it returned a value of some arbitrary type. Kotlin's documentation types a throw expression as Nothing; its official example places a Nothing-returning fail call where a String result is expected.^[1]^[4]

In the cited language designs, bottom has no runtime instances. This does not mean a thrown exception is an inhabitant of Nothing or that an infinite loop somehow produces one. It means the expression can receive a static type while evaluation never completes normally with a value of that type. The distinction between expression typing and returned values is essential to the abstraction.^[1]^[2]

Bottom must also be distinguished from an empty type. An empty type is described by lack of inhabitants and an elimination rule from an impossible term; bottom is described by its universal place in a subtyping order. In common sound language designs one type can play both roles, but absence of constructors alone does not, without the type system's rules, establish that this type is a universal subtype. Agda's empty datatype is presented through an absurd pattern, whereas Kotlin explicitly states the universal subtype relation for Nothing.^[5]^[1]

Structural Signature¶

Sig role-phrases: declared type universe → subtyping order → universal lower type \(\bot\) → expected-type compatibility → static/runtime distinction.

Declared type universe. “Every type” quantifies over a system's admissible types and sometimes a particular kind or nullability regime. Kotlin's specification says Nothing is below all well-formed Kotlin types. A type lower than only reference types would not thereby be bottom for a wider universe that also includes value types.^[1]
Subtyping order. The relation \(<:\) states when one type may be used under another's typing expectations. The bottom claim cannot even be formed without this ordering or an equivalent declared compatibility relation. It is more than a vocabulary label for an empty value set.^[1]^[3]
Universal lower type. A candidate \(B\) qualifies when \(B<:T\) holds for every \(T\) in the stated universe. This is its constitutive property. It is a least element, not merely one type with few inhabitants or a type below a small selection of others.^[1]^[2]
Context compatibility. The ordering lets bottom-typed computations fit places expecting other types. Kotlin's Nothing can stand in a String-expected fallback that throws. TypeScript's never can be assigned to any type, and conversely an attempt to assign a residual non-never union member to never fails.^[4]^[3]
Runtime-value distinction. In the cited mainstream implementations there is no ordinary value of bottom. Typing a nonreturning expression as bottom describes its control-flow status; it does not license extracting a value of every type at runtime. Removing this distinction makes throw and divergence examples misleading.^[1]^[2]

The first three roles define bottom in a type system. The last two explain its use and guard against an erroneous interpretation of “an expression has type bottom.” They are not a universal promise that every language exposes the same syntax, coercions or compiler diagnostics.

What It Is Not¶

It is not Unit or a language's ordinary void return. Such types describe a computation that can finish normally without a useful payload, or with a single unit value. Bottom instead describes a type below all others; Kotlin's Nothing has no runtime instances and marks paths that do not complete normally.^[1]^[4]

It is not merely a null type. Scala's Null is below reference types and has the null value, while Scala's Nothing is below every type and has no instances. The two names occupy different places in the hierarchy and have different value semantics.^[2]

It is not identical to the live Empty Type entry. Empty Type asks about constructors, inhabitants, and elimination from impossibility. Bottom Type asks whether a type is least under a declared subtype order. A concrete Nothing or never often satisfies both perspectives, but one perspective does not replace a proof of the other's formal rule.^[5]^[1]

It is not a runtime exception value or an “error type” meaning the compiler abandons checking. The error object thrown in Kotlin has its own type; the throw expression has type Nothing because it does not return normally. The universal-subtype property is still a static typing rule with a truth condition.^[4]

Scope of Application¶

In language type hierarchies, bottom provides a lower bound when types are compared. Kotlin's specification explicitly places Nothing beneath all well-formed types and uses it in lower-bound reasoning. Scala's API gives the same universal-subtype property for Nothing, while TypeScript's never has the corresponding assignment behavior. The exact context rules of these languages are not identical and should be consulted rather than inferred from the shared label.^[1]^[2]^[3]

In expression-oriented control flow, a nonreturning branch may need a type so the enclosing expression can be checked. Kotlin's fail(message): Nothing throws; its documented val s: String = person.name ?: fail("Name required") is well typed because the fallback never produces a conflicting value. The String assignment says what the successful path yields, not that fail returns a String.^[4]

In static exhaustiveness checking, TypeScript narrows a discriminated union until no case remains. Its never type marks the impossible residual. The handbook assigns a default-branch value to never: the check succeeds if all variants were handled and fails after a new unhandled variant is added. This use is not principally about a thrown exception; it exposes absence of remaining cases in the type order.^[3]

In a covariant type constructor, bottom can also aid polymorphic reuse. Scala's API states that Nil has type List[Nothing]; because List is covariant, it can be used as List[T] for any element type T. Covariance, not bottom alone, licenses this particular container conclusion.^[2]

Clarity¶

“Nothing” can sound like an ordinary value meaning no information. The bottom-type analysis asks instead: what is the subtype relation, and is this type below every type in the relevant universe? The answer can be inspected in a formal specification or compiler rule. It also shows why the bottom of an order is conceptually opposite a top type: top is above all types, while bottom is below them.^[1]

Separating static type from runtime value resolves a common confusion. An expression can have type Nothing precisely because it does not normally finish with a Nothing object. Kotlin says no instance of Nothing exists at runtime and also gives a throw expression that has that type. There is no contradiction once type judgment and evaluation result are kept distinct.^[1]^[4]

The distinction from Empty Type prevents a different shortcut. The fact that an inductive datatype has no constructors yields an impossible pattern and elimination behavior. To call that type bottom, one additionally needs the relevant subtyping or coercion order and the universal-lower-bound result. Agda's coverage documentation and Kotlin's type-system specification illustrate these two different assertions.^[5]^[1]

Manages Complexity¶

Bottom avoids a family of ad hoc typing exceptions for paths that cannot return a normal value. Instead of giving each throw or impossible branch every potential expected type separately, a language can give it one least type and rely on the order. Kotlin's official fallback example demonstrates how a Nothing expression can fit a String-producing context without inventing a successful value.^[1]^[4]

The same least-type idea condenses reasoning about impossible residual cases. In TypeScript, narrowing a union removes handled alternatives; when none remain, the residual is never. A single assignment to never then checks that the list of handled variants is complete. Adding a new variant makes the residual nonempty and triggers a diagnostic.^[3]

This compression has limits. A bottom type does not by itself track why a branch will not return, whether it throws, loops or is unreachable, and it does not guarantee that different languages implement variance, nullability and coercion alike. When those differences matter, the compact order statement must be expanded into the language's actual rules.^[1]^[2]^[3]

Abstract Reasoning¶

First fix the type universe and relation. Is the relevant judgment nominal subtyping, structural subtype compatibility, or assignment compatibility? Then test whether the candidate \(B\) is below every type \(T\) in that universe. A type merely below a useful subset—such as reference types—does not pass a universal-bottom claim for a broader universe.^[1]^[2]

Second inspect a proposed use. If a branch has bottom type, a surrounding expected type can accept it under the language's rules. But ask whether the branch can actually return a value. A Kotlin throw path does not return; this is why putting it in a String-typed expression does not create a value with the impossible type.^[4]

Third decide what follows and what does not. The least-type property can explain a compiler's exhaustiveness diagnostic, as TypeScript shows. It cannot alone prove termination, absence of exceptions, or that a List[Bottom] is usable as List[T] without the constructor's variance rule. Nor can the same conclusion be copied verbatim into another language merely because both expose a type named never or Nothing.^[3]^[2]

Knowledge Transfer¶

The order-theoretic test transfers literally among language type systems that declare a common subtype or assignability hierarchy: find the type below all others, then check how the language uses it in nonreturning expressions or impossible control-flow states. Kotlin, Scala and TypeScript document recognizably related roles while differing in exact syntax and compiler behavior.^[1]^[2]^[3]

It does not transfer unqualified to every empty type. An empty inductive type may support an absurd elimination, yet the presence of a global subtype lattice or coercion into all types is a separate fact. Similarly, Rust's ! is documented through never-to-any coercion, which should not be casually restated as an unrestricted nominal subtype theorem for Rust.^[5]

The portable skeleton “least element in an order” belongs to broader order theory and relates to live prime Order. Bottom Type remains specifically about types, substitution and static semantics. The live Subtyping entry supplies the relation whose existence this entry presupposes; a type itself is not a subtype of the relation.

Examples¶

Kotlin's nonreturning fallback¶

Kotlin documents a function fail(message): Nothing that throws. In its example, person.name may be null, and val s: String = person.name ?: fail("Name required") still type-checks. If the left side supplies a name, s receives a String; otherwise the fallback throws and supplies no value. Nothing is a subtype of every well-formed Kotlin type, so the fallback does not force a non-String result into the expression.^[1]^[4]

Mapped back: declared type universe = Kotlin's well-formed types including String; subtyping order = Kotlin's \(<:\) relation; universal lower type = Nothing; context compatibility = the fallback fits a String-expected expression; runtime-value distinction = throwing yields no Nothing instance.

TypeScript's exhaustive union check¶

The TypeScript handbook defines Shape as Circle | Square and switches on its discriminant. After both cases return, the default arm assigns the remaining shape to a variable of type never. That assignment succeeds when the union has been exhausted. When the handbook adds Triangle without a corresponding case, the residual is Triangle and the assignment to never fails, surfacing the omitted branch. Here the least-type property supports a static coverage test, not a computation that returns a never value.^[3]

Mapped back: declared type universe = TypeScript types in the Shape checking context; subtyping order = the documented never assignment relation; universal lower type = never; context compatibility = a truly impossible residual can be assigned to never, while an unhandled variant cannot; runtime-value distinction = an exhaustive default arm is unreachable, not a source of a value of never.

Boundary: Unit and the empty datatype¶

An ordinary unit value represents a normally completed computation with one trivial result, so it is not the universal uninhabited bottom. Agda's constructor-free empty datatype has no inhabitants and admits an absurd pattern, but that fact alone is an empty-type statement; one must inspect the surrounding system's subtyping/coercion rules before calling it a universal bottom type.^[5]

Structural Tensions¶

T1 — Closed-union exhaustiveness versus later variant extension. Assigning a TypeScript switch's residual to never gives compile-time assurance that current variants are handled. Adding a legitimate new variant then causes existing exhaustive consumers to fail type-checking until they are revised. Relaxing or omitting the check eases extension but gives up that automatic notice of missing cases. Both choices carry costs; neither changes the definition of never. Diagnostic: Should consumers be required to revisit this switch whenever the union grows, or is a permissive unhandled path acceptable here?^[3]

T2 — Uniform nonreturn typing versus cause-specific information. Giving throw and an endless execution path the same bottom result type makes both fit a context expecting any ordinary result. But that least-type fact alone cannot tell a caller whether an exception was raised, execution diverged, or a branch was statically unreachable. Preserving those distinctions requires other control-flow or effect information beyond the bottom label. Diagnostic: Does the analysis need only to know that no normal value returns, or must it distinguish how normal return fails?^[4]

Structural–Framed Character¶

Bottom Type is predominantly structural. Its defining \(\bot<:T\) relation is formal and evaluatively neutral. Evaluative weight: whether a type-system design is convenient is an engineering judgment, but least-element status itself is not praise. Human-practice dependence: programming languages choose syntax and compiler rules, yet the stated relation has a determinate truth condition within each formal system. Institutional origin: standards bodies and language maintainers publish these rules, but naming a type Nothing does not make it bottom unless the universal subtype claim holds. Vocabulary travel: “bottom” comes from order theory and transfers among type systems with a precise ordering; it does not mean the same thing as low priority or an empty container in unrelated settings. Import versus recognition: the analyst recognizes bottom by testing the type relation, not by importing a metaphor from a different language.^[1]^[3]

The portable skeleton is a least element in an order. The named entry adds typed expressions, subtyping and normal-return semantics. Its character: a formal, domain-specific type-system identity that travels across languages only when their actual compatibility rules preserve the least-type relation.

Structural Core vs. Domain Accent¶

The live prime Order supplies a portable notion of ordered elements, but the proposed DAG edge is to live domain-specific Subtyping as a prerequisite: Bottom Type cannot be stated without a type order. It is not a kind of Subtyping relation. “A least element can be used wherever a larger element is expected” is a possible higher-order skeleton, but any further prime status for that formulation is an unadmitted future-prime question, not a hidden graph edge.^[1]

The domain accent is constitutive. Types and typing contexts, language-specific compatibility, bottom expressions and the difference between static judgments and runtime values decide whether the label applies. An empty set in mathematics or a low-ranked node in an organization can be a bottom element of some order, but it is not a Bottom Type until these programming/type-theoretic roles are present. This is why the entry remains domain-specific despite the portable order skeleton.^[1]^[2]

This entry presupposes Subtyping.

Subtyping (live domain-specific; proposed composition/prerequisite parent): a bottom type's defining universal-lower-bound condition requires this relation.
Order (live prime; related upstream skeleton): least-element reasoning is order-theoretic, but Order alone does not supply types or typing contexts.
Empty Type (live domain-specific; overlapping but not automatically identical): no-inhabitant and elimination properties can coexist with bottom status, yet they answer a different formal question.
Type Theory (live domain-specific; wider field): many type theories study such objects, but the field is not a strict genus of one type.
Unit Type (live domain-specific; contrast): an ordinary trivial returned value differs from a type whose values do not normally occur and which sits below every type.

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

Show alternative path (1)

Neighborhood in Abstraction Space¶

Bottom Type sits in a sparse region of the domain-specific corpus (82^nd 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

Computed from structural-signature embeddings · 2026-10-08

Not to Be Confused With¶

Empty Type is identified by no inhabitants and its elimination rule; Bottom Type by least subtype-order position, even when a concrete type serves both roles. Unit describes a normal completion with one trivial value. Scala Null is a reference-related type with a null instance, not its universal Nothing bottom. Top Type is the opposite order extreme, above all admissible types rather than below them. An exception object is a value of an exception type; a throw expression may have bottom type because it produces no normal result. Finally, a compiler error type used to suppress cascaded diagnostics is not automatically a sound universal subtype.^[1]^[4]^[2]^[5]

References¶

[1] Kotlin Language Specification, “Type System,” Built-in Types (kotlin.Nothing) and Upper and Lower Bounds. Official specification. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n ↩o ↩p ↩q ↩r ↩s ↩t ↩u ↩v ↩w

[2] Scala 3.2.2 API, scala.Nothing, definition and Nil: List[Nothing]/covariance explanation. Official Scala API. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m

[3] TypeScript Handbook, “Narrowing,” “The never type” and “Exhaustiveness checking,” including the Shape switch and added Triangle case. Official handbook. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l

[4] Kotlin Documentation, “Exception and Error Handling,” “The Nothing type,” including the fail/Elvis-expression example. Official documentation. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k

[5] Agda 2.6.3 documentation, “Coverage Checking,” empty datatype and absurd-clause case. Official documentation. registry ↩a ↩b ↩c ↩d ↩e ↩f