EPiC Series in Computing
Volume 39, 2016, Pages 1–13
SCSS 2016. 7th International Symposium on
Symbolic Computation in Software Science

Automatic Staging via Partial Evaluation Techniques
Kenichi Asai1 and Yukiyoshi Kameyama2
1

Ochanomizu University, Japan
asai@is.ocha.ac.jp
2
University of Tsukuba, Japan
kameyama@acm.org
Abstract

Partial evaluation and staging are two of the well-known symbolic manipulation techniques of programs which generate efficient specialized code. On one hand, partial evaluation provides us with anautomatic means to separate a program into two (or more) stages but its behavior is perceived as hard
to control. On the other hand, staging (or staged calculus) requires us to manually separate a program
but with full control over its behavior. In the previous work, the first author introduced a framework
to relate the two techniques, giving a unified view to the two techniques. In this paper, we extend theframework to handle the cross-stage persistence (CSP) and show that the 2-level staging annotation
obtained by the automatic separation is the best staging annotation in a system where CSP is allowed
for base-type values only. In the presence of CSP for higher-type values, on the other hand, there is no
single annotation that is better than all the other annotations.

1

Introduction

Programming languages for staged computation prevail; they allow programmers to write code
generators that exploits domain-specific knowledge and optimizations, thus allowing generationof efficient code. They are used in a wide range of application domains including numericcomputation [8, 10], image processing [11], and other high-performance computing applications[2, 15]. Staged languages including MetaOCaml [7, 14] let programmers control the behavior
of code generators, by manually inserting staging annotations.
Although their manual insertion allows the fine control which is often necessary for expressing domain-specific optimizations, it soon becomes cumbersome for increasingly large programs,
especially when the process is mechanical. This situation is in contrast to partial evaluation [6]where binding-time analysis automatically separates a program into multiple stages and thus no
manual intervention is needed. Even though binding-time analysis sometimes requires careful
modification of the source program to produce satisfactory results, it can certainly save theprogrammers’ efforts for manual separation.
To benefit from both approaches, our previous work [1] introduced a unified framework that
relates the staged λ-calculus (the base theory for staged languages) with the 2-level λ-calculus(the base theory for partial evaluation), and showed that they are essentially the same.
In this paper, we extend the previous framework to handle cross-stage persistence (CSP)
which appears in many staged languages. We are particularly interested in the problem of
J.H.Davenport and F.Ghourabi (eds.), SCSS 2016 (EPiC Series in Computing, vol. 39), pp. 1–13

Automatic Staging via Partial Evaluation Techniques

Asai and Kameyama

finding the best staging annotation where the best staging annotation informally means thata program with it generates the most evaluated (specialized) code. The problem turns out tobe non-trivial in the presence of CSP; defining the best annotation is already problematic instaged languages.
Our results show that, for a calculus with CSP restricted to base-type values, we can define
the best staging annotation naturally, and an algorithm to obtain the best staging annotation
by transforming the result of binding-time analysis to staging annotations.
Interestingly, if we allow CSP of higher-type values, things change drastically. We show thatin the presence of CSP of higher-type values, there are distinct staging annotations neither ofwhich is better than the other, which means that there is no best staging annotation in thissetting. Such discussion becomes possible because we can define a natural notion of the beststaging annotation.
The contributions of this paper are summarized as follows.
• We define the best staging annotation in terms of binding times of terms and types.
• We show an algorithm to obtain the best staging annotation for the staged λ-calculus with
CSP of base-type values.
• We show that in the presence of CSP of higher-type values, there does not necessarily exist
the best staging annotation.
Glossary. Staged computation separates a program into multiple stages. At runtime, earlierstage (compile-time) computation is first performed, leaving later-stage (runtime) computationas code values, effectively achieving code generation. In this paper, we focus on a certain kindof staged computation where we write staging annotations on terms explicitly. The staging
annotations usually include bracket to create a piece of code and escape to perform earlier-stage
computation within a code segment. In addition, it is often useful if we can use earlier-stage
values directly in the later-stage computation, which is called cross-stage persistence or CSP.
The original CSP allows any values, including higher-type values (functions), to be lifted to laterstages. Some staged languages restrict the use of CSP to base-type values (non-function values
such as integers and strings) and higher-type primitives (such as the predefined + operation).
Partial evaluation, on the other hand, is a program transformation technique that, given a
general program and some of its input, produces a specialized efficient version of the programusing the given input. The offline variant of partial evaluation first separates a program into
multiple stages by assigning each program part a binding time indicating if it can be executedat partial evaluation time. The two-stage binding times consist of static (known at partial
evaluation time) and dynamic (deferred to runtime). Partial evaluation then executes all thestatic parts to produce a specialized program.
Organization. The paper is organized as follows. We introduce the staged λ-calculus in
Section 2 and discuss various forms of CSP in Section 3. We then introduce the 2-level λcalculus and discuss the best binding time in Section 4. In Section 5, we relate the two calculi
and show how to obtain the best staging annotation from the result of binding-time analysis.
Related work is in Section 6 and the paper concludes in Section 7.

2

Staged λ-calculus

The base calculus we consider is a simply-typed λ-calculus extended with integers and additions.
We assume that the input term is already well typed according to the standard typing rules as2

