Reflections of Closures
Loading...
Date
2024-03-25
Authors
Sullivan, Zachary
Journal Title
Journal ISSN
Volume Title
Publisher
University of Oregon
Abstract
The idea that programs are data forms the bedrock of functional programming languages, but it is also found in object-oriented languages and
recent iterations of systems languages. Since passing and returning programs
as data is incompatible with the architecture of modern machines,
implementations of such a feature gives rise to closures, which package
code with the environment that it needs to run. The first implementations of
these objects are as part of the runtime system of an abstract
machine. However, to be able to optimize these structures, compiler writers
often choose instead to embed this structure in their code when compiling to
lower-level languages in a transformation called closure conversion. While
this transformation and closures more generally are well studied with respect
to certain types of programming languages, how such a language interacts with
different evaluation strategies still remains unstudied in a theoretical
setting. Moreover, the current approaches to performing, optimizing, and
proving correct this transformation lack the flexibility of other language
features.
This thesis develops these ideas by presenting closure conversions for missing evaluation strategies, specifying a new implementation approach that allows
for the flexible implementation and optimization of closures, and formalizing
them in an intermediate language that captures multiple notions of closures
and evaluation strategies in one. Our approach follows from first principles
meaning that our closures are a reflection of the environment-based abstract
machines that birth them. We develop an approach to reasoning about closures
that connects their equational properties with the abstract machines on which
they run. Thereby, we can prove not only that closure conversion does not
change the output of programs, but that closure conversion removes the need
for the runtime system to capture closures.
Description
Keywords
closures, compilers, intermediate languages