Bottom Type--Type Theory

Johannes Loher johannesloher at fg4f.de
Thu Jan 17 20:48:52 UTC 2019


Am 17.01.19 um 21:04 schrieb H. S. Teoh:
> 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!

This is a great analogy, I need to keep that in mind!

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

I don't actually think declaring a variable of the Bottom type is
required to be illegal. It just needs to be impossible for it to ever be
initialized. This can trivially be done by only allwoing it to be
initialized by copying because whenever you have an expression of type
Bottom to which you "initialize" a variable of type Bottom, that
expression never returns and thus the initialization never actually
takes place. This would still allow things like
```
Bottom var = assert(0);
```
and also
```
void fun(Bottom b)
{
    // whatever, this function can never actually be called
}

void main()
{
    fun(assert(0));
}
```
Why would anyone want this? Simple, you do not have to include a special
case for the Bottom type in generic code.

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

I totally agree. It is basically the same for me. I do have a strong
mathematical background which might help, but all my knowledge about
type theory is basically from google, wikipedia and a few blog posts.


More information about the Digitalmars-d mailing list