Bottom Type--Type Theory

[Johannes Loher]

Am 16.01.19 um 23:32 schrieb Walter Bright:> [...]
> 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.
> [...]
In a later post, H. S. Theo describes some of the problems with void in
more detail. What is your stance on actually fixing void from a type
theoretical perspective? Do you think that is practical?