Stream: wg-traits

Topic: simplify chalk context trait and logic-engine #255


Jack Huey (Oct 21 2019 at 21:42, on Zulip):

@nikomatsakis Here's a topic for the issue, in case there end up being multiple related PRs

Jack Huey (Oct 21 2019 at 21:44, on Zulip):

I haven't started too much down the rabbit hole of your suggestion, but the only hiccup I see happening is that program_clauses calls self.infer.var_is_bound

Jack Huey (Oct 21 2019 at 21:46, on Zulip):

But the only place it's called (push_initial_strands_instantiated), we have an infer, so I think it'll be fine

nikomatsakis (Oct 21 2019 at 21:48, on Zulip):

@Jack Huey I suppose we can pass the infer into that fn -- that's what you mean, right?

Jack Huey (Oct 21 2019 at 21:49, on Zulip):

Yep exactly

Jack Huey (Oct 21 2019 at 22:12, on Zulip):

Ok so I was able to move program_clauses to ContextOps. Did end up needing to make InferenceTable an associated type on Context, but I think it actually mirrors the other associated types well. Now I need to actually move infer back onto Strand

Jack Huey (Oct 22 2019 at 17:50, on Zulip):

@nikomatsakis So I was able to move infer back to strand and remove CanonicalStrand, but a lot of tests are failing, so I didn't correctly account for canonicalization. But I looked again at rustc's use of Chalk, and it's InferenceTable has a lifetime, so I don't know if we can store InferenceTable in Strand anyways.

nikomatsakis (Oct 22 2019 at 19:36, on Zulip):

@Jack Huey it should be fine, it only has the tcx lifetime, and so does the Context type

nikomatsakis (Oct 22 2019 at 19:36, on Zulip):

well, i've not double checked :) but that should be the case

Jack Huey (Oct 22 2019 at 19:37, on Zulip):

Yeah, looking again, I think it should be okay. Mostly just have to figure out why I made the tests fail

Jack Huey (Oct 24 2019 at 15:09, on Zulip):

@nikomatsakis you around? I have some questions/discussion.

nikomatsakis (Oct 24 2019 at 15:09, on Zulip):

Yes

Jack Huey (Oct 24 2019 at 15:09, on Zulip):

What's the advantage of having a separate UCanonicalGoalInEnvironment versus just a CanonicalGoalInEnvironment?

nikomatsakis (Oct 24 2019 at 15:10, on Zulip):

I'm trying to remember :) Ah, well, I think that the different is

nikomatsakis (Oct 24 2019 at 15:10, on Zulip):

UCanonicalGoalInEnvironment "renumbers" the universes to be minimal

nikomatsakis (Oct 24 2019 at 15:11, on Zulip):

this makes sense for a query or at the "start" of things

nikomatsakis (Oct 24 2019 at 15:11, on Zulip):

but CanonicalGoalInEnvironment does not, which makes sense for an answer or other thing that occurs inside of some context

nikomatsakis (Oct 24 2019 at 15:11, on Zulip):

at least, that's the main difference UCanonical and Canonical in general

nikomatsakis (Oct 24 2019 at 15:11, on Zulip):

not sure specifically about GoalInEnvironment

nikomatsakis (Oct 24 2019 at 15:12, on Zulip):

well I guess that's the type we use for the "answer" to a query, maybe

Jack Huey (Oct 24 2019 at 15:13, on Zulip):

And, I'm still trying to wrap my head around where things get canonicalized/uncanonicalized. When I removed CanonicalGoal, I sort of just assumed that I should just be able to pass around the CanonicalizedExClause (with accessing the inner ExClause), but that wasn't an accurate assumption. So seems like still need to more or less keep the canonicalization/uncanonicalization as things get passed around

Jack Huey (Oct 24 2019 at 15:15, on Zulip):

Right, so I guess my question between UCanonicalGoalInEnvironment and CanonicalGoalInEnvironment is it is ever necessary to know that you're not the first universe? Like, if all canonicalization renumbered the universe to be minimal?

nikomatsakis (Oct 24 2019 at 15:15, on Zulip):