Automatic Staging via Partial Evaluation Techniques

raw types:
raw terms:
typing rules:teΓ ` i : int

Asai and Kameyama:= int | t1 → t2:= i | x | e1 @ e2 | λx. e1 | e1 + e2
(TInt1 )Γ(x) = tΓ ` e1 : t2 → t1 Γ ` e2 : t2
(TVar1 )(TApp1 )Γ`x:tΓ ` e1 @ e2 : t1

Γ, x : t2 ` e1 : t1
Γ ` e1 : int Γ ` e2 : int(TLam1 )(TSum1 )Γ ` λx. e1 : t2 → t1
Γ ` e1 + e2 : int
Figure 1: Simply-typed λ-calculus
shown in Figure 1.
On top of the simply-typed λ-calculus, the staged λ-calculus introduces three new constructs(staging annotations) to handle code values (Figure 2). First, a bracket expression hei builds a
piece of code representing e. For example, h(λx. x) @ (1 + 2)i is a piece of code that applies anidentity function to the result of 1 + 2 when executed. In the MetaOCaml syntax, it is writtenas:# .<(fun x -> x) (1 + 2)>. ;;- : int code = .<(fun x_1 -> x_1) (1 + 2)>.

When the type of e is t, the type of hei becomes hti (t code in the MetaOCaml syntax). To
build a larger code value from a smaller one, we use an escape expression ∼ e. When ∼ eappears within h. . .i, the result of evaluating e, which must be a code value, is spliced in to
the surrounding code h. . .i. For example, h3+ ∼ ((λx. x) @ h1 + 2i)i evaluates to h3 + (1 + 2)i,where the function application has been reduced and its result is spliced in to the surroundingcode.
# .<3 + .~((fun x -> x) .<1 + 2>.)>. ;;- : int code = .<3 + (1 + 2)>.

Note that we cannot (yet) reduce 1 + 2 in this program as in h3+ ∼ ((λx. x) @ (1 + 2))i, because
the result of evaluating (λx. x) @ (1 + 2) is not a code value h3i but a present-stage value 3.
# .<3 + .~((fun x -> x) (1 + 2))>. ;;Error: This expression has type int but an expression was expected of type
int code
To reduce 1 + 2, we need to turn the integer 3 to a code value h3i. The % expression isused for this purpose. By writing %x, we can use a base-type variable x holding a presentstage value (i.e., a non-code value) at the future stage (i.e., within h. . .i). For example,
h3+ ∼ ((λx. h%xi) @ (1 + 2))i evaluates to h3 + 3i. The present-stage value 3 in x is promoted
to a code value at h%xi and is spliced in to the surrounding code.1# .<3 + .~((fun x -> .<x>.) (1 + 2))>. ;;- : int code = .<3 + (* CSP x *) Obj.magic 3>.

Another way to reduce 1 + 2 is to insert % in front of 1 + 2 as in h3+ ∼ ((λx. x) @ %(1 + 2))i.
The result of 1 + 2 (i.e., 3) is promoted to a code value h3i, and passed to the identity function
1 In MetaOCaml, this promotion of variables is done automatically. We do not have to write it explicitly.

3

Automatic Staging via Partial Evaluation Techniques

