Empty type

From Quire, the open reference·In type theory, a type with no terms·1 min read

In type theory, an empty type or absurd 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 \forall t.t}$ ^[2]

For any type ${\displaystyle P}$ , the type ${\displaystyle \neg P}$ is defined as ${\displaystyle P\to \mathbb {0} }$ . As the notation suggests, by the Curry–Howard correspondence, a term of type ${\displaystyle \mathbb {0} }$ is a false proposition, and a term of type ${\displaystyle \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 also uninhabited for any inhabited type ${\displaystyle 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 ${\displaystyle \bot }$ .

References#edit

^ a b Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study.
^ a b Meyer, A. R.; Mitchell, J. C.; Moggi, E.; Statman, R. (1987). "Empty types in polymorphic lambda calculus". Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL '87. Vol. 87. pp. 253–262. doi:10.1145/41625.41648. ISBN 0897912152. S2CID 26425651. Retrieved 25 October 2022.

This article is mirrored from “Empty type” on English Wikipedia, revision 1326215327, written by Wikipedia's contributors and licensed CC BY-SA 4.0. Editing it here creates a Quire copy with its own history.

Synced with Wikipedia revision 1326215327 · just now