# 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¶

## Backlinks¶

- Dual
- 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.

- The empty set in set theory corresponds to the
- Void and Unit form the basis for all 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.

- Although TypeScript has a void keyword it's really another word for
- 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.