Stream: wg-traits

Topic: design meeting 2019.11.11


nikomatsakis (Nov 11 2019 at 18:42, on Zulip):

Hey @WG-traits -- so for today's design meeting I was thinking we could talk over the work that @Jack Huey has been doing around handling co-induction in the chalk engine (it's currently unsound; rustc used to be unsound in the same way but we fixed it, albeit in a rather inefficient fashion). We've got a kind of writeup here summarizing some of the problems and a proposed solution.

nikomatsakis (Nov 11 2019 at 18:42, on Zulip):

Anyway that starts in ~20 minutes

nikomatsakis (Nov 11 2019 at 19:01, on Zulip):

:wave: @WG-traits -- design meeting start?

nikomatsakis (Nov 11 2019 at 19:02, on Zulip):

So yeah as I wrote above I thought we'd focus for today on this coinduction problem

nikomatsakis (Nov 11 2019 at 19:02, on Zulip):

But maybe it's worth giving a bit of context :)

nikomatsakis (Nov 11 2019 at 19:02, on Zulip):

Not sure who's around today

nikomatsakis (Nov 11 2019 at 19:03, on Zulip):

So let me ask this -- while I run to get a glass of water -- please :wave: if you feel you want me to cover what the heck coinduction has to do with trait solving and/or auto traits

Jack Huey (Nov 11 2019 at 19:04, on Zulip):

I think I mostly understand it at this point?

Jack Huey (Nov 11 2019 at 19:04, on Zulip):

(not sure if anyone else is around)

nikomatsakis (Nov 11 2019 at 19:04, on Zulip):

I see a few waves above :)

nikomatsakis (Nov 11 2019 at 19:06, on Zulip):

OK, well, the TL;DR is that coinductive solving is "trait solving where cycles are ok", and we use it for auto traits :)

nikomatsakis (Nov 11 2019 at 19:06, on Zulip):

but at some point I realized that the existing chalk solver has a bug here

nikomatsakis (Nov 11 2019 at 19:06, on Zulip):

actually the bug cropped up first in rustc, which had the same bug

nikomatsakis (Nov 11 2019 at 19:06, on Zulip):

this is chalk#248

nikomatsakis (Nov 11 2019 at 19:06, on Zulip):

the example being

C1 :- C2, C3.
C2 :- C1.
nikomatsakis (Nov 11 2019 at 19:07, on Zulip):

you can think of C1 as "co-inductive" goal, like maybe Foo: Send

nikomatsakis (Nov 11 2019 at 19:07, on Zulip):

or maybe better, just think of it as short for Implemented(C1: Send)

nikomatsakis (Nov 11 2019 at 19:08, on Zulip):

anyway, the problem here is that C1 and C2 should not be provable, as there is no rule to prove C3

nikomatsakis (Nov 11 2019 at 19:08, on Zulip):

unfortunately, if you execute things in the wrong order, our existing solver would conclude that C2 is true

nikomatsakis (Nov 11 2019 at 19:09, on Zulip):

the reason is because of caching, in short

nikomatsakis (Nov 11 2019 at 19:09, on Zulip):

basically we would start to prove C1...

nikomatsakis (Nov 11 2019 at 19:09, on Zulip):

...and then try to prove C2...

nikomatsakis (Nov 11 2019 at 19:09, on Zulip):

proving C2 recursively requires proving C1, but this is coinductive, so "cycles are ok", and hence we conclude that C2 holds (and we cache this)

nikomatsakis (Nov 11 2019 at 19:10, on Zulip):

...then we continue trying to prove C1 and we encounter C3 -- but C3 cannot be proven (no rules for that), so we conclude that C1 is not true

nikomatsakis (Nov 11 2019 at 19:10, on Zulip):

but we still have a cached result saying that C2 is true

nikomatsakis (Nov 11 2019 at 19:10, on Zulip):

our sol'n in rustc was basically just not to cache anything if a cycle occurs, but sometimes this can lead to us doing a lot of extra work

nikomatsakis (Nov 11 2019 at 19:10, on Zulip):

the underlying problem here is that it is a simplification to say that "cycles are ok"

