Stream: t-compiler/wg-rls-2.0

Topic: understanding type checker


nikomatsakis (Feb 25 2019 at 15:05, on Zulip):

So @Florian Diebold, we were talking and we realized that it'd be great to sync up a bit more about what you've been doing with respect to the type checker in rust-analyzer. I'm particularly interested in the idea of sharing code between chalk and rust-analyzer (and eventually rustc). This would probably mean sharing (to start) the representation of types and the logic for lowering a traits + impls into logical rules (and of course the chalk solver itself). In the meantime, the idea would be that rust-analyzer continues to kind of "explore" what a new type checker impl might look like (I have thoughts on that, but also want to understand first what you've been up to) and then we try to bridge what rustc has + what rust-analyzer has to create a spec / shared library at some point in the future

nikomatsakis (Feb 25 2019 at 15:06, on Zulip):

To that end I was going to propose that maybe we should do some of the following steps (not necessarily in this order =):

1. recorded walkthrough of what rust-analyzer has implemented
2. recorded walkthrough of how rustc type checker works
3. some design discussion of how to ideas around how to represent types and maybe sketching out what a shared library would look like

I think this would potentially be a good source for collaboration with some folks from @WG-compiler-traits

nikomatsakis (Feb 25 2019 at 15:06, on Zulip):

What do you think? :)

Florian Diebold (Feb 25 2019 at 20:20, on Zulip):

Sure! We're actually at a point now where I've started thinking about how to handle traits and trying to understand rustc's trait solving in more detail, so it's good timing :) I think as far as the design of the type inference goes, I think it's actually not very far from the rustc implementation, only much simpler of course -- apart from the lots of missing features, the focus has been on type inference as opposed to checking so far, to get good enough information for completion and assists. (also, performance isn't a concern so far since we only need to type-check one function at a time :) )

nikomatsakis (Feb 25 2019 at 20:28, on Zulip):

@Florian Diebold ok two questions. First, would you be up for giving a little talk about what you've done so far? That is probably the easiest way for me to come to understand it more deeply :)

nikomatsakis (Feb 25 2019 at 20:28, on Zulip):

Nothing formal, i imagine basically a (Recorded) Zoom where you kind of walk through how some test case would get type-checked

nikomatsakis (Feb 25 2019 at 20:29, on Zulip):

and I (along with anyone else who is listening) interrupt you every 22 seconds to ask for clarifications :)

nikomatsakis (Feb 25 2019 at 20:29, on Zulip):

If you are up for that, what rough times work for you?

Florian Diebold (Feb 25 2019 at 20:37, on Zulip):

sure, I could probably do that. In general, on weekdays, after 8pm CET would work best for me, though I could maybe do after ~5pm if necessary depending on the situation at work

nikomatsakis (Feb 28 2019 at 18:19, on Zulip):

@Florian Diebold Hmm, I missed this message when you sent it, sorry.

Late CET is of course decent for me, since I'm in Boston -- that's basically my afternoon. Though I think there's some funny business around daylight savings time coming up, so I don't trust myself to get the conversion exactly right. How about you (and others who may be listening!) fill out this doodle poll and I'll do the same?

Florian Diebold (Feb 28 2019 at 18:58, on Zulip):

I was starting to wonder whether I should ping you ;) Filled out the doodle.

matklad (Mar 01 2019 at 07:18, on Zulip):

Let's ping @WG-rls2.0 about the poll in case anybody else is interested

nikomatsakis (Mar 01 2019 at 16:59, on Zulip):

ok, looking over this poll, I'm thinking Tuesday at 13:00 UTC-05:00 (Boston time) -- actually I may be off by an hour because of DST, but hopefully doodle got that right -- is a good match. It doesn't get everybody but no slot does.

nikomatsakis (Mar 01 2019 at 17:00, on Zulip):

or maybe 2 hours later, 15:00

nikomatsakis (Mar 01 2019 at 17:00, on Zulip):

I'm not sure whether "later" in CET time is better or worse :)

nikomatsakis (Mar 01 2019 at 17:02, on Zulip):

Seems like 15:00 in Boston is 21:00 in Paris on Mar 5

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

OK, let's do that.

davidtwco (Mar 01 2019 at 17:05, on Zulip):

Is 21:00 Paris time when the meeting starts or ends?

nikomatsakis (Mar 01 2019 at 17:08, on Zulip):

Actually, @scalexm, you around? We're discussing the idea of a meeting to discuss the RLS 2.0 type checker :point_up: and I am wondering if you are interested. More specifically, I've been meaning to ping you about chalk + RLS 2.0 integration.

nikomatsakis (Mar 01 2019 at 17:08, on Zulip):

I was thinking that it would be interesting to try and have chalk + rust-analyzer share a common library defining Rust types

nikomatsakis (Mar 01 2019 at 17:09, on Zulip):

(Though discussing that is not necessarily the point of this particular meeting)

