empty type

{{Short description|In type theory, a type with no terms}}

In type theory, an empty type or absurd type, typically denoted $\backslash 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).{{cite book|author=Univalent Foundations Program|title=Homotopy Type Theory: Univalent Foundations of Mathematics|year=2013|publisher=Institute for Advanced Study|url=http://homotopytypetheory.org/book/}} It may also be defined as the polymorphic type $\backslash forall\; t.t${{cite book |year=1987 |volume=87 |doi=10.1145/41625.41648 |chapter-url=https://dl.acm.org/doi/10.1145/41625.41648 |access-date=25 October 2022|last1=Meyer |first1=A. R. |last2=Mitchell |first2=J. C. |last3=Moggi |first3=E. |last4=Statman |first4=R. |title=Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL '87 |chapter=Empty types in polymorphic lambda calculus |pages=253–262 |isbn=0897912152 |s2cid=26425651 }}

For any type $P$, the type $\backslash neg\; P$ is defined as $P\backslash to\; \backslash mathbb\; 0$. As the notation suggests, by the Curry–Howard correspondence, a term of type $\backslash mathbb\; 0$ is a false proposition, and a term of type $\backslash 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\; \backslash to\; \backslash 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,{{cite journal | last = Pierce | first = Benjamin C. | year = 1997 | title = Bounded Quantification with Bottom | journal = Indiana University CSCI Technical Report |issue= 492 |url=http://www.cis.upenn.edu/~bcpierce/papers/bqb.ps |pages=1 }} so no distinction is drawn between them and both are denoted $\backslash bot$.