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

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

Brendan Zabarauskas

@brendanzab

Replying to

@jonmsterling

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

12:48 PM · Aug 31, 2021Twitter Web App