Stream: wg-traits

Topic: weekly meeting 2019-03-04


nikomatsakis (Mar 04 2019 at 18:59, on Zulip):

Howdy all :wave:

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

cc @WG-compiler-traits -- meeting soon

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

When we last met, we had these conclusions:

nikomatsakis (Mar 04 2019 at 19:02, on Zulip):

Maybe we can quickly check-in on how those went. I can speak to the first: @Taylor Cramer and I had a meeting, and we found some solutions to the problems that async await faces, -- the tl;dr is that we can desugar async fn differently, so we don't need to change anything "fundamental" here.

nikomatsakis (Mar 04 2019 at 19:03, on Zulip):

Specifically, the issue had to do lifetime capture in async fn.

nikomatsakis (Mar 04 2019 at 19:03, on Zulip):

That said, @Alexander Regueiro and I have been talking about still pursuing some solution to the so-called "captures problem" in impl Trait, even if it turns out not to be needed in this instance.

nikomatsakis (Mar 04 2019 at 19:04, on Zulip):

I think probably the thing to do there would be to schedule a meeting and try to talk out the problem.

nikomatsakis (Mar 04 2019 at 19:05, on Zulip):

As for the second bullet, exploring the use cases for lazy normalization -- I did a bit of this, as I wrote in this Zulip comment here. I reached out to a few folks. I concluded that the best thing would be to dig into and document better the flow of how normalization is working now. I didn't really have the time to finish that up last week, but I was hoping to schedule a recorded Zoom call to walk through it

nikomatsakis (Mar 04 2019 at 19:05, on Zulip):

I am not sure if I'll have time to do that exploration this week or not, but I'd still like to.

nikomatsakis (Mar 04 2019 at 19:06, on Zulip):

Third bullet (GATs) I think we had said @Aaron Turon and @centril might pursue?

Aaron Turon (Mar 04 2019 at 19:06, on Zulip):

For the third bullet, I ended up spending the week rewriting Tide and didn't dive into GATs yet

Aaron Turon (Mar 04 2019 at 19:06, on Zulip):

@centril after this meeting, let's set a time for you and I to dig into GATs this week

nikomatsakis (Mar 04 2019 at 19:07, on Zulip):

OK, I think I had mentioned that I had a use case or two and I forget, @centril, if I ever sent those to you

Aaron Turon (Mar 04 2019 at 19:07, on Zulip):

(i still think the stated goal is a good one)

nikomatsakis (Mar 04 2019 at 19:08, on Zulip):

If not, it's basically an "iterable" pattern, for iterating over the successors of graph nodes; you can see the traits here that the compiler uses, which basically work-around the lack of GATs by having auxiliary traits.

Aaron Turon (Mar 04 2019 at 19:08, on Zulip):

noted, thanks @nikomatsakis

nikomatsakis (Mar 04 2019 at 19:08, on Zulip):

OK, on to the fourth bullet -- Chalk integration -- well, @scalexm and I never scheduled a meeting, but I did schedule a different meeting that is relevant.

nikomatsakis (Mar 04 2019 at 19:09, on Zulip):

Specifically, tomorrow "around" this time -- see the rustc calendar -- is the "RLS 2.0 Type Checker Overview"

nikomatsakis (Mar 04 2019 at 19:09, on Zulip):

I'm thinking a lot about the idea of trying to integrate chalk into the RLS 2.0 system

nikomatsakis (Mar 04 2019 at 19:09, on Zulip):

As a quicker and less risky route to proving the system out

nikomatsakis (Mar 04 2019 at 19:10, on Zulip):

The meeting there is meant to cover how the RLS 2.0 system is currently handling types and type checking

nikomatsakis (Mar 04 2019 at 19:10, on Zulip):

But I think what I would like to shoot for is that we can establish a shared library to represent types

nikomatsakis (Mar 04 2019 at 19:10, on Zulip):

That is used by the chalk front-end (not rustc) and RLS 2.0

nikomatsakis (Mar 04 2019 at 19:10, on Zulip):

And then perhaps also share the "lowering" code in chalk between RLS 2.0 and chalk

nikomatsakis (Mar 04 2019 at 19:11, on Zulip):

So that we have dramatically more code sharing

nikomatsakis (Mar 04 2019 at 19:11, on Zulip):

With the hope that -- eventually -- rustc could be ported to share these libraries too

nikomatsakis (Mar 04 2019 at 19:11, on Zulip):

(Plus, eventually, that these libraries would be used to build a canonical type checker library that can be shared between RLS 2.0 and rustc)

nikomatsakis (Mar 04 2019 at 19:11, on Zulip):

Anyway, I think @scalexm plans to attend that RLS 2.0 meeting, and I suppose we'll try to schedule a follow-up to talk things out

