Why is C's void type not analogous to the empty/bottom type?

Question

Wikipedia as well as other sources that I have found list C's void type as a unit type as opposed to an empty type. I find this confusing as it seems to me that void better fits the definition of an empty/bottom type.

• No values inhabit void, as far as I can tell.
• A function with a return type of void specifies that the function does not return anything and thus can only perform some side-effect.
• A pointer of type void* is a subtype of all other pointer types. Also, conversions to and from void* in C are implicit.

I am not sure if the last point has any merit as an argument for void being an empty type, as void* is more or less a special case with not much relation to void.

On the other hand, void itself is not a subtype of all other types, which as far as I can tell is a requirement for a type to be a bottom type.

Answer 1

In C, void is used for multiple unrelated things. Depending on what it's used for, its meaning may be a unit type, an empty type, or something else.

When void is used by itself (as opposed to void*, a pointer to void), it's a unit type, i.e. a type with a single value. Functions that return void are said to “return nothing”, but what this really means is that they don't return any information. They return $0$ bits of information, which means that they return a value of a type that contains $2^0 = 1$ distinct values, i.e. a unit type.

This is not an empty type: a function that returns an empty type cannot return a value, since there is no value of that type. A function whose return type is empty can only loop forever, or abort the program, or raise an exception (longjmp) (or otherwise arrange not to return, e.g. by transferring control to another thread or process using functionality beyond standard C). To keep things confusing, it is conventional in C to use void in lieu of an empty type (C doesn't have an empty type).

The void type requires $0$ bits of storage. Because C insists on every object occupying a whole, nonzero number of bytes of storage, it's forbidden to create an object of type void, and there's a special syntax to return the void value (a return statement with the value omitted). There's no syntax that yields the value of type void, but that value is there whenever a function whose return type is void returns.

C does not have a bottom type in the sense of allowing any possible type. Even incomplete types specify the general nature of its values, e.g. pointers or structs or unions or functions. But void* is a pointer to any non-function type: it's the least element of the algebra of object pointer types, i.e. it's the bottom object pointer type. Unlike the general case of T* where T is some non-void type, void* is not the type of pointers to a value of type void, but the type of pointers to a value of unspecified type.

Answer 2

The name “empty type” is perhaps confusing. What this means is, as you say yourself, the type contains no values. The “empty” refers not to any individual values of the type, it refers to the type as a whole, considered as a ~set of possible values. So this does not say something like “a function returning void returns no information”, but “there exists no value of type ⊥”.

This means a function whose result type is ⊥ can never terminate. If it did terminate, if would have to return a value of ⊥, but, well, such a value doesn't exist.

It also means, it's not even possible to discuss how much information a value of empty type would contain, because there is no such value. (Or if you will, a nonsensical statement like “any value of empty type contains exactly 35093658 bits of information” is vacuously true.) It's somewhat useful (though not really correct) to think of ⊥ values as containing an infinite amount of information.

Whereas a C function with “return type” void clearly can return, but doesn't give you any information in its return value. Well, that's precisely what characterises a unit type: its values don't contain any information, because there is only one such value (hence you can always say what the return value will be, even without bothering to ever call the function).

To quote Conor McBride (transliterated to C):

void means "Boring". It means the boring type which contains one thing, also boring. There is nothing interesting to be gained by comparing one element of the boring type with another, because there is nothing to learn about an element of the boring type by giving it any of your attention.

It is very different from the empty type [...]. The empty type is very exciting, because if somebody ever gives you a value belonging to it, you know that you are already dead and in Heaven and that anything you want is yours.