DIP 1017--Add Bottom Type--Final Review

[Olivier FAURE]

On Thursday, 17 January 2019 at 23:34:17 UTC, H. S. Teoh wrote:
> At the very least, it would seem that the *name* of the type 
> plays an essential role in its identification.  I.e., it's 
> almost as if a struct declaration is actually defining a type 
> that, in addition to the types of its fields, contains also an 
> implicit string type identifying the name of the struct. Or 
> alternatively, we're dealing with a type system where types are 
> additionally decorated with string identifiers that distinguish 
> otherwise-identical types from each other.

I wonder if there's a body of research in type theory about 
"decorated members" structural type systems; eg, where the name 
of an aggregate isn't part of its type, but the name of its 
members is.

For instance, in the following example:

     struct Point {
         float x;
         float y;
     }

     struct CartesianCoors {
         float x;
         float y;
     }

     struct PolarCoors {
         float theta;
         float radius;
     }

Point would be equivalent to CartesianCoors, but different from 
PolarCoors

> (Or it could be that I've no idea what I'm talking about, and 
> this is the consequence of this community having very few 
> people who actually know type theory thoroughly enough to be 
> able to work out a sane solution to all of these issues. :-P)

Don't feel bad. Type theory communities aren't exactly great at 
designing sane solution usable by human beings either :P