Bottom Type--Type Theory

[Nicholas Wilson]

On Wednesday, 16 January 2019 at 22:32:33 UTC, Walter Bright 
wrote:
> The thing is, I know little about formal type theory. As far as 
> I can tell, nobody in this community does either, aside from 
> Timon Gehr.

I shows, the rationale for this DIP as it stands is wafer thin.
You should try to recruit Timon as a co-author and send the whole 
thing back to draft.
There is zero reason this for the DIP to have got this far 
through the process.

> Back to the bottom type. C's ability to manipulate types is so 
> primitive nobody misses type calculus. But D can do type 
> calculus, and I worry that the lack of a bottom type, far from 
> creating corner cases, causes corner cases and awkward problems 
> analogous to what the lack of an identity function causes.

Please point me to the section of the DIP where it says this, 
'cause I'm not seeing it.
This is an interesting potential  but needs to be discussed in 
the draft phase.

> The trouble is, I don't know enough about type theory to know 
> if this is the case or not. I only know analogies to problems 
> other systems have when the boundary cases are not expressible.

You need examples to give the DIP any credibility, as it stands 
the DIP makes two arguments : documentation and optimisation. 
Both of these exist already for LDC and GDC as attributes and it 
takes all of _6 lines+ to unify them and make the documentation 
aspect available to DMD.

> An example of an awkward corner case caused by lack of a bottom 
> type:
>
>    @noreturn int betty();
>
> How can it return an int yet not return? It makes no sense.

Yes that is stupid. Does anyone write it now, given that it is 
already possible with LDC/GDC? No, because D is a pragmatic 
language, just because you can write something non-sensical 
doesn't mean that anyone will, especially when you have to go out 
of your way to do it.
_We shouldn't be designing around the fact that you can do stupid 
things_.

>And
> if one was doing type calculus on the return value of betty(), 
> it would show up as 'int' and botch everything up.

First of all, the return type would canonically be void, not int 
(if you've gone out of your way to do something stupid  its your 
fault).
Second, I suspect the frequency of functions that always never 
return are a minute fraction of the total functions of a program, 
who is .
Third even if bottom coverts to everything else functions of 
bottom won't, so, from what I can see that breaks a lot of its 
supposed advantages anyway.
Finally, the addition of bottom its going to botch up a whole lot 
of existing code that isn't expecting it/doesn't care about it.

> The trouble with 'void' as a bottom type is it is only half 
> done. For example, 'void' functions are procedures, and 
> certainly do return. A void* is certainly a pointer to 
> something, not nothing. 'void' is the one with awkward corner 
> cases, it's just we're so used to them we don't see them, like 
> few C++ people recognized the identity function problem.

Links please?

> My trouble explaining the immediate value of a bottom type 
> stems from my poor knowledge of type theory. Other languages 
> aren't necessarily good role models here, as few language 
> designers seem to know much about type calculus, either. I was 
> hoping that someone who does understand it would help out!
>
> (I.e. it's not just about functions that don't return. That's 
> just an obvious benefit.)

That DIP doesn't make that point at all! If you don't know what 
you're talking about, you should find out _before_ you waste 
everyones time reviewing it!

This whole DIP needs to be sent back to draft. You need to come 
up with convincing ideas as to why a type is _practically_ more 
useful than an attribute that takes into account the fact that 
the claimed benefits already exist and that the implementation, 
learning curve and other external costs don't outweigh doing it.