Bottom Type--Type Theory

[H. S. Teoh]

On Thu, Jan 17, 2019 at 11:32:42PM +0100, Johannes Loher via Digitalmars-d wrote:
[...]
> [...] In particular, what does this mean:
> 
> ```
> Tbottom fun()
> {
>     Tbottom b = void;
>     return b;
> }
> ```
> ?
> 
> With regular types, void initialization is no problem from a type
> system perspective because the memory the variable uses always holds
> some data which can be interpreted as data of that type. This is not
> true for Tbottom because there can not be any data at all. So I think
> we would still need to make (at least explicit) void initialization an
> error.

Hmm that's a good question.  I was going to suggest that the very act of
declaring a variable of type Bottom should be defined to be equivalent
to writing `assert(0)`, but then it wouldn't have the correct semantics
when you write:

	Bottom b = func(); // func returns Bottom

since it would abort before calling func(), which is wrong.

So it looks like we'll have no choice but to special-case
void-initialization of Bottom to be illegal, much as I don't like
special cases.

It does lead to other corner cases like structs that contain Bottom
fields -- instantiating such a struct should abort at runtime, and void
initialization should be illegal -- so this special case is infectious
and may lead to increased compiler complexity. OTOH, maybe this
complexity can be nipped in the bud by stipulating that any aggregate
that contains Bottom reduces to Bottom, i.e., any struct or class that
contains a Bottom field will be defined to be Bottom itself (since it
would be impossible to create an instance of such a struct or class
without also creating an instance of Bottom).

A particularly interesting (in a nasty way) case is a union that
contains Bottom fields. How would you define its semantics?  Since
technically, if you only assign to its non-Bottom components, you aren't
actually creating an instance of Bottom.  But since the field is there,
you can access it anytime.  I'm tempted to say that such a union should
also reduce to Bottom -- since one could argue that the Bottom field
already exists in the union, even if it's uninitialized.  This could
fall under the auspices of the no-void-initialization rule.

But there might be a type-theoretic issue here, though: unions being
(approximately) a sum type, one would expect that it's legal to take a
sum of Bottom with other types: since Bottom is uninhabited, the sum of
Bottom with any other type should reduce to the other type (rather than
Bottom itself!).  Then again, D unions aren't really the same thing as a
sum type in type theory AFAICT, so this may not be saying very much.
But it's a tricky case that needs to be addressed before we start adding
Bottom to the language.


T

-- 
"I suspect the best way to deal with procrastination is to put off the procrastination itself until later. I've been meaning to try this, but haven't gotten around to it yet. " -- swr