nikomatsakis (Mar 04 2019 at 19:12, on Zulip):

I also had some other chalk-related thoughts over the weekend

nikomatsakis (Mar 04 2019 at 19:12, on Zulip):

One thing I was thinking is that we should try to find standard "logic programming" benchmarks and build harnesses that connect them to chalk-engine

nikomatsakis (Mar 04 2019 at 19:13, on Zulip):

so we can benchmark and optimize chalk-engine

nikomatsakis (Mar 04 2019 at 19:13, on Zulip):

independently from rustc and anything else

scalexm (Mar 04 2019 at 19:13, on Zulip):

Regarding GATs, maybe it would be worth reviewing the various logical rules we modeled in chalk before even trying to implement them in rustc, as I believe they correctly describe the « type-checking » rules and disclose the few corner cases

nikomatsakis (Mar 04 2019 at 19:13, on Zulip):

And I guess just that there remains some amount of refactoring etc that make sense to do on chalk itself, as we've said before.

nikomatsakis (Mar 04 2019 at 19:14, on Zulip):

Yeah, that makes sense to me -- I guess once we have some idea of the use cases, it would be good to try and evaluate those use cases on Chalk itself?

nikomatsakis (Mar 04 2019 at 19:14, on Zulip):

And talk out how it works?

nikomatsakis (Mar 04 2019 at 19:14, on Zulip):

I'm thinking a lot about the idea of trying to integrate chalk into the RLS 2.0 system

@scalexm I'm curious what you think about this direction, btw

scalexm (Mar 04 2019 at 19:15, on Zulip):

@nikomatsakis I think that’s a very good idea

nikomatsakis (Mar 04 2019 at 19:15, on Zulip):

OK, cool, for some reason I think I felt you were skeptical :)

nikomatsakis (Mar 04 2019 at 19:15, on Zulip):

But the more I think about it, the better I feel about it

scalexm (Mar 04 2019 at 19:15, on Zulip):

Hopefully it will help us refactor chalk so that its API is more user-friendly

scalexm (Mar 04 2019 at 19:16, on Zulip):

And eventually may help us integrate it in rustc

nikomatsakis (Mar 04 2019 at 19:16, on Zulip):

Right. It also helps to close a gap that RLS 2.0 has -- basically I think it's imperative that we are able to get RLS 2.0 up and going as fast as possible

nikomatsakis (Mar 04 2019 at 19:17, on Zulip):

So that we can kind of sell it as a reasonably full featured (if experimental) alternative to RLS 1.0

nikomatsakis (Mar 04 2019 at 19:17, on Zulip):

I guess we'll see how far we get in the meeting tomorrow; we can talk follow-up plans after that

nikomatsakis (Mar 04 2019 at 19:18, on Zulip):

OK, so that's 18 minutes in, I guess we should turn to what we plan to do this week. I'm guessing to some extent we'll continue the same basic goals as last week.

Aaron Turon (Mar 04 2019 at 19:18, on Zulip):

SGTM -- I do have one additional item to raise

Aaron Turon (Mar 04 2019 at 19:19, on Zulip):

which is that Derek Dreyer has a potential research intern and is considering trying to have them do something with Chalk

Aaron Turon (Mar 04 2019 at 19:19, on Zulip):

but needs help figuring out whether that would make sense

Aaron Turon (Mar 04 2019 at 19:19, on Zulip):

@nikomatsakis i know you're extremely busy, but would you be interested in joining that discussion? if not, could spend a couple minutes here brainstorming

Aaron Turon (Mar 04 2019 at 19:19, on Zulip):

(he was hoping to chat about this today or tomorrow)

nikomatsakis (Mar 04 2019 at 19:20, on Zulip):

What do you mean "joining"? Ah, ok

nikomatsakis (Mar 04 2019 at 19:20, on Zulip):

Not sure if I'll have time today/tomorrow

nikomatsakis (Mar 04 2019 at 19:20, on Zulip):

What kind of tasks did he have in mind?

nikomatsakis (Mar 04 2019 at 19:20, on Zulip):

I could imagine this person working on the specialization stuff

nikomatsakis (Mar 04 2019 at 19:20, on Zulip):

(for example)

Aaron Turon (Mar 04 2019 at 19:20, on Zulip):

yeah -- i think it would need to hew toward the theoretical

Aaron Turon (Mar 04 2019 at 19:21, on Zulip):

here's what i initially wrote him

nikomatsakis (Mar 04 2019 at 19:21, on Zulip):

Or perhaps trying to prove soundness of things like implied bounds (@scalexm did some preliminary proofs, but we could make them tighter)

Aaron Turon (Mar 04 2019 at 19:21, on Zulip):

## Theory

## Implementation

Aaron Turon (Mar 04 2019 at 19:21, on Zulip):

