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 typeVoid
, 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'sVoid
. In Haskell, a function returningVoid
can never return at all, whereas inC
languages a function returningvoid
can return, but the return value is uninteresting -- there's only one thing it could be so why bother?