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
As the notation suggests, by the Curry–Howard correspondence, a term of type
is a false proposition, and a term of type
Where it exists, an empty type is not generally unique.
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
This theoretical computer science–related article is a stub.