Intype theory, anempty type orabsurd type, typically denoted${\displaystyle \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).^[1] It may also be defined as the polymorphic type${\displaystyle \mathrm{\forall }t.t}$^[2]

For any type${\displaystyle P}$, the type${\displaystyle \mathrm{\neg }P}$ is defined as${\displaystyle P\to \mathbb{0}}$. As the notation suggests, by theCurry–Howard correspondence, a term of type${\displaystyle \mathbb{0}}$ is a false proposition, and a term of type${\displaystyle \mathrm{\neg }P}$ is a disproof of proposition P.^[1]

A type theory need not contain an empty type. Where it exists, an empty type is not generally unique.^[2] For instance,${\displaystyle T\to \mathbb{0}}$ is alsouninhabited for any inhabited type${\displaystyle T}$.

If a type system contains an empty type, thebottom type must be uninhabited too, so no distinction is drawn between them and both are denoted${\displaystyle \mathrm{\perp }}$.

• Theoretical computer science stubs
• Type theory
• Unknown content

• Articles with short description
• Short description matches Wikidata
• All stub articles