The Wikipedia page on unit types is completely accurate with regards to what a unit type is, and a unit type is the correct model for the type that a void function returns in C. Sure, void can be interpreted in a few different ways, but void in function return or argument position definitely cannot be interpreted as the bottom type. As far as I know, C does not really have bottom as a first-class concept, however useful it might be. So while I agree with you that it would be theoretically possible for C's statement about void not having any inhabitants to coincide with the type theoretic defintion of void, in practice it does not (for all the reasons I mentioned earlier).

You will note that all the differences mentioned between void and unit in the Wikipedia article are syntactic, not semantic; this is because semantically there is no real distinction between them.

What is bizarre to me, though, is that you didn't read the Wikipedia article you just carelessly edited, which already mentions Common Lisp and explicitly tells you not to confuse the NULL type (which has single inhabitant NIL--i.e. you agree with me that it is the same as void, and they are both unit types) with the NIL type (bottom). Firstly, the existence of a subtyping relationship that lets you upcast values of type unit to values of type symbol (or indeed, any other type) does not somehow make it not a unit type (only subtyping in the other direction would accomplish such a thing), and certainly does not invalidate any of the article's claims as you assert. Secondly, no implementation detail of Common Lisp will affect the definition of a unit type, regardless of how many edits one makes to a Wikipedia page, any more than the C standard claiming void functions don't have a return type changes how they are modeled mathematically. Notions as fundamental as unit types are defined semantically and aren't really tied to specific language syntax.

Fun fact, in C++ void(); is a syntactically valid statement.

I think the best way to sum up the discussion is. void in c has no values. But the most straightforward way of modeling void mathematically is a type with one value.

A type with no values is not any less straightforward.

ISO C already provides a mathematical model, and one in which void is a type with no value.

Neither concept extends well to functions that return multiple values. The proper generalization which covers that case is that a function has an ordered list of return types. A function returning nothing has an empty such list: a zero-length list of return types.

Under this model, we don't require any unit type or bottom type or anything of the sort in connection with functions that don't return anything.

Note that this is similar to a parameter list: an empty return value list is similar to an empty parameter list, in which there are no parameters and hence no parameter types at all.

This model can be applied to single-value return languages like C, if we pretend that functions return multiple values, restricted to the zero or one plurality.

For what I hope is the last time, whatever the merits of a type with no values, that does not describe the semantics of void in argument and return position in C. ISO's definition is not relevant at all here, since they are using definitions specific to C rather than type-theoretic ones, and given that you haven't addressed any of the points I've made except to cite various standards bodies, I'm not really sure how else to explain this to you.

You are correct that it is possible to forego unit in exchange for defining vectors of length N as a fundamental type. This is the solution used by Rust, for example, in defining its tuple types, and in Rust indeed the empty tuple and unit are equivalent. Personally, I do not find this simpler than defining unit as a base type and pairing as a fundamental operation on types, since you are effectively just hiding the same cons/nil definition in the definition of natural numbers used for the list length. In any case, unit is not intended to automatically generalize to multiple types, and the rule for product types is a completely orthogonal feature that is useful by itself, so this seems like a bit of an aside. It also seems a bit pointless to introduce a general type like tuples of arbitrary length if you are going to restrict "arbitrary" to 0 or 1 (well, not pointless in some contexts, but in this one it seems strictly more complicated than just having a unit type, since any type you could use with a 1-tuple already has to exist in the first place).

I don't know why you assert that we don't need bottom under this model, however. A list of length zero is not the same as bottom, it is the same as unit (I believe you may have a fundamental misunderstanding about this?). To model bottom in an equivalent fashion, you would want a mechanism for defining sum types with N constructors--0 constructors represents bottom. And just like with the tuple case, this functionality is effectively equivalent to providing the bottom type plus a two-constructor sum type (although depending on the strength of your type theory, a more elaborate construction may be preferred, generally speaking you don't need to be able to define more than two constructors at a time).

Just to reiterate (and close the door on my end of this conversation): bottom and unit are not the same, and your proposed solution does not allow you to represent bottom. It allows you to represent void because void is not semantically bottom, it is semantically unit. I am extremely confident that whatever solution you come up with for representing void, whatever its individual merits, will either be interpretable as unit, or not reflect the actual semantics of C.

> void in argument and return position in C

void in the argument position in C is just a punctuation that was added by ANSI C to denote a prototyped empty parameter list. This is because () already had the meaning of "unspecified parameter list".

C++ fixed this issue from the beginning by banning the concept of an unspecified parameter lists and so initially it had no (void). In C++, () means "empty, fully declared parameter list". C++ added (void) for ANSI C compatibility.

Note that a parameter list like (void, void) or (void, int) and other possibilities is not allowed. It really is just a syntactic hack for that special case and not a parameter type declaration.

The (void) spelling could instead have used some other token. ANSI C could plausibly have chosen, say, the token sequence (!) to distinguish a prototyped empty parameter list from (). The shape is certainly available because (!) is a syntax error. Would ! then denote the unit type, even though it's not a type specifier?

> I don't know why you assert that we don't need bottom under this model, however.

That's nothing compared to the question of where I assert such a thing.

(Still, why would we need to represent a bottom type in describing a language that doesn't have it as a concept? It's handy for "internal use" in the model. Every type system should have a bottom type.)

> your proposed solution does not allow you to represent bottom

We can easily establish the existence of more than one empty type, and stipulate that they are all distinct and incompatible, even though their domain is the same empty set. So if we have used one such type U for a specific purpose which somehow makes it unsuitable as bottom, we can invent another type V very similar to it, and call that one bottom. We endow V (and only V) with the required property that it's the subtype of every type, including itself. Since U is not endowed that way, it's not the bottom type, but U does not hinder the existence of V in any way.

As long as we don't create a conflict in a system, giving rise to a contradiction, we are not prevented from adding anything.

I understand that if the role for U is to represent something like the C void, then it could be a unit type. A unit type will do everything we need in the model. Yet, it's not elegant; the unit type carries a useless value which has no manifestation in the system being modeled.