ok, so we can add specialization + implied bounds

nikomatsakis (Mar 04 2019 at 19:22, on Zulip):

There remain some sticky issues around recursive trait implementations

I don't know exactly what this means

Aaron Turon (Mar 04 2019 at 19:22, on Zulip):

ah sorry, that was meant to refer to the old auto trait issues and how they interacted with implied bounds -- i wasn't sure if that's now fully settled or if there's more we'd like to understand

nikomatsakis (Mar 04 2019 at 19:22, on Zulip):

I guess what I was talking about (soundness of implied bounds) probably fits under this heading:

Once we have a theory of the underlying logic established, we could go on to study the trait system as elaborated into that underlying logic.

nikomatsakis (Mar 04 2019 at 19:23, on Zulip):

ah sorry, that was meant to refer to the old auto trait issues and how they interacted with implied bounds -- i wasn't sure if that's now fully settled or if there's more we'd like to understand

I see. Well, I still feel like there are some "question marks" in my mind, especially around inductive/co-inductive reasoning

nikomatsakis (Mar 04 2019 at 19:23, on Zulip):

Right now we use a mix, for example, which I'm not crazy about. And there are times when you would really like co-inductive reasoning everywhere -- e.g. to enable so-called "perfect derive"

nikomatsakis (Mar 04 2019 at 19:24, on Zulip):

But we'd need to address the soundness problems there, particularly (only?) when you add implied bounds to the mix

Aaron Turon (Mar 04 2019 at 19:24, on Zulip):

OK, it sounds like my initial response was at least in the ballpark; i should be able to elaborate it out with him this week, and then if the intern ends up happening we can work out a specific project

nikomatsakis (Mar 04 2019 at 19:24, on Zulip):

Yeah, I think that's right

tmandry (Mar 04 2019 at 19:24, on Zulip):

One question related to async-await.. at the all-hands someone mentioned a solution to async fn in traits "without GATs"... has that effort basically morphed into the effort to implement GATs in rustc without chalk, or is it a separate ongoing effort? (or did I misunderstand?)

scalexm (Mar 04 2019 at 19:25, on Zulip):

Auto traits are a weird thing indeed, notably we can form cycles of the form p :- q :- p where p is co-inductive and q is not; we currently reject these cycles, but I remember that in the original co-induction paper, programs which exhibit these kinds of cycles are considered ill-formed

scalexm (Mar 04 2019 at 19:25, on Zulip):

Maybe that « works » in our setup because indeed auto traits are very simple predicates with no super traits etc

nikomatsakis (Mar 04 2019 at 19:25, on Zulip):

Maybe that « works » in our setup because indeed auto traits are very simple predicates with no super traits etc

well this is partly why they have no supertraits, I think

scalexm (Mar 04 2019 at 19:26, on Zulip):

But I’m definitely not sure we have solved all the theoretical issues around them

nikomatsakis (Mar 04 2019 at 19:26, on Zulip):

but indeed that's the sort of thing where I feel like we could have a "crisper" statement of what we want

scalexm (Mar 04 2019 at 19:26, on Zulip):

Yes

nikomatsakis (Mar 04 2019 at 19:26, on Zulip):

One question related to async-await.. at the all-hands someone mentioned a solution to async fn in traits "without GATs"... has that effort basically morphed into the effort to implement GATs in rustc without chalk, or is it a separate ongoing effort? (or did I misunderstand?)

@tmandry we haven't really talked about this here; I think it was @boats pondering whether it would be possible (or desirable) to try and support async fn in traits. The idea would basically be to sort of "hard-code" the GAT in question in the compiler. I haven't thought very much about whether this makes sense and what would be needed on the impl side.

nikomatsakis (Mar 04 2019 at 19:27, on Zulip):

that said, we effectively do a similar thing for all methods now

nikomatsakis (Mar 04 2019 at 19:27, on Zulip):

e.g.,

trait Foo {
  fn bar<T>(); // <-- since each method has a unique type, this is a kind of GAT
}
nikomatsakis (Mar 04 2019 at 19:28, on Zulip):

so I think the idea was that perhaps we could handle async fn in a similar way

nikomatsakis (Mar 04 2019 at 19:28, on Zulip):

in the compiler, this is done by having a TyFnDef item whose substitutions (substs) include the values for the method's type parameters

nikomatsakis (Mar 04 2019 at 19:28, on Zulip):

so you might imagine having a sort of TyFnFuture for async fn or something

nikomatsakis (Mar 04 2019 at 19:28, on Zulip):

kind of a built-in concept that we only handle and resolve during trans process

nikomatsakis (Mar 04 2019 at 19:29, on Zulip):

I'm kind of luke-warm on the idea. It might make sense, but it's not the overall direction I want rustc's type system to be moving

