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?
2
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
For example It'd be cool to have things like:
⊢ { A : Type, a : A } = { a : A, A : Type }
⊢ { a = b, A = Int, b = 3 } : { A : Type, a : A, b : A }
f : { A : Type, a : A, b : A } → A ⊢ f { b := 3 } : { a : Nat } → Int
Pretty bad examples though 😅