Empty type
In type theory, an empty type or absurd type, typically denoted [math]\displaystyle{ \mathbb 0 }[/math] 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 [math]\displaystyle{ \forall t.t }[/math][2] For any type [math]\displaystyle{ P }[/math], the type [math]\displaystyle{ \neg P }[/math] is defined as [math]\displaystyle{ P\to \mathbb 0 }[/math]. As the notation suggests, by the Curry–Howard correspondence, a term of type [math]\displaystyle{ \mathbb 0 }[/math] is a false proposition, and a term of type [math]\displaystyle{ \neg P }[/math] 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, [math]\displaystyle{ T \to \mathbb 0 }[/math] is also uninhabited for any inhabited type [math]\displaystyle{ T }[/math].
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 [math]\displaystyle{ \bot }[/math].
References
- ↑ 1.0 1.1 Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. http://homotopytypetheory.org/book/.
- ↑ 2.0 2.1 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. 87. pp. 253–262. doi:10.1145/41625.41648. ISBN 0897912152. https://dl.acm.org/doi/10.1145/41625.41648. Retrieved 25 October 2022.
- ↑ Pierce, Benjamin C. (1997). "Bounded Quantification with Bottom". Indiana University CSCI Technical Report (492): 1. http://www.cis.upenn.edu/~bcpierce/papers/bqb.ps.
 |  |
