Stream: wg-traits

Topic: chalk-engine lecture 2019.05.06


nikomatsakis (May 06 2019 at 18:34, on Zulip):

Paper document

nikomatsakis (May 06 2019 at 18:35, on Zulip):

Zoom link

detrumi (May 06 2019 at 19:50, on Zulip):

That went well, with us adding some notes here and there

nikomatsakis (May 06 2019 at 19:51, on Zulip):

Yeah, seems good

detrumi (May 06 2019 at 19:51, on Zulip):

Maybe we could also write down questions inline next time?

nikomatsakis (May 06 2019 at 19:51, on Zulip):

Good idea

nikomatsakis (May 06 2019 at 20:00, on Zulip):

So one thing I didn't make very clear at the end:

nikomatsakis (May 06 2019 at 20:01, on Zulip):

I think that if we don't care about negative cycles, it somewhat simplifies the question of "when to undelay"

nikomatsakis (May 06 2019 at 20:01, on Zulip):

But I'd like to understand better the importance of negative cycles here

nikomatsakis (May 06 2019 at 20:02, on Zulip):

It seems... plausible that we could just propagate "non-enumerable" things all the way out, and push the "undelay logic" to some outer loop, too

nikomatsakis (May 06 2019 at 20:02, on Zulip):

Also, one last thing: region constraints can be considered a kind of delayed literal

detrumi (May 06 2019 at 20:03, on Zulip):

Won't there be a problem with delaying too many things, in that you'd have to undelay in a certain order to make progress?

nikomatsakis (May 06 2019 at 20:03, on Zulip):

I don't think so

nikomatsakis (May 06 2019 at 20:03, on Zulip):

Well, it depends what you mean

nikomatsakis (May 06 2019 at 20:04, on Zulip):

I guess the answer is "maybe"

detrumi (May 06 2019 at 20:04, on Zulip):

Heh, that's what you get for asking a vague question, I guess

nikomatsakis (May 06 2019 at 20:04, on Zulip):

(Anyway I think we probably want to undelay more aggressively than what I was suggesting)

nikomatsakis (May 06 2019 at 20:04, on Zulip):

Well, so, specifically -- things like Sized don't "help" with progress

nikomatsakis (May 06 2019 at 20:04, on Zulip):

i.e., Sized never "constrains" its argument really

nikomatsakis (May 06 2019 at 20:05, on Zulip):

but this is perhaps untrue for other traits

nikomatsakis (May 06 2019 at 20:05, on Zulip):

(As an aside,

nikomatsakis (May 06 2019 at 20:05, on Zulip):

one thing I think we could/should also do is to apply some heuristics to the impls of a given trait,

nikomatsakis (May 06 2019 at 20:05, on Zulip):

to try and aid our selection order)

nikomatsakis (May 06 2019 at 20:10, on Zulip):

Another clarification: on quantum

nikomatsakis (May 06 2019 at 20:10, on Zulip):

It looks like the time that we use quantum is this

nikomatsakis (May 06 2019 at 20:10, on Zulip):
nikomatsakis (May 06 2019 at 20:11, on Zulip):
nikomatsakis (May 06 2019 at 20:11, on Zulip):
nikomatsakis (May 06 2019 at 20:11, on Zulip):

because the strands are in a LIFO, we'll come back to them only after trying the other work anyway

nikomatsakis (May 06 2019 at 20:12, on Zulip):

you might wonder why we bother to "stash" the cyclic strnads into the vector anyway

nikomatsakis (May 06 2019 at 20:12, on Zulip):

the idea is that we want to know if ALL of the remaining strands are cyclic

nikomatsakis (May 06 2019 at 20:12, on Zulip):

because that means there are no more answers at all

tmandry (May 06 2019 at 20:13, on Zulip):

one thing I think we could/should also do is to apply some heuristics to the impls of a given trait,

as a strawman, we could have a hierarchy where you have
1. Traits with non-quantified impls (we can even count the impls here)
2. Traits with universally quantified impls (e.g. impl<T> Foo for Vec<T>)
- maybe we should split this into bounded (e.g. impl<T: Bar>) and unbounded?
3. Auto traits
- we can include impl<T> Foo for T in this category

nikomatsakis (May 06 2019 at 20:14, on Zulip):

Yeah, something like that

nikomatsakis (May 06 2019 at 20:14, on Zulip):

I think the "bounded and unbounded" -- it might be that we are interesting in DAGs

nikomatsakis (May 06 2019 at 20:14, on Zulip):

i.e., if trait Foo includes a bound T: BAr, but Bar has no T: Foo bounds -- that's more ok?

nikomatsakis (May 06 2019 at 20:15, on Zulip):

(I always imagined we would kind of look at what impls exist "in practice" to help us drive said heuristics)

