Great question, and don't worry — this is one of those things that's intimidating from the name but actually quite elegant once you see the core idea.

What problem does NbE solve?

You have terms in a lambda calculus. Two terms are definitionally equal if they reduce to the same normal form. Your type checker needs to check this constantly. The naive way: apply beta-reduction rules over and over until you can't anymore. That works, but it's slow and fragile for real type theories.

The NbE insight: instead of grinding through reductions syntactically, you evaluate your term into a richer semantic domain (like Haskell functions for arrow types), and then read it back into syntax. The round-trip reify ∘ eval produces the normal form.

As one nice summary puts it: "NbE does not work by finding redexes and reducing them. Instead it works by evaluating terms in a suitable model and then reifying them back into the syntax — the result is a normal form of the original term."

More precisely, in the most general formulation: to perform NbE for a set X of objects, we introduce another set M of meanings with two functions: eval: X → M and reify: M → X. The normal form of x is defined to be reify(eval(x)).

Now for reflect and reify — the heart of it.

There are a pair of type-indexed functions that move back and forth between the syntactic and semantic layers:

• reflect (written ↑τ) — takes a syntactic term and "lifts" it into the semantic domain. This is used for free variables whose values are unknown.
• reify (written ↓τ) — takes a semantic value and "reads it back" as a syntactic normal form.

They are mutually recursive, defined by induction on the type τ. Here's the classic SML-style formulation (slightly simplified):

See how they chase each other? reflect at arrow type wraps a term into a semantic function — but to apply it, it'll have to reify the argument first. And reify at arrow type generates a fresh variable, reflects it, applies the semantic function, then reifys the result. This mutual dance is what produces η-long β-normal forms.

The type of reify then makes it clear that the result is normalized — and if the datatype of normal forms is typed, reify makes it clear that normalization is type-preserving.

Ooh okay that makes intuitive sense! The semantic domain for arrow types is actual Haskell functions (or SML functions, or whatever metalanguage you're using), so beta reduction is just... function application in the host language. And then when you need the syntax back, you do the fresh-variable trick to read the function back out!

But wait — what does "η-long" mean? I see it everywhere and I feel like it's important 👀

Good question! So you know β-reduction: (λx. f x) a reduces to f a. The η-rule says the reverse: f is the same as λx. f x (at function type). A β-normal form has no more β-redexes. An η-long form has been fully expanded with η so that every function-typed subterm is syntactically a lambda.

Example: id at type A → A beta-normalizes to just id. But the η-long β-normal form is λx. id x, which further reduces to λx. x. NbE naturally produces η-long forms because reify always generates a fresh lambda when it sees an arrow type, regardless of whether the semantic value was already a lambda.

This is actually crucial for type-checking! η-equality is the reason you can replace f with λx. f x freely. Without η-long normal forms, you might fail to see that two definitionally equal terms are actually equal.

Typed NbE gives you η-long β-normal forms basically for free. That's one of the big wins over naive beta-reduction, which doesn't naturally η-expand anything.

Let me drop some actual Haskell pseudocode for a tiny simply-typed lambda calculus. This won't compile as-is but captures the full structure: