haskell - What is the kind of Void?

Question

Seeing as the type of Void is uninhabited, can it be regarded as a type "constructor"? Or is this just a quick "hack" to be able to safely disregard / disable functionality and am I looking too deep into this?

question from:https://stackoverflow.com/questions/29953219/what-is-the-kind-of-void

Answer 1

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 b^a), () (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?