nikomatsakis (May 06 2019 at 20:15, on Zulip):

but some kind of "locally testable heuristics" seem very good

tmandry (May 06 2019 at 20:20, on Zulip):

This resembles a kind of pathfinding algorithm where our nodes are strands, and the cost of traversing each node is its outdegree

tmandry (May 06 2019 at 20:52, on Zulip):

So it seems kind of like one could think about this in terms of "collecting constraints", kind of like we do for regions

tmandry (May 06 2019 at 20:53, on Zulip):

basically any non-enumerable goal is added as a constraint on a particular strand

tmandry (May 06 2019 at 20:53, on Zulip):

I guess that's equivalent to the delayed literals approach niko mentioned

tmandry (May 06 2019 at 20:54, on Zulip):

except for the question of "how does this interact with negative reasoning"

tmandry (May 06 2019 at 20:54, on Zulip):

..maybe we could have two separate mechanisms, one (delayed literals) for negative reasoning, the other (constraints) for non-enumerable goals

tmandry (May 06 2019 at 20:55, on Zulip):

I don't know if I'm making sense :)

nikomatsakis (May 06 2019 at 20:55, on Zulip):

you are, I've been debating if they should be unified or not

nikomatsakis (May 06 2019 at 20:57, on Zulip):

I've also been reading the source to remember how this logic works

nikomatsakis (May 06 2019 at 20:58, on Zulip):

I think I have to page back in the EWFS paper as well

tmandry (May 06 2019 at 20:59, on Zulip):

another related question is, if we collect these non-enumerable goals as constraints, how complicated could they get, and can we solve them outside of the main engine path?

tmandry (May 06 2019 at 21:02, on Zulip):

