One of these days I want to give a compiler talk called "name lookup is the absolute worst" that's just 100 slides of screaming goat memes.
Conversation
As a counter-point, what language(s) would you say have "good" name lookup rules, where "good" ?= easy and convenient for the programmer as well as the implementer?
1
Possibly Forth. Or APL or something. Combinatory forms rather than binding forms.
2
5
Name binding is so frustrating arrrgh
1
1
I even made a thing for this, but it's slowww github.com/brendanzab/mon - was thinking of going nominal and using visitors like in Visitors Unchained… that way I can fuse traversals together… but apparently you pay for it in other ways. 😭
3
2
2
Unfortunately there are several additional name lookup dimensions in many languages that don’t even have particularly clear concepts of a binding scope. Like they fade in or out depending on types & overloads & extension structure & order & ambiguity & goodness knows what else.
1
1
Replying to
Indeed. That's where stuff really becomes fun and messy. Kind of almost want to do some of that stuff in the elaborator? But then you also need to think of how you want to do support for incrementalism and editors...
But yeah, I'm just trying to avoid that kind of thing as much as I can for now!
1
My advice: keep the rules as minimal and simple as you can, as long as you can. When someone complains that they want some new naming sugar, reject on the grounds that it’ll mess up all your proofs, then point to a git repo full of random unrelated coq code.
1
6
Show replies