Bottom Type--Type Theory

H. S. Teoh hsteoh at quickfur.ath.cx
Thu Jan 17 00:09:50 UTC 2019


On Wed, Jan 16, 2019 at 02:32:33PM -0800, Walter Bright via Digitalmars-d wrote:
[...]
> The trouble with 'void' as a bottom type is it is only half done. For
> example, 'void' functions are procedures, and certainly do return. A
> void* is certainly a pointer to something, not nothing. 'void' is the
> one with awkward corner cases, it's just we're so used to them we
> don't see them, like few C++ people recognized the identity function
> problem.
[...]

Actually, the *real* problem with `void` is that it has been overloaded
to mean multiple, context-dependent things that are somewhat but not
really the same, and aren't really compatible with each other.

1) When specified as a function return type, `void` signifies that the
function does not return a meaningful value. In this sense, one might
argue that it's a unit type (that requires no representation because it
always holds the same value).

2) When `void` is specified as the type of a variable, it is an error,
the justification being that you cannot have a variable that holds
nothing.  However, this is incompatible with being a unit type: if it
were *really* a unit type, we'd be allowed to declare as many variables
as we want of that type. They would take up zero storage space (because
there's no need to store a value that's the only value that can exist in
that type), and every variable of this type would vacuously equal every
other variable, because they can only hold the same value, so
comparisons with == will always be vacuously true. You'd be able to pass
it as a function parameter, though that'd be pretty useless since it
conveys no information, and hence no code actually needs to be generated
for it (there's no need to actually pass anything at the machine code
level).  None of this is permitted for `void`, thereby making `void` not
a unit type.  In fact, `void` in this usage seems closer to being a
bottom type -- a type that holds no value, and therefore it makes no
sense to instantiate a variable of that type.  So this isn't really
consistent with (1).

3) The pointer type derived from `void`, that is, `void*`, has an ad hoc
meaning that is not consistent with either (1) or (2): void* behaves
like a top pointer type, i.e., every pointer implicitly casts to it. But
that means that the `void` in `void*` does not mean the same thing as
the `void` in (1) or (2) above, because if (1) were true, then it makes
no sense to be able to construct a pointer to it. You cannot construct a
pointer to nothing!  The closest thing you could get to constructing a
pointer to nothing is null, however, typeof(null) != void* (even though
null is implicitly convertible to void* due to void* behaving like a
pointer to a top type).  Furthermore, if (2) were to hold, then `void*`
couldn't possibly point to any other type, because a pointer to a unit
type can only have one value (a "magic" pointer value that points to the
non-physical storage location of the only value of the unit type).  So
`void*` is inconsistent with (2).  What `void*` actually means is NOT a
pointer to `void`, but rather a pointer to a top type that can represent
any value.  However, even here, the language is not consistent: you
cannot dereference a void* without casting it into something else first.
If indeed it were a true top type, then dereferencing void* ought to
give us a value of the top type (i.e., any value that can be represented
in the language).  So (3) is not consistent with (1) and (2), and is
closer to being a pointer to a top type, but not really because you can
never dereference it.


So you see, `void` is a rats' nest of special cases and ad hoc
monkey-patched semantics that's inconsistent with itself.  Sometimes it
behaves like a unit type, sometimes it behaves like a bottom type, and
sometimes it behaves like a top type, and none of these usages are
consistent with each other, nor are they truly consistent with
themselves either.  It's like working with a number system that has no
concept of zero, negative numbers, or infinity, and then patching in a
new number (let's call it X) that sometimes behaves like zero, sometimes
like a negative number, and sometimes like infinity.  Good luck doing
calculations involving X.

The only reason our brains haven't exploded yet from these
inconsistencies is because we have become acclimatized to interpreting
`void` in different ways depending on the context.  But because of that,
trying to make sense of `void` as a consistent entity in itself is an
exercise in futility.

And now we're proposing to add a Tbottom type to try to fix the missing
corner cases in the type system... Just *how* is it going to interact
with the existing inconsistent meanings of `void`?  I just can't wait to
see the glorious chaos that will surely result. :-/


T

-- 
Genius may have its limitations, but stupidity is not thus handicapped. -- Elbert Hubbard


More information about the Digitalmars-d mailing list