Bottom Type--Type Theory

[luckoverthere]

On Wednesday, 16 January 2019 at 22:32:33 UTC, Walter Bright 
wrote:
> 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. And 
> if one was doing type calculus on the return value of betty(), 
> it would show up as 'int' and botch everything up. It'd be like 
> substituting '5' in calculations that need a '0', but have no 
> notion of '0'.
>
> 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.
>
> 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.)

So you want to add something you don't fully understand and 
aren't sure if there is even any benefit at all. You just presume 
there to be a benefit? I don't think you should think of void and 
void* as the same thing. Pointers are their own type, if all you 
have is a void* and no other information, you might as well be 
pointing at nothing. I suggest you figure out what it is you 
actually want to implement, this is no better than cowboy 
programming. Hell might even be worse than a pilot wearing a 
blindfold with someone whispering in his ear that he is going the 
right direction. Don't implement something you obviously don't 
know enough about. I can only imagine what kind of disaster this 
is going to be in comparison to auto-encoding.