Fusion with Stacks and Accumulating Parameters ∗Susumu Nishimura
Department of Mathematics, Faculty of Science, Kyoto University, Kyoto 606–8502, Japansusumu@math.kyoto-u.ac.jp

ABSTRACT
We propose a new algorithm for fusion transformation thatallows both stacks and accumulating parameters. The newalgorithm can fuse programs that cannot be handled by existing fusion techniques, e.g., XML transformations. The
algorithm is formulated in a modular, type-directed stylewhere the transformation process is comprised of severaltransformation steps that change types but preserve the observational behavior of programs. We identify a class offunctions to which our new fusion method successfully applies and show that a closure property holds for that class.

Categories and Subject Descriptors
D.1.2 [Programming Techniques]: Automatic Programming—program transformation; D.1.1 [Programming Techniques]: Functional Programming; D.3.3 [Programming
Languages]: Language Constructs and Features—data types
and structures

General Terms
Algorithms, Languages

Keywords
Stacks, accumulating parameters, higher-order removal, shortcut fusion, type-directed program transformation.

1.

INTRODUCTION

Modular programming, where a program is written as acollection of smaller parts that solve subproblems, makes
programs significantly easier to understand and implement.
However, finer modularity often goes against efficiency, because of the overhead of interfacing between subprograms.
∗Part of preliminary result of this paper was informally presented in Asian Workshop on Programming Languages andSystems 2002 (APLAS’02).

Permission to make digital or hard copies of all or part of this work forpersonal or classroom use is granted without fee provided that copies are
not made or distributed for profit or commercial advantage and that copies
bear this notice and the full citation on the first page. To copy otherwise, torepublish, to post on servers or to redistribute to lists, requires prior specificpermission and/or a fee.
PEPM’04, August 24–26, 2004, Verona, Italy.
Copyright 2004 ACM 1-58113-835-0/04/0008 ...$5.00.

Functional programs, in which interfacing is explicit as function composition, are well-suited for studying this issue, andthe research within the last two decades has developed afamily of novel optimization techniques called fusion (or deforestation) [27, 4, 8, 20, 14, 22, 11]. Fusion is a programtransformation which unifies two recursive functions into
one. A remarkable improvement on efficiency is achieved
when the two functions are interfaced by a large sized intermediate recursively defined data structures, such as lists.
In this paper, we propose a new fusion algorithm that candeal with stacks and accumulating parameters, which are
difficult or even impossible to handle in the existing fusion
methods. The new algorithm is intended to encompass more
realistic applications. For example, consider a program for
XML document transformation. Such a program would be
implemented in the following modular style.
parse

f

unparseXML −→ XML tree −→ XML tree −→ XML
The input XML text is parsed by the function parse to produce an internal tree representation. Then, a function ffor document transformation is applied to produce anotherintermediate tree representation for the output. The resulting tree is translated back into the text representation
by unparse for the final output. In this program, stacks
and accumulating parameters naturally arise. Stacks areneeded in order to parse against non-regular languages [10].
Accumulating parameters are also required for propagating
the context information during parsing, unparsing, and anyother computation of a reasonable complexity. (The discussion above holds for many software systems that operate on
non-regular languages, e.g., compilers.)
The technical contributions of this paper are as follows.
• Our algorithm is formulated in a highly modular manner in the sense that the algorithm is comprised of aseries of type-directed transformation steps, where eachstep represents a type conversion on the program. This
type-directed formulation gives a logically clean separation of the transformation process into smaller pieces
that are easier to handle. Higher-order functions areintensively used for interfacing between transformation
steps. This differentiates our work from existing program composition techniques. (See the discussion in
Section 6.)• Our fusion algorithm always succeeds if the source program meets a linearity condition. It is also shown thata closure property holds, i.e., if the source program
meets a (stronger) linearity condition, the transforma-tion result is also linear. This closure property guarantees that a program comprising of more than two
functions can be fused by repeated applications of ouralgorithm.
In this paper, we discuss a fusion algorithm for two functions, each of which recurses over a single input data structure. (We do not consider zip-like functions that recurse
over two or more inputs simultaneously.) We assume a callby-name semantics for a functional language we consider.
When we discuss fusion for a function composition g ◦ f ,we call f the producer function and g the consumer function, where the latter consumes the intermediate result produced by the former. Each function may have accumulating parameters, while only the producer function can havestacks in its accumulating parameters and/or return results
for managing data elements in the LIFO order. Parts offinal output may be held in accumulating parameters andstacks, whereas no inspection into these data elements (e.g.,case distinction) is allowed.
The rest of this paper is organized as follows. Section 2
gives our running example for which we demonstrate our
fusion algorithm. In Section 3, we explain our fusion transformation in a simplified setting. Section 4 presents thefull transformation algorithm, which extends the aforementioned algorithm with stacks and multiple accumulating parameters and return results. In Section 5, we provide a
condition for successful transformation and show a closure
property. Section 6 mentions related work and finally Section 7 concludes with a brief summary and some issues for
future work.
For the lack of space, we omit proofs and some programcodes from this paper. The omitted materials are available on-line from the author’s homepage http://www.math.
kyoto-u.ac.jp/~susumu/.

2.

TRANSFORMATION EXAMPLEAs an example of fusion transformation, let us consider aprogram that operates on sequences of matching parentheses. We chose this simple example for explanatory purposes
only. We can consider a more involved example, say, XML
transformation systems [16, 18].
Throughout the paper, we present programs by borrowing
the syntax from Haskell [9] and extending it with records
and overloaded functions. (See Section 4 for the definitionof overloaded functions.) We write M [x1 \N1 , . . . , xn \Nn ]to represent a substitution to expression M , where the freeoccurrences of variables x1 , . . . , xn in M are simultaneously
replaced with N1 , . . . , Nn , respectively. We also use a special
symbol Ω to represent an arbitrary well-typed expression.
Every occurrence of Ω represents an unreachable point in the
program and hence can be replaced with any (appropriately
typed) expression without affecting the program’s behavior.
In practice, we can encode Ω = error "unreachable".
We model the sequence of (possibly unmatching) parentheses by the following datatype
data L = Begin L | End L | Nil
where the constructor Begin stands for the left parenthesis, End for the right parenthesis, and Nil for the end of
sequence.
A sequence of matching parentheses is internally represented by a binary tree as defined below.

