Bottom Type--Type Theory

[H. S. Teoh]

On Fri, Jan 18, 2019 at 12:34:39AM +0100, Johannes Loher via Digitalmars-d wrote:
> 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);
> ```

Hmm you're right, in this case, we're not actually declaring b as a
separate step from calling func(); we're actually *initializing* b with
the return value of func(). Meaning that, in implementation, we're
calling func() then initializing b with the return value.  So that
initialization would fall under the same case as declaring `Bottom b;`,
defined to lower to `assert(0);`.


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

You're right, the product of anything with the bottom type is the bottom
type.  No special casing required here.


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

Makes sense.  But worthy of note, since it may not be immediately
obvious to those of us less well-versed with type theory. :-D  And
definitely this needs to be stated clearly in the DIP, otherwise it will
be overlooked and who knows what buggy behaviour would result.


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

Yeah I'm not sure what should happen either.  But I think lowering to
assert(0) makes sense.  It's how I'd implement a function declared to
return Bottom:

	Bottom func() {
		for(;;) {
			doStuff();
		}

		return Bottom.init; // equivalent to assert(0);
	}

In other words, in order for func to implement its declared return type
of Bottom, it ought to return an instance of Bottom, and the
construction of this impossible instance should abort the program. Which
would be consistent with current practice of unreachable code being
self-documented by inserting `assert(0);`.


> 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
> }
> ```

Ick.  This is one dark corner of D that I really dislike.  But it makes
sense, in its own way, given D's guarantee that .init must always exist
and be well-defined.  And the choice of initializing a union by its
first member's .init is as good as any other choice, since we have to
initialize it with *something*.  Just that when TBottom is involved, the
order of declaration suddenly can mean the difference between aborting
and initializing with an innocuous value.


Another case to consider: what should .typeid of Tbottom return?


T

-- 
Lottery: tax on the stupid. -- Slashdotter