Note I hope we agree that this issue is very important; thus the need to retain some skepticism until convinced we have correctly/completely understood and clairvoyantly articulated this issue in sufficient detail. We must be very careful that when we claim analogies between language features and typing models, that we haven't missed some crucial details. Handwaving can be counter productive, if it is perceived to be fact.
Afaics, the currently relevant unsafety problem that I have gleemed from the Intersection, Universally Quantified, and Reference Types white paper you cited, only applies in the case where mutable references are combined with intersection inheritance (e.g. trait NatPos : Nat, Pos
) wherein the intersected supertypes can have implementations which do not have disjoint semantics, e.g. Nat
and Pos
are not actually disjoint sets.
This unsafety arises because the compiler assumes all intersected nominal types (i.e. which are not super/subtypes) are disjoint (even when they are not). Thus the compiler will erroneously allow subsumption (assignment) of an instance of NatPos
to either Nat
and/or Pos
; and thus assignment (i.e. writing) of a 0
value to the instance referenced with a type Nat
(natural numbers). And this same instance is also read by a reference of type Pos
, which is thus an unsafe type error at runtime because 0
is not a valid value for the Pos
(positive integers) type's sematics.
Afaics, this unsafety exists in Rust now, but... the unsafety apparently also exists in any programming language that allows subsuming a subtype separately to each of its intersected supertypes, while also allowing read/write access to instances of those supertypes via references that allow mutable (i.e. write) access to the referenced instance.
Is there any disagreement about this claim, and if so, can anyone explain any error in my aforementioned conceptualization?
Thus I was apparently mistaken (due to being awake too long when I should have slept) when I implied this problem applies only to ad hoc polymorphism. This unsafety is due to the fact that subtyping is unable to check that the semantics of nominal types are disjoint (in the presence of mutable access via references), yet the type system implicitly assumes that all intersected nominal types are disjoint. Thus only linearized inheritance would absolve this unsafety (because super/subtypes aren't assumed to be disjoint) in the presence of mutable references (but tangentially, even that wouldn't absolve the anti-pattern of subclassing for other unrelated reasons). Thus so many popular programming languages are implicated, including C++, Java, etc. I am thinking the reason this problem has been ignored in the past, is because most of the implicated languages also provide the anti-pattern subclassing which also leads to virtual methods violations of the Liskov Substitution Principle, thus I am thinking the industry punted and decided it was not possible to check the invariants so allows the programmer to manually check for inconsistency of inheritance semantics. In that sense, the above linked research paper apparently offers the red-herring of an old unsafety problem that has been pervasively, de facto ignored.
Note also that subtyping subsumption with mutable access via reference (even without the intersected inheritance), is equivalent to virtual method access; thus the virtual method aspect of the subclassing anti-pattern "sneaks in through the back door" even if the programming language doesn't offer virtual method dispatch in classes.