Stream: wg-traits

Topic: scalexm's trait object thoughts


Jake Goulding (Jan 07 2019 at 20:01, on Zulip):

I’ll spawn another topic to explain myself later because I’m on my phone now

Where have I heard that before...

scalexm (Jan 07 2019 at 22:17, on Zulip):

@nikomatsakis so about trait objects

scalexm (Jan 07 2019 at 22:17, on Zulip):

my main concern is whether we want to have implied bounds on dyn Trait or not

scalexm (Jan 07 2019 at 22:18, on Zulip):

e.g., if you have:

trait Foo<T: Clone> { }

// do I want `Implemented(T: Clone)` to be implied or do I need to state it explicitly?
fn foo<T>(x: &dyn Foo<T>) {
}
scalexm (Jan 07 2019 at 22:19, on Zulip):

I believe having full implied bounds on dyn Trait seems natural but may be a difficult problem :)

scalexm (Jan 07 2019 at 22:20, on Zulip):

(at least a problem for which a margin could not contain the solution, cc @Jake Goulding )

scalexm (Jan 07 2019 at 23:06, on Zulip):

@nikomatsakis well here is my proposal for full implied bounds on dyn Trait, I don't know if it is sound but I've not been able to break it yet (nor tried to actually prove it was sound)

scalexm (Jan 07 2019 at 23:06, on Zulip):

so the idea is that, when you have a trait object say dyn Foo<T>, the things we are afraid of are what we can deduce about T

scalexm (Jan 07 2019 at 23:08, on Zulip):

the things we can deduce about T are basically:

scalexm (Jan 07 2019 at 23:10, on Zulip):

any other bound not mentioning T (i.e. only mentioning Self) are harmless, because we cannot derive anything more about T from them

scalexm (Jan 07 2019 at 23:11, on Zulip):

so suppose a full trait declaration is given by:

trait Foo<T> where WC1, ..., WCn { }
scalexm (Jan 07 2019 at 23:13, on Zulip):

I propose we define a specially marked symbol SELF and a new co-inductive predicate Shallow(Type<...>: Foo<...>) defined as:

forall<...> {
    Shallow(Type<...>: Foo<...>) :- MaybeShallow(WC1), ..., MaybeShallow(WCn)
}

where MaybeShallow(WC) is syntactic sugar for:

So actually you can think of it as an infinite family of rules indexed by all the possible locations where SELF might appear

scalexm (Jan 07 2019 at 23:16, on Zulip):

then we define the following rules for the well-formedness of dyn Foo<T>:

WellFormed(dyn Foo<T>) :- Shallow(SELF: Foo<T>)

Eventually, if we manage to prove Shallow(SELF: Foo<T>), the only thing we will have left are region constraints on SELF: we'll substitute SELF with dyn Foo<T> and prove that the region constraints are syntactically correct

We now define the following implied bound:

FromEnv(dyn Foo<T>: Foo<T>) :- FromEnv(dyn Foo<T>)

and the impl:

// Note that this impl is WF thanks to the above implied bound,
// because `dyn Foo<T>` is an input type of our impl hence we have
// `FromEnv(dyn Foo<T>)` in our environment.
impl<T> Foo<T> for dyn Foo<T> { }

Note the asymmetry between the WF rule and the implied bound rule: in the former we only prove Shallow(SELF: Foo<T>) while in the latter we get the full set of bounds implied by dyn Foo<T>: Foo<T>

scalexm (Jan 07 2019 at 23:18, on Zulip):

let's run this proposal through some examples

scalexm (Jan 07 2019 at 23:20, on Zulip):
trait Animal<X> where Self: 'static { }
// `Shallow(SELF: Animal<?X>) :- Outlives(SELF: 'static)`

// `WellFormed(dyn Animal<&'a i32>) :- Outlives(SELF: 'static)`
// Provable, but we have `Outlives(SELF: 'static)` as a region constraint.
// If we substitute `SELF` with `dyn Animal<&'a i32>`, this is yntactically wrong:
// `&'a i32` does not outlive `'static`.
scalexm (Jan 07 2019 at 23:23, on Zulip):
trait Bar { }
// `Shallow(SELF: Bar).`

trait Foo<T>: Bar where T: Copy { }
// `Shallow(SELF: Foo<?T>) :- Shallow(SELF: Bar), Implemented(?T: Copy)`