staged types:
staged terms:
typing rules:teΓ `b i : int

Asai and Kameyama:= int | t1 → t2 | ht1 i:= i | x | e1 @ e2 | λx. e1 | e1 + e2 | he1 i | ∼ e1 | %e1(TInt2 )Γ(xb ) = tΓ `b e1 : t2 → t1 Γ `b e2 : t2
(TVar2 )(TApp2 )Γ `b x : tΓ `b e1 @ e2 : t1

Γ, xb : t2 `b e1 : t1
Γ `b e1 : int Γ `b e2 : int(TLam2 )(TSum2 )Γ `b λx. e1 : t2 → t1
Γ `b e1 + e2 : intΓ `0 e1 : ht1 iΓ `1 e1 : t1
Γ `0 e1 : int(TCod2 )(TCsp2 )(TEsc2 )Γ `0 he1 i : ht1 iΓ `1 ∼ e1 : t1
Γ `1 %e1 : int
Figure 2: Staged λ-calculus
λx. x. The final result becomes h3 + 3i. (We cannot show this example in MetaOCaml, since
MetaOCaml does not support promotion of an expression other than a variable — but we canemulate it; see Section 3.1). The promotion of present-stage values to the future stage is calledcross-stage persistence or CSP. There are several forms of CSP and we will discuss them in thenext section.
The typing rules for the staged λ-calculus are shown in Figure 2. The typing judgement has
the form Γ `b e : t, which reads: under a typing environment Γ, a term e has type t at stageb. The stage b indicates within how many brackets h. . .i the term e is located. For example,
λx. x in h(λx. x) @ (1 + 2)i is at stage 1. Within a bracket, an escaped expression is at stage
0 because it is evaluated at the present stage ((TCod2 ) and (TEsc2 )). For example, λx. x in
h3 + ∼ ((λx. x) @ h1 + 2i)i is at stage 0. When % is used, a present-stage value is promoted to
the later stage (TCsp2 ). The stage changes only when hei, ∼ e, or %e is used. The stage stays
the same for the other standard constructs.
If an expression is surrounded by more than one bracket, the stage can be bigger than 1.
For example, 1 + 2 in hh1 + 2ii is at stage 2. In this paper, however, we restrict ourselves totwo stages only, and thus the stage b is either 0 or 1.

3

Variations of Cross-Stage Persistence

In the previous section, we introduced a staged λ-calculus that allows CSP for arbitrary expressions, but restricted to base types (the rule TCsp2 in Figure 2). This differs from the current
MetaOCaml which allows CSP for variables of arbitrary type.
In this section, we discuss the difference and justify our choice.

3.1

CSP of Arbitrary Expressions vs. CSP of Variables

The rule TCsp2 in Figure 2 allows us to promote an arbitrary expression e1 , whereas MetaOCaml
allows the promotion of variables only. This does not bring an essential difference; instead ofwriting the expression %e, we can write (λx. h%xi) @ e which is typable if and only if %e istypable, and the two terms have the same operational behavior. (We elide the operationalsemantics of the calculi, as it is fairly standard. See [14] for instance.)
Although this paper employs a calculus that supports CSP of arbitrary expressions, theresults in this paper carry over to a calculus with CSP of variables only via the above encoding.
4Automatic Staging via Partial Evaluation Techniques

3.2

Asai and Kameyama

CSP of Base-Type Values vs. CSP of Higher-Type Values

The rule TCsp2 imposes a restriction that an expression of only base type can be promoted.
We could obtain a calculus closer to the current MetaOCaml by allowing CSP of higher-type
expressions. However, as we will see below, we would then lose an important property that thebest staging annotation always exists.
Consider the term λp. (λf. p @ f @ (f @ 1)) @ (λx. (λy. y) @ x). In this term, the function
λx. (λy. y) @ x is bound to f and used twice. By regarding p as a pairing function, we can thinkof the term as returning a pair of f and f @ 1.
Suppose we are given the above term and the type h((int → int) → (int → int)) → inti, andare asked to add staging annotations to the term such that the resulting staged term has thetype above. What would be the best annotations? By the best annotation, we informally mean
the one that evaluates to the most reduced form. (The precise definition of the best annotation
is non-trivial, and will be given in the next section.)
The point here is that the function λx. (λy. y) @ x bound to f is used in two different ways,
but we can annotate it in only one way (i.e., monovariantly). Since the value of p is not available
yet, we have to leave the application of p in the resulting code.
The best annotation that does not use CSP is given as follows:
hλp. ∼ ((λf. hp @ ∼ f @ (∼ f @ 1)i) @ h(λx. ∼ ((λy. y) @ hxi))i)i
which evaluates to hλp. p @ (λx. x) @ ((λx. x) @ 1)i. Although λx. (λy. y) @ x is reduced to λx. xwhich is inlined in place of f , the application of λx. x to 1 is not reduced, because λx. x is apiece of code and cannot be applied. In the presence of CSP of higher-type values, on the other
hand, we can annotate the above term as follows:
hλp. ∼ ((λf. hp @ %f @ ∼ (f @ h1i)i) @ (λx. (λy. y) @ x))i
which evaluates to hλp. p @ f @ 1i where f is a pointer to the runtime value representing theclosure λx. (λy. y) @ x. Here, λx. (λy. y) @ x is evaluated to a closure and is used to reducef @ 1. However, since f is bound to a runtime closure rather than a piece of code, the resultof evaluation contains a pointer to the runtime value (closure) and cannot be represented asa program text. It may not be a problem, if we only have to execute the resulting codeand do not have to obtain the result as a printable program text. A bigger problem is that
λx. (λy. y) @ x evaluates to a closure under call-by-value and its body is not reduced. Thus, theresult behaves in the same way as hλp. p @ (λx. (λy. y) @ x) @ 1i, which is clearly unsatisfactory,
because (λy. y) @ x is not reduced.
Without CSP of higher-type values, we could reduce the body of λx. (λy. y) @ x but not
f @ 1. With CSP of higher-type values, the situation is the other way around. Thus, neither
solution is better than the other. To reduce f @ 1, we need to classify λx. (λy. y) @ x as apresent-stage function whereas to reduce its body, we need to classify it as a piece of code. Put
differently, we need polyvariant annotation: we need to annotate λx. (λy. y) @ x in two differentways.
CSP of higher-type values is thus problematic. One simple case where CSP of higher-type
values is useful is CSP of primitive functions such as + or functions defined in other modules.
Since they are already in the reduced form, we do not encounter the above problem; we only
have to treat the references to them as runtime values, and use CSP to embed them into codevalues.
5

Automatic Staging via Partial Evaluation Techniques

4

Asai and Kameyama

The Best Binding Time

Given an unannotated well-typed term and its staged type, we want to add staging annotations
to the term to obtain a staged term which has the specified type. For this problem, there aremany possible staging annotations in general. In this section, we consider the best staging
annotation among them. Intuitively, the best staging annotation is the one that evaluates
as many expressions and as early as possible, which would result in the most reduced form.
However, since staging annotations express only the stage of each expression and not whether
the expression is a code value or not, we cannot immediately judge which staging annotation
is better. Furthermore, there exist distinct but equally good staging annotations.
For example, consider the following three staged terms of the same type that we saw earlier:h3+ ∼ ((λx. x) @ h1 + 2i)i
h3+ ∼ ((λx. h%xi) @ (1 + 2))ih3+ ∼ ((λx. x) @ h%(1 + 2)i)i
In the first annotation, 1 + 2 is at stage 1 but x is at stage 0. In the second one, 1 + 2 is atstage 0 but x occurs in the stage 1 context. Thus, the stages of expressions do not apparently
tell us which annotation is better. Furthermore, although the second and the third ones havedifferent staging annotations, they both reduce to the same result. These examples show that
it is difficult to find the best staging annotation by simply looking at the staging annotations.
What we really want to know is the stages of the values of expressions (rather than thestages of the expressions). In the first annotation, both 1 + 2 and x are code values. In thesecond one, they are both integers. In the third one, 1 + 2 is an integer but x holds a codevalue. Because we obtain more reduced form if we know values of expressions earlier, we canconclude that the second one is a better annotation than the first one. Even for equally goodstaging annotations (that reduce to the same result), we can introduce a sensible order: thesecond one is better than the third one, because the value of x is known earlier; it would havebeen in fact the better annotation if x were used within the body of the lambda abstraction.
How can we obtain the stages of the values of expressions? The answer is well known in thepartial-evaluation community — by binding-time analysis.

4.1

2-level λ-calculus

Given a well-typed term, binding-time analysis assigns a binding time to each of its subexpressions and types, producing a term in the so-called 2-level λ-calculus [4]. Figure 3 shows avariant of the 2-level λ-calculus formulated as a multi-level λ-calculus [3] restricted to 2 levels.
The binding time takes a value of either 0 (static; meaning the expression is at stage 0) or 1
(dynamic; meaning the expression is at stage 1, producing a piece of code). A binding time ofa type represents when the value of an expression of that type is available. The base types int0
and int1 represent that an integer is available at stage 0 and 1, respectively. For the function
type, not only the toplevel type but also its argument and result types come with binding times.
When the toplevel binding time is static, it means that the function is available at stage 0: it
can be applied to either a static or dynamic argument and produce either a static or dynamic
result. If the toplevel binding time of a function is dynamic, on the other hand, the function isa piece of code. In this case, both the argument and result types must also be dynamic. This
constraint is formalized as the well-formed condition on types shown in Figure 3.
In contrast to the binding time of a type, a binding time of a term represents when theterm can be evaluated. A present-stage integer has the binding time 0, while integer code has
6Automatic Staging via Partial Evaluation Techniques

binding times:bannotated types: tb
annotated terms: eb
well-formed types:

Asai and Kameyama:= 0 | 1:= intb | t1 b1 →b t2 b2:= ib | xb | e1 b1 @b e2 b2 | λb x. e1 b1 | e1 b1 +b e2 b2 | %1 e0
t1 b1 wft t2 b2 wft b ≤ b1 b ≤ b2
(t1 b1 →b t2 b2 ) wft

intb wft
typing rules:(TInt3 )Γ ` ib : intb