nikomatsakis (Nov 11 2019 at 19:11, on Zulip):

coinduction is really about everything being "internally consistent", so to speak. "True until proven false" might be a good intuition :)

nikomatsakis (Nov 11 2019 at 19:12, on Zulip):

So here C2 was true, assuming C1 was true; but C1 wasn't.

nikomatsakis (Nov 11 2019 at 19:12, on Zulip):

(Make sense?)

nikomatsakis (Nov 11 2019 at 19:13, on Zulip):

OK, so I guess I'll outline briefly the fix that I had in mind, but I'm curious to hear @Jack Huey's latest thoughts as well

nikomatsakis (Nov 11 2019 at 19:15, on Zulip):

trying to decide where to begin in the explanation :)

nikomatsakis (Nov 11 2019 at 19:15, on Zulip):

I'll real fast loop back

nikomatsakis (Nov 11 2019 at 19:15, on Zulip):

the solver has this notion of "tables" -- basically, when you're trying to prove some goal like C1, it creates a table for that goal, and within each goal it has a number of strands --

nikomatsakis (Nov 11 2019 at 19:15, on Zulip):

each strand is like "some viable way prove that goal"

nikomatsakis (Nov 11 2019 at 19:16, on Zulip):

the strand has two bits of state, a substitution (values for any inference variables in the goal) and a set of subgoals (things left to prove)

nikomatsakis (Nov 11 2019 at 19:16, on Zulip):

so when we start to prove C1, we would make a table for that goal, and then look for any rules we can use to prove it

nikomatsakis (Nov 11 2019 at 19:16, on Zulip):

in this case, there is just one, C1 :- C2, C3

nikomatsakis (Nov 11 2019 at 19:16, on Zulip):

so we would create a strand with an empty substitution (no inference variables in this simple example) and two subgoals ([C2, C3])

nikomatsakis (Nov 11 2019 at 19:16, on Zulip):

this is called an ExClause in the code

nikomatsakis (Nov 11 2019 at 19:17, on Zulip):

that comes from some papers I was reading, which called it an X-clause

nikomatsakis (Nov 11 2019 at 19:17, on Zulip):

anyway, the idea here is to extend that list of subgoals with a list of delayed subgoals -- basically, things we had to assume were true due to a coinductive cycle, but they are not fully proven yet

nikomatsakis (Nov 11 2019 at 19:18, on Zulip):

(maybe delayed isn't the best name, I'm somewhat adopting terminology the papers were using for handling other things, but the concept seems very similar to me)

nikomatsakis (Nov 11 2019 at 19:18, on Zulip):

so in particular when we go to solve C2, and we encounter the subgoal of proving C1, we would find there is a cycle;

Jack Huey (Nov 11 2019 at 19:18, on Zulip):

I think delayed works. Or coinductive

nikomatsakis (Nov 11 2019 at 19:18, on Zulip):

but instead of just considering it true

nikomatsakis (Nov 11 2019 at 19:18, on Zulip):

we would make it delayed

nikomatsakis (Nov 11 2019 at 19:19, on Zulip):

the notation I used in the hackmd for an ExClause is Goal :- DelayedSubgoals | Subgoals

nikomatsakis (Nov 11 2019 at 19:19, on Zulip):

which...is kind of arcane

nikomatsakis (Nov 11 2019 at 19:19, on Zulip):

but I guess I'll run with it

nikomatsakis (Nov 11 2019 at 19:19, on Zulip):

so if we had C2 :- | C1 (no delayed goals, just one subgoal)

nikomatsakis (Nov 11 2019 at 19:19, on Zulip):

we would convert it to C2 :- C1 | (now C1 is delayed)

nikomatsakis (Nov 11 2019 at 19:20, on Zulip):

maybe better to use a notation like { substitition: [], delayed: [C1], subgoals: [] } :)

nikomatsakis (Nov 11 2019 at 19:20, on Zulip):

well anyway the point is that this delay list can propagate into the answer

nikomatsakis (Nov 11 2019 at 19:20, on Zulip):

so where the thing we cache as the "answer" for C2 used to just be "true", it's now (effectively) "true if C1 is true"

