Bottom Type--Type Theory

[Johannes Loher]

Am 18.01.19 um 00:05 schrieb H. S. Teoh:
> 
> 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.

What we can do is simply replace this by
```
func();
assert(0);
```

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

Structs with a bottom type member lowering to the bottom type member is
the natural thing to do. Structs are product types and the product of
any type with the bottom type is the bottom type.

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

As far as I am concerned, unions are sum types, you just have no option
to actually to find out which type they actually hold at runtime. While
this is a feature that is very useful and often implied when talking
about sum types (e.g. you can do it with std.variant.Algebraic), I donÄt
think it is stricly necessary.

This means that as you mentioned, any union type with a bottom type
member should "lower" to the union type without the bottom type member.
Actually trying to access it could either be a compile error or lower to
`assert(0)`. I am not completely sure what is preferrable, it probably
also depends on what would happen in other cases of usage of the bottom
type (compile error or assert(0);). It should be as consistent as possible.

There is a slightly weird situation with the default initialization of
unions. Usually, the first member of the union is initialized in that
case. however, in the case of
```
union A
{
    Tbottom i;
    long j;
}
```
this would mean that doing `auto A = A();` basically lowers to
`assert(0);` while for
```
union A
{
    long j;
    Tbottom i;
}
```
it would work fine and `j` would be initialized to `0`. This sounds
weird at first, but it is consistent with how unions of other types work:

```
import std.stdio;

union A
{
    float i;
    long j;
}

union B
{
    long j;
    float i;
}

void main()
{
    writeln(A().j); // 2145386496
    writeln(B().j); // 0
}
```