Mapping environment classifiers to contextual modal types for safer code
Compiling Environment Classifiers to Contextual Modal Types
Programming Languages
Summary
Programming languages that generate code need ways to keep track of variable scopes safely. One method uses names to identify where variables belong, while another uses the structure of those scopes. The authors show how to turn the first method into the second by converting named scopes into structured contexts. They prove this conversion keeps the types and behaviors intact, using a tool called Agda for the proofs. This work shows that the structural approach can do at least what the naming method can, but going the other way might be harder.
What this means in practice
- •For programming language designers: Design type-safe metaprogramming languages by using contextual modal types to guarantee scope correctness.
- •For compiler developers: Implement compilers that translate between environment classifiers and contextual modal types to unify metaprogramming safety checks.
A theory result. No direct application yet.
Authors
Tianyu Chen, Darshal Shetty, Jeremy G. Siek, Chao-Hong Chen, Weixi Ma, Arnaud Venet, Rocky Liu
Abstract
Type systems for metaprogramming take one of two approaches to safeguarding the scopes of variables in generated code. They either use Environment Classifiers (EC) to identify scopes by name (Taha and Nielsen, 2003), or they use Contextual Modal Type Theory (CMTT) to match scopes by structure (Nanevski, Pfenning, and Pientka, 2008). In this paper, we connect these two approaches by compiling a calculus with polymorphic environment classifiers, subtyping, and mutable references to a CMTT-based calculus with polymorphic contexts, mutable references, and first-class substitutions. The key idea is to map each environment classifier to a context. We prove that the compilation preserves types and that compilation preserves the behavior of metaprograms. Both proofs are mechanized in Agda. The compilation shows that CMTT is at least as expressive as environment classifiers. We conjecture that the converse compilation is difficult, because environment classifiers impose a stricter regime on the metaprogram.