Bottom Type--Type Theory

[Jonathan Marler]

On Thursday, 17 January 2019 at 18:11:10 UTC, H. S. Teoh wrote:
> On Thu, Jan 17, 2019 at 02:39:18AM -0800, H. S. Teoh via 
> Digitalmars-d wrote:
>> [...]
>
> Further thoughts on empty enums in D: according to the spec, an 
> enum always has an underlying base type, the default of which 
> is int.  So an empty enum as declared above, if we were to 
> hypothetically allow it, would be a subtype of int (a bottom 
> int subtype).  Which also means we can declare:
>
> 	enum BottomStr : string { }
>
> which, AFAIK, would be treated as something distinct from the 
> bottom int type.  So it would represent a different bottom type.
>
> You'd need a "true" bottom type to get the direct equivalent of 
> the Bottom of type theory.
>
> Of course, we could stipulate that all empty enums are 
> interpreted as Tbottom, which would clear up this mess -- but 
> this is yet another area where the DIP in question failed to 
> address.
>
>
>> [...]
> [...]
>
> And furthermore, as somebody has already pointed out, Unit as 
> declared above would be distinct from empty structs of any 
> other name that you might declare.  So there'd be multiple 
> incompatible unit types. Which again is a mess, since two 
> functions that don't return values ("procedures") could 
> ostensibly return distinct unit types (let's say one returns 
> void and the other returns Unit, or one returns Unit and the 
> other returns another empty struct of a different name), and 
> you'd have a messy incompatibility situation.
>
>
> T

The compiler could "decay" these various "unit types" to the same 
type (with different names).

struct EmptyStruct { }
enum EmptyEnum { }

static assert( is (EmptyStruct == TUnit) );
static assert( is (EmptyEnum == TUnit) );

At that point they just become different ways of writing the same 
thing, but should keep the type theory sound.