Stream: t-compiler/rust-analyzer

Topic: Formalizing name resolution


matklad (Dec 07 2020 at 10:59, on Zulip):

This is a topic to discuss what mathematical models exists for name resolution. Some links:

cc @Brendan Zabarauskas

Overall mood: https://twitter.com/graydon_pub/status/1052359170601566210

Brendan Zabarauskas (Dec 07 2020 at 11:06, on Zulip):

Fwiw I've moved away from using Moniker on Pikelet - I now use a 'trick' called semantic type checking that combines de Bruijn levels and de Bruijn indices for fast evaluation… Locally Nameless just wasn't pulling it's weight for an actual implementation of dependent type theory. Like a lot of things it depends on the context, and what you are trying to do. Name binding is a frightening rabbit warren of a topic.

Brendan Zabarauskas (Dec 07 2020 at 11:09, on Zulip):

The scope graph stuff is suuper interesting though - I haven't looked to deeply into it though, simply because it wasn't super useful for what I want, which is fast evaluators for dependent type checkers. I'll see if I can remember any more interesting things I've seen.

Brendan Zabarauskas (Dec 07 2020 at 11:11, on Zulip):

There's was interesting work on contextual modal type theory (most seen in the Beluga theorem prover).

Brendan Zabarauskas (Dec 07 2020 at 11:12, on Zulip):

I had some links in this issue on Pikelet: Move away from using Moniker for variable binding - but this was more in relation to dependent type checking.

Brendan Zabarauskas (Dec 07 2020 at 11:13, on Zulip):

"Name Binding is Easy with Hypergraphs" might be interesting.

matklad (Dec 07 2020 at 11:14, on Zulip):

I have a super high-level question:

One of the most interesting bits of Rust's name res is the "fixed point iteration" thing. Ie, things like

mod a {
  use b::x as y;
}
mod b {
   use a::y as z;
    struct x;
}

Are there models which handle that? Or are there models only for stack of scopes?

Brendan Zabarauskas (Dec 07 2020 at 11:15, on Zulip):

Oooooh yeah that looks closer to the Spoofax scope graph stuff

Brendan Zabarauskas (Dec 07 2020 at 11:17, on Zulip):

Like, I'm not sure if it can handle it - there's been continued work since that paper you linked, but it might be worth trying it out, or even extending it to support it? Like, if it's a student project you could even use the spoofax workbench to make up a prototype?

Brendan Zabarauskas (Dec 07 2020 at 11:18, on Zulip):

http://www.metaborg.org/en/latest/

matklad (Dec 07 2020 at 11:21, on Zulip):

Yeah, that'd be fun!

Brendan Zabarauskas (Dec 07 2020 at 11:21, on Zulip):

I think the relevant part of it is Static Semantics Definition with NaBL2? Could be wrong though, I only have a vague understanding that the theory of name resolution/scope graph stuff is used in there.

matklad (Dec 07 2020 at 11:21, on Zulip):

Although the end goal is to arrive at the production impl of the name resolution, as the current three versions (rustc, rust-analyzer, intellij) are all a bit of a mess

matklad (Dec 07 2020 at 11:22, on Zulip):

Heh, the docs do not inspire confidence: http://www.metaborg.org/en/latest/source/langdev/meta/lang/nabl2/introduction.html#name-resolution-with-scope-graphs

Brendan Zabarauskas (Dec 07 2020 at 11:22, on Zulip):

HAHA oh dear

Brendan Zabarauskas (Dec 07 2020 at 11:22, on Zulip):

yeah you would probably have to look at the examples or something sadly

Brendan Zabarauskas (Dec 07 2020 at 11:23, on Zulip):

researchware is always fun

matklad (Dec 07 2020 at 11:24, on Zulip):

Production-ready compilers are no less fun, sadly :D

Brendan Zabarauskas (Dec 07 2020 at 11:24, on Zulip):

I think this might be the implementation? https://github.com/metaborg/nabl

Brendan Zabarauskas (Dec 07 2020 at 11:26, on Zulip):

They have a funny eclipse IDE thing that you can define languages in using these DSLs

Brendan Zabarauskas (Dec 07 2020 at 11:26, on Zulip):

I think I've seen demos in videos of Elco Visser playing around

matklad (Dec 07 2020 at 11:27, on Zulip):

HAHA oh dear

Added appropriate tweet to the first message in the thread

Brendan Zabarauskas (Dec 07 2020 at 11:27, on Zulip):

amazing!

Brendan Zabarauskas (Dec 07 2020 at 11:28, on Zulip):

I remember that tweet

Brendan Zabarauskas (Dec 07 2020 at 11:30, on Zulip):

You can probably find videos if you search for Elco Visser if that's more consumable (I often find it a bit easier than launching into papers first, but I'm weird).

Brendan Zabarauskas (Dec 07 2020 at 11:30, on Zulip):

I think he's the main researcher working on this stuff if you are looking for somebody to chat to: https://eelcovisser.org/

Brendan Zabarauskas (Dec 07 2020 at 11:32, on Zulip):

/me remembers the days when cyclic imports would crash the rust compiler

Brendan Zabarauskas (Dec 07 2020 at 11:36, on Zulip):

