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

[Stefan Monnier <monnier@iro.umontreal.ca>]

> I was thinking more of functions that take void* as a parameter.  What's
> usually expressed by that is "here's some memory that we're not actually
> telling you what the type of is explicitly", so it's (sort of) a pointer
> to something typeless.  It's not a pointer to something of an empty
> type.  :-)

That still fits within the definition of "unit type" to me: basically
the unit type is the type of everything (the set that contains all
possible values), and for that reason the type gives no information
about the value and you can't do anything with a value of that type
because you don't even know if it's an int or a struct so you can't even
begin to choose which kinds of operations might be applicable.

Again, in type theory, the void (aka empty) type is encoded typically as
"forall t . t" which means something like "this object has type t, no
matter what that t is" (kind of like the intersection of all types)
whereas the unit type is encoded as "exist t . t" which can be read as
"all I can say is that this object does have a type" (kind of
like the union of all types).

> So calling "void" a "typeless type" makes some sense.  At least to me --
> in a C context.

It's still not typeless: it's just that the type you get gives you no
information about the data.


        Stefan