Stream: wg-traits

Topic: chalk roadmap


nikomatsakis (Apr 23 2019 at 14:13, on Zulip):

@scalexm I spent some time this morning organizing a dropbox paper with a kind of "brain dump" of all the things that I think chalk specifically needs. It's probably not complete and some items continue to need elaboration. Feel free to add more items or comments.

varkor (Apr 23 2019 at 14:57, on Zulip):

const generics should probably be on there too

varkor (Apr 23 2019 at 14:58, on Zulip):

(re. "complete the chalk lowering")

varkor (Apr 23 2019 at 14:58, on Zulip):

what definition of "intersection type" are you using?

varkor (Apr 23 2019 at 14:59, on Zulip):

the concept of intersection type doesn't seem to be very well-defined in general

varkor (Apr 23 2019 at 14:59, on Zulip):

should it be different from a product of the two types?

nikomatsakis (Apr 23 2019 at 16:02, on Zulip):

well, this is something of a home-brew definition, but I think it fits fairly well the standard usage

nikomatsakis (Apr 23 2019 at 16:02, on Zulip):

it is quite distinct from a product type, yes

nikomatsakis (Apr 23 2019 at 16:02, on Zulip):

the idea is "some value is both T1 and T2 simultaneously"

nikomatsakis (Apr 23 2019 at 16:04, on Zulip):

const generics should probably be on there too

hmm. yes, I agree, though I wonder how much work there is here. some, at least, but likely minimal

nikomatsakis (Apr 23 2019 at 16:04, on Zulip):

i.e., this is basically a new kind of unifiable thing (in addition to types/lifetimes)

nikomatsakis (Apr 23 2019 at 16:04, on Zulip):

well, it'd be good to answer that question

nikomatsakis (Apr 23 2019 at 16:06, on Zulip):

(@scalexm you around?)

nikomatsakis (Apr 23 2019 at 16:07, on Zulip):

