Bottom-up rewriting with smart constructors, hereditary substitution & normalization by evaluation: julesjacobs.com/notes/smartcon
Conversation
Replying to
Is your definition of NbE a bit more narrow than mine? I use a closure-converted form, for example, with De Bruijn levels in neutral values. I've also seen strings used in place of levels in other implementations of NbE.
I dunno if this is related at all? 🤔
Quote Tweet
Almost like NbE is a bit like 'lazy closure conversion + partial evaluation' perhaps…?
I'm pretty bad at theory stuff, so it's likely I'm wrong about this, misunderstanding, or that you are already aware! Just thought I'd mention it in case it's of any use! 
Show this thread
1
1
I think normalization under lamdbas is related to partial evaluation, and furthermore typed NbE seems indeed related to type directed partial evaluation. I'd also like to know what the exact correspondence is, let me know if you find out!
1
1
Show replies
Replying to
Yes, possibly :) My current thinking is that which representation you use for binders is an orthogonal choice (HOAS / De Bruijn levels|indices / strings). I think the simplest formulation is obtained when you use HOAS for the initial terms as well as the semantic terms.
1
2
But you can also not use HOAS at all, as in hereditary substitution. Separate from this choice is another choice of how to represent semantic values: you can use a representation more tailored to normal forms. For instance for untyped NbE you can define neutral/normal data types.
2
1
Show replies
“Closure-converted NbE” is definitely a thing (used by e.g. Abel) and the term seems to generates vigorous* reactions in people** who are only used to “normal” NbE.
*almost wrote “violent”
**including me a while ago
1
2
What is “normal” NbE? Are you saying people felt weoird about the term “Closure-converted NbE”, or the people using “Closure-converted NbE” calling what they are doing “NbE”? More just curious to know the history that I am stumbling into!
1
Show replies