Bottom Type--Type Theory

[Johannes Loher]

Am 17.01.19 um 23:13 schrieb H. S. Teoh:
> Even better yet, this means we don't even need to make it an error to
> declare and initialize a variable of type Bottom: the initialization can
> just be defined to be `assert(0);`, i.e.:
> 
> 	Bottom b;
> 
> becomes equivalent to (in pseudo-code):
> 
> 	Bottom b = void;
> 	b = assert(0);
> 
> which simplifies to just:
> 
> 	assert(0);

I didn't actually think this far, but you are right! We'd still somehow
need to deal with void initialization though. 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.