A Generic Account of Continuation-Passing Styles

Abstract

We unify previous work on the continuation-passing style (CPS) transformations in a generic framework based on Moggi's computational met a-language.This framework is used to obtain GPS transformations for a variety of evaluation strategies and to characterize the corresponding administrative reductions and inverse transformations.We establish generic formal connections between operational semantics and equational theories.Formal properties of transformations for specific evaluation orders follow as corollaries.Essentially, we factor transformations through Moggi's computational meta-language.Mapping A-terms into the met a-language captures computational properties (e.g., partiality, strictness) and evaluation order explicitly in both the term and the type structure of the meta-language.The CPS transformation is then obtained by applying a generic transformation from terms and types in the meta-language to CPS terms and types, based on a typed term representation of the continuation monad.We prove an adequacy property for the generic transformation and establish an equational correspondence between the meta-language and CPS terms.These generic results generalize Plotkin's seminal theorems, subsume more recent results, and enable new uses of CPS transformations and their inverses.We discuss how to apply these results to compilation.