nikomatsakis (Nov 11 2019 at 19:20, on Zulip):

note that this remains valid even if C1 turns out to be false

nikomatsakis (Nov 11 2019 at 19:21, on Zulip):

so where an "answer" used to be { substitution, region_constraints } (we can ignore region constraints here), it is now { substitution, delayed, region_constriants }

nikomatsakis (Nov 11 2019 at 19:22, on Zulip):

and when we incorporate an answer, we have to add those delayed goals to our own subgoal list

nikomatsakis (Nov 11 2019 at 19:22, on Zulip):

so the strand for C1 starts as

Jack Huey (Nov 11 2019 at 19:22, on Zulip):

Well, also an answer can be ambiguous too

nikomatsakis (Nov 11 2019 at 19:22, on Zulip):
nikomatsakis (Nov 11 2019 at 19:22, on Zulip):

(yeah, I'm ignoring things that aren't too relevant)

nikomatsakis (Nov 11 2019 at 19:23, on Zulip):
nikomatsakis (Nov 11 2019 at 19:23, on Zulip):
nikomatsakis (Nov 11 2019 at 19:23, on Zulip):
nikomatsakis (Nov 11 2019 at 19:23, on Zulip):

and so it just gets an error

nikomatsakis (Nov 11 2019 at 19:23, on Zulip):

but then later if we try to use the answer from C2 in some other context, it too will fail to prove C1

nikomatsakis (Nov 11 2019 at 19:23, on Zulip):

so everything works out ok

nikomatsakis (Nov 11 2019 at 19:23, on Zulip):

