Loading AI tools
In type theory, a type with no terms From Wikipedia, the free encyclopedia
In type theory, an empty type or absurd type, typically denoted 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 [2]
For any type , the type is defined as . As the notation suggests, by the Curry–Howard correspondence, a term of type is a false proposition, and a term of type 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, is also uninhabited for any inhabited type .
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 .
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.