Skip to content

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


why is the absurd function useful?