Any idea why a pure debruijn approach was used, as opposed to something like locally nameless? (Just curious)
Conversation
They don’t quite say, but I’m not sure LN is warranted at this point (other than complexity with multi-sorted syntaxes). I also don’t kmow if sigma-calculus still works for LN (you need to adapt it, but is the result a confluent, terminating and complete rewrite system?)
1
1
Yeah, just curious mainly because I'm using it in my Moniker library: github.com/brendanzab/mon (it's based on Unbound). One of my current annoyances is that it seems like it is getting in the way of me moving toward a visitor-based approach in Pikelet: github.com/pikelet-lang/p
1
By 'sigma-calculus' do you mean the specific explicit substitution calculus that they are using in austosubst? Kind of curious if explicit substitutions could get me out of my visitor woes... by allowing me to delay applying the substitutions as I traverse... 🤔
1
1
That’s the name they use. But I’m not familiar with all the variants of sigma-calculus; if you add beta-reduction, some variants lose strong normalization, and I’ve never browsed the relevant literature as it’s not gentle. ps.uni-saarland.de/Publications/d has pointers.
1
Yeah, I found delving into all the variants of naming and substitution and autobinding and explicit substitutions and scope graphs and director strings and indices and levels and.... arrrgh.... super overwhelming.
1
1
Hence me just porting Unbound which was confusing in itself (hopefully I managed to simplify and clarify some things in the process).
1
And this is all *with* skipping the proofs and stuff because I haven't really got to grips with all that stuff yet.
1
1
I was pretty thankful for Charguéraud's "The Locally Nameless Representation", which was a great help early on: chargueraud.org/research/2009/
1
1
Yep, it's a very good tutorial, one of the best thing going for LN (I was also happy they have an actual proof scripts since they omit some proof details — such as generalizing the statement to make the induction go through).
1
1
Replying to
Heh, yeah I do actually forget it’s actually kind of a tutorial for LN as well. I was just using it as a tute for learning the technique itself!
One of the cool things it also covers is pattern matching. Alas I didn’t find any examples of implementing pattern matching with autosubst... 🤔
1
Never gotten to that part, but pattern matching seems just another set of binders, no? Oh, not sure how to annotate that for autosubst tho...
2
Show replies