The structure of continuation-passing styles
John Hatcliff · 1995
Continuation-passing style (CPS) is a method of representing program evaluation order in a purely functional manner. Many applications of CPS rely on CPS transformations which explicitly encode evaluation strategies (e.g., call-by-name, call-by-value, etc.) into the structure of programs. Existing CPS transformations are based almost entirely on the call-by-name and call-by-value CPS transformations defined by Plotkin, Reynolds, and Fischer over twenty years ago. These transformations introduce the same pattern of evaluation (either call-by-name or call-by-value) throughout the entire program. Such rigidness ignores additional computational properties such as strictness and termination that are used to optimize program evaluation. We take a more general approach to CPS--we direct CPS transformations by computational properties instead of by fixed evaluation strategies. For example, a CPS transformation directed by strictness properties subsumes both the call-by-name transformation (in case all functions are non-strict) and the call-by-value transformation (in case all functions are strict). Moreover, it can transform programs with both strict and non-strict functions such as a call-by-name program after strictness analysis. Considering termination properties allows CPS transformations to avoid introducing unnecessary continuations. Based on the property of value, we show how CPS transformations (e.g., the strictness-directed transformation) can be factored into the call-by-value transformation and a thunk-based transformation. This simplifies reasoning about the factored transformations. To formalize the approach, extensions of traditional $\lambda$-calculi are proposed to capture strictness and termination properties. Our general CPS transformations translate the extended calculi into the standard $\lambda$ and $\lambda\sb{v}$ calculi. The transformations are shown to preserve operational semantics and equational properties of the extended languages. As a result, we obtain a variety of CPS transformations which have applications to compilation and partial evaluation. Standard CPS transformations (as well as the new ones presented here) have striking structural similarities. However, these similarities have never been exploited since previous work has always dealt with each transformation separately. To remedy this, we propose a generic framework for studying CPS transformations based on Moggi's computational meta-language. The framework captures the essence of the structure of continuation-passing styles and allows generic formalizations of CPS transformations, proofs of preservation of operational semantics and program calculi, optimizations known as administrative reductions, typing properties, and inverse transformations. Results for specific evaluation orders follow as corollaries of the generic results. Because the extended type system of the meta-language directly captures computational properties, we can describe all aspects of the standard call-by-value and call-by-name CPS transformations as well as the variations presented in the first part of the dissertation. Thus, previous work on CPS and CPS transformations is unified in a single framework.