Polymorphic environments enable substitution free typed code execution
Polymorphic First-Class Environments
Programming Languages
Summary
Computer programs often use environments, which are like containers for information needed while running code. Usually, changing these environments involves complicated substitution steps that can introduce errors. The authors developed a system called FE that treats these environments as first-class values supporting polymorphism, making operations cleaner by avoiding substitution. FE builds on an advanced type theory called System F and allows code to be safely run in controlled environments, enabling features like modules and sandboxing. They prove that their system works correctly and tested its theory with a proof assistant.
What this means in practice
- •For programming language designers: Use substitution-free polymorphic environments to build modular and safe language features like first-class modules and sandboxing.
- •For software security engineers: Improve runtime isolation by leveraging code execution under local environments to enforce sandboxing policies.
A theory result. No direct application yet.
Authors
Jinhao Tan, Jam Kabeer Ali Khan, Bruno C. d. S. Oliveira
Abstract
First-class environments expose runtime environments as ordinary values and support a substitution-free, environment-based operational semantics. They also support applications such as first-class modules, dynamic composition of environment fragments, and sandboxing via local environments. Existing environment-based calculi, however, are mostly studied in a simply typed setting and stop short of System F and polymorphism. We present $F_E$, a polymorphic calculus with first-class environments that conservatively extends System F with a small-step environment semantics. $F_E$ eliminates all forms of substitution in System F. Term and type abstractions evaluate to closures, boxes run code under local environments, and box types expose the local typing assumptions of both. Manifest types, together with a two-sided type equivalence, play a dual role: they model type-level instantiation, and enable transparent type components in environments and modules. We prove type soundness, normalization, decidability, and standard properties of type equivalence, and conservativity over System F. The metatheory of $F_E$ is based on instantiation lemmas rather than substitution lemmas. This foundation supports polymorphic first-class modules with dynamic composition and sandboxing. We study $F_E$ in two forms. Our main presentation is an explicit, type-passing calculus that follows conventional System F. We also develop an implicitly-typed variant aligned with the semantics of polymorphic functional languages. All metatheory is mechanized in the Rocq theorem prover.