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
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.
3
6
I'm not familiar with using NbE directly for formalizing syntax, I'll have to look into it!
1
1
Replying to
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).
Is your goal just formalizing the syntax? I'd assume you'd need to deal with stuff like conversion checking in a formalization of Agda's core?
1
I guess in looking back at your post, it seems you are mainly focused on syntactic concerns. In that case I think I might be confusing things by bringing up NbE… Sorry! 😅