Bottom Type--Type Theory

[Olivier FAURE]

On Thursday, 17 January 2019 at 00:09:50 UTC, H. S. Teoh wrote:
> So you see, `void` is a rats' nest of special cases and ad hoc 
> monkey-patched semantics that's inconsistent with itself.  
> Sometimes it behaves like a unit type, sometimes it behaves 
> like a bottom type, and sometimes it behaves like a top type, 
> and none of these usages are consistent with each other, nor 
> are they truly consistent with themselves either.  It's like 
> working with a number system that has no concept of zero, 
> negative numbers, or infinity, and then patching in a new 
> number (let's call it X) that sometimes behaves like zero, 
> sometimes like a negative number, and sometimes like infinity.  
> Good luck doing calculations involving X.

Noob question, but wouldn't a top type also be a unit type?

I'm visualizing a top type as the type of an aggregate with zero 
member, which makes it a supertype of any other aggregate 
(whereas a bottom type would be the type of an aggregate with 
infinite members); wouldn't that type then have only one single 
value?