Empty type

Template:Short description In type theory, an empty type or absurd type, typically denoted $\mathbb{𝟘}$ 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 $\mathrm{\forall }t.t$

For any type $P$, the type $\mathrm{\neg }P$ is defined as $P\to \mathbb{𝟘}$. As the notation suggests, by the Curry–Howard correspondence, a term of type $\mathbb{𝟘}$ is a false proposition, and a term of type $\mathrm{\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{𝟘}$ 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 $\mathrm{\perp }$.