DIP 1017--Add Bottom Type--Final Review

[Timon Gehr]

On 15.01.19 14:31, Johan Engelen wrote:
> On Tuesday, 15 January 2019 at 11:18:20 UTC, Simen Kjærås wrote:
>> On Tuesday, 15 January 2019 at 10:59:40 UTC, Johan Engelen wrote:
>>> 4 - D already has a bottom type: `void`, why is a new type needed?
>>
>> Because `void` is not a bottom type - a bottom type has no values, 
>> while void has exactly one, and is thus a unit type. Proof: you can 
>> return from a void function (hence it has at least one value), and no 
>> information is transmitted through a void (hence it has at most one 
>> value).
> 
> Although I am not a mathematician, this argumentation feels broken. The 
> argumentation of "a function returning bottom can never return" assumes 
> mathematical functions (which must return a value), but in D a 
> "function" is not necessarily a mathematical function. A function is a 
> procedure,

But procedures are not outside the reach of mathematics. A procedure is 
a mathematical function that takes a state together with some arguments 
and gives you back a modified state. Its type is State×Args→State.
The syntactic sugar that imperative languages put on top of this does 
not make this any less true, it is just a distraction.

A procedure that returns a value gives you both the modified state and a 
value. Its type is State×Args→State×Ret. If Ret has no values then 
State×Ret has no values.

You have the following natural isomorphisms:

State×Unit ≈ State
and State×Bottom ≈ Bottom

So if your D function returns Unit, it is essentially a procedure, and 
if it has return type Bottom, it automatically does not return a state 
either. I.e. it just does not return.

The entire thing is completely uniform, there are no weird special cases.

> and can return no value, described by "void". For example, 
> this is not allowed:
> ```
> void foo();
> void g() {
>    auto f = foo(); // not allowed, foo does not return any value
> }
> ```
> ...

But that's because the compiler explicitly checks for void. It's an 
unprincipled special case arising from the misunderstanding that void 
has no values.

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.

But of course you have a point. The only (and valid) reason to argue 
against the concept of a bottom type in D is that it tries to shoehorn a 
principled concept on top of the unprincipled and messy C legacy; as you 
said, you indeed lose compatibility, because C++ functions can both be 
annotated with [[noreturn]] and have a specified return type. Therefore, 
we might need both an attribute and a bottom type, such that the bottom 
return type automatically infers the attribute. You can also argue that 
putting only the attribute is "pragmatically" good enough, because it is 
needed anyway and "PL theory is useless" because you can just hack 
around non-uniformity with explicit special cases (like we have to do 
for void already).

> Interestingly, the proposal defines `a || b()` to be OK when `b()` 
> returns Tbottom, but does not change that it is not OK when `b()` 
> returns `void`...

I don't get why it would. What boolean value would you assign to a void b()?