(I'm skimming over the comments you left in the paper doc right now)

nikomatsakis (Apr 23 2019 at 16:08, on Zulip):

Let's ask an interesting question

nikomatsakis (Apr 23 2019 at 16:08, on Zulip):

It seems like we're moving in a direction in which the chalk-solve crate should be able to handle all of Rust

nikomatsakis (Apr 23 2019 at 16:08, on Zulip):

Presently, chalk elides some things -- like arbitrary arity tuples, as you pointed out

nikomatsakis (Apr 23 2019 at 16:09, on Zulip):

but also things like Sized trait

nikomatsakis (Apr 23 2019 at 16:09, on Zulip):

and other builtin traits

nikomatsakis (Apr 23 2019 at 16:10, on Zulip):

but trying to setup the crates from chalk#214, it seems like a number of those details become relevant precisely around this "give me the program clauses for the goal X" callback

nikomatsakis (Apr 23 2019 at 16:10, on Zulip):

and...that is probably a good thing?

nikomatsakis (Apr 23 2019 at 16:11, on Zulip):

that said, maybe we should talk through the doc a bit systematically? One of the things I was curious to start with was the set of goals I outlined. I am particularly interested in trying to get more specific about what it means to validate the chalk approach -- i.e., what things are we worried about?

scalexm (Apr 23 2019 at 16:11, on Zulip):

@nikomatsakis true, this callback is I think the only one having interactions with those arbitrary arity + builtin bounds etc questions

nikomatsakis (Apr 23 2019 at 16:12, on Zulip):

true, this callback is I think the only one having interactions with those arbitrary arity + builtin bounds etc questions

yeah -- but it seems kind of "right" to me for that logic to ultimately live within the chalk crate

nikomatsakis (Apr 23 2019 at 16:12, on Zulip):

I guess I am thinking now of the chalk-solve crate as being the "adapter" between rust syntax and logical predciates

scalexm (Apr 23 2019 at 16:12, on Zulip):

@nikomatsakis what worries me the most is whether we'll be able to implement a good solution for region constraints

nikomatsakis (Apr 23 2019 at 16:13, on Zulip):

I guess that connects to my top worry

scalexm (Apr 23 2019 at 16:13, on Zulip):

also eventually regarding perfs, I think we still don't know if the chalk approach will be as efficient as the existing solver

scalexm (Apr 23 2019 at 16:14, on Zulip):

also we presume it will be more efficient

nikomatsakis (Apr 23 2019 at 16:14, on Zulip):

I am worried in general about managing the performance -- in particular, I am worried the solver might get "lost" exploring fruitless parts of the search space

scalexm (Apr 23 2019 at 16:14, on Zulip):

yes

nikomatsakis (Apr 23 2019 at 16:14, on Zulip):

But one of the reasons it could do so, I think

nikomatsakis (Apr 23 2019 at 16:14, on Zulip):

is if it is attempting to enumerate out the possible region constraints more fully

nikomatsakis (Apr 23 2019 at 16:15, on Zulip):

but ok so -- our two concerns so far are

nikomatsakis (Apr 23 2019 at 16:15, on Zulip):

are there other parts of "supporting Rust" that we are concerned about?

nikomatsakis (Apr 23 2019 at 16:15, on Zulip):

mostly the things i've listed feel like "just work" to me

nikomatsakis (Apr 23 2019 at 16:15, on Zulip):

not trivial by any means

scalexm (Apr 23 2019 at 16:16, on Zulip):

I don't think there are any other concerns

nikomatsakis (Apr 23 2019 at 16:16, on Zulip):

I'm looking at specialization, primarily. I guess there is some doubt as to what it'll take to make lazy norm work in practice, how many surprises we might hit there

nikomatsakis (Apr 23 2019 at 16:16, on Zulip):

OK, so let's talk out region inference a little bit perhaps

nikomatsakis (Apr 23 2019 at 16:17, on Zulip):

I have a vague plan

nikomatsakis (Apr 23 2019 at 16:17, on Zulip):

Not sure how much we've talked about it before, I forget

nikomatsakis (Apr 23 2019 at 16:18, on Zulip):

roughly speaking what I would like to do

nikomatsakis (Apr 23 2019 at 16:18, on Zulip):

is to distinguish the "base region predicates" that polonius curently understands -- basically 'a: 'b

nikomatsakis (Apr 23 2019 at 16:19, on Zulip):

from the more complex "hereditary harrop predicates" that we sometimes produce (e.g., for<'a> ('a: 'b) and so on)

nikomatsakis (Apr 23 2019 at 16:19, on Zulip):

I think it should be chalk's job to lowering from the HH predicates to the base predicates -- but not the base predicates we have today, which are very simple

nikomatsakis (Apr 23 2019 at 16:20, on Zulip):

today, we have

RC = 'a: 'b | RC && RC
nikomatsakis (Apr 23 2019 at 16:20, on Zulip):

I would want to add

nikomatsakis (Apr 23 2019 at 16:20, on Zulip):
RC = 'a: 'b | RC && RC | RC || RC
nikomatsakis (Apr 23 2019 at 16:20, on Zulip):

which is of course kinda' a big deal

nikomatsakis (Apr 23 2019 at 16:20, on Zulip):

today, we have

let me clarify -- I don't really mean in chalk today, but more like polonius today

nikomatsakis (Apr 23 2019 at 16:21, on Zulip):

I would want to add

specifically, I want to add "or" constraints

scalexm (Apr 23 2019 at 16:21, on Zulip):

yes, I remember that we talked about that

nikomatsakis (Apr 23 2019 at 16:21, on Zulip):

if you have something like

fn foo<'a, 'b, T>()
where T: Trait<'a>, T: Trait<'b> { ... }
nikomatsakis (Apr 23 2019 at 16:21, on Zulip):

it seems like you kind of have to be able to say that T: Trait<'c> if 'c == 'a || 'c == 'b

nikomatsakis (Apr 23 2019 at 16:22, on Zulip):

or else to try and treat regions just like types--

nikomatsakis (Apr 23 2019 at 16:22, on Zulip):

and return an ambiguous result until we infer what region we want

nikomatsakis (Apr 23 2019 at 16:23, on Zulip):

which..may actually be plausible

nikomatsakis (Apr 23 2019 at 16:23, on Zulip):

( it'd be a big mental shift )

nikomatsakis (Apr 23 2019 at 16:24, on Zulip):

in any case, let's run with the "or" constraints for a moment

nikomatsakis (Apr 23 2019 at 16:25, on Zulip):

I think it should be chalk's job to lowering from the HH predicates to the base predicates -- but not the base predicates we have today, which are very simple

so I explored what this would look like

nikomatsakis (Apr 23 2019 at 16:25, on Zulip):

it looks like I didn't commit that code anywhere, I guess it's on my old mac

nikomatsakis (Apr 23 2019 at 16:25, on Zulip):

I should push it somewhere but the tl;dr was that I was messed about with lambda prolog

nikomatsakis (Apr 23 2019 at 16:25, on Zulip):

there are really just a few rules, basically

nikomatsakis (Apr 23 2019 at 16:26, on Zulip):

I think I had a relation like lower(HHRC, RC) where the input was the hereditary harrop region constraint (HHRC) and the output was a list of flat constraints RC; this would of course have multiple solutions sometimes

nikomatsakis (Apr 23 2019 at 16:27, on Zulip):

but let me go look :)

nikomatsakis (Apr 23 2019 at 16:30, on Zulip):

Ah, here it is

scalexm (Apr 23 2019 at 16:32, on Zulip):

@nikomatsakis mmh ok, lambda prolog syntax does not speak much to me :p

nikomatsakis (Apr 23 2019 at 16:33, on Zulip):

yeah, it's more for my own memory I guess

nikomatsakis (Apr 23 2019 at 16:33, on Zulip):

anyway it doesn't matter

nikomatsakis (Apr 23 2019 at 16:35, on Zulip):

I think the basic rule was just something like

forall<x> { 'static: 'x }

nikomatsakis (Apr 23 2019 at 16:36, on Zulip):

and then a rule that said forall<'a, 'b> { ('a: 'b) :- root('a), root('b) }

nikomatsakis (Apr 23 2019 at 16:36, on Zulip):

where "root" means that they exist in the "root universe"

nikomatsakis (Apr 23 2019 at 16:39, on Zulip):

the problem iirc was that you would get more answers than you might like

nikomatsakis (Apr 23 2019 at 16:39, on Zulip):

e.g., you might get 'a: 'b as one possible constraint but also 'a: 'static

nikomatsakis (Apr 23 2019 at 16:39, on Zulip):

so it seemed like we needed some kind of "entailment" step to try and simplify things

nikomatsakis (Apr 23 2019 at 16:39, on Zulip):

I never did explore further

nikomatsakis (Apr 23 2019 at 16:40, on Zulip):

anyway, idk, there's definitely exploration to be done here

nikomatsakis (Apr 23 2019 at 16:40, on Zulip):

let's try to get out of this rathole, I went deeper than I perhaps intended

nikomatsakis (Apr 23 2019 at 16:40, on Zulip):

maybe the question is:

what should be the steps for the next 6 weeks once this sprint is over

nikomatsakis (Apr 23 2019 at 16:40, on Zulip):

anyway, idk, there's definitely exploration to be done here

and, I suppose, it's relevant to talk about how to do this exploration

scalexm (Apr 23 2019 at 16:41, on Zulip):

@nikomatsakis I saw that @tmandry was working on adding more builtin bounds in rustc, which is cool

nikomatsakis (Apr 23 2019 at 16:41, on Zulip):

yes. and some of that logic will need to move to chalk-solve

scalexm (Apr 23 2019 at 16:41, on Zulip):

yes

nikomatsakis (Apr 23 2019 at 16:41, on Zulip):

I feel like we should probably make some part of our focus be

nikomatsakis (Apr 23 2019 at 16:41, on Zulip):

modeling the builtin-traits

nikomatsakis (Apr 23 2019 at 16:41, on Zulip):

and handling "unenumerable" things

nikomatsakis (Apr 23 2019 at 16:41, on Zulip):

which are highly related

nikomatsakis (Apr 23 2019 at 16:41, on Zulip):

do you know what I mean by "unenumerable"?

nikomatsakis (Apr 23 2019 at 16:42, on Zulip):

I guess I wrote “non-enumerable” in the paper doc

scalexm (Apr 23 2019 at 16:42, on Zulip):

yeah at least I understand what you mean, and the solution you proposed

nikomatsakis (Apr 23 2019 at 16:42, on Zulip):

in particular

nikomatsakis (Apr 23 2019 at 16:42, on Zulip):

those feel like an obvious area where the solver could get "lost"

nikomatsakis (Apr 23 2019 at 16:43, on Zulip):

I guess I would nominate Smart predicate order selection as an obvious sprint goal because it feels..well.. kinda easy to do

nikomatsakis (Apr 23 2019 at 16:43, on Zulip):

certainly adding the hook is easy

nikomatsakis (Apr 23 2019 at 16:43, on Zulip):

and it could be used to temporarily side-step some of the non-enumerable problems

scalexm (Apr 23 2019 at 16:43, on Zulip):

yes

nikomatsakis (Apr 23 2019 at 16:43, on Zulip):

longer term, I would like to have some heuristics

nikomatsakis (Apr 23 2019 at 16:43, on Zulip):

that look at the impls for a given trait

nikomatsakis (Apr 23 2019 at 16:44, on Zulip):

and sort of categorize it into "lots of impls" or "few impls"

nikomatsakis (Apr 23 2019 at 16:44, on Zulip):

or something

nikomatsakis (Apr 23 2019 at 16:44, on Zulip):

but that's another story

nikomatsakis (Apr 23 2019 at 16:44, on Zulip):

I feel like that would have to be a data-driven effort

scalexm (Apr 23 2019 at 16:45, on Zulip):

once we have the smart predicate order selection, we may be able to replace the artificial ambiguity hack in program_clauses_for for ?T: Sized goals with just a CannotProve result, right? Because these goals will actually never be hit with ?T unresolved, unless the goal is indeed totally unconstrained

nikomatsakis (Apr 23 2019 at 16:45, on Zulip):

well, not quite

nikomatsakis (Apr 23 2019 at 16:45, on Zulip):

I mean you could

nikomatsakis (Apr 23 2019 at 16:45, on Zulip):

but I think are cases that won't work right

nikomatsakis (Apr 23 2019 at 16:46, on Zulip):

in particular

nikomatsakis (Apr 23 2019 at 16:47, on Zulip):

if you had one goal like P(X) :- Q(X), R(X), perhaps Q(X) requires that X: Sized but R(X) would have specified was X is

nikomatsakis (Apr 23 2019 at 16:47, on Zulip):

but if we start processing Q(X) first

nikomatsakis (Apr 23 2019 at 16:47, on Zulip):

we would propagate a CannotProve

nikomatsakis (Apr 23 2019 at 16:47, on Zulip):

that then infects R

nikomatsakis (Apr 23 2019 at 16:47, on Zulip):

but if we had started first with R, it would be ok

nikomatsakis (Apr 23 2019 at 16:48, on Zulip):

the goal of the "bubble up" option I was proposing was that we wouldn't propagate a do-not-prove result, but more like a conditional answer (which is what a "delayed goal" is, really, but also a region constraint)

scalexm (Apr 23 2019 at 16:48, on Zulip):

ok

scalexm (Apr 23 2019 at 16:48, on Zulip):

so we really need that un-enumerable result

nikomatsakis (Apr 23 2019 at 16:48, on Zulip):

so once R(X) completed (and X is known) we could process it

nikomatsakis (Apr 23 2019 at 16:48, on Zulip):

so we really need that un-enumerable result

yes, I think so, but also

nikomatsakis (Apr 23 2019 at 16:48, on Zulip):

it seems like, just from a practical POV, that having impls which accept any type T so long as T: Sized is likely to be common

nikomatsakis (Apr 23 2019 at 16:49, on Zulip):

though I imagine .. maybe more general than that even?

nikomatsakis (Apr 23 2019 at 16:49, on Zulip):

i.e., this may not be entirely specific to sized

nikomatsakis (Apr 23 2019 at 16:49, on Zulip):

well, ignore what I'm saying, it's not that relevant

nikomatsakis (Apr 23 2019 at 16:49, on Zulip):

I guess what I'm saying is -- it may be useful regardless to have the option of "breaking down" a top-level goal into "mid-level goals". This is what the trait solver does today.

nikomatsakis (Apr 23 2019 at 16:49, on Zulip):

Admittedly, it is what I am trying to get away from :)

nikomatsakis (Apr 23 2019 at 16:50, on Zulip):

but it seems like it's useful at least for ?T: Sized

nikomatsakis (Apr 23 2019 at 16:50, on Zulip):

maybe we would want it other times for various reasons (primarily efficiency, I imagine)

nikomatsakis (Apr 23 2019 at 16:50, on Zulip):

I guess what I'm saying is -- it may be useful regardless to have the option of "breaking down" a top-level goal into "mid-level goals". This is what the trait solver does today.

not sure if you know what I mean by this

nikomatsakis (Apr 23 2019 at 16:50, on Zulip):

I guess I'm imagining something like impl<H: Hasher> Hash<H> for Foo

nikomatsakis (Apr 23 2019 at 16:51, on Zulip):

presently if you were asked Foo: Hash<?H>, the answer is ambiguous -- maybe we might find we would like to "convert" this into a ?H: Hasher constraint?

nikomatsakis (Apr 23 2019 at 16:51, on Zulip):

(Of course, we don't have to, because once ?H is "more precisely known", we'll have a different canonical query, which was the original plan)

nikomatsakis (Apr 23 2019 at 16:52, on Zulip):

so we really need that un-enumerable result

to circle back to this: I feel like implementing this idea isn't that complex

nikomatsakis (Apr 23 2019 at 16:52, on Zulip):

maybe i'm overlooking things

nikomatsakis (Apr 23 2019 at 16:54, on Zulip):

so the question is, maybe that is a candidate for a sprint goal, I guess

scalexm (Apr 23 2019 at 16:55, on Zulip):

presently if you were asked Foo: Hash<?H>, the answer is ambiguous -- maybe we might find we would like to "convert" this into a ?H: Hasher constraint?

ah ok I see

nikomatsakis (Apr 23 2019 at 16:55, on Zulip):

I suppose it will ultimately depend on how many people there are who have time

scalexm (Apr 23 2019 at 16:55, on Zulip):

yes, that does not seem overly complex to me either

nikomatsakis (Apr 23 2019 at 16:55, on Zulip):

so, if our goal is to "validate" chalk more

scalexm (Apr 23 2019 at 16:56, on Zulip):

but it probably requires a bit of knowledge of how the SLG solver works

nikomatsakis (Apr 23 2019 at 16:56, on Zulip):

yes. I think it's probably a good mentoring task

scalexm (Apr 23 2019 at 16:56, on Zulip):

so it would be maybe a "more advanced" issue

nikomatsakis (Apr 23 2019 at 16:56, on Zulip):

but "active mentoring"

nikomatsakis (Apr 23 2019 at 16:56, on Zulip):

or "intermediate level mentoring"

nikomatsakis (Apr 23 2019 at 16:56, on Zulip):

i.e., it's not trivial, for sure

nikomatsakis (Apr 23 2019 at 16:56, on Zulip):

but it'd be a good way to learn how the solver works :)

nikomatsakis (Apr 23 2019 at 16:57, on Zulip):

so, if our goal is to "validate" chalk more

I was going to say: there are two options here. Option 1 of course is to pursue more integration with rustc itself

nikomatsakis (Apr 23 2019 at 16:57, on Zulip):

Option 2 is to pursue more with RLS

nikomatsakis (Apr 23 2019 at 16:57, on Zulip):

I am inclined to do a bit of both ;)

