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

Problem Detail: 

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.

Asked By : Meta

Answered By : Gilles

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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/63203