What is the kind of Void?

It's a type of kind * just like Int, Bool or (). It just happens to have 0 values instead of 1 or 2 or more.

It's not a hack but rather a fundamental part of Haskell's type system. It plays the role of 0 to ()'s 1 and, if we look at types as propositions, Void corresponds to the proposition "false". It's also an identity to sum types (Either) just like () is an identity to product types: Either a Void is isomorphic to a.

In practice, it often acts as a dual of (); the best example of this I've seen is in pipes where () is used to tag things that don't take inputs and Void (named X) is used to tag things that don't produce outputs. (See Appendix:Types in the tutorial.)

It is a way to mark things as impossible or missing, but it is by no means a hack.


0 was once not considered to be a number. "How can nothing be something?" But over time we came to accept 0 as a number, noticing its properties and its usefulness. Today the idea that 0 is not a number is as absurd as the idea that it was one 2,000 years ago.

Void is a type the same way 0 is a number. Its kind is *, just like all other types. The similarity between Void and 0 runs quite deep, as Tikhon Jelvis's answer begins to show. There is a strong mathematical analogy between types and numbers, with Either playing the role of addition, tupling (,) playing the role of multiplication, functions (->) as exponentiation (a -> b means ba), () (pronounced "unit") as 1, and Void as 0.

The number of values a type may take is the numeric interpretation of the type. So

Either () (Either () ())

is interpreted as

1 + (1 + 1)

so we should expect three values. And indeed there are exactly three.

Left ()
Right (Left ())
Right (Right ())

Similarly,

(Either () (), Either () ())

is interpreted as

(1 + 1) * (1 + 1)

so we should expect four values. Can you list them?

Coming back to Void, you can have, say, Either () Void, which would be interpreted as 1 + 0. The constructors of this type are Left (), and Right v for every value v of type Void -- however there are no values of type Void, so the only constructor for Either () Void is Left (). And 1 + 0 = 1, so we got what we expected.

Exercise: What should the mathematical interpretation of Maybe a be? How many values of Maybe Void are there -- does this fit with the interpretation?

Notes

  • I am ignoring partiality in this treatment, pretending Haskell is total. Technically undefined can have type Void, but we like to use fast and loose reasoning which ignores these.
  • The way void is used in C-based languages is actually much more like Haskell's () than Haskell's Void. In Haskell, a function returning Void can never return at all, whereas in C languages a function returning void can return, but the return value is uninteresting -- there's only one thing it could be so why bother?

Tags:

Haskell