Encyclopedia

Empty type

In type theory, a type with no terms

Wikipedia contributorsAdapted for Fathomly · View authors

1 min read
Source updated December 7, 2025

In type theory, an empty type or absurd type, typically denoted $\mathbb {0}$ is a type with no terms. Such a type may be defined as the nullary coproduct (i.e. disjoint sum of no types). It may also be defined as the polymorphic type $\forall t.t$

For any type $P$ , the type $\neg P$ is defined as $P\to \mathbb {0}$ . As the notation suggests, by the Curry-Howard correspondence, a term of type $\mathbb {0}$ is a false proposition, and a term of type $\neg P$ is a disproof of proposition P.

A type theory need not contain an empty type. Where it exists, an empty type is not generally unique. For instance, $T\to \mathbb {0}$ is also uninhabited for any inhabited type $T$ .

If a type system contains an empty type, the bottom type must be uninhabited too, so no distinction is drawn between them and both are denoted $\bot$ .

Watch videos about Empty typeExplainers and documentaries on YouTube (opens in a new tab)

Sources and credits

This article is adapted from the Wikipedia article “Empty type”, written by its contributors and licensed under CC BY-SA 4.0. Fathomly has changed the layout, removed citation markers, navigation and maintenance notices, and adjusted punctuation. This adapted version is shared under the same license. For references, see the original article.

Fathomly is not affiliated with or endorsed by the Wikimedia Foundation. Spotted a problem? Tell us.