Conversation

Brendan Zabarauskas
@brendanzab
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
3
3
Kristopher Micinski
@krismicinski
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.
1
Brendan Zabarauskas
@brendanzab
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`
1
1