Empty type
Introduction 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 .
References