Bottom Type--Type Theory

[Walter Bright]

On 1/16/2019 3:40 AM, Olivier FAURE wrote:
> What is your answer to the rebuttal, common in both this thread and the previous 
> thread, that a bottom type has no practical use justifying the complexity (and 
> probable corner cases) it would add to the type system?

That indeed is the correct question.

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.

There are notions in mathematics and programming that seem like nonsense, but 
exist as important boundary conditions:

* zero
* infinity
* black hole objects
* white hole objects
* identity functions
* top type (represents every value, like D's "Object" root type)
* bottom type (represents no value)

Civilization had arithmetic long before zero was discovered. Today, we can't 
imagine doing math without 0. Infinity came along later, and its usefulness can 
be seen as an indispensable foundation of calculus.

C++ muddled along for decades with an identity function being impossible to 
write. Although an identity function seems pointless, it went unrecognized for a 
long time that this was causing all sorts of problems with templates.

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.

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.

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.)