nikomatsakis (Mar 04 2019 at 19:29, on Zulip):

which is fewer "special cases"

nikomatsakis (Mar 04 2019 at 19:29, on Zulip):

OTOH I would like async fn in traits :P

tmandry (Mar 04 2019 at 19:29, on Zulip):

makes sense

nikomatsakis (Mar 04 2019 at 19:32, on Zulip):

So plans for this week are:

nikomatsakis (Mar 04 2019 at 19:33, on Zulip):

I don't love how many things have my name on there ;) I'm curious if we can find someone who has time to kind of "own" chalk

nikomatsakis (Mar 04 2019 at 19:33, on Zulip):

Let me rephrase that

nikomatsakis (Mar 04 2019 at 19:33, on Zulip):

Not own chalk as a whole, but to help organize and guide refactorings on the chalk codebase especially

nikomatsakis (Mar 04 2019 at 19:33, on Zulip):

but I think we probably want to work through the RLS 2.0 integration stuff a bit more to have a better idea what we have planned

Aaron Turon (Mar 04 2019 at 19:34, on Zulip):

yeah -- I was gonna say, I'd be willing/able, but it depends a bit what direction we go with for GATs

nikomatsakis (Mar 04 2019 at 19:34, on Zulip):

Does anyone have any other things they are interested in adding to that list of trait wg goals for the week?

Aaron Turon (Mar 04 2019 at 19:34, on Zulip):

(i.e. whether it makes more sense for me to focus on rustc or Chalk for now)

nikomatsakis (Mar 04 2019 at 19:34, on Zulip):

Yeah, let's let it sit for a bit

nikomatsakis (Mar 04 2019 at 19:34, on Zulip):

I think there's still a bit of uncertainty in my mind about that

Aaron Turon (Mar 04 2019 at 19:35, on Zulip):

yeah, so i think focusing this week on getting more clarity on that question will be really helpful

Aaron Turon (Mar 04 2019 at 19:35, on Zulip):

or like, questions around Chalk direction in general (both RLS and GAT approach)

Aaron Turon (Mar 04 2019 at 19:35, on Zulip):

after we collect GAT usage I'll start up a thread here to start talking about whether it makes sense to massage rustc ahead of Chalk integration or not

nikomatsakis (Mar 04 2019 at 19:36, on Zulip):

Yeah

Aaron Turon (Mar 04 2019 at 19:38, on Zulip):

thanks @nikomatsakis!

nikomatsakis (Mar 04 2019 at 19:39, on Zulip):

OK, great. I expect that for the rest of the day I'm going to be working mostly on Roadmap RFC edits, but I may try to put in a more time on the lazy norm stuff -- I'm thinking about maybe trying to make a goal of being able to walk through how norm works on Friday

nikomatsakis (Mar 04 2019 at 19:39, on Zulip):

Thanks all! <3

nikomatsakis (Mar 04 2019 at 20:27, on Zulip):

Minutes posted to internals and compiler-team repo

Alexander Regueiro (Mar 04 2019 at 20:39, on Zulip):

That said, Alexander Regueiro and I have been talking about still pursuing some solution to the so-called "captures problem" in impl Trait, even if it turns out not to be needed in this instance.

yeah sounds good. let me know when you want to discuss tthat.

Alexander Regueiro (Mar 04 2019 at 20:40, on Zulip):

and sorry, wg-traits meetings aren't the best time for me. usually around dinnertime...

centril (Mar 05 2019 at 06:38, on Zulip):

FCP for type Foo = impl Bar; is done...
I've started a gist for @Alexander Regueiro in https://gist.github.com/Centril/2470b7f89657da457ed25078a9cdab72 but it still needs a lot of work.
Happy to work with @Aaron Turon this week on GATs but I missed this meeting so we'll need to reschedule.

Aaron Turon (Mar 05 2019 at 19:01, on Zulip):

@centril will you have some time tomorrow?

centril (Mar 05 2019 at 19:02, on Zulip):

@Aaron Turon what time-ish?

Aaron Turon (Mar 05 2019 at 19:03, on Zulip):

@centril sometime after 1pm pacific? is that too late for you?

centril (Mar 05 2019 at 19:04, on Zulip):

I have a WG-Grammar meeting at 20:00-20:50 and then a T-Release meeting at 23:30-00:00; otherwise I'm free

centril (Mar 05 2019 at 19:04, on Zulip):

@Aaron Turon that is 22:00 CET which is just perfectly in the middle

Aaron Turon (Mar 05 2019 at 19:05, on Zulip):

@centril awesome, i'll put something on our calendars

centril (Mar 05 2019 at 19:05, on Zulip):

@Aaron Turon much obliged

Last update: Nov 12 2019 at 16:40UTC