Γ(xb ) = t1 b1
Γ ` xb : t 1 b1

0

0

Γ, xb : t2 b2 ` e1 b1 : t1 b1bΓ ` λ x. e1Γ ` e1 b1 : intbb01b

Γ ` e1 b1 +b e2 b2 : int0Γ ` e2 b2 : t2 b20Γ ` e1 b @b e2 b2 : t1 b1

t2 b2 wft b ≤ b1
: t2

Γ ` e2 b2 : intb0

Γ ` e1 b : t2 b2 →b t1 b1(TVar3 )

b2

b

→ t1

(TSum3 )b1b ≤ b2(TApp3 )(TLam3 )Γ ` e0 : int0 (TCsp )3
Γ ` %1 e0 : int1

Figure 3: 2-level λ-calculus with lifting (0: static, 1: dynamic)
the binding time 1. The binding time of a variable is determined by the time the variable
is introduced. A static variable can hold either a static or dynamic value, while a dynamic
variable is a code value representing the variable itself. An application is static when thefunction part is static and can be applied. In that case, the result of application can be either
static or dynamic depending on the result type of the function. Note that the binding time ofan application and the binding time of the type of the application may be different. The former
represents whether the application can be reduced, while the latter represents what we obtainas the result of application. A static and dynamic abstraction introduces a static and dynamic
variable, respectively. The condition on binding times ensures that the introduced function typeis well formed. Addition can be done statically only when both of its arguments are available.
This constraint is expressed by having the same binding time b for the addition and the types of
its arguments. Finally, %1 e0 represents CSP (or lifting in the partial-evaluation terminology)
of a base-type expression.

4.2

Binding-Time Analysis

Given a well-typed term, the binding-time analysis proceeds by attaching binding times to theterm and its type according to the typing rules in Figure 3. However, although the typing
rules are mostly syntax directed, the rule TCsp3 is not: we cannot decide syntactically where
to insert TCsp3 . To decide where to insert TCsp3 , we introduce the following slightly modified
typing rule:0Γ ` eb0 : intb0 b00 ≤ b1
(TCsp03 )Γ ` %b1 eb0 : intb1
and insert % to all the subexpressions of type int. After all the binding-time variables obtainconcrete values, we check if the inequality b00 < b1 in TCsp03 holds. If it does, we leave % intact;
we delete it otherwise.
7

Automatic Staging via Partial Evaluation Techniques

Asai and Kameyama

For example, the term λs. λd. (λx. x + s) @ d of type int → int → int is converted toλs. λd. %((λx. %(%x + %s)) @ %d). We can then construct a typing derivation in a syntaxdirected way, introducing binding-time variables to each subterm and type and collecting constraints on them. The typing derivation for λs. λd. %((λx. %(%x + %s)) @ %d) is shown as
follows. In this derivation, unification of binding-time variables are already resolved; alternatively, we can express unification as two symmetric inequality constraints.
(TVar3 )(TVar3 )Γ ` xb4 : intb7
Γ ` sb1 : intb8
0(TCsp3 )(TCsp03 )Γ0 ` %b6 xb4 : intb6
Γ0 ` %b6 sb1 : intb6(TSum3 )Γ0 ` %b6 xb4 +b6 %b6 sb1 : intb6(TCsp03 )(TVar3 )Γ, xb4 : intb7 ` %b5 (%b6 xb4 +b6 %b6 sb1 ) : intb5
Γ ` db2 : intb9(TLam)(TCsp03 )3
Γ ` λb4 x. %b5 (%b6 xb4 +b6 %b6 sb1 ) : intb7 →b4 intb5
Γ ` %b7 db2 : intb7(TApp3 )Γ ` (λb4 x. %b5 (%b6 xb4 +b6 %b6 sb1 )) @b4 %b7 db2 : intb5(TCsp03 )sb1 : intb8 , db2 : intb9 ` %b3 ((λb4 x. %b5 (%b6 xb4 +b6 %b6 sb1 )) @b4 %b7 db2 ) : intb3(TLam3 )sb1 : intb8 ` λb2 d. %b3 ((λb4 x. %b5 (%b6 xb4 +b6 %b6 sb1 )) @b4 %b7 db2 ) : intb9 →b2 intb3(TLam3 )` λb1 s. λb2 d. %b3 ((λb4 x. %b5 (%b6 xb4 +b6 %b6 sb1 )) @b4 %b7 db2 ) : intb8 →b1 intb9 →b2 intb3
where Γ = sb1 : intb8 , db2 : intb9 and Γ0 = Γ, xb4 : intb7 . The collected constraints are as follows:b1 ≤ b2b5 ≤ b3

