bug#9222: 23.3.50; "void" is not "typeless" (but thanks for the koan!)

[Stefan Monnier]

>> It's still not typeless: it's just that the type you get gives you no
>> information about the data.
> Moreover, in C, in which types are not first-class objects, no type
> has a type, so every type is a typeless type.

Actually, you don't need types to be "first class objects" for them to
have a type.  From type theory's point of view, C types all have the
same type, which you could call "Type" or * or ω, i.e. the type
of types.  It's also often called a kind.

To be more precise, in C you could consider "struct" as a type-level
function which takes a descriptor and returns a type.  And "{ int a,b;
char c; }" would then be a structure-descriptor.  I.e.:

   struct has type "StructureDescriptor -> Type"
   { int a,b; char c; } has type "StructureDescriptor"

>From that point of view "struct" is a valid expression in the type
language, but it does not describe a set of values: only types who
have type "Type" describe values.

> I agree, BTW, that "unit type" is a better description of void than my
> original "empty type".

>From a theoretical point of view, yes, but most people are unfamiliar
with "unit type" and its name doesn't lend itself to a good intuitive
understanding of it.


        Stefan