(at least that's the idea :)

nikomatsakis (Nov 11 2019 at 19:24, on Zulip):

(make sense so far?)

nikomatsakis (Nov 11 2019 at 19:26, on Zulip):

one thing worth mentioning: if C3 were provable, then the C1 strand would have gone to a state like { subgoals: [C1] }.

nikomatsakis (Nov 11 2019 at 19:27, on Zulip):

the key point is that here we a trivial coinductive cycle -- basically C1 is true if `C1 is true -- and that we can just ignore as clearly true

nikomatsakis (Nov 11 2019 at 19:27, on Zulip):

we don't have the caching concerns because C1 is exactly the thing we are now proving, so if we fail, no answer is produced, and if we succeed, then the answer is valid

nikomatsakis (Nov 11 2019 at 19:27, on Zulip):

anyway, ok, that's the high-level idea, but there are a few tricky bits --

nikomatsakis (Nov 11 2019 at 19:28, on Zulip):

I'll stop here for the moment, though. I want to leave room for questions, but also check in with @Jack Huey

nikomatsakis (Nov 11 2019 at 19:28, on Zulip):

I saw you mentioned that you had some of the impl work on this strategy

Jack Huey (Nov 11 2019 at 19:28, on Zulip):

I think everything makes sense so conceptually

Jack Huey (Nov 11 2019 at 19:28, on Zulip):

Yeah, I have the key idea implemented

Jack Huey (Nov 11 2019 at 19:29, on Zulip):

I'm not doing something correctly in terms of canonicalization I think

Jack Huey (Nov 11 2019 at 19:30, on Zulip):

Basically though, implementation wise it's pretty similar to how you imagined it

nikomatsakis (Nov 11 2019 at 19:30, on Zulip):

OK

Jack Huey (Nov 11 2019 at 19:30, on Zulip):

the delayed subgoals I have on Answer though, instead of CanonicalConstrainedSubst

nikomatsakis (Nov 11 2019 at 19:30, on Zulip):

Ok, yes. I think that's wrong :)

nikomatsakis (Nov 11 2019 at 19:31, on Zulip):

I'm not doing something correctly in terms of canonicalization I think

and probably related to this

nikomatsakis (Nov 11 2019 at 19:31, on Zulip):

in particular, I think the delayed subgoals and the substitution must be canonicalized together

Jack Huey (Nov 11 2019 at 19:31, on Zulip):

hmm

nikomatsakis (Nov 11 2019 at 19:31, on Zulip):

(because they share inference variables)

Jack Huey (Nov 11 2019 at 19:31, on Zulip):

that makes sense I think

Jack Huey (Nov 11 2019 at 19:32, on Zulip):

just means that now we will need to pass a Context type through a lot more

Jack Huey (Nov 11 2019 at 19:32, on Zulip):

Since a Literal is over C::GoalInEnvironment

nikomatsakis (Nov 11 2019 at 19:32, on Zulip):

if you imagine a rule like

C1(X, Y) :- C2(X, Y)
C2(X, Y) :- C1(Y, X)

then the result for C2 will be something like

{ substitution: [^0, ^1], delayed: C1(^1, ^0) }
Jack Huey (Nov 11 2019 at 19:33, on Zulip):

which also got me thinking: in what cases (if ever) would we have a delayed subgoal on a negative literal?

nikomatsakis (Nov 11 2019 at 19:33, on Zulip):

never, I think

nikomatsakis (Nov 11 2019 at 19:34, on Zulip):

since we only delay on fully coinductive cycles, and I don't think those should include negation

Jack Huey (Nov 11 2019 at 19:34, on Zulip):

It doesn't pop up in any current tests

Jack Huey (Nov 11 2019 at 19:34, on Zulip):

which is why I asked

nikomatsakis (Nov 11 2019 at 19:35, on Zulip):

so certainly when proving not { G }, we should never encounter a cycle on G, I think we already kind of assert this, right?

Jack Huey (Nov 11 2019 at 19:36, on Zulip):

Right, that would be a NegativeCycle

nikomatsakis (Nov 11 2019 at 19:36, on Zulip):

but it is plausible to have something like not { C2 } (to build on our example), where the answer would have delayed subgoals

nikomatsakis (Nov 11 2019 at 19:37, on Zulip):

but I think those should be "refinable" (i.e., as in our example, we could then go and prove C1)

nikomatsakis (Nov 11 2019 at 19:37, on Zulip):

the only reason that would fail is if there is a cycle that includes the negative edge

nikomatsakis (Nov 11 2019 at 19:37, on Zulip):

and I think we want to assert that this doesn't happen by construction

nikomatsakis (Nov 11 2019 at 19:38, on Zulip):

but I think those should be "refinable" (i.e., as in our example, we could then go and prove C1)

this comes back to that note I had about how ensure_root_answer can do refining, but it's really not "special" in this regard

nikomatsakis (Nov 11 2019 at 19:38, on Zulip):

but of course we're way in the weeds here, I doubt anyone else has any idea what I'm talking about

nikomatsakis (Nov 11 2019 at 19:38, on Zulip):

(though I'm not clear if anyone else is here today...)

nikomatsakis (Nov 11 2019 at 19:39, on Zulip):

(does that make any sense, @Jack Huey?)

Jack Huey (Nov 11 2019 at 19:39, on Zulip):

I think so

Jack Huey (Nov 11 2019 at 19:39, on Zulip):

I have to think about it a bit more

Jack Huey (Nov 11 2019 at 19:40, on Zulip):

Probably worth a test, either for panic or pass

nikomatsakis (Nov 11 2019 at 19:40, on Zulip):

I guess an example which we do NOT want would be

C1 :- not { C2 }
C2 :- C1
nikomatsakis (Nov 11 2019 at 19:41, on Zulip):

this would be a case where pursuing the not { C2 } literal would yield an answer with a delayed subgoal for something still on the stack

nikomatsakis (Nov 11 2019 at 19:42, on Zulip):

I'm pondering how can detect that :)

nikomatsakis (Nov 11 2019 at 19:42, on Zulip):

it might be that for now we can just assert that negative literals never have delayed subgoals

nikomatsakis (Nov 11 2019 at 19:42, on Zulip):

I guess I have to check where we use them

nikomatsakis (Nov 11 2019 at 19:42, on Zulip):

but I think they are never for coinductive goals

nikomatsakis (Nov 11 2019 at 19:44, on Zulip):

I'm pondering how can detect that :)

more specifically, what I would like is that ensure_answer can guarantee that answers it gives back only have delayed literals if those things are on the stack -- the idea being that (e.g.) the first time you invoke C2, from within the context of C1, you might get back C2 :- C1 |, but if you invoke it from some other context, we'd refine the answer

nikomatsakis (Nov 11 2019 at 19:45, on Zulip):

but I'm not sure the best way to detect that situation.. it feels like we should be able to use the stack minimums or something..?

Jack Huey (Nov 11 2019 at 19:45, on Zulip):

So I think I've seen a related problem? maybe

Jack Huey (Nov 11 2019 at 19:46, on Zulip):

But maybe not

nikomatsakis (Nov 11 2019 at 19:46, on Zulip):

(this negative thing seems relevant, but also kind of a "user error" situation, so I think for now it probably suffices to panic)

nikomatsakis (Nov 11 2019 at 19:46, on Zulip):

(that is, panic if we are pursuing a negative goal and we get back delayed literals)

nikomatsakis (Nov 11 2019 at 19:46, on Zulip):

(well, maybe:P)

nikomatsakis (Nov 11 2019 at 19:46, on Zulip):

So I think I've seen a related problem? maybe

what's that?

Jack Huey (Nov 11 2019 at 19:47, on Zulip):

So with your

C1 :- C2, C3.
C2 :- C1.

example

Jack Huey (Nov 11 2019 at 19:48, on Zulip):

When it gets to C1 :- | C3 (the delayed subgoal isn't incorporated since it's a trivial cycle)

nikomatsakis (Nov 11 2019 at 19:48, on Zulip):

(well, maybe:P)

ok no I think this is true, so long as not is not used with co-inductive goals. The reasoning is that the answer for any inductive goal cannot have delayed things in it. This is true because anything higher on the stack will not be considered a coinductive cycle and hence would just be handled as we typically handle cycles

Jack Huey (Nov 11 2019 at 19:48, on Zulip):

It's returning C1 :- C3

nikomatsakis (Nov 11 2019 at 19:48, on Zulip):

returning?

Jack Huey (Nov 11 2019 at 19:49, on Zulip):

So ensure_root_answer needs to check that

Jack Huey (Nov 11 2019 at 19:49, on Zulip):

from ensure_answer_recursively

nikomatsakis (Nov 11 2019 at 19:49, on Zulip):

no, it's not

nikomatsakis (Nov 11 2019 at 19:49, on Zulip):

that's not an answer, as it has pending subgoals still

nikomatsakis (Nov 11 2019 at 19:49, on Zulip):

it would rather try to prove C3 (and fail, because there are no rules that can be used to do so)

Jack Huey (Nov 11 2019 at 19:50, on Zulip):

err right, the "answer" that ensure_root_answer is on the table when ensure_answer_recursively returns back to ensure_root_answer is C1 :- C3 |

nikomatsakis (Nov 11 2019 at 19:51, on Zulip):

it will never get that answer in my example though

nikomatsakis (Nov 11 2019 at 19:51, on Zulip):

that would only occur if solving C3 resulted in a coinductive cycle

Jack Huey (Nov 11 2019 at 19:51, on Zulip):

Yeah, I'm not sure. I'll have to look again

nikomatsakis (Nov 11 2019 at 19:52, on Zulip):

if the example were

C3 :- C1.
C1 :- C2, C3.
C2 :- C1.

and we started by proving C3, that could happen

nikomatsakis (Nov 11 2019 at 19:52, on Zulip):

(that's maybe a good example to walk through, actually)

nikomatsakis (Nov 11 2019 at 19:52, on Zulip):

i.e., we would start by proving C3

nikomatsakis (Nov 11 2019 at 19:53, on Zulip):
nikomatsakis (Nov 11 2019 at 19:53, on Zulip):
nikomatsakis (Nov 11 2019 at 19:53, on Zulip):
nikomatsakis (Nov 11 2019 at 19:54, on Zulip):
nikomatsakis (Nov 11 2019 at 19:54, on Zulip):
nikomatsakis (Nov 11 2019 at 19:54, on Zulip):
nikomatsakis (Nov 11 2019 at 19:55, on Zulip):
nikomatsakis (Nov 11 2019 at 19:55, on Zulip):
nikomatsakis (Nov 11 2019 at 19:57, on Zulip):

anyway

Last update: Dec 12 2019 at 00:55UTC