empty type

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$.

References

{{Comp-sci-theory-stub

Type theory
Unknown content