## 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

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):

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

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