// ```
// WellFormed(dyn Foo<String>) :-
//     Shallow(SELF :- Foo<String>) :- Shallow(SELF: Bar), Implemented(String: Copy)
//                                             :- Implemented(String: Copy)
// ```
// Wrong.
scalexm (Jan 07 2019 at 23:52, on Zulip):
trait Baz<X>: where Self: Copy { }
// `Shallow(SELF: Baz<?X>).` // `Shallow(SELF: Copy)` is always true
// But we also have e.g.:
// `Shallow(?T: Baz<SELF>) :- Implemented(?T: Copy)`.

trait FooBaz<T> where T: Baz<Self> { }
// `Shallow(SELF: FooBaz<?T>) :- Shallow(?T: Baz<SELF>)`.

// ```
// WellFormed(dyn FooBaz<String>) :- Shallow(SELF: FooBaz<String>
//    :- Shallow(String: Baz<SELF>)
//    :- Implemented(String: Copy).
// ```
// Wrong.
scalexm (Jan 07 2019 at 23:58, on Zulip):

Mmh ok so there is one thing that does not work 100% in this proposal, is that we can prove other bounds on dyn Foo<T> than just Implemented(dyn Foo<T>: Foo<T>) only if we have FromEnv(dyn Foo<T>) in our environment, because then we can use the implied bound rule

scalexm (Jan 07 2019 at 23:59, on Zulip):

this might be fixable, I'll think about it tomorrow

scalexm (Jan 08 2019 at 00:04, on Zulip):

well, the proposal overall looks complicated, and complicated things are often wrong (but also sometimes they are not, like the proof of Fermat's last theorem to continue on this metaphor lol)

scalexm (Jan 08 2019 at 00:04, on Zulip):

If we didn't allow any implied bounds on dyn Foo<T> other than super-trait bounds from trait Foo<T>, I might have a simpler proposal

scalexm (Jan 08 2019 at 08:08, on Zulip):

@nikomatsakis I don’t know how to go the other way, i.e. if you have trait Foo: Bar, how to show that dyn Foo: Bar so eventually I think my proposal won’t work

scalexm (Jan 08 2019 at 08:09, on Zulip):

But I think the general idea about the soundness issue is right: bounds involving Self outside of outlive requirements must be true, every other must be proven

scalexm (Jan 08 2019 at 08:47, on Zulip):

@nikomatsakis ok I know why the proposal was looking complicated, I was trying to account for bounds like:
trait Foo<T>: Bar<Self, T>
but traits with these bounds cannot be made into a trait object

scalexm (Jan 08 2019 at 08:48, on Zulip):

That becomes simpler then

scalexm (Jan 08 2019 at 08:51, on Zulip):

Let’s take again:

trait Foo<T> where WC1, ..., WCn {}

Define Shallow(?Self: Foo<?T>) :- MaybeShallow(WC1), ..., MaybeShallow(WCn) where again MaybeShallow(WC) is syntactic sugar for:

scalexm (Jan 08 2019 at 08:52, on Zulip):

(Shallow is inductive, I don’t think it needs to be co-inductive)

scalexm (Jan 08 2019 at 08:59, on Zulip):

Define: WF(dyn Foo<T>) :- Shallow(dyn Foo<T>: Foo<T>)

scalexm (Jan 08 2019 at 08:59, on Zulip):

FromEnv(dyn Foo<T>: Foo<T>) :- FromEnv(dyn Foo<T>)

scalexm (Jan 08 2019 at 09:04, on Zulip):

And finally for all super-trait bound SuperTrait<...> transitively derived from trait Foo<T>, you have a generated impl:
Implemented(dyn Foo<T>: SuperTrait<...>)

scalexm (Jan 08 2019 at 09:07, on Zulip):

(The set of all super-trait bounds is easily computed, but this must be done outside of the logic)

nikomatsakis (Jan 08 2019 at 20:00, on Zulip):

argh I did not get time to read this yet @scalexm, hopefully later today

scalexm (Jan 08 2019 at 20:01, on Zulip):

@nikomatsakis no problem, I'm currently writing a prototype in chalk, I'll try to open a WIP PR this evening so that you might want to read that instead of the long and confuse thoughts I wrote in this stream

scalexm (Jan 08 2019 at 22:16, on Zulip):

@nikomatsakis see https://github.com/rust-lang-nursery/chalk/pull/200 for a very sketchy proof of concept

nikomatsakis (Jan 09 2019 at 14:04, on Zulip):

Hmm, implied bounds do add an extra wrinkle @scalexm

nikomatsakis (Jan 09 2019 at 14:04, on Zulip):

one thing that may be relevant is that trait Foo<T> where T: Blah<Self> is not a dyn-safe trait (because of the Self in the where-clauses)

scalexm (Jan 09 2019 at 14:05, on Zulip):

Yes, that’s what I overlooked at the beginning

scalexm (Jan 09 2019 at 14:05, on Zulip):

Without those kind of bounds my proposal is simpler and works

nikomatsakis (Jan 09 2019 at 14:05, on Zulip):

oh I see

nikomatsakis (Jan 09 2019 at 14:05, on Zulip):

I didn't quite get to the end yet :)

nikomatsakis (Jan 09 2019 at 14:06, on Zulip):

you are referring to this variant, I guess — beginning at 3:51am

scalexm (Jan 09 2019 at 14:07, on Zulip):

Mmh could you quote said variant, the link does not work on my phone

nikomatsakis (Jan 09 2019 at 14:08, on Zulip):

it's a lot of messages so hard to quote

nikomatsakis (Jan 09 2019 at 14:08, on Zulip):

Let’s take again:

trait Foo<T> where WC1, ..., WCn {}

Define Shallow(?Self: Foo<?T>) :- MaybeShallow(WC1), ..., MaybeShallow(WCn) where again MaybeShallow(WC) is syntactic sugar for:
* Shallow(WC) for bounds of the form WC == Self: Trait
* WC for other bounds (including outlive requirements)

scalexm (Jan 09 2019 at 14:08, on Zulip):

Right :)

