Empty type explained

In type theory, an empty type or absurd type, typically denoted

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 \forall t.t ^[2]

For any type

P , the type \neg P is defined as P\to 0 . As the notation suggests, by the Curry–Howard correspondence, a term of type 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 0 is also uninhabited for any inhabited type T .

If a type system contains an empty type, the bottom type must be uninhabited too,^[3] so no distinction is drawn between them and both are denoted

\bot .

Notes and References

1. Book: Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. 2013. Institute for Advanced Study.
2. Book: 1987 . 87 . 10.1145/41625.41648 . https://dl.acm.org/doi/10.1145/41625.41648 . 25 October 2022. Meyer . A. R. . Mitchell . J. C. . Moggi . E. . Statman . R. . Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL '87 . Empty types in polymorphic lambda calculus . 253–262 . 0897912152 . 26425651 .
3. Pierce . Benjamin C. . 1997 . Bounded Quantification with Bottom . Indiana University CSCI Technical Report . 492 . 1 .