Metaprogramming enables the generation of performant code, while gradual typing facilitates the smooth migration from untyped scripts to robust statically typed programs. However, combining these features with imperative state - specifically mutable references - reintroduces the classic peril of scope extrusion, where code fragments containing free variables escape their defining lexical context. While static type systems utilizing environment classifiers have successfully tamed this interaction, enforcing these invariants in a gradual language remains an open challenge. This paper presents $λ^{α,\star}_{\text{Ref}}$, the first gradual metaprogramming language that supports mutable references while guaranteeing scope safety. To put $λ^{α,\star}_{\text{Ref}}$ on a firm foundation, we also develop its statically typed sister language, $λ^α_{\text{Ref}}$, that introduces unrestricted subtyping for environment classifiers. Our key innovation, however, is the dynamic enforcement of the environment classifier discipline in $λ^{α,\star}_{\text{Ref}}$, enabling the language to mediate between statically verified scopes and dynamically verified scopes. The dynamic enforcement is carried out in a novel cast calculus $\mathrm{CC}^{α,\star}_{\text{Ref}}$ that uses an extension of Henglein's Coercion Calculus to handle code types, classifier polymorphism, and subtype constraints. We prove that $λ^{α,\star}_{\text{Ref}}$ satisfies type safety and scope safety. Finally, we provide a space-efficient implementation strategy for the dynamic scope checks, ensuring that the runtime overhead remains practical.

翻译：元编程能够生成高性能代码，而渐进类型则有助于将无类型脚本平滑迁移至健壮的静态类型程序。然而，将这些特性与命令式状态——特别是可变引用——相结合时，会重新引入经典的作用域外泄问题，即包含自由变量的代码片段逃逸其定义词法上下文。虽然利用环境分类器的静态类型系统已成功驯服了这种交互，但在渐进式语言中强制实施这些不变量仍是一个开放挑战。本文提出 $λ^{α,\star}_{\text{Ref}}$，这是首个支持可变引用且保证作用域安全性的渐进式元编程语言。为奠定 $λ^{α,\star}_{\text{Ref}}$ 的坚实基础，我们还开发了其静态类型的姊妹语言 $λ^α_{\text{Ref}}$，该语言为环境分类器引入了不受限制的子类型化。然而，我们的核心创新在于 $λ^{α,\star}_{\text{Ref}}$ 中对环境分类器规则的动态强制实施，使该语言能够在静态验证作用域与动态验证作用域之间进行协调。动态强制实施通过一种新颖的强制转换演算 $\mathrm{CC}^{α,\star}_{\text{Ref}}$ 实现，该演算利用 Henglein 强制演算的扩展来处理代码类型、分类器多态性及子类型约束。我们证明 $λ^{α,\star}_{\text{Ref}}$ 满足类型安全性与作用域安全性。最后，我们为动态作用域检查提供了一种空间高效的实现策略，确保运行时开销保持在可接受范围内。