b1 ≤ b8b6 ≤ b5b2 ≤ b3b7 ≤ b6

b2 ≤ b9b8 ≤ b6

b4 ≤ b5b9 ≤ b7b4 ≤ b7for (TLam3 )for (TCsp03 )After collecting constraints on binding-time variables, we assign concrete binding times toall the binding-time variables that satisfy the constraints and the initial constraint given by
the user. The initial binding-time constraint specifies variables that are available only at stage
1. For example, if we want to obtain the binding times where the variable s is known early atstage 0, but d is known only at stage 1, we specify b2 = 1 as the initial constraint. Without theinitial constraint, we can always obtain the best solution trivially: i.e., bi = 0 for all i.
There is an efficient algorithm to obtain the best solution of the constraints [5]. We firstset bi = 0 for all i. We then raise the value of a binding-time variable to 1 if it is specified as
1 in the initial constraint. Whenever the value of a binding-time variable bi is raised to 1, wesearch for constraints of the form bi ≤ bj for some j. When such j is found, bj is also raised to
1 (if it is not raised to 1 yet). We continue this process until values of binding-time variables
are no longer raised and become stable.
For example, from the initial constraint b2 = 1, and the constraints b2 ≤ b3 and b2 ≤ b9 , weset b3 = b9 = 1. From b9 = 1 and b9 ≤ b7 , we need to have b7 = 1. From b7 ≤ b6 and b6 ≤ b5 ,we further have b6 = b5 = 1. We also have b5 ≤ b3 , but since b3 is already set to 1, we are done.
The obtained solution is:b1 = b4 = b8 = 0 b2 = b3 = b5 = b6 = b7 = b9 = 1
Among the constraints for TCsp03 , we find that the inequality holds only for b8 < b6 . Thus, we
keep % for s only. The resulting 2-level term becomes λ0 s. λ1 d. (λ0 x. x0 +1 %1 s0 ) @0 d1 . We
see that β-reduction can be performed at stage 0, but addition is deferred to stage 1. Observethat although x is at stage 0 (b4 = 0), it holds a stage 1 value (b7 = 1).
8

Automatic Staging via Partial Evaluation Techniques

4.3

Asai and Kameyama