scalexm (Apr 23 2019 at 16:57, on Zulip):

yes lol

nikomatsakis (Apr 23 2019 at 16:57, on Zulip):

But I'm wondering, what are the big blockers? i.e., what would it mean to "validate". I feel like we want to be able to run tests

nikomatsakis (Apr 23 2019 at 16:57, on Zulip):

and see where chalk gets stuck

nikomatsakis (Apr 23 2019 at 16:57, on Zulip):

region constraints are obviously a big blocker here

nikomatsakis (Apr 23 2019 at 16:57, on Zulip):

I am wondering, though

nikomatsakis (Apr 23 2019 at 16:58, on Zulip):

like, ignoring them is viable for time being in some sense

scalexm (Apr 23 2019 at 16:58, on Zulip):

rustc integration is already advanced enough to run tests

nikomatsakis (Apr 23 2019 at 16:58, on Zulip):

I know

nikomatsakis (Apr 23 2019 at 16:58, on Zulip):

right now, it kind of ignores region constraints, right? I guess.. this is probably "ok"

scalexm (Apr 23 2019 at 16:58, on Zulip):

last thing I recall is that it was having troubles with inferring type variables in some cases, I didn't know why

nikomatsakis (Apr 23 2019 at 16:58, on Zulip):

i.e., it doesn't lead to spurious compilation failures for the most part?

