Do you want to define syntax with binders in Agda but have no idea whether to use de Bruijn indices, nominal sets, HOAS, or yet something else?
Well then, good news! I have a new blog post for you: jesper.sikanda.be/posts/1001-syn
4
40
133
Conversation
Replying to
Super great overview, thanks for this! I'm still pretty happy with defunctionalized NbE (with indices in terms and levels in values). Makes implementation much easier, and is good for performance, but I dunno how it fares for formalization work.
The reason I mention it is that I wasted a lot of time with trying to use locally nameless, but it turns out NbE makes things so much easier when implementing type systems! I dunno if it would fit into your post anywhere though. 😅
2
What does it mean to be defunctionalised NBE? Does that refer to your encoding of closures?
1
Referring to how it is described in “Implementing a Modal Dependent Type Theory”, section 3.1: jonmsterling.com/pdfs/modal-mlt – but I might be misusing the term. I think I'm more just referring to the approach described in Abel's habilitation thesis: cse.chalmers.se/~abela/habil.p
5
Replying to
I'm not familiar with using NbE directly for formalizing syntax, I'll have to look into it!
1
1
Yeah I'm not too clear on the details either. NbE is weird because it involves syntax and semantics. I think on the syntax side you can use de Bruijn indices, although NbE is not really tied to that. Indices can be good for performance though (in implementations that is).
1
1
Show replies