scalexm (Mar 01 2019 at 17:12, on Zulip):

@nikomatsakis I’m about to take a train so not sure I’ll have internet access

nikomatsakis (Mar 01 2019 at 17:12, on Zulip):

I mostly was just curious if you were interested and if you had an opinion about the time

scalexm (Mar 01 2019 at 17:12, on Zulip):

Which time are you planning to do the meeting?

nikomatsakis (Mar 01 2019 at 17:12, on Zulip):

There is a doodle poll, but two likely times (Paris time) would be 19:00 or 21:00

nikomatsakis (Mar 01 2019 at 17:12, on Zulip):

Tuesday March 5

scalexm (Mar 01 2019 at 17:13, on Zulip):

Ah, yes 21:00 is good

scalexm (Mar 01 2019 at 17:13, on Zulip):

(I’m interested)

nikomatsakis (Mar 01 2019 at 17:14, on Zulip):

OK, great

nikomatsakis (Mar 01 2019 at 17:14, on Zulip):

we'll do that

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

(let me know if you want to be "invited", vs just subscribing to the whole calendar)

nikomatsakis (Mar 01 2019 at 18:02, on Zulip):

those both seem like fine times

nikomatsakis (Mar 01 2019 at 18:02, on Zulip):

Starts

nikomatsakis (Mar 01 2019 at 18:02, on Zulip):

OK, I've added an event to the compile team calendar

nikomatsakis (Mar 01 2019 at 18:02, on Zulip):

@scalexm sorry -- we are scheduling a meeting for next tuesday

nikomatsakis (Mar 01 2019 at 18:03, on Zulip):

I'm also game to do 13:00, which would mean starting at 19:00 in Paris

scalexm (Mar 01 2019 at 18:15, on Zulip):

@nikomatsakis I’m not sure to understand, so 21:00 Tuesday 5th does not work?

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

@scalexm oh sorry, no 21:00 is fine

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

and I added that time to the calendar

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

it seems like somehow you got some old messages resent?

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

(that is, Zulip seems to have sent them out of order or something, not sure)

scalexm (Mar 02 2019 at 16:05, on Zulip):

@nikomatsakis Ah yes it was probably that

scalexm (Mar 05 2019 at 20:03, on Zulip):

@nikomatsakis I might be just a few minutes late for the meeting, got out of work late

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

Hi @WG-rls2.0, @WG-compiler-traits -- we're about to start (on Zoom) the "understanding ttpe checker" meeting

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

it'll be recorded, too

Igor Matuszewski (Mar 05 2019 at 20:07, on Zulip):

That’s great to hear! In the end I can’t participate tonight but I’d mostly want to understand what’s going on and wouldn’t be able to significally contribute, so no loss there I believe

Igor Matuszewski (Mar 05 2019 at 20:07, on Zulip):

Thanks for recording it!

davidtwco (Mar 05 2019 at 20:51, on Zulip):

Thanks @Florian Diebold and @nikomatsakis, that was very interesting.

nikomatsakis (Mar 05 2019 at 20:52, on Zulip):

:tada:

nikomatsakis (Mar 05 2019 at 20:52, on Zulip):

I've got a lot of videos to post, going to try and get them done today, links to come!

nikomatsakis (Mar 05 2019 at 20:53, on Zulip):

/me has basically spent all day recording interesting talks

nikomatsakis (Mar 05 2019 at 20:53, on Zulip):

not a bad way to spend a day

detrumi (Mar 05 2019 at 20:53, on Zulip):

Would be great, I just missed it (there's a calendar for this stuff right?)

nikomatsakis (Mar 05 2019 at 20:54, on Zulip):

@detrumi yes, calendar is here

blitzerr (Mar 06 2019 at 00:28, on Zulip):

@nikomatsakis would it make sense to have one stream or topic on zulip where we post the lecture video link once you complete uploading ? That way we can have one stop shop for all the treasures. I want thank people for taking time to prepare for this and Niko to organize, encode post and most of all coming up with the idea. This is excellent knowledge bank.

Jeremy Kolb (Mar 06 2019 at 13:17, on Zulip):

@nikomatsakis will you post the video here when it's ready?

nikomatsakis (Mar 06 2019 at 14:57, on Zulip):

Video posted

nikomatsakis (Mar 06 2019 at 14:57, on Zulip):

@blitzerr I do feel lke we need some better way to track and announce new videos.

David Laban (Mar 17 2019 at 13:17, on Zulip):

Thanks for posting the recording.

I found that the talk existed via the calendar at https://github.com/rust-lang/compiler-team#meeting-calendar and then searched zulip around March 5th to find this thread.

To make this better, you could add the recording links to the calendar events. Alternatively, you could add a link to the discussion thread when you make the calendar event, and then post the video to the thread. That would make the video easy to find as well, and doesn't need you to edit the calendar event.

Last update: Nov 19 2019 at 19:00UTC