Typed Closure Conversion
Closures are a keystone for the implementation of higher-order programming languages. Intuitively, a closure is a pair where the first component is a piece of "code" and the second component is an "environment" that provides bindings for the free variables of the code. In a closure-based semantics, closures are treated as meta-level constructs which are created and manipulated by an abstract machine.
Closure conversion translates lambda terms to closure terms, thereby reifying closures as object-level constructs. This allows us to simplify the abstract machine, thereby taking the object language one (important) step closer to machine code.
Interestingly, the most "natural" type-theoretic explanation of
closures is obtained by using existentials. In fact, in a quite
formal sense, closures are simply "objects" in the style of
Pierce and Turner. This suggests that there are simple, but
profound connections between functional and object-oriented
languages that could be exploited by an optimizing compiler to
provide a common implementation framework for both classes of