New blog post: Scope Sets as a Piñata for Name Resolution.
typesanitizer.com/blog/scope-set
I describe what scope sets are about, why I think they're cool, how you could use them to implement a name resolution library, and more.
4
10
21
Conversation
Really cool post! I'm wondering if this could be used for dependently typed languages somehow? I'm guessing that Would need to figure out a good evaluation and conversion checking algorithm though… 🤔
1
A big thing I want to be able to do is be more flexible about permutations on application order and field order in dependent function and record types respectively. Wondering if this could help?
Would also be interested in how fast this could be made - I would assume that using high level hash sets with strings would be rather slow - would it be possible to use bit sets and stuff to make this more speedy. 🤔
1
For perf, there are many options. Intern identifiers. Scopes are unique integers. Intern scope sets. Cache lookup results. Cache subset check results. There's also the question of multithreading. I don't have a good sense of where the bottlenecks would be.
1
Replying to
Without more details it's hard to tell, that sounds like it'd very much depend on how your typing judgements are set up... That said, the paper does discuss recursive definition contexts, so the system can certainly handle those.
1
I guess the complication I'm having right now is how I'm using debruijn indices+levels for my NbE -based elaborator. It's very quick for elaboration, but makes being flexible with the ordering of binders tricky. Dunno if sets of scopes helps or hinders here…
1
Show replies