The Best Binding TimeLet e0 be a term in the simply-typed λ-calculus, and t1 be a type in the 2-level λ-calculus.
Then a solution for these data is a term e1 in the 2-level λ-calculus such that (1) e0 and e1 are
the same except for the binding times and insertion of %, and (2) ` e1 : t1 is derivable.
Definition 1 (The best binding time). Let e0 and t1 be the same as above, and e1 and e2 besolutions for these data. We define that e1 has a better binding time than e2 does if, for all thesubexpressions of e1 other than %e, the binding time of its type is equal to or smaller than thecorresponding binding time of e2 . If e1 has a better binding time than any other solutions fore0 and t1 , e1 has the best binding time for e0 and t1 .
It is easy to show the result of binding-time analysis produces the best binding time.
Theorem 2. The result of the binding-time analysis presented in the previous section produces
the best binding time that is consistent with the initial constraint, if there is any solutions
consistent with the initial constraint.
Proof sketch. We show that the result of the binding-time analysis e1 is better than any otherterm e2 with different binding times for the same term. Suppose that there is a subexpression
where the binding time b of its type is 1 in e1 , but 0 in e2 . Since the binding-time analysis
raises the value of a binding-time variable b only when (1) it is set to 1 in the initial constraint,or (2) there is a path of constraints that transitively requires that b must be 1. Setting b = 0
violates one of these two cases. Thus, e2 cannot be a valid 2-level λ-calculus term.

5

The Best Staging Annotation

In the previous section, we have seen that we can obtain the best binding time via the bindingtime analysis. In this section, we transform the result of the binding-time analysis into astaging annotation. In the previous work [1], we have established the relationship between the2-level λ-calculus and the staged λ-calculus. Here, we review it and extend it to support CSP.
Previously, CSP of expressions were not supported and CSP of variables were supported onlyin an ad-hoc way.

5.1

Relating Binding Times and Staging Annotations

The key difference between the two calculi is that the 2-level λ-calculus maintains stages as thebinding times of types (and terms) while the staged λ-calculus maintains a stage in a judgement,
which is close to the binding times of terms. To relate these two calculi, we introduce anintermediate calculus called the staged 2-level λ-calculus that has both features; see Figure 4.
The types and terms of the staged 2-level λ-calculus are based on those of the 2-level λcalculus: every node has its own binding time. In addition, we have added a code type andstaged expressions to indicate where we should place these staging annotations. The typing
rules are also similar to the corresponding rules in the 2-level λ-calculus. The first five rules
are obtained simply by attaching a stage b to judgements. The stage b roughly corresponds
to the binding time of terms. In fact, they coincide in the conclusion of the first five rules.
However, they deviate in the premises of these rules (except for (TSum4 )). For example, in thefirst premise of (TApp4 ), the binding time of e1 is b0 rather than b: even though the application
is at stage 1, it does not necessarily mean that the function part is a piece of code; e1 can be
9Automatic Staging via Partial Evaluation Techniques

binding times:
annotated types:
annotated terms:
typing rules:

b
tb
eb

Asai and Kameyama:= 0 | 1:= intb | t1 b1 →b t2 b2 | htb i:= ib | xb | e1 b1 @b e2 b2 | λb x. e1 b1 | e1 b1 +b e2 b2 | heb i | ∼ eb | %1 e000

Γ(xb ) = t1 b1
Γ `b e1 b : t2 b2 →b t1 b1 Γ `b e2 b2 : t2 b2(TApp4 )
(TInt
)
(TVar
)
4
0
0
4
Γ `b ib : intb
Γ `b xb : t1 b1
Γ `b e1 b @b e2 b2 : t1 b1
0

Γ, xb : t2 b2 `b e1 b1 : t1 b1bΓ `b λ x. e1b01

Γ `b e1 b1 : intb

t2 b2 wft: t2b2b ≤ b1b→ t1

Γ `b e2 b2 : intb

Γ `b e1 b1 +b e2 b2 : intbb ≤ b2b1(TLam4 )(TSum4 )Γ `0 e0 : ht1 iΓ `0 e0 : int0
Γ `1 e1 : t1
(TCsp4 )
(TCod
)
(TEsc
)
4
4
Γ `0 he1 i : ht1 iΓ `1 ∼ e0 : t1
Γ `1 %1 e0 : int1
Figure 4: Staged 2-level λ-calculus (Well-formed types are defined in Figure 3.)
a function at stage 0 that produces a code value. To adjust the discrepancy between the stageof the judgement and the binding time of the term, (TCod4 ) and (TEsc4 ) are used.
Given a typing derivation of the 2-level λ-calculus, we can mechanically transform it to thetyping derivation of the staged 2-level λ-calculus by attaching stages to judgements. We startfrom the root of the tree and assign stage 0 to it. We then build a tree using the corresponding
typing rules of the staged 2-level λ-calculus. Whenever the stage of the judgement and thebinding time of the term differ, (TCod4 ) or (TEsc4 ) is used. For example, we have the following
typing derivation for the example term in Section 4.2 after removing unnecessary %.
(TVar3 )Γ ` s0 : int0 (TCsp )
(TVar
)
3
3
Γ0 ` x0 : int1
Γ0 ` %1 s0 : int1
(TSum3)
Γ, x0 : int1 ` x0 +1 %1 s0 : int1
(TLam)
(TVar3 )3Γ ` λ0 x. x0 +1 %1 s0 : int1 →0 int1
Γ ` d1 : int1
(TApp3 )s0 : int0 , d1 : int1 ` (λ0 x. x0 +1 %1 s0 ) @0 d1 : int1
(TLam3 )s0 : int0 ` λ1 d. (λ0 x. x0 +1 %1 s0 ) @0 d1 : int1 →1 int1
(TLam3 )` λ0 s. λ1 d. (λ0 x. x0 +1 %1 s0 ) @0 d1 : int0 →0 int1 →1 int1
To transform this derivation to the one for the staged 2-level λ-calculus, we first assign stage 0
to the root judgement and apply the corresponding rule to it:..
.
s0 : int0 `0 λ1 d. (λ0 x. x0 +1 %1 s0 ) @0 d1 : int1 →1 int1
`0 λ0 s. λ1 d. (λ0 x. x0 +1 %1 s0 ) @0 d1 : int0 →0 int1 →1 int1

