Conversation

In my implementation of normalisation by evaluation, I have two partial functions: f₁ : Env × Term → Value f₂ : Level × Value → Term What should I call them? I'd love to know why, if possible!

reflect, reify
20%
eval, readback
17.1%
eval, quote
62.9%
other (please write)
0%

35 votesFinal results

12:41 AM · Aug 31, 2021Twitter Web App

Replying to

Thanks for votes so far! Seems like lots of people like ‘eval, quote’! Curious to hear about people's reasoning (if they have any, that is). Have I been making a mistake in using ‘eval, readback’ in my stuff? 🤔

Replying to

sorry for being naive here, but what is level here? how is f1 not just interpretation as a (say) C,E (control, environment) machine? I guess the idea is these are mutually recursive, but not sure what level is here.

Brendan Zabarauskas

@brendanzab

Aug 31, 2021

No worries! Sorry for being unclear. It is the de Bruijn level of the environment. I'm using de Bruijn indices in my terms and levels in my values. The level of the environment lets you convert the levels in the values back to indices using `envLevel - varLevel + 1`

Show replies

You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more

Brendan Zabarauskas

@brendanzab

Aug 31, 2021

Thanks a bunch! I think I might switch to ‘quote’, actually - mainly for aesthetics I think! 😅 Yeah reify/reflect still seems to be on the Wikipedia article, alas! I think you mentioned something along these lines in your NbE paper?

en.wikipedia.org

Normalisation by evaluation - Wikipedia