Stream: wg-traits

Topic: alternate implied bounds lowering


nikomatsakis (Nov 07 2018 at 22:13, on Zulip):

So, @scalexm, I am curious to get your thoughts about this alternate idea for implied bounds lowering.

The idea is to introduce two things:

So for something like

trait Ord: Eq { }

you would produce

Implemented(T: Ord) :- Declared(T: Ord), Implemented(T: Eq).
Implemented(T: Eq) :- Implemented(T: Ord).

and then if you have impl Ord for Foo that would produce

Declared(Foo: Ord).

along with the proof obligation that Implemented(Foo: Ord).

Without a impl Eq for Foo impl, though, this proof obligation cannot be satisfied.

One nice property of this is that fn foo<T: Ord>() can simply convert T: Ord into Implemented(T: Ord) in all cases, we don't have this "sometimes convert to FromEnv, sometimes to Implemented" thing going on.

I've not tried to go through all the examples though -- maybe it falls apart somewhere?

I am particularly interested in coinduction. Presumably Implemented, like WellFormed, is coinductive (but Declared is not).

nikomatsakis (Nov 07 2018 at 22:15, on Zulip):

To expand on the fn foo<T: Ord> thing, if the "goal" for foo to be well-formed is G, the idea is that we would produce a proof-obligation like

forall<G> { Implemented(T: Ord) => G }
nikomatsakis (Nov 07 2018 at 22:15, on Zulip):

and similarly if someone were to reference foo::<X>, we would produce a proof obligation like Implemented(X: Ord)

nikomatsakis (Nov 07 2018 at 22:16, on Zulip):

One downside is that you are "re-proving" T: Eq each time you prove T: Ord (via the impl, anyway). However, we should be caching, so probably that's ok.

scalexm (Nov 07 2018 at 22:18, on Zulip):

mmh, I'll try to test this setting on my usual battery of tricky examples

scalexm (Nov 07 2018 at 22:18, on Zulip):

at first sight, it seems similar to our setting where we only had WellFormed and Implemented, and used WellFormed for both well-formedness checks and implied bounds

nikomatsakis (Nov 07 2018 at 22:19, on Zulip):

Indeed I think it is equivalent?

nikomatsakis (Nov 07 2018 at 22:19, on Zulip):

It seems to be the same basic idea, but shifting the proof obligation from the impl to the places that reference the impl

scalexm (Nov 07 2018 at 22:19, on Zulip):

we did not have the Implemented(...) in the same places so maybe not equivalent

nikomatsakis (Nov 07 2018 at 22:19, on Zulip):

(although you also prove it at the impl)

nikomatsakis (Nov 07 2018 at 22:19, on Zulip):

in our current scheme, we are basically saying that impl proves the transitive case once (WellFormed), and everybody else relies on that

scalexm (Nov 07 2018 at 22:20, on Zulip):

(I meant maybe not equivalent to the WF/Implemented-only setting)

nikomatsakis (Nov 07 2018 at 22:20, on Zulip):

oh ok I see, yes, yes

nikomatsakis (Nov 07 2018 at 22:20, on Zulip):

and I agree it felt very "familiar"

nikomatsakis (Nov 07 2018 at 22:20, on Zulip):

so that was part of why I wanted to run it by you

nikomatsakis (Nov 07 2018 at 22:20, on Zulip):

and see if we had rejected it already for some reason

nikomatsakis (Nov 07 2018 at 22:20, on Zulip):

or if it differed in some particular

scalexm (Nov 07 2018 at 22:21, on Zulip):

yes at first sight I can't tell :) I'll look into it tomorrow morning, I'm going to sleep now :p

Alexander Regueiro (Nov 07 2018 at 22:23, on Zulip):

@scalexm want to r+ if you're happy then? it will fail to go through in the case a test fails of course (which is unlikely given we've verified locally)

Alexander Regueiro (Nov 07 2018 at 22:28, on Zulip):

@scalexm thanks. and for the advice as well. good night :-)

scalexm (Nov 08 2018 at 11:26, on Zulip):

Ok @nikomatsakis some thoughts about this alternate encoding

scalexm (Nov 08 2018 at 11:27, on Zulip):
// `Implemented(T: Foo) :- Declared(T: Foo), Implemented(<T as Foo>::Item: Foo).`
// `Implemented(<T as Foo>::Item: Foo) :- Implemented(T: Foo).`
trait Foo where <Self as Foo>::Item: Foo {
    type Item;
}

// `Declared(i32: Foo).`
impl Foo for i32 {
    type Item = i32;

    // Prove `Implemented(i32: Foo)` --> ok if `Implemented` is co-inductive
}
scalexm (Nov 08 2018 at 11:27, on Zulip):

