Stream: t-compiler/wg-polonius

Topic: Quantifier elimination for HRTBs


ecstatic-morse (May 05 2021 at 21:50, on Zulip):

Howdy @WG-polonius. I recently published a blog post describing a strategy for reducing higher-ranked trait bounds to unquantified region constraints. It's a response to "Polonius and the case of the hereditary harrop predicate", although that post is quite old and may not reflect the current thinking around HRTBs. Even if some or all of my ideas are already known to the Polonius team, the blog post may still be useful since I was able to find relevant prior art that I haven't seen discussed anywhere, specifically some results on precedence constraints in atomic Boolean algebras showing a limit on how powerful our region logic can be while remaining

I had these ideas back when I was making some trivial fixes to get up to speed with Polonius. I was hesitant to share them at the time because I was both unsure about their novelty and worried I had made a trivial mistake somewhere: I'm an amateur mathematician and a lousy one at that. I had planned to start with a more concrete proposal about using a variant of the SSA transformation to speed up computing borrow errors, but that idea turned out to have a fatal flaw. Partly because of that negative result and partly because of some health problems, I stopped working on Polonius in my free time. Now that I'm feeling better, however, it seemed wasteful not to publish my results despite the possibility of a minor embarrassment.

lqd (May 05 2021 at 21:53, on Zulip):

@ecstatic-morse hey Dylan <3

lqd (May 05 2021 at 21:55, on Zulip):

this looks lovely I'll read it carefully; hope everything's better health-wise

lqd (May 05 2021 at 21:56, on Zulip):

from the top of my head, your mentioning the variant of the SSA transformation, reminds me, IIRC, of arielb talking about Graph SSA for easier borrow checking :thinking:

lqd (May 05 2021 at 21:58, on Zulip):

(but maybe I'm conflating this with their Ref 2 Φ model)

lqd (May 05 2021 at 22:00, on Zulip):

it would be cool if @nikomatsakis had an update to that plan to share btw ? :pray: since chalk has made a lot of progress since then (and they may have some of those ideas fresh from the recent rust verification workshop)

ecstatic-morse (May 05 2021 at 22:03, on Zulip):

Yeah, I've seen an IRLO thread where they discussed SSA, although my idea's a bit different. I'm hoping to write it up and let others take a crack at fixing it.

lqd (May 05 2021 at 22:04, on Zulip):

the Revesz paper also looks very interesting, thanks a bunch for writing this up

lqd (May 05 2021 at 22:35, on Zulip):

(maybe the algorithm they had in mind isn't exactly the same as yours, but I agree that it does sound a lot like the discussions I remember from Niko & wg-traits, that chalk would handle the quantifiers from higher-ranked constraints and emit quantifier-free constraints for polonius to solve ; maybe it was also because this would be needed during trait-solving, rather than a concern solely about borrow checking ?)

lqd (May 06 2021 at 00:15, on Zulip):

(or maybe operational concerns on how to apply this within existing datalog engines ? hopefully they'll explain :)

lqd (May 06 2021 at 00:16, on Zulip):

what an enjoyable read

lqd (May 06 2021 at 00:16, on Zulip):

I believe that lower bounds on universal quantification are similarly eliminated in current NLLs, for<'a> 'b: 'a being eliminated as 'b: 'static. Interestingly, this substitution does show up sometimes in user code as an unexpected 'static bound surfaced in error messages and diagnostics, and surprises them of course.

lqd (May 06 2021 at 00:16, on Zulip):

I'm not exactly sure what Niko had in mind when they mentioned implication as a richer constraint we'll eventually need, but I believe that disjunction would be used for the now-existing member constraints that arise from impl Trait, and the async fn desugaring. As you mention, I'm not sure either whether quantifiers are allowed there (I'd be surprised), so maybe indeed we could allow disjunction only outside of quantifiers.

lqd (May 06 2021 at 00:21, on Zulip):

again, lovely post, thanks for writing it. I'm excited for more :)

ecstatic-morse (May 06 2021 at 21:05, on Zulip):

lqd said:

I believe that lower bounds on universal quantification are similarly eliminated in current NLLs, for<'a> 'b: 'a being eliminated as 'b: 'static. Interestingly, this substitution does show up sometimes in user code as an unexpected 'static bound surfaced in error messages and diagnostics, and surprises them of course.

Yeah, I suspect all of my rules are already used in the NLL implementation, though I wasn't able to find where. NLL also has sets with subset relations, they're just sets of program locations instead of loans, so the QE stuff still applies. At least now there's a long-winded justification for them somewhere :laughing:.

ecstatic-morse (May 06 2021 at 21:14, on Zulip):

lqd said:

I'm not exactly sure what Niko had in mind when they mentioned implication as a richer constraint we'll eventually need, but I believe that disjunction would be used for the now-existing member constraints that arise from impl Trait, and the async fn desugaring. As you mention, I'm not sure either whether quantifiers are allowed there (I'd be surprised), so maybe indeed we could allow disjunction only outside of quantifiers.

Thanks. That's good to know. AFAICT, the main problem is disjunction inside a universal quantifier. We don't have to deal with negation, so we can convert to disjunctive normal form using only the distributive law, and existential quantifiers distribute over disjunction. I don't know how to prove statements like forall<'x> { 'x : 'a || 'a : 'x }, however. It might not be an issue.

nikomatsakis (May 17 2021 at 13:40, on Zulip):

so @ecstatic-morse I read your post btw :)

nikomatsakis (May 17 2021 at 13:40, on Zulip):

I keep meaning to write here!

nikomatsakis (May 17 2021 at 13:40, on Zulip):

tl;dr yes I was aware of that, but it's too simplistic to really work

nikomatsakis (May 17 2021 at 13:40, on Zulip):

I have more thoughts that I've not gotten arond to writing up in blog post form

nikomatsakis (May 17 2021 at 13:40, on Zulip):

though I'm expecting to consult with some folks soon about this very topic!

nikomatsakis (May 17 2021 at 13:40, on Zulip):

who have deeper knowledge than me

Last update: Jun 20 2021 at 00:30UTC