(since we're already going to be doing this for region constraints, it seems natural to wonder if things like ?T: Sized could take on a similar shape)

nikomatsakis (May 06 2019 at 21:02, on Zulip):

Right, so, if we focus on the case of compiler-builtins, then they would be quite simple. It seems like you could just give up the answer including the delayed literals

nikomatsakis (May 06 2019 at 21:02, on Zulip):

and then have an outer loop to process them

nikomatsakis (May 06 2019 at 21:02, on Zulip):

this would probably include things like Clone though

nikomatsakis (May 06 2019 at 21:03, on Zulip):

process the literal itself can definitely require arbitrary logic

nikomatsakis (May 06 2019 at 21:03, on Zulip):

but this is roughly equivalent to our current solver, but different

nikomatsakis (May 06 2019 at 21:04, on Zulip):

i.e., we assume that during type-checking or whatever you have some "fulfillment context" accumulating things you must prove

nikomatsakis (May 06 2019 at 21:04, on Zulip):

so if you get back an answer with delayed things, it can just add those to its list of "stuff to prove eventually"

nikomatsakis (May 06 2019 at 21:04, on Zulip):

(the existing rustc solver does something similar)

nikomatsakis (May 06 2019 at 21:06, on Zulip):

( I am pondering to what extent this can solve the negative problem too )

nikomatsakis (May 06 2019 at 21:06, on Zulip):

let me try to spell out what i'm saying

nikomatsakis (May 06 2019 at 21:06, on Zulip):

imagine we had

impl<T: Sized> Foo for Vec<T>
nikomatsakis (May 06 2019 at 21:07, on Zulip):

and then we had to prove ?A: Foo

nikomatsakis (May 06 2019 at 21:07, on Zulip):

this might result in ?A = Vec<?B> modulo ?B: Sized

nikomatsakis (May 06 2019 at 21:07, on Zulip):

er, that's a confusing notation :)

nikomatsakis (May 06 2019 at 21:07, on Zulip):

maybe that's less unclear ;)

nikomatsakis (May 06 2019 at 21:07, on Zulip):

point is, it could delay the ?B: Sized part (non-enumerable)"

nikomatsakis (May 06 2019 at 21:07, on Zulip):

and hence we would consider ?A: Foo "proved" but we would enqueue ?B: Sized

nikomatsakis (May 06 2019 at 21:08, on Zulip):

now, maybe other parts of the type-checker constrain ?B: Sized, and so at some point we have ?B = u32

nikomatsakis (May 06 2019 at 21:08, on Zulip):

now when we go to "re-prove" ?B: Sized, we get u32: Sized and we're all set

nikomatsakis (May 06 2019 at 21:09, on Zulip):

(it seems like a similar thing could work for the coinductive case)

nikomatsakis (May 06 2019 at 21:09, on Zulip):

what's nice about this is

nikomatsakis (May 06 2019 at 21:09, on Zulip):

the chalk-engine tables never change

nikomatsakis (May 06 2019 at 21:09, on Zulip):

one thing that's been bugging me with delayed literals is that there is this "simplification" step

nikomatsakis (May 06 2019 at 21:10, on Zulip):

that takes the existing answers, re-evaluates their delays, and can kind of rule them as "succeeded", "failed", or "unknown" as a result

nikomatsakis (May 06 2019 at 21:10, on Zulip):

I mean I guess editing the answers in place is .. fine. It just makes me kind of nervous.

nikomatsakis (May 06 2019 at 21:10, on Zulip):

Because part of the reasoning here is that Answer(Table, Index) (once computed) is always the same

nikomatsakis (May 06 2019 at 21:11, on Zulip):

what's nice about this is

what's less nice is that something this is silly

nikomatsakis (May 06 2019 at 21:11, on Zulip):

i.e., if we "delay ?B: Sized" but later find out what ?B is, we could go ahead and process it right then and there

nikomatsakis (May 06 2019 at 21:12, on Zulip):

otoh, who cares...

nikomatsakis (May 06 2019 at 21:12, on Zulip):

seems (to me) like this 'outer loop' idea is the way to go; there's caching and if it winds up being a perf problem, we could look into something more sophisticated

nikomatsakis (May 06 2019 at 21:13, on Zulip):

(in short, we likely got bigger perf problems to solve first)

tmandry (May 06 2019 at 21:13, on Zulip):

is that going to avoid the "editing answer in-place" problem you mentioned?

tmandry (May 06 2019 at 21:13, on Zulip):

(seems like it could)

nikomatsakis (May 06 2019 at 21:14, on Zulip):

the outer loop idea?

tmandry (May 06 2019 at 21:14, on Zulip):

yes

nikomatsakis (May 06 2019 at 21:14, on Zulip):

yeah, I mean, the idea is that we just .. never simplify

nikomatsakis (May 06 2019 at 21:14, on Zulip):

we let the outer loop do it

tmandry (May 06 2019 at 21:14, on Zulip):

so we'd have our internal ensure_answer(T0, 0) returns ?A = Vec<?B> modulo ?B: Sized and then we remove the modulo part every time

nikomatsakis (May 06 2019 at 21:15, on Zulip):

right

nikomatsakis (May 06 2019 at 21:15, on Zulip):

(but those results are cached etc)

nikomatsakis (May 06 2019 at 21:15, on Zulip):

still, it's probably also fine to remove it in the table itself

tmandry (May 06 2019 at 21:16, on Zulip):

if we did that we'd have to do something with the answers that don't work, i.e. do we leave a placeholder so the index doesn't change

nikomatsakis (May 06 2019 at 21:16, on Zulip):

I don't know that this works for the negative cycle case; well, it works in a sense, I think you would wind up just "reprocessing" the same constraints over and over

nikomatsakis (May 06 2019 at 21:17, on Zulip):

if we did that we'd have to do something with the answers that don't work, i.e. do we leave a placeholder so the index doesn't change

yes, they would presumably get transformed to "fail" or something

tmandry (May 06 2019 at 21:19, on Zulip):

I think you would wind up just "reprocessing" the same constraints over and over

I have to go in a sec, but don't quite see why this is true :)

nikomatsakis (May 06 2019 at 21:21, on Zulip):

I don't know that it's entirely true :)

nikomatsakis (May 06 2019 at 21:22, on Zulip):

(I need to work through some of the examples)

nikomatsakis (May 06 2019 at 21:22, on Zulip):

I really do wonder if we should worry about negative reasoning though. Maybe this is all reason enough to rule it out and simplify our lives.

nikomatsakis (May 06 2019 at 21:22, on Zulip):

For some reason, I am reluctant to do that, but it's hard for me to say why that is

nikomatsakis (May 06 2019 at 21:23, on Zulip):

I guess beacuse I'd like to be able to articulate very precisely what the tricky cases are, at minimum, so when people ask, we can answer them

nikomatsakis (May 07 2019 at 17:59, on Zulip):

I realized some problems here with this "un-enumerable predicates" idea. I don't know how well it interacts with hereditary harrop predicates like forall<T> { Goal } and so forth. In particular, it seems like you have to capture the universe / environment and things when you propagate the goal back. I .. guess we can do this, it's just kind of an interesting twist.

Julius-Beides (May 08 2019 at 18:43, on Zulip):

Was the Zoom meeting not recorded as usual?
I'm asking because there is no video on the YouTube channel.

nikomatsakis (May 08 2019 at 18:47, on Zulip):

I just didn't post it yet

nikomatsakis (May 08 2019 at 18:47, on Zulip):

Will try to do that soon

Julius-Beides (May 08 2019 at 19:09, on Zulip):

Thanks :)

nikomatsakis (May 08 2019 at 21:34, on Zulip):

@Julius-Beides video is uploading at this url, but it's not available yet

Last update: Nov 12 2019 at 16:40UTC