Minimum dyn trait subtyping (single inheritance)

[bill_myers]

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

[drXor]

(lifetimes don’t count)

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).

[ExpHP]

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

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.

[drXor]

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.

[ExpHP]

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

[drXor]

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

[Centril]

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

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

// Crawls back into corner…

[drXor]

Please

Pronounced puh-leaze, right? =P

[RalfJung]

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

What about coercions?

No.

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

[drXor]

Please please no subtyping please.

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.

[scottmcm]

In a way, we’re already on the way to a spooky version of T:Trait => T <: impl Trait .

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

[drXor]

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.

[Centril]

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

What about coercions?

No.

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

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.

[withoutboats]

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.

[Gankro]

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.

[RalfJung]

I’m genuinely curious why you think this.

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

Coercions are not always great and give the inferencer more choices to pick from

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

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

That would resolve my reservations. 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.)

[stjepang]

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

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

[RalfJung]

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

Well, having no subtyping at all sure would make things simpler – but it would probably also be a serious ergonomic hit. As usual there is a trade-off between expressiveness and simplicity.

Whether I would use an entirely different approach to lifetimes… that’s not something I have thought about much, to be honest. Given how much work went into Rust, it’d sure not be easy to come up with something competitive.

[SlightlyOutOfPhase]

Sounds a lot like Object Pascal also (single inheritance for concrete classes, which can also optionally implement any number of abstract interfaces.)

[system]

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.