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 .