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

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.

• By "does not return anything" you actually mean "does not return anything of interest", whereas a function with output empty does not return at all (i.e. crashes or loops infinitely). – Turion Sep 7 '16 at 7:45
• As a return type, void is a unit type. – user253751 Sep 7 '16 at 9:10

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.

• One can return void in C++ and C89. stackoverflow.com/questions/35987493/… – BartekChom Sep 7 '16 at 7:06
• The 4th paragraph is formally wrong. In C, the amount of storage for void is undefined, not zero. This is not the reason why objects of type void are disallowed. The formal reason is that void is an incomplete type, and objects cannot have an incomplete type. – MSalters Sep 7 '16 at 8:38
• @MSalters No, what I wrote is formally correct. “Because” refers to the motivation for the language design, not to the logical inferences inside the language specification. The void type requires 0 bits of storage. This is the reason why the designers of C decided to make void an incomplete type, as opposed to defining it taking 0 bytes of storage (which would have a lot of impact on the language design) or 1 byte of storage (which would waste space). – Gilles 'SO- stop being evil' Sep 7 '16 at 9:01
• @Gilles: Sorry, but that doesn't make sense either. If allowed, the space used would be 1 byte per object of void type, and you obviously don't need many objects of void type. Not to mention that these objects could alias all other objects, so the actual usage would be zero anyway. – MSalters Sep 7 '16 at 9:10
• @CodesInChaos: Well, C++ actually allows empty structs, i.e. struct E { };. When used as a base class, this can be zero-sized. (There's really no such thing as C/C++, the two languages make their own choices and they can differ in these areas. C obviously doesn't have empty base classes, as it doesn't have OO in the first place) – MSalters Sep 7 '16 at 13:41

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.

• Interesting; if the definition of ⊥ is the function whose return type is ⊥ can never terminate, then C has such a type. We call it volatile void. – Joshua Sep 7 '16 at 18:23
• Interesting, I didn't know that. I doesn't seem to be actually standard-conformant, though. – leftaroundabout Sep 7 '16 at 19:30