Concept

Empty type

Summary
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). It may also be defined as the polymorphic type 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. A type theory need not contain an empty type. Where it exists, an empty type is not generally unique. For instance, is also uninhabited for any inhabited type . 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 .
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.