DIP 1017--Add Bottom Type--Final Review

[Paul Backus]

On Friday, 18 January 2019 at 01:31:47 UTC, H. S. Teoh wrote:
> I don't argue that it's not a unit type.  But that's not the 
> same thing as saying it's *the* unit type.  There may be 
> multiple, distinct unit types, because D types are not 
> structural types in the type theoretic sense; for example:
>
> 	struct A { int x; }
>
> is a distinct type from:
>
> 	struct B { int x; }
>
> in spite of being identical product types according to type 
> theory.

The official term for this is "nominal typing" [1]. In a 
nominally-typed language, it is perfectly normal for there to be 
many distinct types that are structurally identical. In fact, the 
entire *point* of a nominal type system is to allow the 
programmer to distinguish between types that are structurally 
identical. For example, without nominal typing, it would be 
impossible to write code like this:

struct XY { double x, y; }
struct Polar { double r, theta; }

Polar xyToPolar(XY src) {
     return PolarCoords(
         sqrt(src.x^^2 + src.y^^2),
         atan2(src.y, src.x)
     );
}

// In a structurally-typed language, this assertion would fail
assert(!__traits(compiles, xyToPolar(Polar(1, 3.14))));

The downside of a nominal type system is, as you've noticed, that 
one cannot speak of "the" unit type, or indeed "the" type with 
any particular structure.

However, even if there are many possible unit types in D, that 
does not mean we cannot single one out for special 
treatment--indeed, we *do* single one out, already. `void`, in 
its role as a function return type, is different from all other 
(structurally-equivalent) unit types in that it is the only one 
that can be returned implicitly:

struct Unit {}

void foo() { return; } // Implicitly, `return void();`
Unit bar() { return Unit(); } // Can't just write `return;` here

So, even though `void` is not "the" unit type in the sense of 
uniqueness, it is still "special" in a way that no other unit 
type in D is.

Another way to think of it is that, in a nominally-typed 
language, it is not enough for "the" unit type (if such a thing 
is to exist) to have a canonical structure. It must also have a 
canonical *name*.

[1] https://en.wikipedia.org/wiki/Nominal_type_system