The Wikipedia article suggests that NbE is a technique for obtaining "the normal form of terms" by translating the object language into abstractions of the meta (host) language:
The denotational semantics of (closed) terms in the meta-language interprets the constructs of the syntax in terms of features of the meta-language; thus, lam is interpreted as abstraction, app as application, etc.
One consequence is that we are now restricted to use Higher-Order Abstract Syntax (HOAS) to represent lambda terms, since De Bruijn indices and named representations are formally not "features" of the host language, e.g., Haskell. That article uses HOAS, accordingly.
Another publication (or rather a tutorial) called "Checking Dependent Types with Normalization by Evaluation: A Tutorial", however, uses a bit different approach; in particular, it employs string variable identifiers instead of HOAS and a so-called "closure" construction, which is essentially a lambda abstraction packaged up with all the free variables occurring in its body:
| VAdd1 Value
| VClosure (Env Value) Name Expr
| VNeutral Ty Neutral
Another thing to note is that the closure's body is not fully evaluated even after invoking
eval (under eager evaluation), as witnessed by the
Expr type. Also, in the aforementioned Wikipedia article,
readBack) are mutually recursive, whereas in the Haskell tutorial only
eval when it encounters an unevaluated closure body. The author still recognizes the approach as NbE though.
Many NbE implementations that I was able to find throughout the Internet differ in these tiny but important aspects. I am therefore a tad perplexed with regard to what to call "Normalization by Evaluation". The only common thing I was able to notice is that all implementations include the evaluation (
reflect) and quoting (
reify) functions which, when composed together, yield an interpreter.
In the PLT discourse, what is NbE exactly?