Search papers, labs, and topics across Lattice.
This paper introduces $\lambda^{\alpha,\star}_{\text{Ref}}$, a gradual metaprogramming language with mutable references that ensures scope safety by dynamically enforcing environment classifier disciplines. They develop a statically typed counterpart, $\lambda^{\alpha}_{\text{Ref}}$, with unrestricted subtyping for environment classifiers, and a novel cast calculus $\mathrm{CC}^{\alpha,\star}_{\text{Ref}}$ to handle code types, classifier polymorphism, and subtype constraints. The authors prove type safety and scope safety for $\lambda^{\alpha,\star}_{\text{Ref}}$ and provide a space-efficient implementation strategy for dynamic scope checks.
Finally, a gradually typed metaprogramming language with mutable references that *doesn't* let your variables escape scope, thanks to clever dynamic enforcement of environment classifiers.
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.
