A general fine-grained reduction theory for effect handlers

Effect handlers are a modern and increasingly popular approach to structuring computational effects in functional programming languages.However, while their traditional context-capturing operational semantics is well-suited to implementation tasks, it is less ideal as a reduction theory.We therefore introduce a fine-grained reduction theory for deep effect handlers, inspired by an existing reduction theory for shift0, along with a standard reduction strategy.We relate this strategy to the contextcapturing operational semantics via a simulation argument, and show that the reduction theory preserves observational equivalence with respect to the classical semantics of handlers, thus allowing its use as a rewriting theory for handler-equipped programming languages-this rewriting system mostly coincides with previously studied type-based optimisations.In the process, we establish theoretical properties of our reduction theory, including confluence and standardisation theorems, adapting and extending existing techniques.Finally, we demonstrate the utility of our semantics by providing the first normalization-by-evaluation algorithm for effect handlers, expressed both as an abstract machine and as a higher-order normalizer, and we prove its soundness and completeness.Additionally, we establish non-expressibility of the lift operator, found in some effect-handler calculi, by the other constructs.