Stream: wg-traits

Topic: ambiguous answer replacement


Jack Huey (Jan 05 2020 at 21:11, on Zulip):

So, let's talk about https://github.com/rust-lang/chalk/issues/302

Jack Huey (Jan 05 2020 at 21:11, on Zulip):

Been thinking about this, and the "correct" way to solve it

Jack Huey (Jan 05 2020 at 21:14, on Zulip):

So, before, we set the existing subst to not ambiguous when we encounter a new non-ambiguous subst. But showed in the issue, this could have caused a panic (or maybe bad logic) because the way it was handled, we assumed elsewhere that that was a "new" answer

Jack Huey (Jan 05 2020 at 21:15, on Zulip):

But thinking about this, having an ambiguous answer for a table means that strands that depend on that table could also be ambiguous

Jack Huey (Jan 05 2020 at 21:16, on Zulip):

and if the original answer is no longer ambiguous, then those dependent strands don't need to be ambiguous either

Jack Huey (Jan 05 2020 at 21:17, on Zulip):

now, its obvious (since the new panic didn't cause any tests to fail), that this case isn't tested

Jack Huey (Jan 05 2020 at 21:17, on Zulip):

so it's mostly theoretical

Jack Huey (Jan 05 2020 at 21:18, on Zulip):

but I had an interesting idea, that I'm not sure if it can work

Jack Huey (Jan 05 2020 at 21:18, on Zulip):

but, what if instead of "ambiguous", we stored that ambiguity as a delayed subgoals?

Jack Huey (Jan 05 2020 at 21:20, on Zulip):

So, right now there are two cases where an strand can be ambiguous (without depending on an ambiguous strand): CannotProve and truncation

Jack Huey (Jan 05 2020 at 21:22, on Zulip):

there is one more that is slightly different, which is one when the root table flounders, the aggregator uses an ambiguous identity subst

Jack Huey (Jan 05 2020 at 21:24, on Zulip):

but that also matters for whether an answer is Unique or not

Jack Huey (Jan 05 2020 at 21:26, on Zulip):

(now that I'm thinking about it, I'm wondering if storing truncation as a delayed subgoal could also have fixed https://github.com/rust-lang/chalk/issues/280)

Jack Huey (Jan 05 2020 at 21:30, on Zulip):

it's also a bit interesting because the delayed subgoals are similar to the delayed literals

Jack Huey (Jan 05 2020 at 21:31, on Zulip):

and that got removed in favor of marking as ambiguous

Jack Huey (Jan 05 2020 at 21:31, on Zulip):

and this is somewhat thinking the opposite: all ambiguity is represented as a delayed subgoal

Jack Huey (Jan 06 2020 at 20:05, on Zulip):

@nikomatsakis any thoughts about this (don't know if you've put any thought into it)

nikomatsakis (Jan 06 2020 at 20:06, on Zulip):

one thought I had is that

nikomatsakis (Jan 06 2020 at 20:06, on Zulip):

when we were discussing coinduction

nikomatsakis (Jan 06 2020 at 20:06, on Zulip):

I was at some point advocating for including the idea of a "canceled" answer -- or something like that --

nikomatsakis (Jan 06 2020 at 20:06, on Zulip):

you wound up adding it, but only at the "top level"

nikomatsakis (Jan 06 2020 at 20:07, on Zulip):

but I think that "canceling" the existing answer and adding a new one seems .. maybe reasonable here

Jack Huey (Jan 06 2020 at 20:07, on Zulip):

So, I thought about that

Jack Huey (Jan 06 2020 at 20:07, on Zulip):

But I think ultimately that would be wrong

Jack Huey (Jan 06 2020 at 20:07, on Zulip):

Because there might have been other answers that "depended" on that answer

Jack Huey (Jan 06 2020 at 20:08, on Zulip):

(so, they were ambiguous when they could have not been)

nikomatsakis (Jan 06 2020 at 20:11, on Zulip):

I don't see the problem

nikomatsakis (Jan 06 2020 at 20:11, on Zulip):

if there was a thread that was pulling from the table

nikomatsakis (Jan 06 2020 at 20:11, on Zulip):

it will also see the new answer

nikomatsakis (Jan 06 2020 at 20:11, on Zulip):

and so the dependent answers will eventually be themselves canceled

nikomatsakis (Jan 06 2020 at 20:11, on Zulip):

(I could see a concern around efficiency, perhaps)

Jack Huey (Jan 06 2020 at 20:12, on Zulip):

ah, true

nikomatsakis (Jan 06 2020 at 20:12, on Zulip):

(that said, I wonder if I should review how some of the existing solvers I was copying from handled this situation)

nikomatsakis (Jan 06 2020 at 20:13, on Zulip):

the papers are a bit opaque but "mappable" :)

Jack Huey (Jan 06 2020 at 20:13, on Zulip):

hmm

nikomatsakis (Jan 06 2020 at 20:16, on Zulip):

(specifically the "Efficient Top-Down Computation of Queries Under the Well-formed Semantics (Chen, Swift, and Warren; Journal of Logic Programming '95)" paper)

Jack Huey (Jan 06 2020 at 20:16, on Zulip):

maybe I should take a look at it

nikomatsakis (Jan 06 2020 at 20:17, on Zulip):

it's a good paper but it took me many, many reads to understand it

nikomatsakis (Jan 06 2020 at 20:17, on Zulip):

it's written I think for a narrow set of folks, all of whom have implemented Prolog WAM engines :)

nikomatsakis (Jan 06 2020 at 20:17, on Zulip):

of course at this point you sort of have :)

