Minimum dyn trait subtyping (single inheritance)


#22

How about a generalized explicit solution:

trait A {}
trait B : A {}
trait C {}
trait D {}

#[is(B), convert(C, A)]
trait T: D, B, C {}

“is” (which only supports one trait) creates dyn subtyping and would be implemented by making the vtable start with the specified trait’s vtable.

“convert” enables dyn casts and would be implemented by adding vtable slots that contain a pointer to the vtable to use when converting to the specified supertrait (if a trait is specified as both “is” and “convert”, the “convert” is ignored).

Advantages:

  • No new semver compatibility issue like @Gankro 's proposal
  • Supertrait order does not become meaningful like my “first trait” proposal
  • Rustc continues free to layout vtables in any way if you use “convert”
  • Can support multiple supertraits via “convert”
  • Can support supertraits that aren’t immediate parents via “convert”
  • Generalization of all other current proposals
  • Explicit

Disadvantages:

  • Explicit
  • Slightly more complex

#23

I don’t think you can completely dismiss lifetimes, because we can study the for<'a> &'static T <: &'a T relation. In particular, the following error suggests how to handle the code you’ve written down:

error[E0119]: conflicting implementations of trait `main::T` for type `&'static str`:
 --> src/main.rs:5:5
  |
4 |     impl T for &'static str {}
  |     ----------------------- first implementation here
5 |     impl<'a> T for &'a str {}
  |     ^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `&'static str`

In a similar way, we might imagine that proving dyn Base: T means we can’t directly implement T for dyn Derived.

The only language I know of with both classical inheritance and typeclasses is Scala, but the way typeclasses are implemented in Scala requires giving the instantiations names, and having multiple instantiations in scope for K: T will result in a compile-time error (specifically, an implicit resolution ambiguity error).


#24

But we already can write both of these impls.

The reason why those impls regarding lifetimes are forbidden is because the type system does not consider lifetimes to be part of the type for the purposes of type inference and checking.


#25

No, you can’t, because the concept of a coercible supertrait doesn’t exist yet. Going from

trait T: U, V { .. }
// to
trait T: #[super] U, V { .. }

is clearly a breaking change. What you suggest is only true if one day trait T: U suddenly causes dyn T <: dyn U.


#26

Okay. I thought you were talking about the main proposal.


#27

I think this back and forth is good evidence that the original proposal has a bit of a hole. =P


#28

Please… Scala does not have type classes… they have modular implicits (as does Agda & Idris).

// Crawls back into corner…


#29

Pronounced puh-leaze, right? =P


#30

Please please no subtyping please. Subtyping from lifetimes is already bad enough, can we please not have more?

In my view, coercions are much simpler than subtyping. Care to elaborate?


#31

I’m genuinely curious why you think this. In a way, we’re already on the way to a spooky version of T:Trait => T <: impl Trait.


#32

Really? I thought impl trait was just adding a unification variable, which is very different from subtyping.


#33

I thought about it for a while, and you’re right. I’m very used to thinking of impl Trait as an erasure, in the way that I used to use supertypes in other languages as erasure, without realizing that not all impl Traits, in different contexts, are created equal.


#34

I second^10 this.

Adding more subtyping, especially that which doesn’t arise from lifetimes, is a step which complicates the type system pervasively and doesn’t want to stay in its corner and the consequences might not even be clear until very later when you are very sorry. This makes the type system that much harder to reason about both for users and language designers.

Coercions are not always great and give the inferencer more choices to pick from so it might throw up its hands, and there’s always the “what about explicit?” aspect of it… but at least coercions are somewhat local to the place it happens.


#35

taked to @Gankro about this briefly privately. Very excited about this, but I think its important to be careful that we are forward compatible with multiple supertrait casting, which would like involve introducing an offset. I think that coercions are viable to support that eventually, but not subtyping.


#36

To be clear by “no coercions” I was responding to how in previous discussion coercions opened the door to do actual runtime adjustments which gave people room to demand this work for multiple-inheritance or T + U which is what sunk this entire feature from making progress.

I am 100% fine with landing the exact proposal but only as a coercion and not subtyping. (a restriction of the proposal)

I am not, however, interested in entertaining using coercions as a vehicle to request an expansion of the proposal.


#37

Subtyping is an extremely strong property: It lets you replace A by B below arbitrary [covariant] unknown type constructors. In formal analysis of programming languages, this is known to lead to thorny problems: It took a decade to get a formal model of Scala’s type system, and one of the involved researchers told me subtyping played a big role in this delay. Only very recently, someone found a formulation of subtyping for ML-style languages that actually seems to work well – and that’s after several decades of research into ML-style type systems.

When I worked on the RustBelt paper, subtyping for lifetimes was already hard enough to incorporate. I’d rather if we didn’t add more of it :smiley:

But so does subtyping: The inference goes from equalities to inequalities, making it a much less constrained problem.

That would resolve my reservations. :slight_smile: I mean “coercion” purely in the sense of “only applies top-level”, not in the sense of “does run-time work”. (E.g., &mut -> & is a coercion even though it does no run-time work.)


#38

Curious - if you could design lifetimes from scratch, would you still use subtyping or would lifetimes be modeled somehow differently?