Taming Scope Extrusion in Gradual Imperative Metaprogramming

TL;DR

This paper introduces a new gradual metaprogramming language supporting mutable references with guaranteed scope safety through static and dynamic enforcement, addressing scope extrusion issues in imperative metaprogramming.

Contribution

It presents $ ext{lambda}^{, ext{star}}_{ ext{Ref}}$, the first language combining gradual typing, metaprogramming, and mutable references with scope safety, along with its theoretical foundation and implementation.

Findings

Proves type safety and scope safety of the language.

Develops a novel cast calculus for dynamic scope enforcement.

Provides a space-efficient runtime implementation.

Abstract

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 $\lambda^{\alpha,\star}_{\text{Ref}}$, the first gradual metaprogramming language that supports mutable references while guaranteeing scope safety. To put $\lambda^{\alpha,\star}_{\text{Ref}}$ on a firm foundation, we also develop its statically typed sister language, $\lambda^{\alpha}_{\text{Ref}}$, that introduces unrestricted subtyping for environment classifiers. Our key innovation, however, is the dynamic enforcement of the environment classifier discipline in $\lambda^{\alpha,\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}^{\alpha,\star}_{\text{Ref}}$ that uses an extension of Henglein's Coercion Calculus to handle code types, classifier polymorphism, and subtype constraints. We prove that $\lambda^{\alpha,\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.