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.

翻译：元编程与效应处理器以意外且有时不尽人意的方式相互作用。一个典型例子是作用域外泄：即生成作用域错误的代码。作用域外泄既可通过静态类型系统进行预防性阻止，也可通过动态检查进行追溯性检测。静态类型系统在理论上存在，但在实践中面临一系列实现与可用性问题。相比之下，动态检查已在实践中应用（例如MetaOCaml），但其理论研究尚不充分。因此，元语言设计者在检查机制的设计与实现方面缺乏指导。本文首次对动态作用域外泄检查进行形式化研究，引入演算系统（$λ_{\langle\langle\text{op}\rangle\rangle}$）来描述和评估检查机制。进一步，我们提出一种新型动态检查——"风险预警"检查——并证明其正确性，通过非实现依赖的方式描述其特征，论证其综合了现有动态检查的优势。最后，我们通过引入精化环境分类器扩展研究框架，该机制能静态预防作用域外泄，并与动态检查进行了表达能力的对比分析。