DIP 1017--Add Bottom Type--Final Review

[Olivier FAURE]

On Tuesday, 22 January 2019 at 16:09:39 UTC, Neia Neutuladh wrote:
> And these two types *do* convert to each other, but not in the 
> way you'd want:
>
>     struct A { bool destroyEarth; bool preserveHumanity; }
>     struct B { bool preserveHumanity; bool destroyEarth; }
>
> Passing the wrong type flips the fields around, because the 
> order of the fields is what matters, because that's part of the 
> structure. And that's why nobody actually suggests this.

See, this is exactly what I was talking about earlier.

I thought you were saying "structs as NamedTuples are not very 
useful", while you were saying "structs as pure Tuples are not 
very useful". I think people often forget the distinction between 
the two in type theory.

For the record, in an ideal C-style type system, I think both 
field order and names would be important, and nothing else. Eg:

     struct Tuple2Int { int; int; }
     struct Point2d { int x; int y; }
     struct Vec3Int { int x; int y; int z; }
     struct MyVec3 { int x; int y; int z; }
     struct MyCoord { int x; int z; int y; }

In my ideal type system:
- Tuple2Int is a supertype of Point2d is a supertype of Vec3Int
- Vec3Int and MyVec3 are interchangeable
- Tuple2Int is a supertype of MyCoord
- MyCoord is not a subtype or a supertype of Point2d or Vec3Int

That said, there should also be some idiomatic way to write

     MyCoord pt = ...;
     foobar(..., Vec3Int(pt), ...);

and have it Just Work.

> Because it makes field order significant. It means that these 
> two types are different:
>
>     struct A { int x; string y; }
>     struct B { string y; int x; }

I think that's a fair distinction to make.

Except for the most hardcore "virtualize every member" type 
system implementations, most languages will require a non-trivial 
amount of operations (as many as there are fields) to get an A 
from a B and vice-versa, whereas prefix casting is essentially 
free.

So it makes sense that getting A from B would require an explicit 
operation.