Published August 5, 2025 | Version v1
Journal article Open

Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages

  • 1. University of Chicago
  • 2. University of Maryland
  • 3. Northeastern University

Description

The representation of functions in higher-order languages includes both the function's code and an environment structure that captures the bindings of the function's free variables. This paper explores caller-provided environments, where instead of packaging the entirety of a function's environment in its closure, a function can be provided with a portion of its environment by its caller. In higher-order languages, it is difficult to determine where functions are called, let alone what pieces of the function's environment are available to be provided by the caller, thus we need a higher-order control-flow analysis to enable caller-provided environments.

In this paper, we present a new abstract-interpretation-based analysis that discovers which pieces of a function's environment are always shared between its definition and its callers. In such cases, the caller can provide the environment to the callee. Our analysis has been formalized in the Rocq proof assistant. We evaluate our analysis on a collection of programs demonstrating that it is both scalable and provides significantly better information over the common syntactic approach and better information than lightweight closure conversion. In fact, it yields the theoretical upper-bound for many programs.

For caller-provided environments, deciding how to transform the program based on these revealed facts is also non-trivial and has the potential to incur extra runtime cost over standard strategies. We discuss how to make these decisions in a way that avoids the extra costs and how to transform a program accordingly. We also propose other uses of the analysis results beyond enabling caller-provided environments. We evaluate our transformation using an instrumented interpreter, showing that our approach is effective in reducing dynamic allocations for environments.

Data availability

Our implementation in the 3CPS compiler containing our environment sharing analysis, experiments, and Rocq proofs of soundness are available as an artifact via Zenodo [3CPS 2025]. The artifact contains instructions on how to reproduce our results and documentation relating the paper to the implementation. There is a separate README.md for the Rocq proofs.

Files

Environment-Sharing-Analysis-and-Caller-Provided-Environments-for-Higher-Order-Languages.pdf

Additional details

Identifiers

DOI
10.1145/3747516
Other
oai:uchicago.tind.io:16322

Funding

National Science Foundation
2212537
National Science Foundation
221253

UChicago Information

Division(s)
Physical Sciences Division
Department(s)
Computer Science