Handling Scope Checks (Extended Version)

TL;DR

The paper addresses scope extrusion in metaprogramming with effects, where generated code may become ill-scoped. It develops a formal framework using the calculi $λ_{⟨⟨\texttt{op}⟩⟩}$ and $λ_{\texttt{AST}(\texttt{op})}$ to model two-stage MSP with handlers and AST elaboration, and introduces a continuation-aware dynamic check called the Cause-for-Concern (C4C) check that blends eager and lazy checking. It further extends the framework with refined environment classifiers $λ_{⟨⟨\texttt{op}⟩⟩}^{γ}$ to statically prevent extrusion and provides correctness arguments via a logical relation, alongside practical implementations in MacoCaml and discussion of expressiveness vs. safety. The work offers a principled pathway for designers of metalanguages to reason about dynamic scope checks, delivering both theoretical insights and actionable artifacts for real-world MSP systems.

Abstract

Metaprogramming and effect handlers interact in unexpected, and sometimes undesirable, ways. One example is scope extrusion: the generation of ill-scoped code. Scope extrusion can either be preemptively prevented, via static type systems, or retroactively detected, via dynamic checks. Static type systems exist in theory, but struggle with a range of implementation and usability problems in practice. In contrast, dynamic checks exist in practice (e.g. in MetaOCaml), but are understudied in theory. Designers of metalanguages are thus given little guidance regarding the design and implementation of checks. We present the first formal study of dynamic scope extrusion checks, introducing a calculus ($λ_{\langle\langle\text{op}\rangle\rangle}$) for describing and evaluating checks. Further, we introduce a novel dynamic check $\unicode{x2014}$ the "Cause-for-Concern" check $\unicode{x2014}$ which we prove correct, characterise without reference to its implementation, and argue combines the advantages of existing dynamic checks. Finally, we extend our framework with refined environment classifiers, which statically prevent scope extrusion, and compare their expressivity with the dynamic checks.