CHAPTER 1
Best Student Paper: A New Approach to One-Pass Transformations
Kevin Millikin
Abstract: We show how to construct a one-pass optimizing transformation by fusing a non-optimizing transformation with an optimization pass. We state the transformation in build form and the optimization pass in cata form, i.e., as a catamorphism; and we use cata/build fusion to combine them. We illustrate the method by fusing Plotkin's call-by-value and call-by-name CPS transformations with a reduction-free normalization function for the λ-calculus, thus obtaining two new one-pass CPS transformations.
1.1 INTRODUCTION
Compiler writers often face a choice between implementing a simple, non-optimizing transformation pass that generates poor code which will require subsequent optimization, and implementing a complex, optimizing transformation pass that avoids generating poor code in the first place. A two-pass strategy is compelling because it is simpler to implement correctly, but its disadvantage is that the intermediate data structures can be large and traversing them unnecessarily can be costly. In a system performing just-in-time compilation or run-time code generation, the costs associated with a two-pass compilation strategy can render it impractical. A one-pass optimizing transformation is compelling because it avoids generating intermediate data structures requiring further optimization, but its disadvantage is that the transformation is more difficult to implement.
The specification of a one-pass transformation is that it is extensionally equal to the composition of a non-optimizing transformation and an optimization pass. A one-pass transformation is not usually constructed this way, however, but is instead constructed as a separate artifact which must then be demonstrated to match its specification. Our approach is to construct one-pass transformations directly, as the fusion of passes via shortcut deforestation [GLJ93, TM95], thus maintaining the explicit connection to both the non-optimizing transformation and the optimization pass.
Shortcut deforestation relies on a simple but powerful program transformation rule known as cata/build fusion. This rule requires both the transformation and optimization passes to be expressed in a stylized form. The first pass, the transformation, must be written as a build, abstracted over the constructors of its input. The second pass, the optimization, must be a catamorphism, defined by compositional recursive descent over its input.
The non-optimizing CPS transformation generates terms that contain administrative redexes which can be optimized away by β-reduction. A one-pass CPS transformation [DF90, DF92] generates terms that do not contain administrative redexes, in a single pass, by contracting these redexes at transformation time. Thus β-reduction is the notion of optimization for the CPS transformation. The normalization function we will use for reduction of CPS terms, however, contracts all β-redexes, not just administrative redexes. In Section 1.6 we describe how to contract only the administrative redexes.
When using a metalanguage to express normalization in the object language, as we do here, the evaluation order of the metalanguage is usually important. However, because CPS terms are insensitive to evaluation order [Plo75], evaluation order is not a concern.
This work. We present a systematic method to construct a one-pass transformation, based on the fusion of a non-optimizing transformation with an optimization pass. We demonstrate the method by constructing new one-pass CPS transformations as the fusion of non-optimizing CPS transformations with a catamorphic normalization function.
The rest of the paper is organized as follows. First, we briefly review cata-morphisms, builds, and cata/build fusion in Section 1.2. Then, in Section 1.3 we restate Plotkin's call-by-value CPS transformation [Plo75] with build, and in Section 1.4 we restate a reduction-free normalization function for the untyped λ-calculus to use a catamorphism. We then present a new one-pass CPS transformation obtained by fusion, in Section 1.5. In Section 1.6 we describe how to modify the transformation to contract only the administrative redexes. We compare our new CPS transformation to the one-pass transformation of Danvy and Filinski [DF92] in Section 1.7. In Section 1.8 we repeat the method for Plotkin's call-by-name CPS transformation. We present related work and conclude in Section 1.9.
Prerequisites. The reader should be familiar with reduction in the λ-calculus, and the CPS transformation [Plo75]. Knowledge of functional programming, particularly catamorphisms (i.e., the higher-order function fold) [MFP91] is expected. We use a functional pseudocode that is similar to Haskell.
1.2 CATA/BUILD FUSION FOR λ-TERMS
The familiar datatype of λ-terms is defined by the following context-free grammar (assuming the metavariable x ranges over a set Ident of identifiers):
Term [contains as member] m :: = var x | lam x m | app m m
A catamorphism [GLJ93, MFP91, TM95] (or fold) over λ-terms captures a common pattern of recursion. It recurs on all subterms and replaces each of the constructors var, lam, and app in a λ-term with functions of the appropriate type. We use the combinator foldλ, with type [for all]A. (Ident->A)->(Ident ->A->A)->(A ->A->A)->Term->A, to construct a catamorphism over λ-terms:
[MATHEMATICAL EXPRESSION OMITTED]
We use the combinator buildλ to systematically construct λ-terms. It takes a polymorphic function f which uses arbitrary functions (of the appropriate types) instead of the λ-term constructors to transform an input into an output, and then applies f to the λ-term constructors, producing a function that transforms an input into a λ-term. It has type [for all]A. ([for all]B.(Ident->B) ->(Ident->B->B)->(B->B->B) ->A->B)->A ->Term:
buildλf = f var lam app
Cata/build fusion [GLJ93, TM95] is a simple program transformation that fuses a catamorphism with a function that produces its output using build. For λ-terms, cata/build fusion consists of the rewrite rule:
(foldλvr lm ap) ο (buildλf) [??] f vr lm ap
The fused function produces its output without constructing intermediate data structures.
1.3 THE CALL-BY-VALUE CPS TRANSFORMATION USING BUILD
The non-optimizing call-by-value CPS transformation [Plo75] is given in Figure 1.1. We assume the ability to choose fresh identifiers when needed; the identifiers k, v0, and v1 are chosen fresh.
Fusion with a catamorphic normalization function requires that the transformation is written using build, i.e., parameterized over the constructors used to produce its output. The transformation using build thus constructs a Church encoding of the original output. The non-optimizing transformation in build form is shown in Figure 1.2. As before, the identifiers k, v0, and v1 are chosen fresh.
The transformation is non-optimizing because it produces terms that contain extraneous administrative redexes. Transforming the simple term λx. λy. y x (written with the usual notation for λ-terms) produces the term
[MATHEMATICAL EXPRESSION OMITTED]
containing administrative redexes (for simplicity, we have used only a single continuation identifier).
1.4 A CATAMORPHIC NORMALIZATION FUNCTION
Normalization by evaluation (NBE) is a reduction-free approach to normalization that is not based on the transitive closure of a single-step reduction function. Instead, NBE uses a non-standard evaluator to map a term to its denotation in a residualizing model. The residualizing model has the property that a denotation in the model can be reified into a syntactic representation of a term, and that reified terms are in normal form. A reduction-free normalization function is then constructed as the composition of evaluation and reification.
NBE has been used in the typed λ-calculus, combinatory logic, the free monoid, and the untyped λ-calculus [DD98]. We adopt the traditional normalization function for the untyped λ-calculus as our optimizer for CPS terms. We show it in Figure 1.3. Just as in the CPS transformation, we assume the ability to choose a fresh identifier when needed. We note, however, that our approach works equally well with other methods of name generation such as using de Bruijn levels or threading a source of fresh names through the evaluator. We opt against the former approach here because we want to compare our resulting one-pass transformation with existing one-pass transformations. The latter approach goes through without a hitch, but we opt against it here because the extra machinery involved with name generation distracts from the overall example without contributing anything essential.
The normalization function maps terms to their β-normal form. Normal forms are given by the grammar for Norm in Figure 1.3. Elements Val of the residualizing model are either atoms (terms that are not abstractions, given by the grammar for Atom), or else functions from Val to Val.
Environments are somewhat unusual in that the initial environment maps each identifier to itself as an element of the residualizing model, which allows us to handle open terms:
[MATHEMATICAL EXPRESSION OMITTED]
Abstractions denote functions from Val to Val. The recursive function reify ([down arrow]) extracts a normal term from an element of the residualizing model. The function apply dispatches on the value of the operator of an application to determine whether to build a residual atom or to apply the function. Normalization is then the composition of evaluation (in the initial environment) followed by reification.
Because the evaluation function is compositional, we can rewrite it as a catamorphism over λ-terms, given in Figure 1.4. The domains of terms, atoms, values, and environments do not change, nor do the auxiliary functions [down arrow] and apply.
Using this normalization function to normalize the example term from Section 1.3 produces [MATHEMATICAL EXPRESSION OMITTED], where all the β-redexes have been contracted (and fresh identifiers have been generated for all bound variables).
1.5 A NEW ONE-PASS CALL-BY-VALUE CPS TRANSFORMATION
We fuse the non-optimizing CPS transformation buildλf : Term->Term of Section 1.3 and the catamorphic evaluation function foldλvr lm ap : Term->Env ->Val of Section 1.4 to produce a one-pass transformation from λ-terms into the residualizing model. This one-pass transformation is simply f vr lm ap : Term->Env ->Val. We then extract β-normal forms from the residualizing model by applying to the initial environment and reifying, as before.
Inlining the definitions of f, vr, lm and ap, performing β-reduction, and simplifying environment operations (namely, replacing environment applications that yield a known value with their value and trimming bindings that are known to be unneeded) yields the simplified specification of the one-pass transformation shown in Figure 1.5. The domains of normal terms, atoms, values, and environments as well as the auxiliary functions [down arrow] and apply are the same as in Figure 1.3.
We have implemented this one-pass transformation in Standard ML and Haskell, letting the type inferencer act as a theorem prover to verify that the transformation returns a β-normal form if it terminates [DRR01].
1.6 SUPPRESSING CONTRACTION OF SOURCE REDEXES
Compared to traditional one-pass CPS transformations, our transformation is overzealous. The normalization function we use contracts all β-redexes; it cannot tell which ones are administrative redexes. Therefore our CPS transformation does not terminate for terms that do not have a β-normal form (e.g., (λx.x x) (λx.x x)). Of course, if we restricted the input to simply-typed λ-terms, then the transformation would always terminate because the corresponding normalization function does.
We can modify the new CPS transformation to contract only the administrative redexes. We modify the datatype of intermediate terms (and the associated catamorphism operator) to contain two types of applications, corresponding to source and administrative redexes. This is an example of a general technique of embedding information known to the first pass in the structure of the intermediate language, for use by the second pass.
Term [contains as member] m :: = var x | lam x m | app m m | srcapp m m
We then modify the non-optimizing CPS transformation to preserve source applications (by replacing the app (var v0) (var v1) with srcapp (var v0) (var v1) in the clause for applications) and we modify the normalization function (to always reify both the operator and operand of source applications). The datatype of normal forms now includes source redexes:
Norm [contains as member] n :: = atomNa | lamNx n
Atom [contains as member] a :: = varNx | appNa n | srcappNn n
The result of fusing the modified call-by-value CPS transformation with the modified normalization function is shown in Figure 1.6. Again, the domains of values and environments, and the auxiliary functions ? and apply are the same as in Figure 1.3.
Given the term from Section 1.3, the modified transformation produces
[MATHEMATICAL EXPRESSION OMITTED]
(i.e., it does not contract the source redex).
1.7 COMPARISON TO DANVY AND FILINSKI'S ONE-PASS CPS TRANSFORMATION
Danvy and Filinski [DF92] obtained a one-pass CPS transformation by anticipating which administrative redexes would be built and contracting them at transformation time. They introduced a binding-time separation between static and dynamic constructs in the CPS transformation (static constructs are represented here by metalanguage variables, abstractions, and applications; and dynamic constructs by the constructors var, lam, and app). Static β-redexes are contracted at transformation time and dynamic redexes are residualized. We present their transformation in Figure 1.7.
