DIP 1017--Add Bottom Type--Final Review

[Timon Gehr]

On 17.01.19 03:32, Q. Schroll wrote:
> On Tuesday, 15 January 2019 at 16:23:57 UTC, Timon Gehr wrote:
>> [...]
>> It makes little sense to define a type "void" that has "no values" and 
>> then say "but as a special case, a function with return type void is a 
>> procedure instead", because you can just have a unit type. The whole 
>> "variables cannot be of type void"-nonsense is also nothing but annoying.
> 
> The void type is one of *three* type-theoretically different types:
> 1. For any variables (local, parameter, field, ...), it *is* the bottom 
> type: You cannot have values of it.

No, you cannot have _variables_ of this type. There is nothing like this 
in type theory. If you can't have a variable of a certain "type", it's 
not a type.

> 2. For function returns, it is a unit type. In D, we have another one: 
> typeof(null). In fact, we could deprecate void returning functions and 
> use typeof(null) instead.

No, that has different low-level semantics.

> 3. For pointer (i.e. void*) (and arrays (void[n]) and slices (void[])), 
> void is neither of the above. It's rather a top type (or any, or unknown 
> in TypeScript) which can hold any value. As it is with Object, you 
> cannot do anything (meaningful) with it without explicit downcast.
> ...

No, this is the "untyped block of memory" usage of 'void'. This does not 
have a parallel in type theory because _untyped_ and only useful if used 
in an unsafe manner.

> This is not new -- it's inherited from C. If we get a bottom type, void 
> in the sense of 2. can be defined as void = bottom*.

See 2.