I wonder if there's anything in the mutually recursive module system stuff (in ML land) that might be of use

Brendan Zabarauskas (Dec 07 2020 at 11:37, on Zulip):

Might be a bit focused on a specific language feature than a more general theory though

matklad (Dec 07 2020 at 11:38, on Zulip):

Heh, I wish we just didn't do this at all. Makes writing fast IDE a pain in the back (as it precludes map-reduce approach: https://rust-analyzer.github.io/blog/2020/07/20/three-architectures-for-responsive-ide.html#map-reduce)

Brendan Zabarauskas (Dec 07 2020 at 11:41, on Zulip):

yeah, seems rather frustrating :cry:

Brendan Zabarauskas (Dec 07 2020 at 11:43, on Zulip):

So yeah, dunno if any of this has helped at all! I do think you might be on the right track with the scope graph stuff - I'm just not sure how close it would be to getting it to getting it to a production implementation

matklad (Dec 07 2020 at 11:44, on Zulip):

This all is definitely very helpful!

Brendan Zabarauskas (Dec 07 2020 at 11:44, on Zulip):

Like, does it support the fixed point stuff you want, and how do you get it to work for a responsive, incremental compiler.

matklad (Dec 07 2020 at 11:44, on Zulip):

Even if it turns out to be a negative resul in the end with respect to actual impl D

Brendan Zabarauskas (Dec 07 2020 at 11:45, on Zulip):

Yeah, still always good to have people looking at this stuff, and sometimes interacting with the researchers, showing them potential use cases/applications that they might not have thought of.

lqd (Dec 07 2020 at 11:49, on Zulip):

(the scope graphs parts have dedicated papers and implementations, + talks & videos eg https://eelcovisser.org/talks/2017/06/20/scope-graphsa-fresh-look-at-name-binding-in-programming-languages/)

Brendan Zabarauskas (Dec 07 2020 at 11:50, on Zulip):

yeah, papers+implementations are always super nice and handy!

lqd (Dec 07 2020 at 11:51, on Zulip):

(fun fact I somehow watched your compose talk yesterday Brendan :)

Brendan Zabarauskas (Dec 07 2020 at 11:51, on Zulip):

oh no!

Brendan Zabarauskas (Dec 07 2020 at 11:52, on Zulip):

hahah :)

Brendan Zabarauskas (Dec 07 2020 at 11:53, on Zulip):

I did finally come up with a name in the year or so since that talk https://github.com/yeslogic/fathom

(and also figured out a bunch of nasty snags that I glossed over in there, hoping one day I might be able to do a follow up talk on it)

lqd (Dec 07 2020 at 11:55, on Zulip):

Brendan Zabarauskas said:

They have a funny eclipse IDE thing that you can define languages in using these DSLs

that's "Spoofax" ^^

Brendan Zabarauskas (Dec 07 2020 at 11:56, on Zulip):

have you played around with Spoofax before?

lqd (Dec 07 2020 at 11:56, on Zulip):

(ah you've all already mentioned everything here sorry)

lqd (Dec 07 2020 at 11:57, on Zulip):

I haven't but I've read a couple papers, such as the scope graphs and more, and I've seen conference tutorials and talks from Eelco and students

lqd (Dec 07 2020 at 11:57, on Zulip):

(including one where he hopes to model Haskell in Spoofax, and SPJ seemed interested :)

matklad (Dec 07 2020 at 11:58, on Zulip):

@Brendan Zabarauskas have you seen https://github.com/GaloisInc/daedalus? Seems to be roughly in the same spot as fathom, from the cursory look at it.

Brendan Zabarauskas (Dec 07 2020 at 11:58, on Zulip):

oooh, not seen that one

Brendan Zabarauskas (Dec 07 2020 at 11:59, on Zulip):

I'm aware of Kaitai, Nacissus, Everpass/QuackyDucky

lqd (Dec 07 2020 at 12:00, on Zulip):

daedalus seems new, I wonder if David Christiansen didn't mention it somewhere

Brendan Zabarauskas (Dec 07 2020 at 12:00, on Zulip):

and there are some interesting ones for lisp and Dylan

Brendan Zabarauskas (Dec 07 2020 at 12:01, on Zulip):

yeah this looks pretty close

Brendan Zabarauskas (Dec 07 2020 at 12:03, on Zulip):

Wonder if the can unparse as well :thinking:

Brendan Zabarauskas (Dec 07 2020 at 12:05, on Zulip):

OOOH lol the PDF stuff will be interesting for YesLogic

lqd (Dec 07 2020 at 12:14, on Zulip):

(if you want to prototype some rust-like rules to validate/invalidate the scope graphs approach, https://eelcovisser.org/talks/2020/06/16/spoofax-tutorial-at-pldi/ was the "tutorial" I remember watching as well)

okterakt (Dec 08 2020 at 13:44, on Zulip):

The work on scope graphs is indeed interesting and the nice thing is that it seems somewhat extensible, at a first glance at least. Does anyone know of other relevant papers on the topic? Most of what I've been able to find is related to Eelco Visser's work.

Last update: Jul 24 2021 at 21:00UTC