OK. I guess I would summarize it as:

nikomatsakis (Oct 24 2019 at 15:16, on Zulip):

So imagine that we had a query like Implemented(?X: Foo<!22, !23>)

nikomatsakis (Oct 24 2019 at 15:16, on Zulip):

here we are saying -- give me all types that implement Foo<!22, !23>, and maybe ?X is in universe 0

nikomatsakis (Oct 24 2019 at 15:16, on Zulip):

in that case, it doesn't really matter that the placeholders are in universes 22 and 23

nikomatsakis (Oct 24 2019 at 15:17, on Zulip):

what's important is the relative ordering

nikomatsakis (Oct 24 2019 at 15:17, on Zulip):

we canonicalize this to Implemented(?X: Foo<!1, !2>)

nikomatsakis (Oct 24 2019 at 15:17, on Zulip):

ok, maybe not the best example, I hit a minor roadbock -- let's say that ?X is in universe 23, so it can name either !22 or !23

nikomatsakis (Oct 24 2019 at 15:17, on Zulip):

(I'm kind of assuming some basic familiarity with how universes work, let me know if that's incorrect)

nikomatsakis (Oct 24 2019 at 15:18, on Zulip):

we canonicalize this to Implemented(?X: Foo<!1, !2>)

I should have said we ucanonicalize this

nikomatsakis (Oct 24 2019 at 15:18, on Zulip):

and if we include all the info, I guess it's like exists<?X in U2> { Implemented(?X: Foo<!1, !2>) }

nikomatsakis (Oct 24 2019 at 15:18, on Zulip):

or you could sort of "rephrase" that as saying that we canonicalize to forall<A> { forall<B> { exists<C> { Implemented(C: Foo<A, B>) } } }

nikomatsakis (Oct 24 2019 at 15:18, on Zulip):

with me so far?

Jack Huey (Oct 24 2019 at 15:19, on Zulip):

one sec, let me try to follow

nikomatsakis (Oct 24 2019 at 15:21, on Zulip):

OK, here's a way to look at it. Every universe corresponds to some forall that we are "inside" of --

So

forall<A> { A: Foo }

when we enter the forall, we replace A with !1, etc

nikomatsakis (Oct 24 2019 at 15:21, on Zulip):

the problem is that sometimes we have foralls which we are inside of but which are not relevant

nikomatsakis (Oct 24 2019 at 15:21, on Zulip):

e.g.

Jack Huey (Oct 24 2019 at 15:21, on Zulip):

Can you clarify the syntax here? !22 means universe 22, right?

nikomatsakis (Oct 24 2019 at 15:22, on Zulip):

if we start with

forall<A> { forall<B> { A: Foo, B: Bar<A> } }

we would then have to prove just the first part (to start)

forall<A> { forall<B> { A: Foo } }

but here, B is not relevant

nikomatsakis (Oct 24 2019 at 15:22, on Zulip):

Can you clarify the syntax here? !22 means universe 22, right?

yeah, "placeholder in universe 22"

Jack Huey (Oct 24 2019 at 15:23, on Zulip):

As opposed to ^0 or ?0?

nikomatsakis (Oct 24 2019 at 15:23, on Zulip):

right so ^0 refers to a bound variable--

nikomatsakis (Oct 24 2019 at 15:23, on Zulip):

so e.g. forall<X> { ... }, in there, X is bound (we see the binder)

Jack Huey (Oct 24 2019 at 15:23, on Zulip):

Ok, then when canonicalized X would be converted to ^0?

nikomatsakis (Oct 24 2019 at 15:24, on Zulip):

but when we "enter" the forall, and wish to look at the terms inside, we kind of move that binder into the environment (by making a univese) and replace X with !U where U is that new universe

nikomatsakis (Oct 24 2019 at 15:24, on Zulip):

Ok, then when canonicalized X would be converted to ^0?

yes, because canonicalization basically adds a level of binder around the whole thing

Jack Huey (Oct 24 2019 at 15:24, on Zulip):

Also, the only place that infer.canonicalize_goal is called is in abstract_positive_literal and abstract_negative_literal, but that immediately get's converted to a UCanonicalizedGoalInEvironment in get_or_create_table_for_subgoal

