Bottom Type--Type Theory

[H. S. Teoh]

On Thu, Jan 17, 2019 at 06:47:33PM +0000, Olivier FAURE via Digitalmars-d wrote:
> On Thursday, 17 January 2019 at 18:38:54 UTC, Olivier FAURE wrote:
> > For instance, I think it would make sense to call a function `int
> > foobar(void, void)` with as `foobar(1, "abd")`, which is basically
> > the function saying it will ignore these parameters.
> 
> To expand on this, I'm understanding supertyping (at least in D and
> similar languages) as the *discarding* of type information. Eg, A is
> the supertype of B if B has more specific information about what
> values it can hold than A, which means A can accept more different
> values.

Think of Top as the analogue of D's Object class.  Every class inherits
from Object.  Conversely, being handed an Object also gives you very
little information about the underlying concrete class.  Top would just
be Object as applied to *all* types in the language.


> In that mindset, void seems like the logical top type, because it
> describes no information at all about any value it could hold.

As I've said, `void` is an overloaded keyword that has different
meanings in different contexts.  In the case of `void*`, it certainly
behaves like a Top type -- void* can point to literally *anything*, but
it also tells you basically nothing about the type it's pointing to.

However, `void` as used in function return types means something else
altogether.  A void function is *not* the same as a function that
returns Object, to use the OO analogy.  A function that returns Object
(resp. returns Top) is returning an actual object with actual values --
it just so happens that the function doesn't specify anything more
specific about said value.  A `void` function, in the sense that it's
used in C/C++ and also D, is a function that does not return a
meaningful value.  In that sense, it's closer to a Unit type: the Unit
type can only ever hold a single value, and since this value cannot be
distinguished from any other value of the same type (there is only one
value of this type, so different values do not exist), it conveys zero
information and can basically be elided. I.e., the function can be said
to "return nothing" or "does not return a value (but it still does
return)".  This is not the same thing as "function returns a value, but
it doesn't tell you what you can do with this value".

The distinction is subtle, but important.  The problem is that we're so
used to `void` as it is used in C/C++/D, that we're essentially working
with a defective "arithmetic" where "1" and "infinity" are both regarded
as "not a number", and so we have trouble telling them apart, even
though their distinction is very important!

Furthermore, `void` as used in variable declarations behaves like a
Bottom type -- it's illegal to declare a variable of type Bottom because
Bottom by definition does not have *any* values -- yet the existence of
a variable implies that it holds a value of that type, which is a
contradiction.  Hence, a function declared to return Bottom is basically
a function that never returns, because if it did, you'd have a value of
type Bottom, which is impossible.  D does not allow you to declare a
variable of type `void`, but if indeed `void` were Top, then variables
of type `void` ought to be allowed, and would behave like
std.variant.Variant!  The fact that `void` variables are not allowed
implies that, in the context of variable declarations, `void` means
Bottom.

So you see, `void` means different things depending on the context it's
used in.  Sometimes it's Top, sometimes it's Unit, sometimes it's
Bottom.  Again, this is like the deficient arithmetic of the ancients:
"zero" was not a number, "infinity" was not a number, and the square
root of a negative number was also not a number, so all three get lumped
together as "not a number".  So you'd talk about X being "not a number"
or NaN, and sometimes NaN means your calculation yielded a 0, sometimes
NaN means your calculation yielded infinity, and sometimes NaN means
your calculation tried to take the square root of a negative number.
They are all lumped together under the label of NaN, but they are
actually very different things.  Confusing the different things for one
another would lead to contradictions and other (seemingly) unsolvable
problems.

Similarly, confusing the various different meanings of `void` just
because textually they are all written as v-o-i-d will eventually lead
to trouble and inconsistencies.

If we want to "fix" `void` in D, the first step would be to write these
different usages differently, so that they are clearly distinct from
each other. Stop calling them all "void"; call them by three distinct
names so that we don't confuse ourselves as to what we actually mean.
Then we can talk about completing the type system with top/bottom/unit
types.

//

And BTW, it makes me very scared that people seem to think I'm some kind
of expert on type theory, which I most certainly am not.  I know what I
know simply by googling on the subject and reading a few articles --
which anyone could do in a couple o' hours at the most. If *that* is
enough to make me an "expert" relative to the majority of the forumites
here, then I really have to wonder just how much hope we have of
resolving this issue in any sane way that doesn't introduce even more
problems.


T

-- 
Some days you win; most days you lose.