Void Type

In type theory, the void type is a type with a cardinality of $0$. It is therefore impossible to construct. It's dual is the unit type. It corresponds to the empty set from set theory.

A value of type Void cannot be constructed, just as a falsity cannot be proved.

This leads to functions like absurd in Haskell, which can be seen as 'bluffs'. If you can provide a value of type Void, they can provide any other type.

absurd :: Void -> a

Question

why is the absurd function useful?

References

• Book: Thinking with Types
• Video Series: Category Theory

Backlinks

• Dual
  • Void Type
• Unit Type
  • It is related to the singleton set from set theory and dual to the void type
• The empty set and the void type
  • The empty set in set theory corresponds to the Void type in type theory or to false in logic. There's also the 0-category in category theory.
• Void and Unit form the basis for all types
  • In type theory, void and unit form the basis for all other types.
• The void type is called 'never' in TypeScript
  • Although TypeScript has a void keyword it's really another word for undefined for historical reasons - it isn't the void from type theory.
• Sum Type
  • The monoidal identity of the sum operation is the void type, as $|Void| = 0$.
• Void is impossible to construct
  • In type theory, void is a type with no elements. This means that it is impossible to construct a void type.