nikomatsakis (Oct 24 2019 at 15:24, on Zulip):

I'm struggling with how to convey this sense but basically

Jack Huey (Oct 24 2019 at 15:25, on Zulip):

Thanks for going through this with me. Like I said, trying to wrap my head around it all

nikomatsakis (Oct 24 2019 at 15:25, on Zulip):

you have terms (types, etc) and they can either reference things from the surrounding environment ("free variables") or they can include a binder and reference back to that -- and there is some implicit point that we are maintaining always

nikomatsakis (Oct 24 2019 at 15:25, on Zulip):

so e.g. in terms of our representation when you see forall<type> { ^0: Debug }, that ^0 is referring back to the innermost binder (a "type")

nikomatsakis (Oct 24 2019 at 15:26, on Zulip):

(that's our debug notation, the variables are not named)

nikomatsakis (Oct 24 2019 at 15:26, on Zulip):

in more conventional notation it would be like forall<T> { T: Debug }

Jack Huey (Oct 24 2019 at 15:27, on Zulip):

These are debruijn indices right?

nikomatsakis (Oct 24 2019 at 15:27, on Zulip):

but when we want to try and prove that to be true, we "enter" the forall -- kind of shifting the "current point" between what is bound and free. So we create the next universe U and replace the bound variable (^0, or T) with !U, leaving us with a new term !U: Debug -- note that there is no forall here, it's in the environment now

nikomatsakis (Oct 24 2019 at 15:27, on Zulip):

Also, the only place that infer.canonicalize_goal is called is in abstract_positive_literal and abstract_negative_literal, but that immediately get's converted to a UCanonicalizedGoalInEvironment in get_or_create_table_for_subgoal

it may be that we don't need to have CanonicalizedGoalInEnvornment as a separate type

nikomatsakis (Oct 24 2019 at 15:28, on Zulip):

but the distinction between u-canonical and canonical is still important more generally

Jack Huey (Oct 24 2019 at 15:30, on Zulip):

Ok I think I understand a bit better now, thanks

nikomatsakis (Oct 24 2019 at 15:30, on Zulip):

to circle back to my example, basically the output of just canonicalization our query is something like this

forall<A> { forall<B> { A: Foo } }
                        ^ implicit point is here, in terms of what's in environment and what's in the terms we are manipulating

so u-canonicalization is just removing that unused forall<B>, basically

nikomatsakis (Oct 24 2019 at 15:30, on Zulip):

but the thing I was going to say was that when you produce an output, you don't want to do that, because the output is expressed in terms of those foralls that were in the environment

nikomatsakis (Oct 24 2019 at 15:31, on Zulip):

e.g., we might say ?X: SomeTrait is true if ?X = !1, and we need to know which !1 that is

nikomatsakis (Oct 24 2019 at 15:31, on Zulip):

we could I guess renumbering things but it'd be silly because we'd immediately want to reference back

Jack Huey (Oct 24 2019 at 15:42, on Zulip):

Ok so, to just sort of sum it up, if I understand correctly:
If our query is
forall<A> { forall<B> { A: Foo } }
that would be canonicalized to
forall<type> { forall<type> { ^1: Foo } }
and then ucanonicalized to
!1: Foo
I feel like I've missed something.

nikomatsakis (Oct 24 2019 at 15:49, on Zulip):

well

nikomatsakis (Oct 24 2019 at 15:49, on Zulip):

ok so

nikomatsakis (Oct 24 2019 at 15:50, on Zulip):

it would be canonicalized for forall<type> { forall<type> { ^1: Foo } and then ucanonicalized to

forall<type> { ^0: Foo }

Jack Huey (Oct 24 2019 at 15:50, on Zulip):

oh

nikomatsakis (Oct 24 2019 at 15:50, on Zulip):

then when we start processing the query

nikomatsakis (Oct 24 2019 at 15:50, on Zulip):

we would convert that to !1: Foo

Jack Huey (Oct 24 2019 at 16:07, on Zulip):

Ok so, taking a step back. What exactly is the goal of removing CanonicalStrand? Or, more-so, what's the benefit of storing infer in Strand? Is the intention that we pass a canonicalized strand around or the uncanonicalized strand then canonicalize where needed?

Jack Huey (Oct 24 2019 at 16:09, on Zulip):

I guess I should probably go back to the commit that added CanonicalStrand and look at how it was used before

nikomatsakis (Oct 24 2019 at 16:43, on Zulip):

Ok so, taking a step back. What exactly is the goal of removing CanonicalStrand? Or, more-so, what's the benefit of storing infer in Strand? Is the intention that we pass a canonicalized strand around or the uncanonicalized strand then canonicalize where needed?

the benefit is not having to canonicalize when we suspend a strand and to "de-canonicalize" when we restore one

nikomatsakis (Oct 24 2019 at 16:43, on Zulip):

it's a purely a runtime optimization

nikomatsakis (Oct 24 2019 at 16:43, on Zulip):

perhaps also a (to my mind) conceptual simplification

nikomatsakis (Oct 24 2019 at 16:44, on Zulip):

in that I think you want to have one inference context per .. hmm .. "active environment" in which work is being done, and a strand is one such environment (similarly, the code in the compiler creates one inference context per function, etc)

Jack Huey (Oct 25 2019 at 00:23, on Zulip):

Ok. So. I think there's some subtlety here that I'm not seeing. I have a feeling that it has to do with the InferenceTable now being persistent instead being re-created every time a CanonicalStrand get instantiated into a Strand. Either that, some state is getting shared when Strands are supposed to cloned fresh. Which is causing a bunch of tests to fail, and I honestly don't know why. So I think a better approach to this is to take a step back to the known-passing code, add some unit tests that specifically test behavior in chalk-engine, instead of only the integration tests in the root.

nikomatsakis (Oct 25 2019 at 16:44, on Zulip):

@Jack Huey I can also take a look

nikomatsakis (Oct 25 2019 at 16:45, on Zulip):

unit testing chalk-engine seems fine too, though in general I'd prefer to keep most of our unit tests "high level" precisely so they survive big refactorings like this

Jack Huey (Oct 25 2019 at 16:50, on Zulip):

@nikomatsakis If you want to take a look/have time, I've pushed a branch to my fork with that commit that removes CanonicalStrand https://github.com/jackh726/chalk/commit/511b4f247e48a5b0d8ddc5e8bf84f0e3c1cd3337

nikomatsakis (Oct 25 2019 at 16:50, on Zulip):

is that in the PR, @Jack Huey ?

Jack Huey (Oct 25 2019 at 16:50, on Zulip):

Not in the PR because tests are failing, but I could push it to the PR branch

nikomatsakis (Oct 25 2019 at 16:50, on Zulip):

I'd say push it to the PR branch

nikomatsakis (Oct 25 2019 at 16:51, on Zulip):

it's usually easier to give feedback if there's an open PR

Jack Huey (Oct 25 2019 at 16:51, on Zulip):

will do

Jack Huey (Oct 25 2019 at 16:52, on Zulip):

Ok PR is updated

Jack Huey (Oct 25 2019 at 16:54, on Zulip):

Overall, all but 19 tests pass

Jack Huey (Oct 28 2019 at 18:55, on Zulip):

Btw @nikomatsakis I've updated the PR and rebased to master

Jack Huey (Nov 04 2019 at 17:41, on Zulip):

@nikomatsakis Working off of the work I've done so far (using the coinduction fix branch as a base), I was able to make Table store Strands rather than CanonicalStrands

Jack Huey (Nov 04 2019 at 17:41, on Zulip):

the only test not passing is only_draw_so_many_blow_up

Jack Huey (Nov 04 2019 at 17:42, on Zulip):

but I think it's probably because new InferenceTables aren't being created

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

@Jack Huey great! Sorry i've not finalized my review of your PRs yet

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

I did read them but I didn't have time to come back to it yet, been having some last-minute demands on my time fri/today

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

though from my first read I was very happy with the coinduction PR

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

No problem :)

Last update: Nov 12 2019 at 16:55UTC