In type theory, an empty type or absurd type is a type with no terms. Such a type may be defined as the nullary coproduct (i.e. disjoint sum of no types).

. As the notation suggests, by the Curry–Howard correspondence 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. is also uninhabited.

If a type system contains an empty type, the bottom type.

References