Concept# Empty type

Summary

In type theory, an empty type or absurd type, typically denoted \mathbb 0 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 \forall t.t
For any type P, the type \neg P is defined as P\to \mathbb 0. As the notation suggests, by the Curry–Howard correspondence, a term of type \mathbb 0 is a false proposition, and a term of type \neg P 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, T \to \mathbb 0 is also uninhabited for any inhabited type T.
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 \bot.

Official source

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.

Related publications

Loading

Related people

Loading

Related units

Loading

Related concepts

Loading

Related courses

Loading

Related lectures

Loading

Related publications

Related units

No results

No results

Related people

Related concepts

No results

No results

Related courses

No results

Related lectures

No results