scalexm (Apr 23 2019 at 16:59, on Zulip):

it only ignores region constraints coming from unification

scalexm (Apr 23 2019 at 16:59, on Zulip):

region constraints like in struct S<T> where T: 'static are propagated

scalexm (Apr 23 2019 at 16:59, on Zulip):

I think

nikomatsakis (Apr 23 2019 at 16:59, on Zulip):

ok

nikomatsakis (Apr 23 2019 at 16:59, on Zulip):

sounds plausible

nikomatsakis (Apr 23 2019 at 16:59, on Zulip):

last thing I recall is that it was having troubles with inferring type variables in some cases, I didn't know why

so one plausible thing would be to set a goal of running the test suite

nikomatsakis (Apr 23 2019 at 16:59, on Zulip):

or some fraction of it

nikomatsakis (Apr 23 2019 at 16:59, on Zulip):

not sure how much runs now :)

nikomatsakis (Apr 23 2019 at 17:00, on Zulip):

or perhaps another way of saying it would be

nikomatsakis (Apr 23 2019 at 17:00, on Zulip):

running the test suite might help us to determine some goals

nikomatsakis (Apr 23 2019 at 17:01, on Zulip):

I gotta run for some other meetings etc, this was useful so far -- I guess running the test suite isn't too hard though

scalexm (Apr 23 2019 at 17:04, on Zulip):

I gotta run too

tmandry (Apr 24 2019 at 22:24, on Zulip):

@scalexm I don't know if you saw, I had a question for you on my PR: https://github.com/rust-lang/rust/pull/60183#discussion_r277843999

scalexm (Apr 24 2019 at 22:44, on Zulip):

@tmandry replied, hope that makes sense

scalexm (Apr 24 2019 at 22:45, on Zulip):

Btw eventually we won’t need this « ambiguity trick » anymore, as soon as we implement @nikomatsakis’s « non-enumerable » solution

tmandry (Apr 24 2019 at 22:49, on Zulip):

Yeah that does make sense, thanks!

Alexander Regueiro (Jun 10 2019 at 15:16, on Zulip):

Hey folks. How's lifetime support in Chalk coming along lately? Will we get to see a usable version in nightly any time soon? :-)

Last update: Nov 12 2019 at 16:05UTC