nikomatsakis (Jan 09 2019 at 14:08, on Zulip):

(Shallow is inductive, I don’t think it needs to be co-inductive)

nikomatsakis (Jan 09 2019 at 14:09, on Zulip):

etc

nikomatsakis (Jan 09 2019 at 14:10, on Zulip):

one other thing to keep in mind is that we want to support dyn (Foo+Bar)

scalexm (Jan 09 2019 at 14:10, on Zulip):

Yes, I think the proposal does support them (my chalk PR implements multi-trait objects actually)

nikomatsakis (Jan 09 2019 at 14:11, on Zulip):

I'll have to read the PR

scalexm (Jan 09 2019 at 14:11, on Zulip):

With the above notations you have WF(dyn Foo+Bar) :- Shallow(dyn (Foo+Bar): Foo), ObjectSafe(Foo), Shallow(dyn (Foo+Bar): Bar), ObjectSafe(Bar)

nikomatsakis (Jan 09 2019 at 14:30, on Zulip):

ok I skimmed the PR

nikomatsakis (Jan 09 2019 at 14:31, on Zulip):

I still have to wrap my head around the Shallow concept somehow

nikomatsakis (Jan 09 2019 at 14:32, on Zulip):

I guess the point is that Shallow gives you the (transitive) non-supertrait where clauses

scalexm (Jan 09 2019 at 15:10, on Zulip):

@nikomatsakis exactly, + the outlive requirements

scalexm (Jan 09 2019 at 15:10, on Zulip):

(Although they are not modeled in chalk)

scalexm (Jan 09 2019 at 15:10, on Zulip):

Shallow is probably not a good name btw

scalexm (Jan 09 2019 at 15:13, on Zulip):

But the idea behind Shallow is summarized by these two messages:

scalexm (Jan 09 2019 at 15:13, on Zulip):

« so the idea is that, when you have a trait object say dyn Foo<T>, the things we are afraid of are what we can deduce about T »

scalexm (Jan 09 2019 at 15:13, on Zulip):

« the things we can deduce about T are basically:

scalexm (Jan 09 2019 at 21:39, on Zulip):

@nikomatsakis I think we may not even need Shallow if we write the impl SuperTrait for dyn Trait cleverly (i.e. with the right where clauses)

scalexm (Jan 09 2019 at 21:39, on Zulip):

I'll try this week-end

Last update: Nov 12 2019 at 17:00UTC