Handling Scope Checks (Extended Version)

TL;DR

This paper provides a formal framework for understanding and evaluating dynamic scope extrusion checks in metaprogramming, introducing a novel check and comparing static and dynamic approaches.

Contribution

It introduces the first formal calculus for dynamic scope extrusion checks, including a new 'Cause-for-Concern' check, and compares static and dynamic methods using refined environment classifiers.

Findings

The 'Cause-for-Concern' check is proven correct.

Dynamic checks can be effectively characterized and evaluated.

Static environment classifiers can prevent scope extrusion statically.

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 ($\lambda_{\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.