parse :: L → (se:: Stk T) → (l:: T, sp:: Stk T)
parse (Begin t) x0 =let x1 = parse t (se=Stk Leaf (#se x0))
Stk a as = #sp x1
in (l=Node (#l x1) a, sp=as)
parse (End t) x0 =let x1 = parse t (se=as)
Stk a as = #se x0
in (l=a, sp=Stk (#l x1) (#sp x1))
parse Nil x0 = (l=Leaf, sp=empty)
cascade :: T → (h:: T) → (l:: T)
cascade (Node t1 t2) x0 =let x1 = cascade t1 (h= Node (#l x2) Leaf)
x2 = cascade t2 (h= #h x0)
in (l= #l x1)
cascade Leaf x0 = (l= #h x0)
unparse :: T → (k:: L) → (j:: L)
unparse (Node t1 t2) u0 =let u1 = unparse t1 (k= End (#j u2))
u2 = unparse t2 (k= #k u0)in (j= Begin (#j u1))
unparse Leaf u0 = (j= #k u0)
Figure 1: Source program
data T = Node T T | Leaf
Each binary node represents a matching pair of parentheses, where its left subtree corresponds to the subsequence
embraced by that pair, while its right subtree corresponds
to the rest of the sequence to follow. For example, a matching sequence ()(()()) is translated into a binary tree depicted
below.
° ° ·· ° ° ···
We consider a fusion for a system that is composed ofthree functions given in Fig. 1, where parse is the parsing function, cascade is the transformation function on theparsed binary tree, and unparse is the unparsing function.
The parsing function utilizes stacks, which we implement
as follows.
data Stk a = Stk a (Stk a)empty = error "empty stack"We represent a stack with n elements a1 , . . . , an (n ≥ 0) bya list-like structure terminated by empty, i.e., Stk a1 (Stka2 ( · · · (Stk an empty)· · ·)). In Fig. 1, we use patternmatching Stk a as = S to bind the topmost element of a
stack S to the variable a and the rest to the variable as.
This corresponds to the “pop” operation on stacks.
The functions in Fig. 1 are all defined as a recursive function that takes a set of accumulating parameters and returns
a set of computation results, where each set is expressedby a record.1 A record, written (l1 = M1 , . . . , ln = Mn )1
The record syntax is available as Trex extension in Haskell
interpreter Hugs (http://www.haskell.org/hugs).

(n ≥ 1), is a tuple whose each element Mi (often called arecord field ) is indexed by a unique record label li . We write(l1 :: τ1 , . . . , ln :: τn ) for the type of records consisting of
n fields where each record field labeled by li has type τi .
(The order of labels is insignificant both in expressions andtypes.) To access a record field labeled by l in a record R,
we use field selection operator, written #l R.
We use record labels as a convenient means for marking
certain set of expressions by syntactical objects. In the final
transformation step of our algorithm (Section 3.4 and 4.6),
it is crucial to identify some expressions according to their
origin. Record labels are convenient for this, as the namesof labels last unchanged throughout the transformation process. (cf. the names of program variables, which are subject
to change due to α-conversion.) Ordinary (unlabeled) tuples
may be used instead, but records can coexist more smoothlywith our transformation process, which includes flattening
and concatenation operations on tuples.
The explanation of the functions given in Fig. 1 follows
below. The parsing function parse takes one accumulating
parameter labeled by se and returns two results labeled by
sp and l, where the se field holds a stack that remembers
the number of parentheses yet to match and the sp field represents the parsing stack. The result of parsing is returnedin the field l. When a malformed input sequence is fed tothe parse function with empty being the initial value of these field, an error will be signaled due to a “pop” operation
on an empty stack.
The cascade function takes one accumulating parameterlabeled by h and returns one result labeled by l. Given Leafas the initial accumulating parameter, cascade recursively
replaces the leftmost leaf node in every binary tree with theright subtree of the root node of that tree. This results in abinary tree where all the input binary nodes are reordered
onto the spine of left branches in the output. For instance,a binary tree corresponding to the sequence ()(()()) is transformed into the one corresponding to (((()))).
The unparse function translates back the binary tree representation into the sequence representation. It takes one
accumulating parameter labeled by k, whose initial value isNil, and returns one result labeled by j.
In the following sections, we will derive a program thatfuses these three functions. The result of fusion is given in
Fig. 5 of Section 4. The resulting program does not produce
any intermediate binary tree representation; it is defined asa first-order function that recurses over the input sequencewith a new set of accumulating parameters and return results, which may circularly refers to each other.

3.

FUSION WITH ACCUMULATINGPARAMETERS

In this section we demonstrate our transformation algorithm by applying it for fusing the producer function cascade
and the consumer function unparse.
Fig. 2 illustrates the outline of the transformation process.2 Our transformation algorithm is type-directed, in asense that each transformation step corresponds to a typeconversion. (In Fig. 2, types that are subject to conversion
2
For the sake of readability, the figure shows the case where
each function takes one accumulating parameter and returns
one result, and stacks are only in the accumulating parameter of the producer function.

are underlined.) It first applies shortcut fusion [8] for unifying the producer function prod and the consumer function
cons. The result is a higher-order function prod’, which
is turned into a first-order function in the remainder oftransformation steps. This section demonstrates a simplified version of our transformation algorithm and does notdeal with transformation steps (II) and (IV), which concern
stack types. We will discuss the general case, allowing stacks
and multiple accumulating parameters and return results, inthe following section.
We will argue the correctness of each transformation step
up to observational equivalence. Let us write M1 = M2
to mean observational equivalence, i.e., M1 and M2 show
the same behavior under any evaluation context. Under acall-by-name evaluation semantics, βη-equality induces anobservational congruence.3 As for records, the following relation holds.
#l (l = M, . . . ) = M(Rec-Cancel)

We will freely use βη-equality and also (Rec-Cancel) for
simplifying programs.
In addition, assuming M is a non-diverging record expression, we will use the following to reason about the correctness of transformation. (In this paper, the type annotation
syntax (M :: τ ) represents a typing constraint that M has
type τ .)(M :: (l1 :: τ1 , . . . , ln :: τn )) = (l1 = #l1 M, . . . , ln = #ln M )(Rec-Eta)
This relation can be safely applied for reasoning about correctness anywhere in this paper, since we assume a particular syntactic form (discussed in Section 5), in which every record is created by the explicit record syntax (l1 =M1 , . . . , ln = Mn ) that never diverge.
In this paper, we carry out the discussion on the correctness in a rather conventional way, in order not to include
too much theoretical details. (The argument on the correctness in this paper should be formalized in the framework of Pitts’ syntactic logical relations [19].) Suppose that
we have a program transformation P, whose corresponding
type conversion is T . To verify the correctness of transformation, we check if P[[M1 ]] = P[[M2 ]] for every observationally equivalent pair of expressions M1 and M2 , andthe interesting proof case is that for expressions of type τsuch that the outermost type constructors in τ and T [[τ ]]differ. In that case, we show that, for any constructor C
and destructor Di for the type τ , observational equivalence
Di (C M1 · · · Mn ) = Mi is preserved by the transformation,i.e., P[[Di (C M1 · · · Mn )]] = P[[Mi ]] holds. As for a record
type, this corresponds to verifying that (Rec-Cancel) ispreserved by the transformation.

3.1

Shortcut fusion

We apply shortcut fusion to fuse the following function
application.
unpcas :: T → L
unpcas x =#j (unparse (#l (cascade x (h=Leaf))) (k=Nil))3
We do not consider Haskell’s seq operator, which breaks
this property.

prod :: σ1 → (h :: Stk σ2 ) → (l :: σ2 )andcons :: σ2 → (k :: σ3 ) → (j :: σ3 )⇓(I) shortcut fusion

prod’ :: σ1 → (h :: Stk ((k :: σ3 ) → (j :: σ3 ))) → (l :: (k :: σ3 ) → (j :: σ3 ))⇓(II) function type lifting for stacks

prod’ :: σ1 → (h :: Stk (k :: σ3 ) → Stk (j :: σ3 )) → (l :: (k :: σ3 ) → (j :: σ3 ))⇓(III) function type lifting for records

prod’ :: σ1 → ((h :: Stk (k :: σ3 )) → (h :: Stk (j :: σ3 ))) → ((l :: (k :: σ3 )) → (l :: (j :: σ3 )))⇓(IV) record type liftingprod’ :: σ1 → ((h :: (k :: Stk σ3 )) → (h :: (j :: Stk σ3 ))) → ((l :: (k :: σ3 )) → (l :: (j :: σ3 )))⇓(V) record type flattening

prod’ :: σ1 → ((hk :: Stk σ3 ) → (hj :: Stk σ3 )) → ((lk :: σ3 ) → (lj :: σ3 ))⇓(VI) higher-order removal

prod’ :: σ1 → (hj :: Stk σ3 , lk :: σ3 ) → (hk::Stk σ3 , lj :: σ3 )Figure 2: Transformation steps
For this, we rewrite cascade and unparse in terms ofbuild and fold, whose definitions on the datatype T of binary trees are given below.
build :: (∀b. (b → b → b) → b → b) → T
build g = g Node Leaf
fold :: (a → a → a) → a → T → afold n l (Node t1 t2) = n (fold n l t1) (fold n l t2)
fold n l Leaf = l
The producer function is expressed as build g, where g isa function that abstracts over all occurrences of constructors
for intermediate data (namely, Node and Leaf) and build
reinstantiates the abstractions with concrete constructors.
The consumer function is expressed as fold c z, using thegeneric recursion operator fold that replaces every Nodeconstructor with c and Leaf with z.
The composition of the producer and consumer functions
are fused by the following fold/build rule [8].
fold c z (build g) = g c z
Intuitively, this equation means that, instead of applying
fold c z to the intermediate result produced by build g,
we can obtain the same effect by instantiating abstracted
constructors in g with c and z.
The correctness of shortcut fusion follows from free theorems [26, 12], the parametericity property induced from thepolymorphic typing constraint on build.
The shortcut fusion applies to the present example as follows. (For general methods for translating normal recursive
programs into fold and build forms, see [14, 5].) The consumer function unparse is defined with fold as follows.
unparse :: T → (k:: L) → (j:: L)
unparse = fold c z
where c t1 t2 =\u0 -> let u1 = t1 (k= End (#j u2))
u2 = t2 (k= #k u0)in (j= Begin (#j u1))z = \u0 -> (j= #k u0)
The producer function, as in the form used in the defini-tion of the unpcas function above, is expressed as follows:#l (cascade x (h=Leaf))= #l (build x(\n l->cascade’ t n l (h=fold n l Leaf)))
where cascade’ is defined as follows.
cascade’ n l (Node t1 t2) = \x0 ->let x1 = cascade’ n l t1 (h= n (#l x2, l))x2 = cascade’ n l t2 (h= #h x0)
in (l= #l x1)
cascade’ n l Leaf = \x0 -> (l= #h x0)
We note that we need to abstract over constructors not
only in the function body of cascade but also its accumulating parameters by applying fold n l, so that cascade’
meets the above mentioned polymorphic typing constraint [7].
Application of the fold/build rule, followed by some simplifications, gives the following result.
cascade’ :: T → (h:: (k:: L) → (j:: L))→ (l:: (k:: L) → (j:: L))
cascade’ (Node t1 t2) = \x0 ->let x1 = cascade’ t1(h= \u -> (j=Begin (#j((#l x2) (k=End (#k u))))))
x2 = cascade’ t2 (h= #h x0)
in (l= #l x1)
cascade’ Leaf = \x0 -> (l= #h x0)
unpcas :: T → L
unpcas x =#j ((#l (cascade’ x (h= \x0 -> (j= #k x0))))(k=Nil))3.2

Function type lifting

The transformation step that follows shortcut fusion iscalled function type lifting, which corresponds to the following type conversion
from(p :: τ1 → τ2 )into

(p :: τ1 ) → (p :: τ2 ),where p is either h or l.

This type conversion is realized by applying a transformation function called L to every defining equation in the
program. L traverses the program structure and applies thefollowing transformation rules wherever possible.
L[[(p = (M :: τ1 → τ2 ))]]
= \y -> (p = L[[M ]] (#p y))
L[[#p (M :: (p :: τ1 → τ2 ))]] = \y -> #p (L[[M ]] (p = y))(In both rules, y denotes a fresh variable.)
We omitted trivial transformation rules that are neededjust for traversing the program structure. The same convention applies to the rest of the paper.
According to the discussion in the beginning of this section, we can verify the correctness of the present transformation by checking (Rec-Cancel) is preserved by the transformation.
L[[#p (p = M )]]=\y -> #p ((\y -> (p = L[[M ]] (#p y))) (p = y))=\y -> L[[M ]]y = L[[M ]]by η-equality

The result of function type lifting transformation is given
as follows.
cascade’ :: T → (((h:: (k:: L)) → (h:: (j:: L)))→ ((l:: (k:: L)) → (l:: (j:: L))))
cascade’ (Node t1 t2) = \x0 ->let x1 = cascade’ t1(\y1 -> (h=(j=Begin (#j (#l (x2(l=(k=End (#k (#h y1))))))))))
x2 = cascade’ t2(\y2 -> (h= #h (x0 (h= #h y2))))in \y0 -> (l= #l (x1 (l= #l y0)))cascade’ Leaf = \x0 ->\y0 -> (l= #h (x0 (h= #l y0)))
unpcas :: T → L
unpcas x =#j (#l (cascade’ x (\y -> (h=(j= #k (#h y))))(l=(k=Nil))))

3.3

Record type flattening

This transformation step intends a type conversion
from(p :: (q :: L))

into(pq :: L),

where p is either h or l, q is either k or j, and pq is a newlabel obtained by concatenating the two.
This type conversion represents a transformation that merges
any pair of nested record labels p and q into a single one pq,
i.e., (p = (q = M )) into (pq = M ) and #q (#p M ) into
#pq M . Formal transformation rules are given below.
F[[(p = (M :: (q :: L)))]] = (pq = #q F[[M ]])F [[#p (M :: (p :: (q :: L)))]] = (q = #pq F[[M ]])We can check this transformation preserves (Rec-Cancel).
F[[#p (p = (M :: (q :: L)))]]=(q = #pq (pq = #q F[[M ]]))=(q = #q F [[M ]]) = F [[M ]]by (Rec-Eta)

The result of record type flattening follows below.

cascade’ :: T → (((hk:: L) → (hj:: L))→ ((lk:: L) → (lj:: L)))
cascade’ (Node t1 t2) = \x0 ->let x1 = cascade’ t1(\y1 -> (hj=Begin (#lj (x2(lk=End (#hk y1))))))
x2 = cascade’ t2(\y2 -> (hj= #hj (x0 (hk= #hk y2))))in \y0 -> (lj= #lj (x1 (lk= #lk y0)))cascade’ Leaf = \x0 ->\y0 -> (lj= #hj (x0 (hk= #lk y0)))
unpcas :: T → L
unpcas x =#lj (cascade’ x (\y -> (hj= #hk y)) (lk=Nil))

3.4

Higher-order removal

Now we are ready for removing higher-order functions.
At the type level, the higher-order removal transformation
conducts a type conversion
from((hk :: L) → (hj :: L)) → ((lk :: L) → (lj :: L))

into(hj :: L, lk :: L) → (hk :: L, lj :: L).

We remark that this type conversion preserves polarity ofrecord fields. That is, record fields that occur positively inthe higher-order function type (namely, hk and lj fields) also
appear in positive positions of the resulting first-order function type; so do record fields in negative positions (namely,
hj and lk fields).
In a previous work [17], the author has proposed a transformation algorithm that applies to a class of higher-orderfunctions whose each defining equation has the following
specific syntactic form
f :: T → ((hk::L)→(hj::L)) → ((lk::L)→(lj::L))f (C t1 . . . tc ) = \x0 ->let x1 = f tj(1) (\y1 -> (hj=N1 ))···xr = f tj(r) (\yr -> (hj=Nr ))(3.1)

in \y0 -> (lj=N0 )where r, c ≥ 0, 1 ≤ j(i) ≤ c for every i (1 ≤ i ≤ r), Ni ’s
belong to a set of first-order expressions defined by the following grammar
M ::= #hj (x0 (hk = M)) | #lj (xi (lk = M))| #lk y0 | #hk yi | C M · · · M(1 ≤ i ≤ r),

and furthermore the uses of variables x0 , . . . , xr are linear.
It follows from the linearity that, for every i and appropriate record labels p and q, there is one and only one expression M such that M occurs in the form #p (xi (q = M )).
Let us write Mx0 for the unique expression M in the form#hj (x0 (hk = M )) and Mxi for the unique expression M in
the form #lj (xi (lk = M )) (1 ≤ i ≤ r).
Each defining equation of the intermediate transformation result in the previous subsection has the above syntactic form. This holds for any program that is derived froma source program that satisfies certain syntactic condition(involving linearity on the uses of variables), which we will
discuss in Section 5.

In what follows, let us explain our higher-order removaltransformation method in a rather informal way, since aformal justification requires an intricate discussion on theobservational equivalence of programs, which is out of thescope of the present paper. Interested readers are deferredto [17].
In the light of the intended conversion on type, we canguess that the transformation would result in a set of defining equations of the following form.
f 0 :: T → (hj :: L, lk :: L) → (hk :: L, lj :: L)
f 0 (C t1 . . . tc ) x0 =let x1 = f 0 tj(1) (hj=M1hj , lk=M1lk )···xr = f 0 tj(r) (hj=Mrhj , lk=Mrlk )in (lj=M0lj , hk=M0hk )cascade’ :: T → (hj::L, lk::L) → (hk::L, lj::L)
cascade’ (Node t1 t2) x0 =let x1 = cascade’ t1(lk= #lk x0, hj= Begin (#lj x2))
x2 = cascade’ t2(lk= End (#hk x1), hj= #hj x0)
in (hk= #hk x2, lj= #lj x1)
cascade’ Leaf x0 = (hk= #lk x0, lj= #hj x0)
unpcas :: T → L
unpcas x = let r = cascade’ x (hj= #hk r, lk=Nil)in #lj r
Figure 3: Fusion result on unpcas

M0lj ,

We need to find appropriate expressions to fill in
M0hk , Mihj ’s, and Milk ’s in the above program. First, we canobserve that expression Ni (1 ≤ i ≤ r) in (3.1) is each appropriate for Mihj , as it represents the one and only one hj
value computed by the recursive call f tj(i) · · · . Similarly, N0
is appropriate for M0lj . However, we notice that any occurrence of yi ’s in these expressions becomes void in the target
program, since there are no binding constructs for them. To
fix this ill-definedness, we rewrite every subexpression #lky0(#hk yi , resp.) into #lk x0 (#hk xi , resp.), expecting thatbindings for x0 , . . . , xr in the target program would give theappropriate lk (hk, resp.) value. We note that this rewrite
gives rise to a circular definition, where some record fields
returned by a function application are referenced from theargument positions of that function call itself. (This circular tupling technique has been demonstrated by Bird [1] andhas also been exploited in [24] to deforest in accumulating
parameters.)
For the above circular binding to be valid, each #hk yi(1 ≤ i ≤ r) in the source program (function f ) should denote the same value as #hk xi does in the target program(function f 0 ). Since the function call f tj(i) (\yi ->· · ·) inf binds the variable x0 to the function \yi ->· · · and uses itin the form #hj (x0 (hk=Mx0 )), yi is bound to (hk=Mx0 )eventually. On the other hand, in f 0 , xi is bound to theresult of function call f 0 tj(i) · · ·, which returns the record(hk=M0hk ,· · ·). Hence, M0hk must be Mx0 .
We also require that #lk y0 in f denotes the same value as#lk x0 in f 0 . (The initial call sites of both functions are also
assumed to meet this condition, as indicated by Eq. (3.3)
that we will see later in this section.) It follows from thisrequirement that, by a similar discussion as above, Milk must
be Mxi for each i (1 ≤ i ≤ r).
To complete the transformation, we rewrite #hj (x0 (hk =M )) into #hj x0 , where the hj value returned by an application of x0 in the source program is given in the target
program through the hj field in the record bound by x0 .
Similarly, we rewrite #lj (xi (lk = M )) into #lj xi for everyi (1 ≤ i ≤ r).
By the discussion so far, we transform the function definition in the form (3.1) into the following first-order programf 0 :: T → (hj :: L, lk :: L) → (hk :: L, lj :: L)
f 0 (C t1 . . . tc ) x0 =let x1 = f 0 tj(1) (hj=H[[N1 ]], lk=H[[Mx1 ]])···xr = f 0 tj(r) (hj=H[[Nr ]], lk=H[[Mxr ]] )in (lj=H[[N0 ]], hk=H[[Mx0 ]])where H is the transformation function defined by the following set of rules.
H[[xi M ]] = xi

(0 ≤ i ≤ r)

(3.2a)

H[[yi ]] = xi

(0 ≤ i ≤ r)

(3.2b)

The following equation, taken from [17], characterizes therelation between the higher-order function f and the resulting first-order function f 0 :#lj (f L G (lk = L0 ))= #lj (f 0 L (hj = #hj (G(hk = #hk (f 0 L (hj = Ω, lk = L0 )))),
lk = L0 )),where L is an expression of type T, L0 is of type L, and G isa function of type (hk :: L) → (hj :: L).
The two different calls to f 0 in the RHS of the equation
can be unified into a single call with a circular definition, as
follows.
#lj (f L G (lk = L0 ))= let r = f 0 L (hj = #hj (G (hk = #hk r)), lk = L0 )in #lj r(3.3)

It is easy to see the former equation follows from the latter,by unwinding the circular let and exchanging Ω with an appropriate expression. (Remember that Ω is a special symbolthat represents arbitrary expression.)
Applying the higher-order removal transformation to cascade’
and rewriting the definition of unpcas according to the equation (3.3), we obtain the fusion result given in Fig. 3.

4.

FUSION WITH STACKSIn this section, we carry out the remaining half of transformation. That is, we apply our fusion algorithm to thefollowing program
unpcaspar :: L → L
unpcaspar x = unpcas (#l (parse x (se=empty)))which expands to
unpcaspar x =let r = cascade’ (#l (parse x (se=empty)))(hj= #hk r, lk=Nil)in #lj r

This section applies our full transformation algorithm,
which refines and augments the one given in the previous
section in two points. First, two new transformation steps
concerning stack types ((II) and (IV) in Fig. 2) are added.
Second, the transformation rules are generalized so that they
allow multiple accumulating parameters and return values.
For this generalization, we extend our language with firstclass overloaded functions, which are expressed by the following syntax.
{\(x1 :: τ1 ) -> M1 ; · · ·; \(xn :: τn ) -> Mn }(n ≥ 1)

An overloaded function is a collection of functions, fromwhich one that has a matching argument type is selected
and evaluated per each application of that overloaded function. (A normal λ-abstraction can be recognized as a special
instance of an overloaded function.) The type of an overloaded function is written as a collection of function types(τ1 → τ10 ; . . . ; τn → τn0 )

(or

Pn

0
i=1 τi → τi for short),

where τ10 , . . . , τn0 can be different types. In this paper, every
different function that is a member of an overloaded function
has a different argument type (p :: τ ) distinguished by therecord label p. Therefore no ambiguity arises in the selectionof function and the return type of each application of an
overloaded function is statically determined.
In the rest of this section, let us write ~p for a non-empty
set of record labels {p1 , . . . , pn } (n ≥ 1). We also write(~p :: τ ) to abbreviate (p1 :: τ, . . . , pn :: τ ) and also write τe
to denote either τ or Stk τ .
We write σ1 , σ2 , and σ3 for the types of the input, intermediate, and output data structures, respectively. We also
write ~h, ~l, ~k, ~j for disjoint sets of record lables, where ~h areused for labeling accumulating parameters of the producer
function and ~l for return results; ~k are used for labeling accumulating parameters of the consumer function and ~j forreturn results.
In this section, we apply the transformation algorithm tothe pair of the producer function parse and the consumer
function cascade’, where σ1 = L, σ2 = T, σ3 = L, ~h = {se},~l = {l, sp}, ~k = {hj, lk}, and ~j = {hk, lj}. We omit someof the intermediate transformation results, in order not toclutter pages with lengthy codes.

4.1

Shortcut fusion

As we did in the previous section, we first apply shortcut
fusion. The result is displayed below.
parse’ ::L → (se:: Stk((hj::L,lk::L)→(hk::L,lj::L)))→ (sp:: Stk((hj::L,lk::L)→(lj::L,hk::L)),l:: (hj::L,lk::L)→(hk::L,lj::L))
parse’ (Begin t) = \x0 ->let x1 = parse’ t(se=Stk (\u0 -> (hk= #lk u0, lj= #hj u0))(#se x0))in (l= \u0 ->let u1 = (#l x1) (lk= #lk u0,
hj=Begin (#lj u2))
u2 = (hd (#sp x1))
(lk=End (#hk u1), hj= #hj u0)in (hk= #hk u2, lj= #lj u1),
sp=tl (#sp x1))

parse’ (End t) = \x0 ->let x1 = parse’ t (se=tl (#se x0))in (l=hd (#se x0), sp=Stk (#l x1) (#sp x1))
parse’ Nil = \x0 ->(l= \u0 -> (hk= #lk u0, lj= #hj u0), sp=empty)
unpcaspar :: L → L
unpcaspar x =let r = #l (parse’ x (se= empty))(hj= #hk r, lk=Nil)in #lj r
This is obtained by a similar derivation in Section 3.1. The
only difference is that we must abstract over constructors
in the accumulating parameter of parse by applying mapS
(fold n l), where n and l are abstraction variables andmapS is a map function on stack elements defined by:mapS f (Stk a as) = Stk (f a) (mapS f as)
For the sake of brevity, we have replaced every reference
to pattern matching variables a and as bound by a local
definition Stk a as =S with hdS and tlS, respectively, where
hd and tl are functions satisfying the following equations.

4.2

hd (Stk A S) = A(Stk-Hd)tl (Stk A S) = S(Stk-Tl)

Function type lifting for stacks

We introduce a new transformation step that represents
the following type conversion:
from
into

Stk(τ1 → τ2 )Stk τ1 → Stk τ2 .

This conversion makes function arrows exposed outside ofthe enclosing stack type constructors, so that the transformation result is ready for the next transformation step. Thisis realized by the following set of transformation rules
S[[(Stk A M :: Stk(τ1 → τ2 ))]] =\w -> Stk(S[[A]](hd w))(S[[M ]](tl w))
S[[hd M ]] = \u -> hd (S[[M ]] (Stk u Ω))
S[[tl M ]] = \w -> tl (S[[M ]] (Stk Ω w))
where w and u are fresh variables.
We remark that the above embedding into the target type
Stk τ1 → Stk τ2 is not full: the resulting function always
maps a stack into another stack of the same length. Furthermore, the function operates on stacks elementwisely. Thatis, each element in the output stack is determined only by
the element at the same depth in the input stack; the otherelements in the input stack are never referenced and are
represented by Ω in the rules above.
By a similar discussion in Section 3, the correctness of thistransformation is verified by checking if the transformation
preserves (Stk-Hd) and (Stk-Tl). We show the formercase only; the verification on the latter is similar.
S[[hd (Stk A M )]]= \w -> hd ((\w0 -> Stk (S[[A]](hd w0 )) (S[[M ]](tl w0 )))(Stk w Ω))= \w -> S[[A]]w = S[[A]]by (Stk-Hd) and η-equality

4.3

Function type lifting for records

This transformation step is a generalization of the one
given in Section 3.2 and corresponds to the following typeconversion:from(p1 :: τ1 → τ10 , . . . , pn :: τn → τn0 )

into((p1 :: τ1 ) → (p1 :: τ10 ); · · · ; (pn :: τn ) → (pn :: τn0 ))where n ≥ 1 and ~p = ~h or ~p = ~l.
This conversion is realized by the following set of transformation rules
L[[(p1 = (M1 :: τ1 → τ10 ), . . . , pn = (Mn :: τn → τn0 ))]] ={\(y :: (p1 :: τ1 )) -> (p1 = L[[M1 ]](#p1 y));··· ;\(y :: (pn :: τn )) -> (pn = L[[Mn ]](#pn y))}L[[#p (M :: (p1 :: τ1 → τ1 , . . . , pn :: τn → τn0 ))]] =in the sense that every field in the resulting record holds a
stack of the same length.
The following derivation verifies that the transformation
preserves (Stk-Hd).
R[[hd (Stk A M :: Stk(~q :: τ ))]]= (q1 = #q1 R[[A]], . . . , qm = #qm R[[A]])= R[[A]]The derivation for (Stk-Tl) is similar.

4.5

Record type flattening

At this transformation step, we flatten nested record types.
We generalize the transformation given in Section 3.3 so thatit can handle records with multiple fields.
Let us write p~q for the set of labels {pq | q ∈ ~q}. The
generalized transformation represents a type conversion\v -> #p(L[[M ]](p = v))
where y and v are fresh variables.
In this transformation step, the set of functions in a record
R = (p1 = F1 , . . . , pn = Fn ) is translated into an overloadedfunction F = {F10 ; · · · ; Fn0 }, where each function Fi0 has type(pi :: τi ) → (pi :: τi0 ). An application of the function Fi in
the form (#pi R)M in the source program is interpreted in
the target program as #pi (F (pi = M )), where the corresponding function Fi0 in the overloaded function is selected
up to the record label pi . A similar translation may be possible by using a function of type hp1 : τ1 , . . . , pn : τn i →hp1 : τ10 , . . . , pn : τn0 i that operates on disjoint sum types.4
However, this not only adds extra syntactic verbosity but
also gives an imprecision in typing: it blurs the fact thatthe function maps every input with a record (or injection)label into an output with the same label.
The correctness of this transformation is verified by aderivation similar to that in Section 3.2.

4.4

Record type lifting

Here we need another new transformation step that operates on stack types:fromStk(~q :: τ )into(~q :: Stk τ ),where ~q = ~j or ~q = ~k.
The following transformation rules realize such type conversion.
R[[(Stk A M :: Stk(~q :: τ ))]] =(q1 = Stk (#q1 R[[A]]) (#q1 R[[M ]]), . . . ,qm = Stk (#qm R[[A]]) (#qm R[[M ]]))
R[[hd (M :: Stk(~q :: τ ))]] =(q1 = hd (#q1 R[[M ]]), . . . qm = hd (#qm R[[M ]]))
R[[tl (M :: Stk(~q :: τ ))]] =(q1 = tl (#q1 R[[M ]]), . . . qm = tl (#qm R[[M ]]))
A similar remark in Section 4.2 applies to this transformation. That is, the embedding into the target type is not full4
hp1 : τ1 , . . . , pn : τn i represents a disjoint sum type with n
distinct injection labels into the sum type.

by (Rec-Cancel)by (Rec-Eta)from(p :: (~q :: ~τ ))into(p~q :: ~τ ),where p ∈ ~h ∪ ~l and either ~q = ~k or ~q = ~j.
The transformation rules are given below.
F [[(p = (M :: (~q :: τ ))]] =(pq1 = #q1 F[[M ]], . . . pqm = #qm F[[M ]])F [[#p (M :: (p :: (~q :: τ )))]] =(q1 = #pq1 F[[M ]], . . . , qm = #pqm F [[M ]])The correctness of this transformation is verified by a derivation similar to that in Section 3.3.
The result of this transformation step is given in Fig. 4,
where we saved space by writing let U in (p1 =M1 , ...,
pn =Mn ) instead of (p1 =let U in M1 , ..., pn =let U in
Mn ).

4.6

Higher-order removalThis section presents a higher-order removal transformation method that generalizes the one given in Section 3.4.
In the following, let us write ~p~q for the set of labels {pq |Qp ∈ ~p, q ∈ ~q}. We write p∈~p (p = Mp ) to abbreviateQ(p1 = Mp1 , . . . , pn = Mpn ) and also write p∈~p (p = Mp ) ⊗Q(q = Nq ) to denote the record expression (p1 = Mp1 , . . . ,q∈~qpn = Mpn , q1 = Nq1 , . . . , qm = Nqm ).
The present transformation can be explained as a typeconversion
from

Pn

~

~

f3 ) → (hi j :: σf3 )i=1 (hi k :: σ

→
into

Pm

~

~

f3 ) → (li j :: σf3 )i=1 (li k :: σ(~h~j :: σf3 ,~l~k :: σf3 ) → (~h~k :: σf3 ,~l~j :: σf3 ).

The transformation steps so far would result in a higherorder function f , whose each defining equation has the following form.
Pn~ f3 ) → (hi~j :: σf :: σ1 →f3 )
i=1 (hi k :: σPm~→f3 ) → (li~j :: σf3 )i=1 (li k :: σf (C t1 . . . tc ) = \x0 -> let x1 = f tj(1) F1···
xr = f tj(r) Fr
in F0

(4.1)

parse’ :: L → ((selk:: Stk L,sehj:: Stk L) → (sehk:: Stk L,selj:: Stk L))→ ((lhj::L,llk::L) → (lhk::L,llj::L); (sphj:: Stk L,splk:: Stk L) → (splj:: Stk L,sphk:: Stk L))
parse’ (Begin t) = \x0 ->let x1 = parse’ t (\y1 -> (sehk=Stk (hd (#selk y1)) (#sehk (x0 (selk=tl (#selk y1), sehj=tl (#sehj y1)))),
selj=Stk (hd (#sehj y1), (#selj (x0 (selk=tl (#selk y1), sehj=tl (#sehj y1)))))))
in {\(y0 :: (lhj::L,llk::L) ) ->let u1 = (hk= #lhk (x1 (llk= #llk y0, lhj=Begin (#lj u2))), lj= #llj (x1 (llk= #llk y0, lhj=Begin (#lj u2))))u2 = (hk= hd (#sphk (x1 (splk=Stk (End (#hk u1)) Ω, sphj=Stk (#lhj y0) Ω))),
lj= hd (#splj (x1 (splk=Stk (End (#hk u1)) Ω, sphj=Stk (#lhj y0) Ω))))
in (lhk= #hk u2, llj= #lj u1) ;\(y0 :: (sphj:: Stk L,splk:: Stk L) ) ->(sphk=tl (#sphk (x1 (splk=Stk Ω (#splk y0), sphj=Stk Ω (#sphj y0)))),
splj=tl (#splj (x1 (splk=Stk Ω (#splk y0), sphj=Stk Ω (#sphj y0))))) }parse’ Nil = \x0 -> {\(y0 :: (lhj::L,llk::L) ) -> (lhk= #llk y0, llj= #lhj y0);\(y0 :: (sphj:: Stk L,splk:: Stk L) ) -> (sphk=empty, splj=empty) }unpcaspar :: L → L
unpcaspar x = let r = parse’ x (\w->(sehk=empty, selj=empty)) (lhj= #lhk r, llk=Nil) in #llj r

Figure 4: Result of recrod type flattening (The End case is omitted.)
where c, r ≥ 0, 1 ≤ j(i) ≤ c for every i (1 ≤ i ≤ r), andQl j
F0 = {\y0 :: (l1~k :: σf3 ) -> l j∈l ~j (l1 j = N01 );
1
1
··· ;
Q
l j
\y0 :: (lm~k :: σf3 ) -> lm j∈lm~j (lm j = N0m )}Q

h j
Fi = {\yi :: (h1~k :: σf3 ) -> h1 j ∈ h1~j(h1 j = Ni 1 );
··· ;
Q
h j
\yi :: (hn~k :: σf3 ) -> hn j ∈ hn~j(hn j = Ni n )}In the form above, each Nipq belongs to a class of expressions specified by the following grammar
M ::= #hj (x0 (~h~k = M)) | #lj (xi (~l~k = M))| #lk y0 | #hk yi | C M · · · M| Stk M M | hd M | tl M | Ω| let u1 = M · · · uv = M in M
where 1 ≤ i ≤ r, h ∈ ~h, k ∈ ~k, l ∈ ~l, j ∈ ~j.
The higher-order removal transformation method in thissection extends the one given in Section 3.4 so that multiple
record fields are properly handled. For this, for each different overloaded function g occurring in f and each different
record label p, we need to identify a unique expression M
such that (p = M ) is the argument to g. In Section 3.4, such
identification was possible, resorting to the linearity on a setof variables. However, in the present generalized setting, thelinearity does not necessarily holds for the following reasons.
First, the rewrite into hd and tl notations in Section 4.1 andthe transformation rules in Section 4.4 and 4.5 may duplicate expressions, thus breaking the linearity. Second, thetransformation rules in Section 4.2 apply the same function
S[[M ]] to different arguments, namely, Stk u Ω and Stk Ω w.
Finally, a function in the target program may not have any
record fields for some labels, when the corresponding fields
are not referenced at all in the source program.
We remedy this problem by adopting a relaxed linearity
condition described below. We allow the same function to be
applied in two or more application sites. If a function is applied to different arguments which have an identical expression for the same field, we recognize the identical expression
as the unique expression for that field. Suppose otherwise,i.e., different expressions are assigned for the same field.

We can observe that such a set of incompatible expressions
is produced only by the transformation rules in Section 4.2,
which transform the same expression into a pair of expressions where Ω appears in complementary positions. This
indicates that we can always make the set S of incompatible expressions turned into an identical expression, written
lub S, by replacing the occurrences of Ω with appropriate
expressions.
The formal definition of lub S is as follows: let us write
M ¹ N if N is obtained by replacing some of the occurrences of Ω in M with arbitrary expressions. Then the binary relation ¹ induces a partial order with Ω being theleast element. For any finite set S of expressions, we write
lub S to denote the least upper bound of S w.r.t. ¹, if any.
In particular, lub ∅ = Ω.
As an example of the relaxed linearity condition, consider
the program given in Fig. 4. In the defining equation of the
Begin case, x0 has two application sites, in both of which theselk field of the argument is assigned tl (#selk y1) andthe sehj field is assigned tl (#sehj y1). Hence the expressions for the selk field and the sehj field are uniquelydetermined. In the same defining equation, x1 is applied todifferent arguments that have incompatible expressions forthe same field: for example, there are two different expressions for the splk field, namely, M1 = Stk Ω (#splk y0)
and M2 = Stk (End (#hk u1)) Ω. These expressions has
the least compatible expression lub {M1 , M2 } = Stk (End(#hk u1)) (#splk y0), which we use as the unique expression for the splk field. Similarly we have Stk (#lhj y0)(#sphj y0) for the sphj field.
In case there is no corresponding application site of a function for some record field, we have lub ∅ = Ω and consider Ω
as the unique expression for that field. This means we consider as if there were a virtual argument expression, which
is a record whose every field is set Ω. For example, in thedefining equation for the case of Nil in Fig. 4, there is no
application site of x0. So we consider as if there were an
invisible application site x0 (selk=Ω,sehj=Ω). We claim
this is valid, since these selk and sehj fields are never referenced in the source program and hence they would represent
unreachable points in the target program too.
The formal definition of the relaxed condition follows below.

parse’ :: L → (lhj::L, llk::L, sehk:: Stk L, selj:: Stk L, sphj:: Stk L, splk:: Stk L)→ (sehj:: Stk L, selk:: Stk L, llj::L, lhk::L, splj:: Stk L, sphk:: Stk L)
parse’ (Begin t) x0 =let x1 = parse’ t (sehk= Stk (hd (#selk x1)) (#sehk x0), selj= Stk (hd (#sehj x1)) (#selj x0), llk= #llk x0,
lhj= Begin (hd (#splj x1)), splk= Stk (End (#lhk x1)) (#splk x0), sphj= Stk (#lhj x0) (#sphj x0))in (lhk= hd (#sphk x1), llj= #llj x1, sphk= tl (#sphk x1),
splj= tl (#splj x1), selk= tl (#selk x1), sehj= tl (#sehj x1))
parse’ (End t) x0 =let x1 = parse’ t (sehk= tl (#sehk x0), selj= tl (#selj x0), llk= hd (#splk x0),
lhj= hd (#sphj x0), splk= tl (#splk x0), sphj= tl (#sphj x0))in (lhk= hd (#sehk x0), llj= hd (#selj x0), sphk= Stk (#lhk x1) (#sphk x1),
splj= Stk (#llj x1) (#splj x1), selk= Stk (#llk x0) (#selk x1), sehj= Stk (#lhj x0) (#sehj x1))
parse’ Nil x0 = (lhk= #llk x0, llj= #lhj x0, sphk=empty, splj=empty, selk=Ω, sehj=Ω)
unpcaspar :: L → L
unpcaspar x = let r = parse’ x (sehk=empty, selj=empty, lhj= #lhk r, llk=Nil, sphj=Ω, splk=Ω) in #llj r

Figure 5: Final transformation result
Definition 1. A defining equation of the form (4.1) iscalled linear if
Mipq= lub {M | M appears in the form xi (pq = M, · · · )}is well-defined for every i and pq such that i = 0 and pq ∈ ~h~kor 1 ≤ i ≤ r and pq ∈ ~l~k.
This relaxed linearity condition is always satisfied when
the original source program meets a certain linearity condition, as we will discuss in the following section.
The higher-order removal transformation in Section 3.4
can be generalized (to allow records with multiple field labels, ~h~j, ~l~k, ~h~k, and ~l~j) as follows. Every defining equation (4.1) of the higher-order function f is transformed into
the following defining equation of the first-order function f 0 .
f 0 :: σ1 → (~h~j :: σf3 ,~l~k :: σf3 ) → (~h~k :: σf3 ,~l~j :: σf3 )f 0 (C t1 . . . tc ) x0 = let x1 = f 0 tj(1) F10···
xr = f 0 tj(r) Fr0
in F00(4.2)

where F00 and Fi0 (0 ≤ i ≤ r) are defined by
F00 =
Fi0 =

Q
Q

Q
(lj = H[[N0lj ]]) ⊗ hk∈~h~k (hk = H[[M0hk ]])lj∈~l~jQ(hj = H[[Nihj ]]) ⊗ lk∈~l~k (lk = H[[Milk ]])
hj∈~
h~
j

with H being the transformation specified by the following
set of rules.
H[[let u1 = M1 · · · uv = Mv in M ]]= H[[M [u1 \M1 , . . . , uv \Mv ]]](4.3a)

H[[xi M ]] = xi

(0 ≤ i ≤ r)

(4.3b)

H[[yi ]] = xi

(0 ≤ i ≤ r)

(4.3c)

We note that the transformation rule (4.3a) never causes
infinite unwinding, since we can prove that, in every mutually recursive local definition let u1 = M1 · · · uv = Mv
in M (appearing in the intermediate transformation result),
every variable uk (1 ≤ k ≤ v) occurs in one of the expressions M1 , . . . , Mv behind some xi , i.e., in the form xi (· · ·uk · · · ). This, together with the rule (4.3b), prevents nested
unwinding.
The equation (3.3) in Section 3.4 is generalized as follows.

For every l0 ∈ ~l and j ∈ ~j,#l0 j (f L G (Q(lk = L0lk ))
lk∈l~
k

Q

= let r = f 0 L ( hj∈~h~j = #hj (GQQ( hk∈~h~k (hk = #hk r) ⊗ lk∈~l~k (lk = L00lk )))),
in #l0 j r
where L00lk = L0l0 k if l = l0 ; otherwise, L00lk = Ω.
Applying this higher-order removal transformation to parse’,
we obtain the final transformation result given in Fig. 5.

5. CONDITION FOR SUCCESSFUL
TRANSFORMATIONThis section discusses the sufficient condition on the source
program (i.e., the pair of a producer and a consumer function) for our transformation algorithm to succeed.
Let us assume that each defining equations of the producer
and consumer functions are given in the following formf (C t1 · · · tc ) x0 =let x1 = f tj(1) (p1 = M1p1 , . . . , pn = M1pn )···xr = f tj(r) (p1 = Mrp1 , . . . , pn = Mrpn )Stk a1 as1 = N1···
Stk am asm = Nm

(5.1)

q 0

in (q1 = M0q1 , . . . , qn0 = M0 n )where c, r, m ≥ 0, 1 ≤ j(i) ≤ c for every i (1 ≤ i ≤ r). We
assume Mip ’s, M0q ’s, and Nk ’s belong to a subset of welltyped first-order expressions, defined by the following grammar.
M ::= #p x0 | #q xi | as | ass | C M · · · M| Stk M M | empty | Ω
where p ∈ ~p, q ∈ ~q, 1 ≤ i ≤ r, 1 ≤ s ≤ m.
Definition 2 (Linearity condition). A function iscalled stack linear if its every defining equation in the form
(5.1) has at most one occurrence of expressions ai and asi
for each i (1 ≤ i ≤ m).
A function is called context linear if it is stack linear andthere is at most one occurrence of #p x0 for each p ∈ ~p.

A function is called recursion linear if it is stack linear,j(1), . . . , j(r) are pairwise distinct, and there is at most one
occurrence of #q xi for each i (0 ≤ i ≤ r) and q ∈ ~q.
Intuitively, a context linear function is constrained to haveat most one reference to each accumulating parameter (indexed by a distinct record label); a recursion linear function
is constrained to visit every substructure of a node of the
input datatype at most once and also every field in the returned record is referenced at most once.
We can show, subject to the following condition on thesource program, that the linearity condition required for thehigher-order transformation in Section 4.6 is satisfied andhence the transformation succeeds.
Theorem 1 (Successful transformation).
The
transformation in Section 4 succeeds, if the producer is acontext linear function and the consumer is a recursion linear function.
We can also show that a closure property holds under astronger condition.
Theorem 2 (Closure). If the transformation in Section 4 is applied to a pair of a producer function and a consumer function that are both context and recursion linear,then the result is also a context and recursion linear function.
In the previous sections, we have implicitly exploited thisproperty. The functions we have considered so far are allboth context and recursion linear and hence we were able
to apply our transformation algorithm repeatedly to derivea single function that fuses three functions.

6.

RELATED WORKTo the best of author’s knowledge, there has been no proposal of a fusion transformation for functions that allows
both stacks and accumulating parameters. Recent studies
on fusion has seen significant advances in dealing with accumulating parameters [13, 21, 25], but none of them deal
with stacks.
Our transformation algorithm, as for fusion of functions
with accumulating parameters, has a competitive transformation power to Voigtländer’s lazy composition [25] — bothof them allow the pair of a context linear producer function
and a recursion linear consumer function. Also, they makeuse of the circular tupling technique. Interestingly, despiteof these similarities, they are based on quite different transformation principles. Lazy composition is an algorithmic
instance of unfold/fold-technique [3], while ours are driven
by a series of type-directed transformations. We leave more
precise comparison to future investigation.
Apart from the researches in functional programming, similar program composition techniques have been studied for
attribute grammars as well. Ganzinger and Giegerich [6]developed an algorithm, called descriptional composition,
where accumulating parameters are allowed as so-called inherited attributes. Recently, Nakano [15] extended this composition method to allow stacks.
The present work draws some ideas from their work —use of record labels and flattening of nested records. However, we emphasize that the present work provides an alternative, modular presentation of the same transformation,

whereas the attribute grammar composition method has a‘big’ transformation step that is hardly modularized. The
modularity of our transformation algorithm is achieved byrepresenting intermediate transformation results as higherorder programs, which cannot be expressed in attribute grammars. We also note that our algorithm allows non-recursion
linear producer functions (Theorem 1), which cannot be
expressed within the limited recursion scheme of attributegrammars.

7.

CONCLUSION AND FUTURE WORK

We have presented a new program transformation algorithm for fusion that allows both stacks and accumulating
parameters. The proposed algorithm is partly comprised ofsome of the transformation techniques that have been developed in the communities of functional programming [8, 1, 17]
and attribute grammars [6, 15], but reformulates and refines
them into a series of type-directed transformations, leading
to a logically clean account for the transformation process.
We have also shown that the transformation algorithm, under a linearity condition, satisfies a closure property, whichallows repeated applications of fusion.
Our algorithm eliminates all the intermediate data structures created by the producer function and yields a firstorder program that uses accumulating parameters and stacks,
on which parts of the final output are held. However, theelimination of intermediate data structures alone does notnecessarily imply a better efficiency, due to the following factors that may degrade the overall run-time efficiency. (i) The
record type flattening in Section 4.5 duplicates every record
field of the producer function by the number of record labelsof the consumer function. This indicates that the execution
cost of each recursive call is increased by a constant factor. (ii) Tupling/untupling operations on records arise pereach recursive call. In other words, records in the resulting
program could be seen as another intermediate structure.
(iii) The resulting function includes a circular let, whose execution could be costly.
These factors of deterioration would be compensated by apost-optimization on the resulting program, however. (Theconcern of this paper is on the derivation of the fusion algorithm and the empirical study on the effect of optimizations
discussed below is left to future investigation.) Voigtländer[25] proposed a post-processing method for reducing “ballasts” in his fused programs (tupling/untupling, circular let,etc.) Van Groningen [23] proposed a compiler optimization
technique for reducing the overhead raised by allocations oftuples. These techniques would be effectively applied to our
fusion results, too. Another prospective direction would beapplication-specific optimizations. In [16, 18], Nakano andthe author developed an algorithm that derives memory efficient XML stream transformers from the result of attributegrammar composition. Refining this method so that it applies to a class of programs involving stacks would be aninteresting topic for future research.
In this paper, we consider stacks in producer functions
only and defined stacks as a datatype that has only one data
constructor. These are not a fundamental restriction of thealgorithm, however. It is easy to allow stacks in consumer
functions, in which case the resulting program would involve“stacks of stacks”. We may also refine our algorithm so thatstacks are defined as a datatype with an explicit empty stack
constructor and with additional stack constructors as well.

(This would be useful, say, for parsing a language that comprises of two or more kinds of braces.) Putting it more general, we may even allow any polynomial datatypes in place ofstacks. Nevertheless, to deal with datatypes that consist of
two or more constructors generally, we would need to allow
case distinction over these constructors. This would complicate the transformation process to a considerable degree,
as so does the extension of the attribute grammar composition with conditionals [2]. A complete solution to this issue
would require further elaboration and is left to future work.

Acknowledgment
I am grateful to Masahito Hasegawa and Jacques Garrigue
for their valuable comments on an earlier draft. I also thankanonymous reviewers, whose comments were very helpful for
improving the paper.

8.

REFERENCES[1] R. S. Bird. Using circular programs to eliminate multiple traversals of data. Acta Informatica, 21:239–250,
1984.
[2] J. Boyland and S. L. Graham. Composing tree attributions. In Proc. of the 21th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages,
pages 375–388. ACM Press, 1994.
[3] R. M. Burstall and J. Darlington. A transformation
system for developing recursive programs. Journal of
ACM, 24(1):44–67, 1977.
[4] W.-N. Chin. Safe fusion of functional expressions II:
Further improvements. Journal of Functional Programming, 4(4):515–555, 1994.
[5] O. Chitil. Type inference builds a short cut to deforestation. In Proc. of International Conference on Functional Programming (ICFP’99), pages 249–260. ACM
Press, 1999.
[6] H. Ganzinger and R. Giegerich. Attribute coupledgrammars. In Proceedings of the ACM SIGPLAN ’84
Symposium on Compiler Construction, volume 19(6) of
SIGPLAN Notices, pages 157–170, June 1984.
[7] A. Gill. Cheap Deforestation for Non-strict Functional
Languages. PhD thesis, University of Glasgow, 1996.
[8] A. Gill, J. Launchbury, and S. Peyton Jones. A short
cut to deforestation. In Proc. of the Conference on
Functional Programming Languages and Computer Architecture, pages 223–232. ACM Press, June 1993.
[9] The Haskell home page. http://www.haskell.org/.
[10] J. E. Hopcroft, R. Motwani, and J. D. Ullman. Introduction to automata theory, languages, and computation. Addison-Wesley, 2nd edition, 2001.
[11] Z. Hu, H. Iwasaki, and M. Takeichi. Deriving structural
hylomorphisms from recursive definitions. In Proc. ofInternational Conference on Functional Programming,
pages 73–82, Philadelphia, Pennsylvania, May 1996.
[12] P. Johann. Short cut fusion is correct. Journal of Functional Programming, 13(4):797–814, 2003.
[13] K. Kakehi, R. Glück, and Y. Futamura. An extensionof shortcut deforestation for accumulative list folding.
IEICE Transactions on Information and Systems, E85D(9):1372–1383, 2002.
[14] J. Launchbury and T. Sheard. Warm fusion: Derivingbuild-catas from recursive definitions. In International
Conference on Functional Programming Languages andComputer Architecture, (FPCA’95), pages 314–323.
ACM Press, 1995.
[15] K. Nakano. Composing stack-attributed tree transducers. Technical Report METR–2004–01, Department ofMathematical Informatics, University of Tokyo, Japan,
2004.
[16] K. Nakano and S. Nishimura. Deriving event-based document transformers from tree-based specifications. In
LDTA’2001 Workshop on Language Descriptions, Tools
and Applications, volume 44 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 2001.
[17] S. Nishimura. Correctness of a higher-order removaltransformation through a relational reasoning. In Programming Language and Systems, First Asian Symposium, APLAS 2003 Proceedings, volume 2895 of
LNCS, pages 358–375. Springer Verlag, 2003. A fullversion is available as a preprint Kyoto-Math 200306 from http://www.math.kyoto-u.ac.jp/~susumu/
papers/aplas03-long.ps.gz.
[18] S. Nishimura and K. Nakano. XML stream transformer
generation through program composition and dependency analysis. submitted.
[19] A. Pitts. Parametric polymorphism and operational
equivalence. Mathematical Structures in Computer Science, 10(3):321–359, 2000.
[20] T. Sheard and L. Fegaras. A fold for all seasons. In
International Conference on Functional Programming
Languages and Computer (FPCA’93), pages 233–242.
ACM Press, 1993.
[21] J. Svenningsson. Shortcut fusion for accumulating parameters & zip-like functions. In Proc. of the 2002
International Conference on Functional Programming,
2002.
[22] A. Takano and E. Meijer. Shortcut deforestation in calculational form. In Proc. of International Conference
on Functional Programming Languages and Computer
Architecture (FPCA’95), pages 306–313. ACM Press,
1995.
[23] J. H. van Groningen. Optimising recursive functions
yielding multiple results in tuples in a lazy functional
language. In Implementation of Functional Languages,
11th International Workshop, IFL’99, volume 1868of Lecture Notes in Computer Science, pages 59–76.
Springer Verlag, 1999.
[24] J. Voigtländer. Using circular programs to deforest inaccumulating parameters. In ASIAN Symposium on
Partial Evaluation and Semantics-Based Program Manipulation, pages 126–137. ACM Press, 2002.
[25] J. Voigtländer. Using circular programs to deforest inaccumulating parameters. Higher-Order and Symbolic
Computation, 17(1), 2004.
[26] P. Wadler. Theorems for free! In International Conference on Functional Programming and Computer Architecture (FPCA’89), pages 347–359. Addison-Wesley,
1989.
[27] P. Wadler. Deforestation: transforming programs
to eliminate trees. Theoretical Computer Science,73(2):231–248, June 1990.