3 ms·

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

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.

kazinator 6y ago
> 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.

kazinator 6y ago

> 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.