Jack Huey (Jan 06 2020 at 20:18, on Zulip):

I suppose that's true

Jack Huey (Jan 06 2020 at 20:21, on Zulip):

I'll give your idea a try

Jack Huey (Jan 06 2020 at 21:44, on Zulip):

@nikomatsakis I've implemented this idea to test here: https://github.com/jackh726/chalk/compare/tests_refactor...jackh726:ambiguous_as_cannotprove

Jack Huey (Jan 06 2020 at 21:44, on Zulip):

in case you're interested

Jack Huey (Jan 06 2020 at 21:44, on Zulip):

still going to try to implement your idea before I PR anything

Jack Huey (Jan 07 2020 at 20:43, on Zulip):

@nikomatsakis you around

Jack Huey (Jan 07 2020 at 20:44, on Zulip):

Implemented your idea: https://github.com/jackh726/chalk/compare/tests_refactor...jackh726:invalid_answers

Jack Huey (Jan 07 2020 at 20:44, on Zulip):

Need to come up with a test that would fail if I didn't check an an answer is invalid, because none of the tests cover that case now

nikomatsakis (Jan 07 2020 at 22:39, on Zulip):

I'm around, but real busy today running from meeting to meeting

Jack Huey (Jan 08 2020 at 16:18, on Zulip):

@nikomatsakis How should I do this? Should I make two separate PRs to discuss? Just one? Do you want just look at the compare links above for now?

nikomatsakis (Jan 08 2020 at 19:39, on Zulip):

Mm the compare links are probably ok for now, sorry, I might not get to this until Friday though :(

Jack Huey (Jan 08 2020 at 20:07, on Zulip):

No problem

matklad (Jan 10 2020 at 11:00, on Zulip):

@Jack Huey if there's some experimental PR we can plug into rust-analyzer, I'll be glad to try it out! I think we know observe these panics pretty regularly :(

Florian Diebold (Jan 10 2020 at 11:43, on Zulip):

hmm... actually even if this gets fixed, we'll have to decide between the fix and support for impl Trait since that got removed without so far a replacement, AFAIK :oh_no:

Jack Huey (Jan 10 2020 at 19:01, on Zulip):

@matklad there's two different branches right now that both should fix this

Jack Huey (Jan 10 2020 at 19:01, on Zulip):

Just waiting for @nikomatsakis to take a look

Jack Huey (Jan 10 2020 at 19:02, on Zulip):

https://github.com/jackh726/chalk/tree/ambiguous_as_cannotprove

Jack Huey (Jan 10 2020 at 19:02, on Zulip):

https://github.com/jackh726/chalk/tree/invalid_answers

Jack Huey (Jan 10 2020 at 19:03, on Zulip):

I'm also currently working on a way to make it possible to yield before an answer is actually generated

Jack Huey (Jan 10 2020 at 19:03, on Zulip):

simplest would be to just yield based on time

Jack Huey (Jan 10 2020 at 19:04, on Zulip):

but, that would allow to use a larger max size without worrying about taking too long

Last update: Jan 21 2020 at 08:25UTC