first, I think that because of this example, we need Implemented to be co-inductive, do you agree?

nikomatsakis (Nov 08 2018 at 16:01, on Zulip):

I agree

nikomatsakis (Nov 08 2018 at 16:01, on Zulip):

However, Declared would presumably not be (except for auto traits, perhaps)

scalexm (Nov 08 2018 at 16:05, on Zulip):

Yes but then I have an example that fails :p

scalexm (Nov 08 2018 at 16:05, on Zulip):

I’m on my phone right now, showing you in a few minutes

scalexm (Nov 08 2018 at 16:05, on Zulip):

I think this setup is basically equivalent to our first one WF/Implemented-only

scalexm (Nov 08 2018 at 16:06, on Zulip):

Either WF is inductive and you have to reject some useful impls, or it is unsound

scalexm (Nov 08 2018 at 16:46, on Zulip):

ok @nikomatsakis, what do you think of this example:

// `Implemented(T: Copy) :- Declared(T: Copy).`
trait Copy { }

// `Implemented(T: Partial) :- Declared(T: Partial), Implemented(T: Copy).`
// `Implemented(T: Copy) :- Implemented(T: Partial).` (*)
trait Partial where Self: Copy { }

// `Declared(T: Partial)`.
impl<T> Partial for T {
    // Prove `Implemented(T: Partial)`:
    //     true if `Declared(T: Partial)`, --> ok
    //             `Implemented(T: Copy)
    //
    // Prove `Implemented(T: Copy)`:
    //     true if `Implemented(T: Partial)` because of (*)
    //     --> co-inductive cycle
}
nikomatsakis (Nov 09 2018 at 16:22, on Zulip):

@scalexm hmm. So this is precisely the example I was thinking of. I'm trying to remember why I thought it would be ok. It may be that in relaying the idea I errored somewhere.

The plan was that trait Partial: Copy lowes to this:

Implemented(T: Partial) iff Declared(T: Partial), Implemented(T: Copy).

which of course means that

Implemented(T: Partial) :- Declared(T: Partial), Implemented(T: Copy).

but I have to think about the reverse rule... honestly my brain does not seem to be functioning right now. It seems though that from this iff we should be able to conclude that Implemented(T: Copy) => Implemented(T: Partial), as I wrote, right? I'll think about it when I'm a bit less worn out perhaps though (or look up the standard handling for iff :P)

scalexm (Nov 09 2018 at 16:24, on Zulip):

If this is an iff, there should definitely be two reverse rules
Declared(T: Partial) :- Implemented(T: Partial) and Implemented(T: Copy) :- Implemented(T: Partial)

scalexm (Nov 09 2018 at 16:25, on Zulip):

Which in that case is exactly our very first setting

nikomatsakis (Jan 22 2019 at 22:32, on Zulip):

Revisiting this, it's really a fascinating failure. =)

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

@nikomatsakis for me, the problem with this approach is that it is the same approach as our first one from summer 2017

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

And we concluded that, we could not soundly handle cyclic things

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

Basically, if Implemented in this setup is not co-inductive, you cannot handle decls like:

trait Foo where Self::Item: Foo {
    type Item;
}

impl Foo for () {
    type Item = ();
}
scalexm (Jan 23 2019 at 08:41, on Zulip):

So I don’t know

nikomatsakis (Jan 23 2019 at 14:35, on Zulip):

yeah I mean I agree it's wrong, @scalexm, I'm just trying to kind of dig a bit into why it's wrong. The core problem I think is that the co-inductive Implemented predicate is used as more than a "carrier"

nikomatsakis (Jan 23 2019 at 14:37, on Zulip):

and co-induction without some guarantee of "productivity" (I think this is the term, iirc) is problematic -- (basically, the existence of cycles without some "step" in between)

nikomatsakis (Jan 23 2019 at 14:37, on Zulip):

anyway, I'm going to try and sketch some sort of "diagram-like thing" for the implied bounds to see if I can capture my intuition for what it was aiming at

nikomatsakis (Jan 23 2019 at 14:37, on Zulip):

I have to revit that soundness failure from WF(Type) that you mentioned though

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

@nikomatsakis my own intuition for implied bounds is that they happen in two steps:

Of course in practice these two steps happen in parallel, where we « discover » the impls graph lazily while checking legality: this works because WellFormed(TraitRef) is co-inductive and hence can handle cycles

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

Then the difference between FromEnv and WellFormed is that WellFormed serves as a graph traversal; while FromEnv serves as finding a path in an oriented graph (going from one goal to prove to a possible clause in our environment)

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

So this is why the two are somehow unrelated, and also why WellFormed should not have any reverse rules: it is somehow incompatible with its « graph traversal » semantics

Last update: Nov 12 2019 at 15:30UTC