PRL Seminars

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 languages.