Back to direct style

Abstract

While a great deal of attention has been devoted to transforming direct-style (DS)functional programs into continuation-passing style (CPS), to the best of our knowledge, the transformation of CPS programs into direct style has not been investigated. This paper describes the mapping of continuation-passing λ-terms to their applicative-order direct style counterpart. We set up foundations and outline applications of the direct style transformation. We derive the direct style transformer from a non-standard denotational semantics of the untyped λv-calculus, that we prove congruent to the standard one. Under precise conditions (linear occurrences of continuation parameters and no firstclass use of continuations due to control operators such as can/co), we show the DS and the CPS transformations to be inverse. The direct style transformation can be used in partial evaluation, based on the fact that semantics-based program manipulation performs better when source programs are first transformed into CPS. As a result, specialized programs are expressed in CPS as well. The DS transformation maps them back to direct style.