(TLam4 )At this point, however, the binding time of the term is 1 which is different from the stage of10

Automatic Staging via Partial Evaluation Techniques

Asai and Kameyama

the judgement. To adjust the stage, we insert (TCod4 ) here:..
.
s0 : int0 `1 λ1 d. (λ0 x. x0 +1 %1 s0 ) @0 d1 : int1 →1 int1
s0 : int0 `0 hλ1 d. (λ0 x. x0 +1 %1 s0 ) @0 d1 i : hint1 →1 int1 i(TCod4 )`0 λ0 s. hλ1 d. (λ0 x. x0 +1 %1 s0 ) @0 d1 i : int0 →0 hint1 →1 int1 i(TLam4 )Notice that to insert (TCod4 ), we also need to insert staging annotations to the term and type:the conclusion of (TCod4 ) says that they must be a piece of code. By continuing this process,we obtain staged 2-level λ-calculus term. It can be shown [1] that (TCod4 ) and (TEsc4 ) aresufficient to recover the harmony between the stage of the judgement and the binding time of
the term. The final result for the above example becomes as follows, where Γ = s0 : int0 , d1 : int1
and Γ0 = Γ, x0 : hint1 i.
(TVar4 )(TVar4 )Γ0 `0 s0 : int0
(TCsp4 )Γ0 `1 ∼ x0 : int1
Γ0 `1 %1 s0 : int1
(TSum4 )Γ0 `1 ∼ x0 +1 %1 s0 : int1
(TCod4 )(TVar4 )Γ, x0 : hint1 i `0 h∼ x0 +1 %1 s0 i : hint1 iΓ `1 d1 : int1
(TLam4 )(TCod4 )Γ `0 λ0 x. h∼ x0 +1 %1 s0 i : hint1 i →0 hint1 iΓ `0 hd1 i : hint1 i(TApp
4)
s0 : int0 , d1 : int1 `0 (λ0 x. h∼ x0 +1 %1 s0 i) @0 hd1 i : hint1 i(TEsc4 )s0 : int0 , d1 : int1 `1 ∼ ((λ0 x. h∼ x0 +1 %1 s0 i) @0 hd1 i) : int1
(TLam4 )s0 : int0 `1 λ1 d. ∼ ((λ0 x. h∼ x0 +1 %1 s0 i) @0 hd1 i) : int1 →1 int1
(TCod4 )s0 : int0 `0 hλ1 d. ∼ ((λ0 x. h∼ x0 +1 %1 s0 i) @0 hd1 i)i : hint1 →1 int1 i(TLam4 )`0 λ0 s. hλ1 d. ∼ ((λ0 x. h∼ x0 +1 %1 s0 i) @0 hd1 i)i : int0 →0 hint1 →1 int1 i
Γ0 `0 x0 : hint1 i(TEsc4 )Once we obtain a typing derivation for a term in the staged 2-level λ-calculus, we can obtainthe final term in the staged λ-calculus by simply removing all the binding times. For the above
example, the final result becomes λs. hλd. ∼ ((λx. h∼ x + %si) @ hdi)i.

5.2

The Best Staging Annotation

It is now straightforward to formally define the best staging annotation.
Let e0 be a term in the simply-typed λ-calculus, and t1 be a type in the staged λ-calculus.
Definition 3 (The best staging annotation). A term e1 in the staged λ-calculus has the beststaging annotation for e0 and t1 , if the 2-level λ-calculus term corresponding to e1 has thebest binding time for the data e0 and t2 where t2 is the type in the 2-level λ-calculus whichcorresponds to t1 .
Note that since there is a one-to-one correspondence between the staged 2-level λ-calculus
and the staged λ-calculus, we can always recover the binding times of e1 and its type in thestaged 2-level λ-calculus, from which t2 is obtained by removing staging annotations.
Theorem 4. For any well-typed term e in the simply-typed λ-calculus and a type t in the staged
λ-calculus, there exists a term in the staged λ-calculus that has the best staging annotation fore and t, if there is any solution for e and t.
11

Automatic Staging via Partial Evaluation Techniques

Asai and Kameyama

Proof. For any well-typed term e, we can perform the binding-time analysis to obtain its best
binding time (by Theorem 2). By removing binding times from the result, we obtain a termin the staged λ-calculus that has the best staging annotation.
This theorem is obvious, once we set up the necessary definition for the best staging annotation and its relationship to binding times. The simple but important idea presented in thispaper is that we can define the best staging annotation in terms of binding times.

6

Related WorkSheard and Linger [12] showed a search-based binding-time analysis for MetaML. Rather thanselecting the best staging annotation, they search for all the possible staging annotations withvarious heuristics to obtain ‘good’ staging annotations earlier. Later, Linger and Sheard [9]presented a constraint-based binding-time analysis for MetaML. However, they only show theconstraints to be satisfied and do not provide the definition for the best staging annotation.
Shimizu [13] extended the latter work to support CSP and showed an algorithm to obtaina possible solution. However, it is not guaranteed to be the best staging annotation, partly
because he did not define the best staging annotation and thus there are multiple staging
annotations that are equally good. In our previous work [1], we related the staged λ-calculus
and the 2-level λ-calculus and showed that the result of binding-time analysis can be transformed
to staging annotations. In this paper, we have extended the framework to handle CSP. Also, we
have formally defined the best staging annotation and proved the existence of the best staging
annotation if there are any annotations.

7

Conclusion

In this paper, we have defined the best staging annotation in terms of the binding times of terms
and types. We then showed an algorithm to obtain the best staging annotation in the presenceof CSP of base-type values. We also discussed that in the presence of CSP of higher-type values,
there is no best staging annotation in general. In the future, we plan to extend the framework
to multiple stages. We also plan to support more realistic language constructs and ultimately
to implement the binding-time analysis in MetaOCaml.
Acknowledgements. We thank the anonymous reviewers for constructive comments. This
work is partly supported by JSPS Grant-in-Aid for Scientific Research (B) 25280020.

References[1] Kenichi Asai. Toward introducing binding-time analysis to MetaOCaml. In Proceedings of the2016 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2016,
St. Petersburg, FL, USA, pages 97–102, 2016.
[2] Zachary DeVito, James Hegarty, Alex Aiken, Pat Hanrahan, and Jan Vitek. Terra: a multistage language for high-performance computing. In ACM SIGPLAN Conference on Programming
Language Design and Implementation, PLDI ’13, Seattle, WA, USA, pages 105–116, 2013.
[3] Robert Glück and Jesper Jørgensen. An automatic program generator for multi-level specialization.
Lisp and Symbolic Computation, 10(2):113–158, 1997.

12

Automatic Staging via Partial Evaluation Techniques

Asai and Kameyama[4] Carsten K. Gomard. A self-applicable partial evaluator for the lambda calculus: Correctness andpragmatics. ACM Trans. Program. Lang. Syst., 14(2):147–172, April 1992.
[5] Fritz Henglein. Efficient type inference for higher-order binding-time analysis. In 5th ACM Conference on Functional Programming Languages and Computer Architecture, Cambridge, MA, USA,pages 448–472, 1991.
[6] Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial evaluation and automatic program
generation. Prentice Hall international series in computer science. Prentice Hall, 1993.
[7] Oleg Kiselyov. The design and implementation of BER metaocaml - system description. In
Functional and Logic Programming - 12th International Symposium, FLOPS 2014, Kanazawa,
Japan, pages 86–102, 2014.
[8] Oleg Kiselyov and Walid Taha. Relating FFTW and split-radix. In Embedded Software andSystems, First International Conference, ICESS 2004, Hangzhou, China, pages 488–493, 2004.
[9] Nathan Linger and Tim Sheard. Binding-time analysis for metaml via type inference and constraint
solving. In Tools and Algorithms for the Construction and Analysis of Systems, 10th International
Conference, TACAS 2004, Barcelona, Spain, pages 266–279, 2004.
[10] Georg Ofenbeck, Tiark Rompf, Alen Stojanov, Martin Odersky, and Markus Püschel. Spiral in
Scala: towards the systematic construction of generators for performance libraries. In Generative
Programming: Concepts and Experiences, GPCE’13, Indianapolis, IN, USA, pages 125–134, 2013.
[11] Jonathan Ragan-Kelley, Connelly Barnes, Andrew Adams, Sylvain Paris, Frédo Durand, andSaman P. Amarasinghe. Halide: a language and compiler for optimizing parallelism, locality, andrecomputation in image processing pipelines. In ACM SIGPLAN Conference on Programming
Language Design and Implementation, PLDI ’13, Seattle, WA, USA, pages 519–530, 2013.
[12] Tim Sheard and Nathan Linger. Search-based binding time analysis using type-directed pruning.
In Proceedings of the ACM SIGPLAN ASIA-PEPM 2002, Asian Symposium on Partial Evaluationand Semantics-Based Program Manipulation, Aizu, Japan, pages 20–31, 2002.
[13] Haruki Shimizu. Automatic generation of optimal code generators in staged languages (injapanese). Master’s thesis, Department of Computer Science, Graduate School of Systems andInformation Engineering, University of Tsukuba, 2014.
[14] Walid Taha. A gentle introduction to multi-stage programming. In Domain-Specific Program
Generation, International Seminar, Dagstuhl Castle, Germany, Revised Papers, pages 30–50, 2003.
[15] Naoki Takashima, Hiroki Sakamoto, and Yukiyoshi Kameyama. Generate and offshore: type-safeand modular code generation for low-level optimization. In Proceedings of the 4th ACM SIGPLAN Workshop on Functional High-Performance Computing, FHPC@ICFP 2015, Vancouver,
BC, Canada, pages 45–53, 2015.

13