Inlining as Staged Computation

STEFAN MONNIER and ZHONG SHAO

Dept. of Computer Science, Yale University, New Haven, CT 06520-8285, U.S.A.

                  (e-mail: monnier@cs.yale.edu, shao@cs.yale.edu)

Abstract

Inlining and specialization appear in various forms throughout the implementation of modern programming languages. From mere compiler optimizations to sophisticated techniques in partial evaluation, they are omnipresent, yet each application is treated differently. This paper is an attempt at uncovering the relations between inlining (as done in production compilers) and staged computation (as done in partial evaluators) in the hope of bringing together the research advances in both fields. Using a two-level lambda calculus as the intermediate language, we show how to model inlining as a staged computation while avoiding unnecessary code duplication. The new framework allows us to define inlining annotations formally and to reason about their interactions with module code. In fact, we present a cross-module inlining algorithm that inlines all functions marked inlinable, even in the presence of ML-style parameterized modules.

1 Introduction

Clear and maintainable code requires modularity and abstraction to enforce well-designed interfaces between software components. The module language of Standard ML (Milner et al., 1997) provides powerful tools for such high-level code structuring. But these constructs often incur a considerable performance penalty which forces the programmer to break abstraction boundaries or to think twice before using advanced features like parameterized modules (e.g., ML functors).

Efficient implementation of these high-level language constructs often rely crucially on function inlining. Inlining algorithms have been used for many years, but their “best-effort” behavior prevents us from knowing or making sure that a function will always be inlined (at least, wherever possible given the compilation model). For example, SML/NJ (Appel & MacQueen, 1991) has several ad-hoc tricks sprinkled in the code to expand primitive operations. These tricks tend to muddy up the abstraction boundaries so it would be nice if they could be replaced by a general-purpose inlining algorithm.

But would the inliner perform as good a job inlining those primitive operations as with the ad-hoc approaches? For simple cases, it is straightforward to ensure that primitive operations are always inlined, but when higher-order functions or even higher-order modules (such as SML/NJ functors or Java generics) come into play, coupled with separate compilation, the question becomes more challenging. In the course of implementing an extension of Blume and Appel’s cross-module inlining algorithm (1997), we tried to understand the relationship between inlining opportunities and separate compilation. We felt a need to formalize our solution to better understand its behavior.

This paper is the result of our efforts to formalize our inlining algorithm. More specifically, we borrow from the partial-evaluation community (Jones et al., 1993) to model inlining as a staged computation. By using a two-level λ-calculus (Moggi, 1997) as our intermediate language, we can assign each function (in our program) with a binding-time annotation of static or dynamic: a static function call is executed at compile time thus is always inlined, while a dynamic call is executed at run time thus is not inlined. The inlining optimization is then equivalent to the standard off-line partial evaluation: first use the binding-time analysis to locate all the inlining candidates, then run the specialization phase to do the actual inlining. The binding-time attributes can also be exported to the source level (or the compiler front-end) to serve as inlining annotations and to allow programmers (or the compiler writer) to control various inlining decisions manually.

Apparently, all partial evaluators support some form of β-reductions as part of the specialization, however, these techniques do not immediately apply to the inlining optimization. Because of the different application domains, partial evaluators are generally much more aggressive than compiler optimizers. Even the binding time annotations can pose problems at the source level because they can clutter the module interface and interact badly with ML functors; for example, we would have to add abstraction over binding-time (commonly called “binding-time polymorphism”) in the type if we want to apply a functor to modules with different binding time (but with same signature otherwise).

The main objective of this paper is to hammer out these details and to see what it would take to launch various partial-evaluation techniques into real compilers. Our paper builds upon previous work on cross-module inlining (Blume & Appel, 1997; Shao, 1998; Leroy, 1995) and two-level λ-calculus (Moggi, 1997; Nielson & Nielson, 1992; Davies & Pfenning, 1996; Taha & Sheard, 1997) but makes the following new contributions:

• As far as we know, our work is the first comprehensive study on how to model inlining as staged computation. The formalism from the staging calculus allows us to explicitly reason about and manipulate the set of inlinable functions. Doing such reasoning is much harder with a traditional inlining algorithm, especially in the presence of ML-style parameterized modules.

• By careful engineering of binding-time coercions, and combined with proper staging and splitting, we show how to model inlining as staged computation without introducing unwanted code duplication (see Sec. 5).

• Adding inlining annotations to a surface language allows a programmer to mark a function as inlinable explicitly. Inlining annotations, however, could pollute the module interface with additional binding-time specifications. This makes the underlying module language more complex. We show how to support inlining annotations while still avoiding such pollution. In fact, our scheme is fully compatible with ML-style modules and requires no change to its module language.

• Using a two-level λ-calculus, we show how inlining annotations are compiled into the internal binding-time annotations and how they interact with the module code. This allows us to propagate inlining information across arbitrarily functorized code, even in the presence of separate compilation.

• We extend binding-time coercions to work with parametric polymorphism.

The rest of this paper is organized as follows: Section 2 gives an overview of a compiler that

Source Language

Typed SRC (Sec. 3) (Sec. 5) Staging+Split

[figure: TLC (Sec. 4); Import Summaries (Sec. 6); Partial Evaluation (Sec. 4)]

TLC

(no static redexes)

\overline{}Export Summary (Sec. 6)

BTR+Opts

(Sec. 5.3) λ-Split

Residual Code

Machine Code

Fig. 1. Structure of the compiler

supports cross-module inlining and shows how inlining annotations (at the source level) and two-level λ-calculus (as intermediate language) fit into the picture; Section 3 formally defines our source language SRC which supports inlining annotations and (indirectly) MLstyle modules; Section 4 formally defines our target language TLC which is a two-level λ-calculus supporting staged computation; Section 5 presents our detailed algorithm for compiling SRC programs into TLC; the algorithm involves staging, splitting, and careful insertion of binding-time coercions; Section 6 shows how to handle top-level issues for inlining across multiple compilation units; Section 7 then presents several extensions over the basic algorithm; finally, Section 8 and 9 describe related work and then conclude.

2 The Big Picture

To model inlining as staged computation, we first give an overview of a compiler that supports cross-module inlining. We use our FLINT compiler (Shao, 1997b; Shao et al., 1998) as an example. Figure 1 shows various stages of compilation used in the compiler. The source code is first turned into a strongly typed intermediate language based on a predicative System-F calculus (we name it SRC and present its details in Sec. 3). The SRC calculus contains a module language and a core language. Each core-language function is annotated with inlining hints to indicate whether the function should be inlined or not. Those hints could be provided by the user or by the earlier phases of a compiler (using some inlining heuristics).

The inlining hints are then turned into staging annotations, mapping inlinable functions to static functions (functions executed at compile-time) and the rest to dynamic code (executed at run-time), by translating the code into a two-level intermediate language extended with polymorphism (we name it TLC and present its details in Sec. 4).

To minimize the performance cost of the module code, we want to mark it as static so as to expose as many inlining opportunities as possible. But this would imply that each functor application (SML’s equivalent to template instantiation) would create a duplicate copy of the full functor body. This approach, while sometimes acceptable, can lead to excessive code growth and compilation times for heavily functorized code, as any programmer who has worked with C++ templates knows.

We use a variant of the λ-splitting technique (Blume & Appel, 1997) to split each module function into a static part and a dynamic part. This splitting is done carefully to ensure that it does not obfuscate any inlining opportunity. Splitting is done together with staging in the main translation algorithm (see Sec. 5.4). The resulting code is completed by incorporating a copy of the summaries from all the import modules (see Sec. 6); a summary contains the code that should be inlined across compilation-units, similarly to OCaml’s approximations (Leroy, 1995).

The static part of the code is then reduced by a straightforward partial evaluation returning the same code but with no remaining static redexes. This code then goes through a binding-time refinement (BTR) or other optimization phases which could introduce new static code requiring a new pass through the partial evaluator.

Once these optimization steps are finished, we reuse the λ-splitting algorithm to split the compilation-unit itself into a summary containing all the remaining static code (i.e. inlinable code for future cross-compilation-unit inlining) and a fully dynamic residual code (encompassing the bulk of the program) which is then passed to the code generator.

Inlining across compilation units increases the coupling between those units. If a unit is modified, all units that import it will now need to be recompiled, even if the modification was only internal and did not change the interface. This is automatically handled in our case by a compilation manager (Blume, 1995).

3 The Source Calculus SRC

This section formally defines our source language SRC which is a variant of the polymorphic lambda calculus System-F (Girard, 1972; Reynolds, 1974). SRC differs from System-F in that it has inlining annotations on the core functions and it has a stratified structure with a polymorphic module language layered on top of a monomorphic core language. Also the module language uses A-normal form (Flanagan et al., 1993) which means that all intermediate values need to be named via let-binding, thus making all sharing between expressions explicit.

The syntax of SRC is given in Fig. 2. Here, an SRC program is just a module term (m). Each module term can be either a variable (x), a structure (ι_{v}(c)) consisting of a single core term (c), a compound module consisting of a collection of other modules (⟨x_{1},…, x_{n}⟩), an i-th component from another module (π_{i}x), a parameterized module (over other modules: λx: σ.m or over types: Λt.m), a module application (over other modules: @x_{1}x_{2} or over types: x[τ]), or a let declaration.

(ctypes) τ ::= int | t | τ_{1} → τ_{2}
(mtypes) σ ::= V(τ) | ⟨σ_{1},…, σ_{n}⟩ | σ_{1} → σ_{2} | ∀t.σ
(inline) a ::= | i
(cterms) c ::= n | z | π_{v}x | λ^{a}z:τ.c | c_{1}c_{2}
(mterms) m ::={x | ι_{v}(c) | ⟨x_{1},…, x_{n}⟩ | π_{i}x | λx:σ.m | @x_{1}x_{2} | Λt.m | x[τ] \atop | let x = m_{1} in m_{2}}

Fig. 2. Syntax for the source calculus SRC

Because the module language can already express polymorphic functions, we intentionally restrict the core language to be a simply typed lambda calculus. A core term can be either an integer constant (n), a variable (z), a value field of a module (π_{v}x), a function definition (λ^{a}z:τ.c) with inlining annotation (a), or a function application (c_{1}c_{2}).

A module type can either be a singleton-value type (V(τ) which refers to a module consisting of a core term of type τ), a compound module type (⟨σ_{1},…, σ_{n}⟩ with n submodules, each with type σ_{i} for i = 1, ..., n), or a parameterized module (over other modules: σ_{1} → σ_{2} or over types: ∀t.σ). A core type can be either the integer type (int), a type variable, or a function type (τ_{1} → τ_{2}). The singleton-value type V(τ) is used to distinguish between cases like V(int → int) and V(int) → V(int).

The SRC language was chosen to be expressive enough to exhibit the main difficulties that an optimizer based on staged computation might encounter. The language is split between the module and the core languages because the inliner needs to use two different compilation strategies. Of course, we could merge the two languages and annotate the terms to indicate whether or not to treat them like module code. Recent work (Shao, 1998; Shao, 1999; Harper et al., 1990) has shown that Standard ML can be compiled into an SRC-like typed intermediate language.

Figure 3 gives the static semantics for SRC. The environment Δ is the list of bound type variables; the type environment Γ maps both core and module variables to their respective types. Both the type- and the term-formation rules are rather straight-forward. The language is predicative in that the module language supports polymorphism but type variables can only be instantiated to core types. SRC uses a call-by-value semantics (omitted since it is straightforward); it is easy to show that the typing system for SRC is sound with respect to the corresponding dynamic semantics.

The most interesting feature of SRC is the inlining annotation a. The annotation i means that the underlying lambda expression should be inlined while the empty annotation means it should not. Notice that we do not track inlining annotations in the types; a core function λ^{a}z:τ.c is still assigned with the same type whether the annotation a is i or empty.

This design choice is deliberate. We believe inlining annotations should be made as nonintrusive as possible. Tracking them in the types would significantly complicate the module language; for example, we would have to add binding-time polymorphism in the type if we want to apply a functor to modules with different inlining annotations (but with the same signature otherwise).

When compiling SML to an SRC-like language, the SML module language maps to the SRC module language as expected, but polymorphic core SML functions also map

kind environment Δ ::= · | Δ, t
type environment Γ ::= · | Γ, z:τ | Γ, x:σ
[figure]

Δ ⊢ τ and Δ ⊢ σ and Δ ⊢ Γ

Δ ⊢ int  {t ∈ Δ \atop Δ ⊢ t}  \begin{matrix}Δ ⊢ τ_{1} & Δ ⊢ τ_{2} \\ Δ ⊢ τ_{1} → τ_{2} \end{matrix}  {Δ ⊢ τ \atop Δ ⊢ V(τ)}  {Δ ⊢ σ_{i} (1≤i≤n) \atop Δ ⊢ ⟨σ_{1},…, σ_{n}⟩}

\begin{matrix}Δ ⊢ σ_{1} & Δ ⊢ σ_{2} \\ Δ ⊢ σ_{1} → σ_{2} \end{matrix}  {Δ, t ⊢ σ \atop Δ ⊢ ∀t.σ}  Δ ⊢ ·  \begin{matrix}Δ ⊢ Γ & Δ ⊢ τ \\ Δ ⊢ Γ, z:τ \end{matrix}  \begin{matrix}Δ ⊢ Γ & Δ ⊢ σ \\ Δ ⊢ Γ, x:σ \end{matrix}

[figure: Δ; Γ ⊢ m : σ and Δ; Γ ⊢ c : τ]

{Δ ⊢ Γ \atop Δ; Γ ⊢ n : int}  {Δ ⊢ Γ \atop Δ; Γ ⊢ z : Γ(z)}  {Δ; Γ ⊢ x : V(τ) \atop Δ; Γ ⊢ π_{v}x : τ}

{Δ; Γ, z:τ_{1} ⊢ c : τ_{2} \atop Δ; Γ ⊢ λ^{a}z:τ_{1}.c : τ_{1} → τ_{2}}  \begin{matrix}Δ; Γ ⊢ c_{1} : τ_{2} → τ_{1} & Δ; Γ ⊢ c_{2} : τ_{2} \\ Δ; Γ ⊢ c_{1}c_{2} : τ_{1} \end{matrix}

{Δ ⊢ Γ \atop Δ; Γ ⊢ x : Γ(x)}  {Δ; Γ ⊢ c : τ \atop Δ; Γ ⊢ ι_{v}(c) : V(τ)}  {Δ; Γ ⊢ x_{i} : σ_{i} (1≤i≤n) \atop Δ; Γ ⊢ ⟨x_{1},…, x_{n}⟩ : ⟨σ_{1},…, σ_{n}⟩}

\begin{matrix}Δ; Γ ⊢ x : ⟨σ_{1},…, σ_{n}⟩ & 1≤i≤n \\ Δ; Γ ⊢ π_{i}x : σ_{i} \end{matrix}  {Δ; Γ, x:σ_{1} ⊢ m : σ_{2} \atop Δ; Γ ⊢ λx:σ_{1}.m : σ_{1} → σ_{2}}

\begin{matrix}Δ; Γ ⊢ x_{1} : σ_{2} → σ_{1} & Δ; Γ ⊢ x_{2} : σ_{2} \\ Δ; Γ ⊢ @x_{1} x_{2} : σ_{1} \end{matrix}  {Δ, t; Γ ⊢ m : σ \atop Δ; Γ ⊢ Λt.m : ∀t.σ}

{Δ; Γ ⊢ x : ∀t.σ \atop Δ; Γ ⊢ x[τ] : \{τ/t\}σ} Δ; Γ ⊢ m_{1} : σ_{1} Δ; Γ, x:σ_{1} ⊢ m_{2} : σ_{2}

Δ; Γ ⊢ let x = m_{1} in m_{2} : σ_{2}

Fig. 3. Static semantics for SRC

to module-level type abstractions (together with a core-level function) in SRC. This does not introduce any problem, however; since polymorphic recursion is not available, type instantiations can be done statically, or hoisted to the top-level (Saha & Shao, 1998).

4 The Target Calculus TLC

This section formally defines our target language TLC. As a typed intermediate language, TLC is is essentially a hybrid of System-F in A-normal form (Flanagan et al., 1993) and the two-level lambda calculus λ2sd by Moggi (1997).

The syntax of TLC is given in Fig. 4. A TLC term (e) can be either a value (v), a record selection, a function application, a type application, or a let expression. A TLC value (v) is either an integer constant, a variable, an n-tuple, a function, or a type function. A TLC type is either the integer type, a type variable, a record type, a function type, or a polymorphic

(kind) b, k ::= s | d
(type)  σ ::= int | t | ⟨σ_{1},…, σ_{n}⟩^{b} | σ_{1} →^{b} σ_{2} | ∀^{b}t:k.σ
(term) e ::= v | π_{i}^{b}v | @^{b}v_{1} v_{2} | v[σ]^{b} | let x = e_{1} in e_{2}
(value) v ::= n | x | ⟨v_{1},…, v_{n}⟩^{b} | λ^{b}x:σ.e | Λ^{b}t:k.e

Fig. 4. Syntax for the target calculus TLC

type. Many of these are annotated with a binding-time annotation (called “kind”) that can either be s for static code (evaluated at compile-time) or d for dynamic code (evaluated at run-time).

Compared to SRC, TLC replaces inlining hints on core functions with staging annotations on tuples, functions and type-abstractions and merges the module and the core languages since the distinction between the two is only needed to direct the translation from SRC. Notice also how ∀ types have two binding-time annotations, one for the type abstraction itself and another that constrains the possible types it can be instantiated to.

To simplify the presentation, we force the ground types (i.e., int) to be considered as dynamic. This is justified by the fact that we are only interested in function-level reductions. We may lift this restriction if we want to model constant propagation.

In the rest of this paper, we will also use the following syntactic sugar:

π_{i}^{b}e ≡ let x = e in π_{i}^{b}x
e[σ]^{b} ≡ let x = e in x[σ]^{b}
@^{b}e_{1} e_{2} ≡ let x_{1} = e_{1} in let x_{2} = e_{2} in @^{b}x_{1} x_{2}
⟨e_{1},…, e_{n}⟩^{b} ≡ let x_{1} = e_{1} in … let x_{n} = e_{n} in ⟨x_{1},…, x_{n}⟩^{b}
λ^{b}⟨x_{1},…, x_{n}⟩^{b′}:σ.e ≡ λ^{b}x:σ.let x_{1} = π_{1}^{b′}x in … let x_{n} = π_{n}^{b′}x in e

Essentially, we will put an e term where only v is allowed, leaving the let transformation implicit and we will use a pattern-matching variant of let; we will also assume that alpharenaming is used so variables are never shadowed.

Figure 5 gives the typing rules for TLC. In addition to the usual type safety, these rules also ensure binding-time correctness. Here the kind environment Δ maps type variables to their binding time; the type environment Γ maps variables to their types. To enforce the usual restriction that no dynamic entity can contain or manipulate a static value, types are classified as being either of dynamic kind or static kind, with a subkind relationship between the two: a type σ of dynamic kind can also be considered to have static kind but not vice versa.

Figures 6 to 9 give the dynamic semantics for TLC as a set of primitive reductions and single-step evaluation relations that determine where those reductions can be applied. Figure 6 defines the primitive static reduction e ⇝_{s} e′. Figure 7 defines the single-step partial evaluation e ↦_{s} e′ together with the corresponding v ↦_{s}^{v} v′ used for values. Note how partial evaluation in this language amounts to reducing all the static redexes of a term. Figures 8 and 9 show the corresponding reductions ⇝ and ↦ of a standard call-by-value evaluator. In contrast to the partial evaluation case, those reductions apply to both static and dynamic redexes but only to the outermost ones.

TLC is a variant of Moggi’s computational lambda calculus λ_{c} (1988) restricted to A-

kind environment Δ ::= · | Δ, t:k
type environment Γ ::= · | Γ, x:σ

[figure: b_{1} ≤ b_{2}]

d ≤ d  d ≤ s  s ≤ s

[figure: Δ ⊢ σ : k and Δ ⊢ Γ]

Δ ⊢ int : d  Δ ⊢ t : Δ(t)  \begin{matrix}Δ ⊢ σ : b_{1} & b_{1} ≤ b_{2} \\ Δ ⊢ σ : b_{2} \end{matrix}  {Δ ⊢ σ_{i} : b (1≤i≤n) \atop Δ ⊢ ⟨σ_{1},…, σ_{n}⟩^{b} : b}

\begin{matrix}Δ ⊢ σ_{1} : b & Δ ⊢ σ_{2} : b \\ Δ ⊢ σ_{1} →^{b} σ_{2} : b \end{matrix}  \begin{matrix}Δ, t:k ⊢ σ : b & k ≤ b \\ Δ ⊢ ∀^{b}t:k.σ : b \end{matrix}  Δ ⊢ ·  \begin{matrix}Δ ⊢ Γ & Δ ⊢ σ : s \\ Δ ⊢ Γ, x:σ \end{matrix}

[figure: Δ; Γ ⊢ e : σ and Δ; Γ ⊢ v : σ]

{Δ ⊢ Γ \atop Δ; Γ ⊢ n : int}  {Δ ⊢ Γ \atop Δ; Γ ⊢ x : Γ(x)}  \begin{matrix}Δ; Γ ⊢ v_{1} : σ_{2} →^{b} σ_{1} & Δ; Γ ⊢ v_{2} : σ_{2} \\ Δ; Γ ⊢ @^{b}v_{1} v_{2} : σ_{1} \end{matrix}

\begin{matrix}Δ; Γ ⊢ v_{i} : σ_{i} (1≤i≤n) & Δ ⊢ ⟨σ_{1},…, σ_{n}⟩^{b} : b \\ Δ; Γ ⊢ ⟨v_{1},…, v_{n}⟩^{b} : ⟨σ_{1},…, σ_{n}⟩^{b} \end{matrix}  {Δ; Γ ⊢ v : ⟨σ_{1},…, σ_{n}⟩^{b} 1≤i≤n \atop Δ; Γ ⊢ π_{i}^{b}v : σ_{i}}

\begin{matrix}Δ; Γ, x:σ_{1} ⊢ e : σ_{2} & Δ ⊢ σ_{1} →^{b} σ_{2} : b \\ Δ; Γ ⊢ λ^{b}x:σ_{1}.e : σ_{1} →^{b} σ_{2} \end{matrix} Δ; Γ ⊢ e_{1} : σ_{1} Δ; Γ, x:σ_{1} ⊢ e_{2} : σ_{2}

Δ; Γ ⊢ let x = e_{1} in e_{2} : σ_{2}

\begin{matrix}Δ, t:k; Γ ⊢ e : σ & Δ ⊢ ∀^{b}t:k.σ : b \\ Δ; Γ ⊢ Λ^{b}t:k.e : ∀^{b}t:k.σ \end{matrix}  \begin{matrix}Δ; Γ ⊢ v : ∀^{b}t:k.σ_{2} & Δ ⊢ σ_{1} : k \\ Δ; Γ ⊢ v[σ_{1}]^{b} : \{σ_{1}/t\}σ_{2} \end{matrix}

Fig. 5. Static semantics for TLC

normal form; in fact, the primitive reduction relations in Fig. 6 and 8 are same as that for λ_{c} (except that we added type applications and removed η-reductions). We can easily show that the type system for TLC is sound and the static reduction ↦_{s} is strongly normalizing and confluent. We can thus define a partial evaluation function P_{e}(e) that returns the static normal form of e. Similarly it is easy to show that ↦ is confluent, so we can also define a partial function R_{e}(e) which does the standard evaluation of e:

P_{e}(e) = e′such that e ↦_{s}^{∗} e′ and there is no e′′ for which e′ ↦_{s} e′′
R_{e}(e) = e′such that e ↦^{∗} e′ and there is no e′′ for which e′ ↦ e′′

where ↦^{∗} and ↦_{s}^{∗} are the reflexive transitive closures of ↦ and ↦_{s}. TLC satisfies the following important residualization property:

Theorem 4.1 (Residualization) If Δ; Γ ⊢ e : σ and Δ ⊢ σ : d and ∀x∈fv(e). Δ ⊢ Γ(x) : d, then P_{e}(e) is free of any static subterms.

Inlining as Staged Computation 9

(β_{λ}) @^{s}(λ^{s}x:σ.e) (v) ⇝_{s} {v/x}e
(β_{Λ}) (Λ^{s}t:k.e)[σ]^{s} ⇝_{s} {σ/t}e
(π) π_{i}^{s}⟨v_{1},…, v_{n}⟩^{s} ⇝_{s} v_{i}  if 1≤i≤n
(let) let x = v in e ⇝_{s} {v/x}e
(asc) let x_{2} = (let x_{1} = e_{1} in e_{2}) in e_{3}
⇝_{s} let x_{1} = e_{1} in let x_{2} = e_{2} in e_{3}

Fig. 6. Primitive static reduction for TLC

e ⇝_{s} e′ ⇒  e ↦_{s} e′
e ↦_{s} e′ ⇒  let x = e in e_{2} ↦_{s} let x = e′ in e_{2}
e ↦_{s} e′ ⇒  let x = e_{2} in e ↦_{s} let x = e_{2} in e′
e ↦_{s} e′ ⇒  λ^{b}x:σ.e ↦_{s}^{v} λ^{b}x:σ.e′
e ↦_{s} e′ ⇒  Λ^{b}t:k.e ↦_{s}^{v} λ^{b}t:k.e′
v ↦_{s}^{v} v′ ⇒ ⟨v_{1}, …, v, …, v_{n}⟩^{b} ↦_{s}^{v} ⟨v_{1}, …, v′, …, v_{n}⟩^{b}
v ↦_{s}^{v} v′ ⇒  @^{b}v v_{2} ↦_{s} @^{b}v′ v_{2}
v ↦_{s}^{v} v′ ⇒  @^{b}v_{2} v ↦_{s} @^{b}v_{2} v′
v ↦_{s}^{v} v′ ⇒  v[σ]^{b} ↦_{s} v′[σ]^{b}
v ↦_{s}^{v} v′ ⇒  π_{i}^{b}v ↦_{s} π_{i}^{b}v′

Fig. 7. Single-step partial evaluation for TLC

(⇝_{s}) e  ⇝ e′  if e ⇝_{s} e′
(β_{λ}) @^{d}(λ^{d}x:τ.e) (v) ⇝ {v/x}e
(β_{Λ}) (Λ^{d}t:k.e)[τ]^{d} ⇝ {τ/t}e
(π) π_{i}^{d}⟨v_{1},…, v_{n}⟩^{d} ⇝ v_{i}  if 1≤i≤n

Fig. 8. Primitive reduction relation for TLC

e ⇝ e′ ⇒  e ↦ e′
e ↦ e′ ⇒ let x = e in e_{2} ↦ let x = e′ in e_{2}

Fig. 9. Single-step call-by-value standard evaluation for TLC

In other words, given an expression e with dynamic type σ, partially evaluating e will inline all of its inlinable functions and result in an expression free of static subterms.

Next we show why inlining does not affect the semantics of the program. We first introduce a notion of semantic equivalence on well-typed TLC values:

Definition 4.2 (Equivalence) If ·; · ⊢ v : σ and ·; · ⊢ v′ : σ, we say that v ≃ v′ if one of the following holds:

(int) v ≡ v′. (×) v = ⟨v_{1},…, v_{n}⟩^{b} and v′ = ⟨v′_{1},…, v′_{n}⟩^{b} and ∀i∈[1..n].v_{i} ≃ v′_{i}. (→) σ = σ_{1} →^{b} σ_{2} and for any value w of type σ_{1} then R_{e}(@^{b}v w) ≃ R_{e}(@^{b}v′ w). (∀) σ = ∀^{b}t:k.σ_{1} and for any well-formed type σ_{2} :k then R_{e}(v[σ_{2}]^{b}) ≃ R_{e}(v′[σ_{2}]^{b}).

The correctness theorem can then be proved by induction over the reduction steps of P_{e}(e).

Theorem 4.3 (Correctness) If ·; · ⊢ e : σ and · ⊢ σ : d then R_{e}(P_{e}(e)) ≃ R_{e}(e).

5 Translation from SRC to TLC

The translation from SRC to TLC involves both staging and splitting, executed in an interleaved manner. Staging translates inlining annotations in the core language into bindingtime annotations. It also calls the splitting algorithm to divide each module term into a static part and a dynamic part. The static part is used to propagate inlining information and implement cross-module inlining. In the rest of this section, we first give a quick overview of our approach; we then show how to stage core terms and split module terms; finally, we give the main translation algorithm that links all the parts together.

5.1 A quick overview

The translation from SRC to TLC mostly consists of adding staging annotations. This is usually known as binding-time analysis and has been extensively studied in the partial evaluation community.

One desirable goal is to make sure that binding-time annotations do not hide opportunities for static evaluation. For example, let’s take the inlinable compose function o defined as follows:

o = λ^{i}f:τ_{1} → τ_{2}.λ^{i}g:τ_{2} → τ_{3}.λx:τ_{1}.g(fx)

When translating it, we probably do not want to assign it the following type:

o : (τ_{1} →^{d} τ_{2}) →^{s} (τ_{2} →^{d} τ_{3}) →^{s} (τ_{1} →^{d} τ_{3})

(i.e. a static function that composes two dynamic functions) since it would force us to make sure that all the functions passed to it are not inlinable, which mostly defeats the purpose of inlining it in the first place. Now clearly, if we mark it as:

o : (τ_{1} →^{s} τ_{2}) →^{s} (τ_{2} →^{s} τ_{3}) →^{s} (τ_{1} →^{d} τ_{3})

that will make it impossible to call it with a non-inlinable function. We could work around this problem by using polymorphism at the binding-time level (Henglein & Mossin, 1994; Glynn et al., 2001), but we decided to keep our calculus simple. With monomorphic staging annotations, we have two options: code duplication to provide a poor man’s polymorphic binding-time, or coercions in the form of binding-time improvements (Danvy et al., 1996; Danvy, 1996).

A compiler needs to be very careful about duplicating code so we decided to use coercions instead, especially since they provide us with a lot of flexibility. More specifically, we can completely avoid the need for a full-blown binding-time analysis and use a simple one-pass translation instead, by optimistically marking s any place that might need to accommodate a static value and inserting coercions when needed, just like the unboxing coercions (Leroy, 1992; Shao, 1997a). It also allows us to simplify our types: all types are either (completely) dynamic or completely static.

5.2 Staging the core

Staging could be done via any kind of binding-time analysis (Consel, 1993; Birkedal & Welinder, 1995), but this would be too costly for our application, so instead of performing global code analysis to add the annotations, we add them in a single traversal of the code using only local information. In order to maximize the amount of static computation, we make extensive use of binding-time improvements (Danvy et al., 1996).

Binding-time improvements are usually some form of η-redexes that coerce an object between its static and dynamic representations. They improve the binding-time annotations by allowing values to be used statically at one place and dynamically at another and even to make this choice “dynamically” during specialization.

Staging is then simple: based on the inlining annotations, SRC terms can either be translated to completely static or dynamic entities (except for int, which is always dynamic). Because inlining annotations are not typechecked in SRC, the resulting TLC terms may use dynamic subterms in a static context or vice versa. We insert coercions whenever there is such a mismatch.

We define two type-translation functions |·|^{s} and |·|^{d} that turn any SRC type into either its fully static or its fully dynamic TLC equivalent, and two coercion functions ↓^{τ}: |τ|^{s} →^{s} |τ|^{d} and ↑^{τ} : |τ|^{d} →^{s} |τ|^{s}. Those coercions (and corresponding type translations) could simply be:

↓^{int}x = x
↓^{τ_{1}→τ_{2}}x = λ^{d}x_{1} :|τ_{1}|^{d}. ↓^{τ_{2}}(@^{s}x (↑^{τ_{1}}x_{1}))
⋯
↑^{int}x = x
↑^{τ_{1}→τ_{2}}x = λ^{s}x_{1} :|τ_{1}|^{s}. ↑^{τ_{2}}(@^{d}x (↓^{τ_{1}}x_{1}))
⋯

|int|^{d} = int
|τ_{1} → τ_{2}|^{d} = |τ_{1}|^{d} →^{d} |τ_{2}|^{d}
⋯
|int|^{s} = int
|τ_{1} → τ_{2}|^{s} = |τ_{1}|^{s} →^{s} |τ_{2}|^{s}
⋯

But this would run the risk of introducing unexpected code duplication.

Spurious copies A naive coercion of a static function to its dynamic equivalent tends to introduce static redexes which cause the function to be inlined unnecessarily at the place where it escapes. Consider the following piece of SRC code:

let

id = λ^{i}x:int.x
big= λf:int → int. ...big body...

in ⟨id, @bigid⟩

A simple-minded staging scheme would turn it into:

let

id = λ^{s}x:int.x
big= λ^{d}f:int →^{d} int. ...big body...

in ⟨ ↓^{int→int}id, @^{d}big(↓^{int→int}id)⟩^{d}

where the coercions get expanded to:

let

id = λ^{s}x:int.x
big= λ^{d}f:int →^{d} int. ...big body...

in ⟨λ^{d}x:int.@^{s}idx, @^{d}big(λ^{d}x:int.@^{s}idx)⟩^{d}

|int|^{d} = int
|τ_{1} → τ_{2}|^{d} = |τ_{1}|^{d} →^{d} |τ_{2}|^{d}
↓^{τ}  : |τ|^{s} →^{s} |τ|^{d}
↓^{int}x  = x
↓^{τ_{1}→τ_{2}}x = π_{2}^{s}x

|int|^{s} = int
|τ_{1} → τ_{2}|^{s} = ⟨|τ_{1}|^{s} →^{s} |τ_{2}|^{s}, |τ_{1} → τ_{2}|^{d}⟩^{s}
↑^{τ}  : |τ|^{d} →^{s} |τ|^{s}
↑^{int}x  = x
↑^{τ_{1}→τ_{2}}x = ⟨λ^{s}x_{1} :|τ_{1}|^{s}. ↑^{τ_{2}}(@^{d}x (↓^{τ_{1}}x_{1})), x⟩^{s}
| Δ; Γ; Σ | = Δ; Γ′
where Γ′ = {x:|Γ(x)|^{s} | x ∈ dom(Γ)} ∪ {z:|τ|^{b} | τ = Γ(z) and b = Σ(z)}

and (binding-time environment) Σ ::= · | Σ, z:b

Fig. 10. Core type translations | · | and coercions ↓ and ↑.

Note that the two escaping uses of id have been turned now into η-redexes where id is called directly. Thus specialization will happily inline two copies of id even though no optimization will be enabled since both uses are really escaping. We do not want to introduce such wasteful code duplication.

In other words, we want to ensure that there can be only one non-inlined copy of any function, shared among all its escaping uses. To this end, we must arrange for ↓^{σ} not to introduce spurious redexes. We could simply introduce a special coerce primitive operation with an ad-hoc treatment in the partial-evaluator, but depending on the semantics chosen (e.g. binding-time erasure) it can end up leaking static code to run-time, introducing unwanted run-time penalties and it does not easily solve the problem of ensuring a unique dynamic copy of a function, even in the presence of cross-module inlining.

So we decided to choose a fancier representation for the static translation of a function, where each static function is now represented as a pair of the real static function and the already-coerced dynamic function. Now ↓^{σ_{1}→σ_{2}} becomes π_{2}^{s} and the only real coercion happens once, making it clear that only one instance of the dynamic version will exist. The definition of our type translations |·|^{s} and |·|^{d} and coercions ↓^{τ} and ↑^{τ} for the core calculus is shown in Fig. 10. The previous example is now staged as follows:

let

id = ⟨λ^{s}x:int.x, λ^{d}x:int.x⟩^{s}
big= λ^{d}f:int →^{d} int. ...big body...

in ⟨ ↓^{int→int}id, @^{d}big(↓^{int→int}id)⟩^{d}

Since the coercion ↓^{int→int} is now π_{2}^{s}, it just selects the dynamic version of id, with no code duplication.

Partial evaluators have long used such paired representation in their specializer for similar reasons (Asai, 1999), although our case is slightly different in that the pairs are explicit in the program being specialized rather than used internally by the specializer.

This pairing approach can also be seen as a poor man’s polymorphic binding-time where we only allow the two extreme cases (all dynamic or all static). Minamide and Garrigue (1998) used the same pairing approach when trying to avoiding the problem of

[figure: Δ; Γ; Σ ⊢ ⟦c : τ⟧ ⇒^{b} e]such that | Δ; Γ; Σ | ⊢ e : |τ|^{b}

Δ ⊢ Γ

Δ; Γ; Σ ⊢ ⟦n : int⟧ ⇒^{b} n

Δ ⊢ Γ Σ(z) = b Δ; Γ; Σ ⊢ ⟦z : Γ(τ)⟧ ⇒^{b} z
Δ; Γ ⊢ x : V(τ)

Δ; Γ; Σ ⊢ ⟦π_{v}x : τ⟧ ⇒^{s} x

Δ; Γ, z:τ_{1}; Σ, z:s ⊢ ⟦c : τ_{2}⟧ ⇒^{s} e

Δ; Γ; Σ ⊢ ⟦λ^{i}z:τ_{1}.c : τ_{1} → τ_{2}⟧ ⇒^{s}

let x_{s} = λ^{s}z:|τ_{1}|^{s}.e

x_{d} = λ^{d}z:|τ_{1}|^{d}. ↓^{τ_{2}}(@^{s}x_{s} (↑^{τ_{1}}z))

in ⟨x_{s}, x_{d}⟩^{s}

Δ; Γ, z:τ_{1}; Σ, z:d ⊢ ⟦c : τ_{2}⟧ ⇒^{d} e

Δ; Γ; Σ ⊢ ⟦λz:τ_{1}.c : τ_{1} → τ_{2}⟧ ⇒^{d} λ^{d}z:|τ_{1}|^{d}.e

Δ; Γ; Σ ⊢ ⟦c_{1} : τ_{1} → τ_{2}⟧ ⇒^{d} e_{1} Δ; Γ; Σ ⊢ ⟦c_{2} : τ_{1}⟧ ⇒^{d} e_{2}

Δ; Γ; Σ ⊢ ⟦c_{1}c_{2} : τ_{2}⟧ ⇒^{d} @^{d}e_{1} e_{2}

Δ; Γ; Σ ⊢ ⟦c_{1} : τ_{1} → τ_{2}⟧ ⇒^{s} e_{1} Δ; Γ; Σ ⊢ ⟦c_{2} : τ_{1}⟧ ⇒^{s} e_{2}

Δ; Γ; Σ ⊢ ⟦c_{1}c_{2} : τ_{2}⟧ ⇒^{s} @^{s}(π_{1}^{s}e_{1}) e_{2}

Δ; Γ; Σ ⊢ ⟦c : τ⟧ ⇒^{d} e

Δ; Γ; Σ ⊢ ⟦c : τ⟧ ⇒^{s}↑^{τ}e

Δ; Γ; Σ ⊢ ⟦c : τ⟧ ⇒^{s} e

Δ; Γ; Σ ⊢ ⟦c : τ⟧ ⇒^{d}↓^{τ}e

Fig. 11. Core code translation.

accumulative coercion wrappers that appears when unboxing coercions are used to reconcile polymorphism and specialized data representation.

The staging algorithm is shown in Fig. 11. The judgment Δ; Γ; Σ ⊢ ⟦c : τ⟧ ⇒^{b} e says that a core SRC term c of type τ (under contexts Δ and Γ) is translated into a TLC term e. The environment Σ maps core variables to the binding-time of the corresponding variable in e. The b on the arrow indicates whether a static or a dynamic term e is expected.

Most rules come in two forms, depending on whether the context expects a dynamic or static term. The dynamic case is trivial (it corresponds to the no-inlining case so we do not need to do anything) while the static case needs to build the static/dynamic pair (in the λ case) or to extract the static half of the pair before applying it (in the @ case).

5.3 Splitting

Module-level functions are typically used differently from core-level functions. They also do not have any inlining annotations thus deserve special treatment during the translation. As noted earlier, it is desirable to mark all the module code as static to “compile it away” or at least, to allow inlining information to flow freely through module boundaries. But that would imply that every single module-level function application gets its own copy of the body, which leads to unnecessary code duplication.

To overcome this difficulty, we use a form of partial inlining inspired from Blume and Appel’s λ-splitting (1997) that splits each function into a static and a dynamic part. It rewrites a TLC expression e into a list of let bindings and copies every inlinable (i.e. static) binding from e into e_{i}, and puts the rest into the expression e_{e} (the e subscript stands for “expansive”) in such a way that the two can be combined to get back an expression equivalent to e with e ≃ let ⟨fv⟩ = e_{e} in e_{i} where fvis the list of free variables of e_{i}. Since

[figure: Δ; Γ ⊢^{split} ⟦e⟧ ⟹^{σ} E_{e} ; e_{i}]where Δ; Γ ⊢ e : |σ|^{s}

Δ; Γ ⊢^{split} ⟦let x_{1} = e_{1} in let x_{2} = e_{2} in e_{3}⟧ ⟹^{σ} E_{e} ; e_{i}
Δ; Γ ⊢^{split} ⟦let x_{2} = let x_{1} = e_{1} in e_{2} in e_{3}⟧ ⟹^{σ} E_{e} ; e_{i}

(sp-asc)

x ∉ fv(e_{i}) ∨ Δ ⊢ σ_{1} : d

Δ; Γ ⊢ e_{1} : σ_{1} Δ; Γ, x:σ_{1} ⊢^{split} ⟦e_{2}⟧ ⟹^{σ} E_{e} ; e_{i}

Δ; Γ ⊢^{split} ⟦let x = e_{1} in e_{2}⟧ ⟹^{σ} (let x = e_{1} in E_{e}) ; e_{i}

(sp-share)

Δ; Γ ⊢ e_{1} : σ_{1} Δ; Γ, x:σ_{1} ⊢^{split} ⟦e_{2}⟧ ⟹^{σ} E_{e} ; e_{i}

Δ; Γ ⊢^{split} ⟦let x = e_{1} in e_{2}⟧ ⟹^{σ}

(let x = e_{1} in E_{e}) ; (let x = e_{1} in e_{i})

(sp-dup)

E_{e} = (let x_{fv} = • in ⟨ ↓^{σ}x, x_{fv}⟩^{d}) Δ; Γ ⊢^{split} ⟦x⟧ ⟹^{σ} E_{e} ; x (sp-var) Δ; Γ ⊢^{split} ⟦let x = e in x⟧ ⟹^{σ} E_{e} ; e_{i} Δ; Γ ⊢^{split} ⟦e⟧ ⟹^{σ} E_{e} ; e_{i} (sp-exp)

Fig. 12. The λ-split algorithm.

e_{i} is small, it can be copied wherever e was originally used, while the main part of the code is kept separate in e_{e}.

Basically, e_{i} is just like e but where all the non-inlinable code has been taken out (and the variables that refer to it are thus free), whereas e_{e} is a complete copy of e except that it returns all those values that have been taken out of e_{i}, so it can be used to close over the free variables of e_{i}. Take for example the following expression e where lookup is inlinable but balance is not (note that the algorithm assumes that the return value of e is completely static):

e = let balance= λ^{d}⟨t, x⟩^{d} :⟨tree^{d}, elem^{d}⟩^{d}…. lookup = λ^{s}⟨t, p⟩^{s} :⟨tree^{s}, elem^{s} →^{s} bool⟩^{s}. let x = @^{s}(@^{s}find p) t in @^{d}balance⟨ ↓^{tree}t, ↓^{elem}x⟩^{d} in lookup

This expression e will be split into a dynamic e_{e} and a static e_{i} where balance has been taken out since it is not inlinable. e_{i} will look like:

e_{i} = let lookup= λ^{s}⟨t, p⟩^{s} :⟨tree^{s}, elem^{s} →^{s} bool⟩^{s}. let x = @^{s}(@^{s}find p) t in @^{d}balance⟨ ↓^{tree}t, ↓^{elem}x⟩^{d} in lookup

The free variables of e_{i} are provided by e_{e} which carries all the old code and returns all the missing bindings for e_{i} to use. In this example, balance is the only free variable, so the result looks like:

e_{e} = let balance= λ^{d}⟨t, x⟩^{d} :⟨tree^{d}, elem^{d}⟩^{d}…. lookup = λ^{s}⟨t, p⟩^{s} :⟨tree^{s}, elem^{s} →^{s} bool⟩^{s}. let x = @^{s}(@^{s}find p) t in @^{d}balance⟨ ↓^{tree}t, ↓^{elem}x⟩^{d} in ⟨balance⟩^{d}

And we can combine e_{e} and e_{i} back together with e ≃ let ⟨fv⟩^{d} = e_{e} in e_{i} where fvis the list of free variables of e_{i}. We could of course remove lookup from e_{e}, but we might need it for something else (as will be shown in the next section) and it is easier to take care of it in a separate dead code elimination pass.

Because e_{e} has to return all the free variables of e_{i}, which are not known until e_{i} is complete, we cannot conveniently build e_{e} directly as we build e_{i}. Instead we build an expression with a hole E_{e} such that e_{e} ≡ E_{e}[⟨fv⟩^{d}]:

E_{e} = let balance = … lookup = … in ⟨•⟩^{d}

Here a TLC term with a hole E is formally defined as follows:

E ::= let x = • in e | let x = e in E

E[e] then fills the hole in E by textually substituting e for • without avoiding name capture:

(let x = • in e)[e_{1}] ≡ (let x = e_{1} in e)
(let x = e in E)[e_{1}] ≡ (let x = e in E[e_{1}])

The splitting rules are shown in Fig. 12. The judgment Δ; Γ ⊢^{split} ⟦e⟧ ⟹^{σ} E_{e} ; e_{i} states that E_{e} and e_{i} are a valid split of e in contexts Δ and Γ assuming that e : |σ|^{s}. The rules only guarantee correctness of the split, but do not specify a deterministic algorithm. In practice, whenever several rules can apply, the splitting algorithm chooses the first rule shown that applies: sp-asc is preferred over sp-share which is preferred over sp-dup, while sp-exp is only applied when there is no other choice (i.e. when e is neither a let binding nor a mere variable). This ensures that we return the smallest e_{i}.

The way the rules work is as follows: sp-asc together with sp-exp turn e into a list of let bindings that ends by returning a variable; sp-share copies dynamic bindings to E_{e} but omits them from e_{i} while sp-dup copies static bindings to both E_{e} and e_{i}; finally sp-var replaces the terminating variable with a hole in E_{e}.

5.3.1 Splitting functions

When splitting a function f, we could apply the above algorithm to the body, and then combine the two results into two functions f_{e} and f_{i}:

f = λ^{s}x:|σ|^{s}.e ⟹ f_{e} = λ^{d}x_{d} :|σ|^{d}.let x =↑^{σ}x_{d} in e_{e} f_{i} = λ^{s}x:|σ|^{s}.let ⟨fv⟩^{d} = @^{d}f_{e} (↓^{σ}x) in e_{i}

From then on f_{i} can be used in place of f (assuming that f_{e} is in scope), so that e_{i} will be inlined without having to ever duplicate e_{e}.

As we have seen before when staging inlinable core functions, the static representation of a function is a pair of the dynamic and the static version of that function f = ⟨f_{d}, f_{s}⟩^{s}. A similar representation needs to be used for module-level functions. One would be tempted to just use f_{i} for f_{s} and f_{e} for f_{d}, but a bit more work is required. First, we cannot use f_{e} directly because it only returns the free variables of f_{i} instead of the expected return value of f_{d}, but we can simply coerce f_{i} (which has f_{e} as a free variable) to a dynamic value:

f_{s} = f_{i}  f_{d} = λ^{d}x_{d} :|σ_{1}|^{d}. ↓^{σ_{2}}(@^{s}f_{i} (↑^{σ_{1}}x_{d}))

The problem with this approach is that there might be some code duplication between e_{i} and e_{e}, so f_{d} might contain unnecessary copies of code already existing in f_{e}. To work around this, we slightly change the way splitting is done, so that e_{e} returns not only the free variables of e_{i} but also the original output of e (see the sp-var rule):

E_{e} = let balance = … lookup = … in ⟨ ↓^{σ}lookup, •⟩^{d}

Of course, we need to adjust f_{i} so as to select the second component of f_{e}’s result to bind to its free variables. On the other hand, f_{e} is unchanged:

f = λ^{s}x:|σ|^{s}.e ⟹ f_{e} = λ^{d}x_{d} :|σ|^{d}.let x =↑^{σ}x_{d} in e_{e} f_{i} = λ^{s}x:|σ|^{s}.let ⟨fv⟩^{d} = π_{2}^{d}(@^{d}f_{e} (↓^{σ}x)) in e_{i}

Since f_{e} now returns the original result in its first field, we can use it directly almost as is to build f_{d} and we can of course still use f_{i} as f_{s}:

f_{s} = f_{i} f_{d} = π_{1} ∘ f_{e} = λ^{d}x_{d} :|σ_{1}|^{d}.π_{1}^{d}(@^{d}f_{e} x_{d})

5.3.2 Properties

To define and show correctness of the splitting algorithm, we need an extended notion of equivalence that applies to expressions rather than just values:

e ≃ e′ if and only if

for any E such that ·; · ⊢ E[e] : σ then ·; · ⊢ E[e′] : σ and R_{e}(E[e]) ≃ R_{e}(E[e′])

Splitting turns an expression e into a dynamic part E_{e} and a static part e_{i}. The following theorems state that combining E_{e} and e_{i} yields a well-typed term that is semantically equivalent to e.

Theorem 5.1 (Type preservation) if Δ; Γ ⊢ e : |σ|^{s} and Δ; Γ ⊢^{split} ⟦e⟧ ⟹^{σ} E_{e} ; e_{i} and fv= fv(e_{i}) − dom(Γ) then Δ; Γ ⊢ let ⟨fv⟩^{d} = π_{2}^{d}(E_{e}[⟨fv⟩^{d}]) in e_{i} : |σ|^{s}.

Theorem 5.2 (Correctness) if Δ; Γ ⊢ e : |σ|^{s} and Δ; Γ ⊢^{split} ⟦e⟧ ⟹^{σ} E_{e} ; e_{i} and fv= fv(e_{i}) − dom(Γ) then e ≃ let ⟨fv⟩^{d} = π_{2}^{d}(E_{e}[⟨fv⟩^{d}]) in e_{i}.

Both theorems can be proved via induction on the splitting derivation with the help of an invariant. For correctness, the invariant is:

For any term e′ and set of variables xs

such that (fv(e′) − fv(E_{e}[e′]) ⊆ xs ⊆ fv(e′) then E_{e}[e′] ≃ let ⟨xs⟩^{d} = π_{2}^{d}(E_{e}[⟨xs⟩^{d}]) in e′

The invariant for type preservation is similar.

The splitting algorithm also satisfies the following property:

Theorem 5.3 (Static closure) if Δ; Γ ⊢ e : |σ|^{s} and Δ; Γ ⊢^{split} ⟦e⟧ ⟹^{σ} E_{e} ; e_{i} then all free variables in e_{i} are either bound in Γ or they have dynamic type (in the context of E_{e}).

t_{co} = ⟨t_{d} →^{s} t_{s}, t_{s} →^{s} t_{d}⟩^{s}
|int|^{s} = int
|t|^{s} = t_{s}
|τ_{1} → τ_{2}|^{s} = ⟨|τ_{1}|^{s} →^{s} |τ_{2}|^{s}, |τ_{1} → τ_{2}|^{d}⟩^{s}
|V(τ)|^{s} = |τ|^{s}
|⟨σ_{1},…, σ_{n}⟩|^{s} = ⟨⟨|σ_{1}|^{s},…, |σ_{n}|^{s}⟩^{s}, |⟨σ_{1},…, σ_{n}⟩|^{d}⟩^{s}
|σ_{1} → σ_{2}|^{s} = ⟨|σ_{1}|^{s} →^{s} |σ_{2}|^{s}, |σ_{1} → σ_{2}|^{d}⟩^{s}
|∀t.σ|^{s} = ⟨∀^{s}t_{s} :s.∀^{s}t_{d} :d.t_{co} →^{s} |σ|^{s}, |∀t.σ|^{d}⟩^{s}

|int|^{d} = int
|t|^{d} = t_{d}
|τ_{1} → τ_{2}|^{d} = |τ_{1}|^{d} →^{d} |τ_{2}|^{d}
|V(τ)|^{d} = |τ|^{d}
|⟨σ_{1},…, σ_{n}⟩|^{d} = ⟨|σ_{1}|^{d},…, |σ_{n}|^{d}⟩^{d}
|σ_{1} → σ_{2}|^{d} = |σ_{1}|^{d} →^{d} |σ_{2}|^{d}
|∀t.σ|^{d} = ∀^{d}t:d.|σ|^{d}
| Δ; Γ; Σ | = Δ′; Γ′
where Δ′={t_{s} :s , t_{d} :d | t ∈ dom(Δ)}
and Γ′ ={x:|Γ(x)|^{s} | x ∈ dom(Γ)} ∪ {x_{t}:t_{co} | t ∈ dom(Δ)}

∪ {z:|τ|^{b} | τ = Γ(z) and b = Σ(z)}

Fig. 13. Type and environment translation.

We prove this property by inspection of the rules: if a variable is free in e_{i} but not in Γ it can only be because the sp-share rule was used, but that rule only applies to dynamic variables or variables which are not free in e_{i}.

Static closure implies that e_{i} contains all the inlinable sub-terms in e so splitting does not hide any inlining opportunities. In other words, when doing partial evaluation of a term containing e, we can substitute e_{i} for e without preventing any reduction (except reductions internal to the terms omitted in e_{i}, obviously). This in turn implies that compilation-unit boundaries have no influence on whether or not a core function gets inlined at a particular call site. We call it the completeness property.

5.4 The main algorithm

The main algorithm is the translation of the module language, which works similarly to (and uses) the core translation presented earlier, but is interleaved with the splitting algorithm. It also relies on the use of pairs that keep both a dynamic and a static version of every module-level value to avoid unnecessary code duplication.

Figures 13 and 14 extend the type translations | · |^{s} and | · |^{d} and the coercions ↓ and ↑ to the module calculus. The main change is the case for the type abstraction which we will explain later.

The full staging algorithm is shown in Fig. 15. The judgment Δ; Γ ⊢ ⟦m : σ⟧ ⇒^{m} e means that under the environments Δ and Γ, the SRC module m of type σ is translated into the TLC term e. Most rules are straightforward. The translation of expressions ι_{v}(c) is delegated to the core translation.

The case for module-level function and type abstraction are most interesting. The translation of a module-level function λx: σ.m begins by recursively translating the body m, and then splitting it. This is done with the judgment Δ; Γ ⊢ ⟦m : σ⟧ ⟹ e_{e} ; E_{i}. We then build a pair f = ⟨f_{d}, f_{s}⟩^{s} as described in the previous section. The translation of a type abstraction Λt.m follows the same pattern, except for a subtle complication introduced by typing problems discussed below.

18 Stefan Monnier and Zhong Shao

[figure] ↓^{σ}: |σ|^{s} →^{s} |σ|^{d} and ↑^{σ}: |σ|^{d} →^{s} |σ|^{s}
↓^{int}x  = x
↓^{t}x  = @^{s}(π_{2}^{s}x_{t}) x
↓^{τ_{1}→τ_{2}}x = π_{2}^{s}x
↓^{V(τ)}x  = ↓^{τ}x
↓^{⟨σ_{1},...,σ_{n}⟩}x = π_{2}^{s}x
↓^{σ_{1}→σ_{2}}x = π_{2}^{s}x
↓^{∀t.σ}x  = π_{2}^{s}x

↑^{int}x  = x
↑^{t}x  = @^{s}(π_{1}^{s}x_{t}) x
↑^{τ_{1}→τ_{2}}x = ⟨λ^{s}x_{1} :|τ_{1}|^{s}. ↑^{τ_{2}}(@^{d}x (↓^{τ_{1}}x_{1})), x⟩^{s}
↑^{V(τ)}x  = ↑^{τ}x
↑^{⟨σ_{1},...,σ_{n}⟩}x = ⟨⟨ ↑^{σ_{1}}(π_{1}^{d}x),…, ↑^{σ_{n}}(π_{n}^{d}x)⟩^{s}, x⟩^{s}
↑^{σ_{1}→σ_{2}}x = ⟨λ^{s}x_{1} :|σ_{1}|^{s}. ↑^{σ_{2}}(@^{d}x (↓^{σ_{1}}x_{1})), x⟩^{s}
↑^{∀t.σ}x  = ⟨Λ^{s}t_{s} :s.Λ^{s}t_{d} :d.λ^{s}x_{t}:t_{co}. ↑^{σ}(x[t_{d}]^{d}), x⟩^{s}

Fig. 14. Binding-time coercions.

[figure: Δ; Γ ⊢ ⟦m : σ⟧ ⇒^{m} e]such that | Δ; Γ; · | ⊢ e : |σ|^{s}

Δ ⊢ Γ Δ; Γ ⊢ ⟦x : Γ(x)⟧ ⇒^{m} x Δ; Γ; · ⊢ ⟦c : τ⟧ ⇒^{s} e

Δ; Γ ⊢ ⟦ι_{v}(c) : V(τ)⟧ ⇒^{m} e

Δ; Γ ⊢ x_{i} : σ_{i} (1≤i≤n) σ = ⟨σ_{1},…, σ_{n}⟩

Δ; Γ ⊢ ⟦⟨x_{1},…, x_{n}⟩ : σ⟧ ⇒^{m} let \begin{matrix}x_{s} = & ⟨x_{1},…, x_{n}⟩^{s} \\ x_{d} = & ⟨ ↓^{σ_{1}}x_{1},…, ↓^{σ_{n}}x_{n}⟩^{d} \end{matrix} in ⟨x_{s}, x_{d}⟩^{s}

Δ; Γ ⊢ x : ⟨σ_{1},…, σ_{n}⟩ 1≤i≤n Δ; Γ ⊢ ⟦π_{i}x : σ_{i}⟧ ⇒^{m} π_{i}^{s}(π_{1}^{s}x) Δ; Γ ⊢ x_{1} : σ_{2} → σ_{1} Δ; Γ ⊢ x_{2} : σ_{2}

Δ; Γ ⊢ ⟦@x_{1} x_{2} : σ_{2}⟧ ⇒^{m} @^{s}(π_{1}^{s}x_{1}) x_{2}

Δ; Γ, x:σ_{1} ⊢ ⟦m : σ_{2}⟧ ⟹ e_{e} ; E_{i}

Δ; Γ ⊢ ⟦λx:σ_{1}.m : σ_{1} → σ_{2}⟧ ⇒^{m}

let

x_{e} = λ^{d}x_{d} :|σ_{1}|^{d}. let x =↑^{σ_{1}}x_{d} in e_{e}
x_{i} = λ^{s}x:|σ_{1}|^{s}. E_{i}[π_{2}^{d}(@^{d}x_{e} (↓^{σ_{1}}x))]

in ⟨x_{i}, λ^{d}x_{d} :|σ_{1}|^{d}.π_{1}^{d}(@^{d}x_{e} x_{d})⟩^{s} Δ, t; Γ ⊢ ⟦m : σ⟧ ⟹ e_{e} ; E_{i}

Δ; Γ ⊢ ⟦Λt.m : ∀t.σ⟧ ⇒^{m}

let x_{e} = Λ^{d}t:d. {t/t_{d}, t/t_{s}, ⟨id_{t}^{s}, id_{t}^{s}⟩^{s}/x_{t}}e_{e}

x_{i} = Λ^{s}t_{s} :s.Λ^{s}t_{d} :d.λ^{s}x_{t}:t_{co}. E_{i}[π_{2}^{d}(x_{e}[t_{d}]^{d})]

in ⟨x_{i}, Λ^{d}t:d.π_{1}^{d}(x_{e}[t]^{d})⟩^{s}

Δ; Γ ⊢ x : ∀t.σ

Δ; Γ ⊢ ⟦x[τ] : {τ/t}σ⟧ ⇒^{m} @^{s}(π_{1}^{s}x)[|τ|^{s}]^{s}[|τ|^{d}]^{s} ⟨ ↓^{τ}, ↑^{τ}⟩

Δ; Γ ⊢ ⟦m_{1} : σ_{1}⟧ ⇒^{m} e_{1} Δ; Γ, x:σ_{1} ⊢ ⟦m_{2} : σ_{2}⟧ ⇒^{m} e_{2}

Δ; Γ ⊢ ⟦let x = m_{1} in m_{2} : σ_{2}⟧ ⇒^{m} let x = e_{1} in e_{2}

[figure: Δ; Γ ⊢ ⟦m : σ⟧ ⟹ e_{e} ; E_{i}]

such that | Δ; Γ; · | ⊢ E_{i}[π_{2}^{d}e_{e}] : |σ|^{s}

Δ; Γ ⊢ ⟦m : σ⟧ ⇒^{m} e | Δ; Γ; · | ⊢^{split} ⟦e⟧ ⟹^{σ} E_{e} ; e_{i}

fv= fv(e_{i}) − dom(Γ) E_{i} = (let ⟨fv⟩^{d} = • in e_{i})

Δ; Γ ⊢ ⟦m : σ⟧ ⟹ E_{e}[⟨fv⟩^{d}] ; E_{i}

Fig. 15. Module code translation. id_{t}^{b} is a shorthand for λ^{b}x:t.x.

Since all module-level code is considered static, it is tempting to think that we do not need pairing at all and can simply represent module entities with the static counterpart. But the e_{e} component obtained from λ-split is dynamic and we thus need coercions to interact with it: both the sp-var rule of λ-split (see Fig. 12) and the construction of f_{i} out of e_{i} (see Sec. 5.3.1) introduce coercions. And since modules tend to be larger than core functions, it is even more important to avoid spurious copies.

Type abstractions As mentioned above, type abstractions introduce some complications. The problem appears when we try to define coercion functions. The naive approach would look like:

↓^{∀t.σ}x=Λ^{d}t:d. ↓^{σ}(x[t]^{s})
↑^{∀t.σ}x=Λ^{s}t:s. ↑^{σ}(x[t]^{d})

but this is not type correct, since t in the second rule can be static and hence cannot be passed to the dynamic x. Obviously, we need here the same kind of (contra-variant) argument coercion as we use on functions, but our language does not provide us with any way to create a ↓ operator to apply to types.

Furthermore, the two inner coercions ↓^{σ} and ↑^{σ} are not very well defined since σ can have a free variable t. This begs the question: what should ↑^{t} do ?

There are several ways to solve these two problems:

• Give up on static type arguments and force any type-variable to be dynamic. This restriction is fairly minor in practice. It only manifests itself when a function is manipulated as data by polymorphic code, such as when a function is passed to the identity function id: the function returned by @id f cannot be inlined even if f is.

• Extend our language with a more powerful type-system that allows intensional typeanalysis (Harper & Morrisett, 1995). This seems possible, but would complicate the type-system considerably and potentially the staging and the coercions as well.

• Use a dictionary-passing approach (Wadler & Blott, 1989): instead of trying to coerce our static t into a dynamic t, we can simply always provide both versions t_{s} and t_{d} along with both ↓^{t} and ↑^{t} so that the coercions are constructed at the type application site, where t is statically known.

The first solution is simple and effective, but we opted for the third alternative because it has fewer limitations. The static version of Λt.m (before pairing with its dynamic counterpart) looks like:

Λ^{s}t_{s} :s.Λ^{s}t_{d} :d.λ^{s}x_{t}:t_{co}.e

This means that for every t in the SRC Δ environment, we now have two corresponding type variables t_{s} and t_{d} plus one value variable x_{t} which holds the two coercion functions ↓^{t} and ↑^{t} As can be seen in Fig. 13 (which refines Fig. 10) where t_{co} is also defined. This notation is used for convenience in all the figures.

Such an encoding might look convoluted and cumbersome, but type abstractions only represent a small fraction of the total code size and the run-time code size is unaffected, so it is a small price to pay in exchange for the ability to inline code that had to pass through a function like id.

Theorem 5.4 (Type preservation) If Δ; Γ ⊢ m : σ and Δ; Γ ⊢ ⟦m : σ⟧ ⟹ e_{e} ; E_{i} then | Δ; Γ; · | ⊢ E_{i}[π_{2}^{d}e_{e}] : |σ|^{s}.

Together with the residualization theorem 4.1, this means that after specialization all the inlinable code has been inlined away.

6 Handling the Top Level

The above presentation only explains how to translate each SRC compilation unit into its TLC counterpart. This section describes in detail how to handle top-level issues to link multiple compilation units together.

Handling of compilation units is not difficult, but is worth looking at not only to get a better idea of how the code flows through the compiler, but also because the treatment of side-effects depends on the specifics of the evaluation of each compilation unit (see Sec. 7.1).

As can be seen in Fig. 1, we apply λ-split twice. This derives from the need to handle the top-level of the compilation unit in a special way where splitting internal module functions should be done early, while splitting the top-level should be done late. Here is a slightly more detailed diagram:

\begin{aligned}sum & 1..n \\ & ↘ \end{aligned}  \begin{matrix}sum \\ ↗ \end{matrix}
PRG_{S} ⟶^{stage+split} PRG_{1} ⟶^{⊕} PRG_{2} ⟶^{P_{e}} PRG_{3} ⟶^{split} PRG_{4}

Instead of spreading the split into two parts, we could of course do it once and for all at the very beginning, but then we would lose the opportunity to move into the export summary copies of wrapper functions (used e.g. for uncurrying, unboxing or flattening) introduced by the intermediate optimization phases.

Doing the split in two steps also forces us to apply the split to TLC terms (it would be silly to have two splitting algorithms). This also motivates our choice to interleave the staging and splitting since the splitting algorithm needs to know which functions are modules and which are not because splitting core functions is often detrimental to performance.

The top-level also gets a special treatment because of separate compilation. A compilation-unit can contain free variables, which are essentially the imports of the unit. Instead of considering such an open term, we close it by turning it into a function from its imports to its exports. More specifically, a compilation-unit in SRC will look like:

PRG_{S} = λ⟨imp_{1},…, imp_{n}⟩:⟨σ_{1},…, σ_{n}⟩.m

The translation to TLC assumes that the function is static as well as the imports (these will be import summaries, which are by essence inlinable, after all) and simply translates the body using:

·; {imp_{i}:|σ_{i}|^{s} | 1 ≤ i ≤ n} ⊢ ⟦m : σ⟧ ⇒^{m} e

This recursively splits each and every internal module-level function (the recursion is done by the staging part of the translation which calls λ-split when needed, see the rules for λ and Λ in Fig. 15), but leaves the top-level function alone. These internal splits are necessary to allow inlining across module boundaries but still within a compilation unit. The program now looks like:

PRG_{1} = λ^{s}⟨imp_{1},…, imp_{n}⟩^{s} :⟨|σ_{1}|^{s},…, |σ_{n}|^{s}⟩^{s}.e

The next step is to bring in copies of the import summaries. Every imp_{i} has a corresponding summary sum_{i} generated when that import was compiled. Summaries are the e_{i} half of a split and thus contain free dynamic variables. So we replace each imp_{i} argument with a copy of sum_{i}, and add the corresponding new free variables imp_{ij} as new arguments:

PRG_{2} = λ^{s}⟨imp_{11},…, imp_{nk}⟩^{d} :⟨σ_{11},…, σ_{nk}⟩^{d}. let imp_{1} = sum_{1} ; ⋯; imp_{n} = sum_{n} in e

After that comes the actual partial-evaluation and optimization which ends with a term PRG_{3} very much like PRG_{2} but with an optimized body e_{o} exempt of any static redex:

PRG_{3} = P_{e}(PRG_{2}) = λ^{s}⟨imp_{11},…, imp_{nk}⟩^{d} :⟨σ_{11},…, σ_{nk}⟩^{d}. e_{o}

We then pass it to the second λ-split, along with the SRC σ output type that we remembered from the staging phase:

Δ; Γ ⊢^{split} ⟦e_{o}⟧ ⟹^{σ} E_{e} ; e_{i}

This split gives us a residual program and an export summary sum that will be used as a sum_{i} next time around:

sum = λ^{s}⟨fv⟩^{d} :⟨σ_{fv}⟩^{d}.e_{i}  where fv= fv(e_{i})
PRG_{4} = λ^{d}⟨imp_{11},…, imp_{nk}⟩^{d} :⟨σ_{11},…, σ_{nk}⟩^{d}.E_{e}[⟨fv⟩^{d}]

The export summary sum will be stashed somewhere to be used when a compilation unit wants to import it. As for PRG_{4}, it continues through the remaining compilation stages down to machine code.

When the program is run, all the compilation units need to be instantiated in the proper order. Once all the imports imp_{ij} of our unit have been built, PRG_{4} is run as follows:

⟨exp, ⟨fv⟩^{d}⟩^{d} = R_{e}(@^{d}PRG_{4} ⟨imp_{11},…, imp_{nk}⟩^{d})

Here exp is the original exports of this compilation unit. They will be ignored for all but the main compilation unit (unless one of the dependent units was compiled without crossmodule inlining, in which case exp will be used by that unit). ⟨fv⟩^{d} is the set of exports generated by the λ-split and needed for all the compilation units that depend on the current unit and hence imported sum. When running those dependent units, the current ⟨fv⟩^{d} will then appear as the arguments imp_{i1} … imp_{ik}.

Note that PRG_{4} will only be run once and for all whereas sum will be evaluated as many times as it is imported by dependent compilation units. Also, PRG_{4} is not completely dynamic since the coercion ↓^{σ} x of the sp-var rule (in Fig. 12) introduces static redexes; we have to perform another round of partial evaluation on PRG_{4} before feeding it to the backend code generator.

(type) σ ::= ... | ∃^{b}t:k.σ
(term) e ::= ... | open^{b} v as (t, x) in e
(value) v ::= ... | pack^{b}(t = σ:k, e)
|σ_{1} → σ_{2}|^{s} = ∃^{s}t:d.⟨|σ_{1}|^{s} →^{s} t →^{s} |σ_{2}|^{s}, |σ_{1}|^{d} →^{d} ⟨|σ_{2}|^{d}, t⟩^{d}⟩^{s}
↓^{σ_{1}→σ_{2}}x = λ^{d}x_{1} :|σ_{1}|^{d}.open^{s} x as (t, x) in π_{1}^{d}(@^{d}(π_{2}^{s}x) x_{1})
↑^{σ_{1}→σ_{2}}x = pack^{s}(t = ⟨⟩^{d} :d, let x_{s} = λ^{s}x_{1} :|σ_{1}|^{s}.λ^{s}x_{2} :t. ↑^{σ_{2}}(@^{d}x x_{1}) x_{d} = λ^{d}x_{3} :|σ_{1}|^{d}.⟨@^{d}x x_{3}, ⟨⟩^{d}⟩^{d} in ⟨x_{s}, x_{d}⟩^{s} )

Δ; Γ ⊢ x_{1} : σ_{2} → σ_{1} Δ; Γ ⊢ x_{2} : σ_{2}

Δ; Γ ⊢ ⟦@x_{1} x_{2} : σ_{2}⟧ ⇒^{m}

open^{s} x_{1} as (t, x)

in

let x_{e} = @^{d}(π_{2}^{s}x) (↓^{σ_{1}}x_{2})

in @^{s}(@^{s}(π_{1}^{s}x) x_{2}) (π_{2}^{d}x_{e})

Δ; Γ, x:σ_{1} ⊢ ⟦m : σ_{2}⟧ ⟹ e_{e} ; E_{i}

Δ; Γ ⊢ ⟦λx:σ_{1}.m : σ_{1} → σ_{2}⟧ ⇒^{m}

pack^{s}(t = σ_{fv}:d, let x_{e} = λ^{d}x_{d} :|σ_{1}|^{d}. let x =↑^{σ_{1}}x_{d} in e_{e} x_{i} = λ^{s}x:|σ_{1}|^{s}.λ^{s}y:t. E_{i}[y] in ⟨x_{i}, x_{e}⟩^{s} )

Fig. 16. New rules using existential types.

The type, kind, and evaluation semantics should be extended correspondingly. Furthermore, the last rule needs the type σ_{fv} of the free variables of e_{i} which can easily be propagated during splitting.

7 Extensions

In order to model real world inliners faithfully, our translation still needs various additions which we have not explored in depth yet. We present some here along with other potential extensions.

7.1 Side effects

Introducing side-effects is mostly straightforward, with just one exception: The sp-dup rule in Fig. 12 cannot be applied to non-pure terms since it would duplicate their effects. But reverting to the sp-share rule (also in Fig. 12) for those side-effecting terms is not an option either because we would then lose the completeness property that we are looking for. An alternative is to use the following sp-move rule that moves the binding to e_{i} instead of merely copying it:

\frac{Δ; Γ ⊢ e_{1} : σ_{1} Δ; Γ, x:σ_{1} ⊢^{split} ⟦e_{2}⟧ ⟹^{σ} E_{e} ; e_{i}}{Δ; Γ ⊢^{split} ⟦let x = e_{1} in e_{2}⟧ ⟹^{σ} let x_{1} = λ^{d}x:σ_{1}.E_{e}[⟨fv⟩^{d}] in • ; let x = e_{1} in let ⟨fv⟩^{d} = @^{d}x_{1} (↓^{σ_{1}}x) in e_{i}}

As presented, this rule is not quite correct because the coercion ↓^{σ_{1}} assumes σ_{1} is an SRC type but σ_{1} is really a TLC type. This can be easily resolved by passing all the SRC types during the translation. Alternatively, we could represent |int|^{s} as ⟨int, int⟩^{s}, then the coercion ↓ simply becomes π_{2}^{s} for all types.

A potential issue is that, as can be seen in Sec. 6, the top-level E_{e} is evaluated once and for all in a global environment, while e_{i} will be evaluated each time it is imported into a client unit. This means that the top-level e_{i} must be free of side-effects. Luckily, we can show that this problem does not appear: the compilation unit does not contain any static free variables or static redexes; so the only static code to split into e_{i} is composed exclusively of values, which have no side effects.

This sp-move rule could also be used for other purposes, such as specializing a binding in the context of the client, as was suggested briefly in Blume and Appel’s paper (they did not have such a rule).

Another approach altogether to the handling of side-effects is to notice that since e_{i} has to be pure, we can turn @^{s}x_{1} x_{2} into @^{d}(@^{s}x_{i} x_{2}) (π_{2}^{d}(@^{d}x_{e} (↓x_{2}))) and then split out the remaining static application which is known to be pure. We do not even need to change the splitting algorithm itself, but just two rules in Fig. 15.

The key is that we can do this rewrite even if we do not know x_{1}. We simply need to represent x_{1} as a pair ⟨x_{i}, x_{e}⟩^{s}. But of course, this is already the case for other reasons, so the changes are very minor.

Of course, there is a catch: the type of the free variables of e_{i} suddenly leak into the type of |σ_{1} → σ_{2}|^{s} which becomes an existential type.

Figure 16 shows what the rules would look like. Some of the work is now shifted from the function definition to the function application, but overall, the complexity of terms is not seriously impacted. Apart from the introduction of existential types, this translation variant also requires an impredicative calculus. TLC was already impredicative, so no changes were required there.

7.2 Recursion

The TLC calculus lacks fixpoint. Adding recursive functions does not pose any conceptual problem, except for the risk of compilation not terminating. There are several reasonable solutions to this problem either from the inlining community or from the partial evaluation community. The most trivial solution is to allow fixpoint on dynamic terms only, which amounts to disallowing inlining of recursive functions, but since it can be important to allow inlining even in the presence of recursion, one can also do a little bit of analysis to find a conservative estimate of whether or not a risk of infinite recursion is present (Peyton Jones & Marlow, 1999).

Recursion on types is more challenging since recursive data-structures cannot (or should not) be coerced. In our case, however, this restriction only applies to coercions from d to s, so we can always work around the problematic cases by forcing recursive data-structures to be dynamic.

7.3 Optimizations as staged computation

With a full λ-calculus available at compile-time, we can now provide facilities similar to macros, or rather to Lisp’s compiler macros. For example, a compiler macro for multiplication could test its arguments at compile time and replace the multiplication with some other operations depending on whether or not one of the value is statically known and what value it takes. Using such a facility we could move some of the optimizations built into the compiler into a simple library, making them easily extensible.

A more realistic use in the short term is to encode the predicate for conditional inlining directly into the language. The current inliner allows inlining hints more subtle than the ones present in SRC. They can express a set of conditions that should hold at the call site in order for the call to be inlined. For example, map will only be inlined if it is applied to a known function.

We could now strip out those ad-hoc annotations and simply write map as a compiletime function that intensionally analyzes its arguments and either returns a copy of its body if the function argument is a λ-expression or returns just a call to the common version if the argument is a variable (i.e. an escaping function).

7.4 Staging refinement

Partial evaluation as well as other optimizations will sufficiently change the shape of the code to justify or even require refining the binding-time annotations. This can happen because a function has been optimized down to just a handful of statements, or because it has been split into a wrapper and a main body or any other reason.

Turning a dynamic function into a static one is not very difficult to implement, but more work needs to be done to express it cleanly within our framework.

It seems to require among other things the ability to optimize away pairs of coercions that cancel each other out such as not only ↓^{σ} ↑^{σ}x (which is trivially done by the partial evaluator) but also ↑^{σ}↓^{σ}x which appears to involve evaluation of dynamic code at compiletime.

7.5 Link-time optimizations

Another extension is to add multiple levels so that we can express compile-time execution, link-time execution, run-time code generation and more.

This will require extending a calculus such as λ^{◯} (Davies, 1996) with at least some form of polymorphism, but should not pose any real problem, except that the kind of tricks we used to work around the lack of simple coercion for type abstraction might need to be generalized to n-levels. If n is unbounded, it might not be possible and even if it is bounded, it might be impractical.

Also, the use of pairs of fully-static and fully-dynamic representations of the same original expressions would not generalize to n-levels easily, but could still be kept for the benefit of the compile stage.

7.6 Implementation

As mentioned in the introduction, this paper was motivated by the need to better understand the behavior of our inliner in SML/NJ. Since our implementation handles the complete SML language in a production compiler, it has to deal with all the issues mentioned above. Here are the most important differences between the model presented in this paper and the actual code:

• For historical reasons, our intermediate language is predicative, which prevents us from using existential packages to solve the problem of side effects. Instead we simply revert to using the sp-share rule and lose the completeness property.

• Our language allows recursion both for dynamic and for static functions. Termination of P_{e}(e) is ensured by a simple conservative loop detection.

• The dynamic and static pairs we use to avoid spurious code duplication are represented in an ad-hoc way that eliminates the redundancy. This ad-hoc representation looked like a good idea at the time, but made it unnecessarily painful to add the refinement described in Sec. 5.3.1.

8 Related Work

Functional-language compilers such as O’Caml (Leroy, 1995), SML/NJ (Appel, 1991), GHC (Peyton Jones & Marlow, 1999), and TIL (Tarditi, 1996), all spend great efforts to provide better support to inlining. Although none of them models inlining as staged computation, the heuristics for detecting what functions should be inlined are still useful in our framework. In fact, our FLINT optimizer (Monnier et al., 1999) inherits most of the heuristics used in the original SML/NJ compiler.

Control-flow analysis (CFA) (Shivers, 1991; Ashley, 1997) is an alternative to λ-splitting to propagate inlining information across functions and functors. It tries to find, for example via abstract interpretation, the set of functions possibly invoked at each call site in the program. It offers the advantage of requiring less code duplication and may expose more opportunities for inlining inside a compilation unit. For example, in a code such as:

let f x y = ..y x.. and g x = ... in ⟨f 1 g, f 2 g⟩

CFA can inline the function g into f without inlining f whereas our inliner will only reach the same result if it can first inline the two calls to f. On the other hand, in a code such as f g x where f is a functor that ends up returning its argument unchanged, our inliner will be able to replace the code with g x, no matter how f is defined, whereas in the case of CFA, if the definition of f is sufficiently complex, a costly polyvariant analysis is needed to discover that the code can be replaced with g x.

Partial evaluation is a very active research area. Jones et al (1993) gives a good summary about some of the earlier results. Danvy’s paper (1996) on type-directed partial evaluation inspired us to look into sophisticated forms of binding-time coercions.

Tempo (Consel & Noël, 1996; Marlet et al., 1999) is a C compiler that makes extensive use of partial-evaluation technologies. Its main emphasis is however on efficient runtime code generation. Sperber and Thiemann (1996; 1997) worked on combining compilation with partial evaluation, however they were not concerned with modeling the inlining optimization as done in a production compiler.

Nielson and Nielson (1992) gave an introduction to a two-level λ-calculus. Davies and Pfenning (1996) proposed to use modal logic to express staged computation. Moggi (1997) pointed out that both of these calculi are subtly different from the two-level calculus used in partial evaluation (Jones et al., 1993). Taha et al (Taha, 1999; Taha & Sheard, 1997; Moggi et al., 1999) showed how to combine these different calculi into a single framework.

Our TLC calculus (see Sec. 4) is an extension of Moggi’s two-level λ2sd calculus (Moggi, 1997) with the System-F-style polymorphism (Girard, 1972; Reynolds, 1974). Davies (1996) used the temporal logic to model an n-level calculus which naturally extends λ2sd.

Foster et al. (1999) proposed to use qualified types to model source-level program directives. Their framework can be applied to binding time annotations but these annotations would have to become parts of the type specifications. Our inlining annotations on the other hand do not change the source-level type specifications.

Blume and Appel (1997) suggested λ-splitting to support cross module inlining. Their algorithm is based on a weakly-typed λ-calculus and provides a convenient cross-module inlining algorithm. Our work extends theirs by porting their algorithm to a much more powerful language and formalizing it. By using the two-level λ-calculus we can express some of the inliner’s behavior in the types.

O’Caml (Leroy, 1995) collects the small inlinable functions of a module into its approximation and then reads in this extra info (if available) when compiling a client module. It works very well across modules and can even inline functions from within a functor to the client of the functor, but is unable to inline the argument of a functor. For example, passing a module through a trivial “adaptor” functor (which massages a module to adapt it to some other signature, e.g.) will lose the approximation, preventing inlining.

By encoding the equivalent of approximations directly into types, Shao (1998) presents an alternative approach which allows the full inlining information to be completely propagated across functor applications by propagating it along with the types. But this comes at the cost of a further complication of the module elaboration. Another problem is that some of the functions we might want to inline (such as uncurry wrappers) do not yet exist at the time of module elaboration.

Recently, Ganz et al (2001) presented an expressive, typed language that supports generative macros. The language, MacroML, is defined by an interpretation into MetaML (Taha & Sheard, 1997). This is similar to our approach because macros can also be viewed as inlinable functions; the translation from MacroML to MetaML resembles our translation from the source calculus SRC to the target calculus TLC. There are, however, several major differences. First, in MacroML, macros and functions are different language constructs; macros never escape so they can be unconditionally marked as “static” and no coercions or polymorphic binding-time annotations are ever needed; in our SRC calculus, however, functions that are marked as inlinable are still treated as regular functions so they can escape in any way they like. Second, it is unclear how MacroML can be extended to support ML-style modules; MacroML assigns different types to macros and functions so exporting macros would require adding new forms of specifications into ML signatures; in our SRC language, however, a function is always assigned the same type whether it is marked as inlinable or not, so we can just reuse the existing ML module language. Third, unlike MacroML, we presented various techniques to control code duplication—this is cruicial for cross-module inlining since naively expanding every functor in ML would certainly cause code explosion.

9 Conclusions and Future Work

Expressing inlining in terms of a staged computation allows us to better formalize the behavior of the inliner and provide strong guarantees of what gets inlined where.

We have shown how this can be done in the context of a realistic two-level polymorphic language and how it interacts with cross-module inlining. The formalism led us to a clean design in which we can easily show that code is only and always duplicated when useful.

The present design eliminates run-time penalties usually imposed by the powerful abstraction mechanism offered by parameterized modules, enabling a more natural programming style. More importantly, our algorithm provides such flexibility while still maintaining separate compilation.

An interesting question is whether or not using monomorphic staging annotations was a good choice. It seems that polymorphism could allow us to do away with the coercions, although it would at least require the use of continuation passing style in order to maintain precision of annotations.

Acknowledgements

We would like to thank the anonymous referees as well as Dominik Madon, Chris League, and Walid Taha for their comments and suggestions on an early version of this paper. This research was sponsored in part by the Defense Advanced Research Projects Agency ISO under the title “Scaling Proof-Carrying Code to Production Compilers and Security Policies,” ARPA Order No. H559, issued under Contract No. F30602-99-1-0519, and in part by NSF Grants CCR-9633390 and CCR-9901011. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the U.S. Government.

References

Appel, Andrew W. (1991). Compiling with continuations. Cambridge University Press. ISBN 0-

521-41695-7. Appel, Andrew W., & MacQueen, David B. (1991). Standard ML of New Jersey. Pages 1–13 of:

Wirsing, Martin (ed), Third int’l symp. on prog. lang. implementation and logic programming. New York: Springer-Verlag.

Asai, Kenichi. 1999 (Sept.). Binding-time analysis for both static and dynamic expressions. Pages

117–133 of: Static analysis symposium. Ashley, Michael J. (1997). The effectiveness of flow analysis for inlining. In: (ICFP’97, 1997). Birkedal, Lars, & Welinder, Morten. (1995). Binding-time analysis for Standard ML. Lsc, 8(3),

191–208. Blume, Matthias. (1995). Standard ML of New Jersey compilation manager. Manual accompanying

SML/NJ software. Blume, Matthias, & Appel, Andrew W. (1997). Lambda-splitting: A higher-order approach to cross-

module optimizations. In: (ICFP’97, 1997). Consel, Charles. (1993). Polyvariant binding-time analysis for applicative languages. Pages 145–154

of: Symposium on partial evaluation and semantics-based program manipulation.

28 Stefan Monnier and Zhong Shao

Consel, Charles, & Noël, Francois. (1996). A general approach for run-time specialization, and its

application to C. In: (POPL’96, 1996). Danvy, Olivier. (1996). Type-directed partial evaluation. In: (POPL’96, 1996). Danvy, Olivier, Malmkjær, Karoline, & Palsberg, Jens. (1996). Eta-expansion does The Trick. Trans-

actions on programming languages and systems, 8(6), 730–751. Davies, Rowan. 1996 (July). A temporal-logic approach to binding-time analysis. Pages 184–195

of: 11^{th} annual symposium on logic in computer science. Davies, Rowan, & Pfenning, Frank. (1996). A modal analysis of staged computation. In: (POPL’96,

1996). Flanagan, Cormac, Sabry, Amr, Duba, Bruce F., & Felleisen, Matthias. (1993). The essence of

compiling with continuations. Pages 237–247 of: Proc. acm sigplan ’93 conf. on prog. lang. design and implementation. New York: ACM Press.

Foster, Jeffrey S., Fähndrich, Manuel, & Aiken, Alexander. (1999). A theory of qualified types. In:

(PLDI’99, 1999). Ganz, Steve, Sabry, Amr, & Taha, Walid. (2001). Macros as multi-stage computations: Type-safe,

generative, binding macros in macroml. International conference on functional programming. ACM Press.

Girard, J. Y. (1972). Interprétation fonctionnelle et élimination des coupures dans l’arithmétique

d’ordre supérieur. Ph.D. thesis, University of Paris VII. Glynn, Kevin, Stuckey, Peter J., Sulzmann, Martin, & Sndergaard, Harald. (2001). Boolean con-

straints for binding-time analysis. Pages 39–62 of: Program as data objects. Harper, Bob, & Morrisett, Greg. 1995 (Jan.). Compiling polymorphism using intensional type anal-

ysis. Pages 130–141 of: Symposium on principles of programming languages. Harper, Robert, Mitchell, John C., & Moggi, Eugenio. (1990). Higher-order modules and the phase

distinction. Pages 341–344 of: Seventeenth annual acm symp. on principles of prog. languages. New York: ACM Press.

Henglein, Fritz, & Mossin, Christian. 1994 (Apr.). Polymorphic binding-time analysis. Pages 287–

301 of: European symposium on programming. ICFP’97. (1997). International conference on functional programming. ACM Press. ICFP’98. (1998). International conference on functional programming. ACM Press. Jones, Neil D., Gomard, Carsten K., & Sestoft, Peter. (1993). Partial evaluation and automatic

program generations. Prentice Hall International. Leroy, Xavier. 1992 (Jan.). Unboxed objects and polymorphic typing. Pages 177–188 of: Symposium

on principles of programming languages. Leroy, Xavier. 1995 (nov). Le système Caml Special Light: Modules et compilation efficace en Caml.

Tech. rept. 2721. Institut National de Recherche en Informatique et Automatique. Marlet, Renaud, Consel, Charles, & Boinot, Philippe. (1999). Efficient incremental run-time special-

ization for free. In: (PLDI’99, 1999). Milner, Robin, Tofte, Mads, Harper, Bob, & MacQueen, David B. (1997). The definition of Standard

ML revised. Cambridge, Massachusetts: MIT Press. Minamide, Yasuhiko, & Garrigue, Jacques. (1998). On the runtime complexity of type-directed

unboxing. In: (ICFP’98, 1998). Moggi, Eugenio. (1988). Computational lambda-calculus and monads. Tech. rept. ECS-LFCS-88-

86. University of Edinburgh. Moggi, Eugenio. 1997 (Mar.). A categorical account of two-level languages. 13^{th} conference on the

mathematical foundations of programming semantics. Moggi, Eugenio, Taha, Walid, Benaissa, Zine El-Abidine, & Sheard, Tim. 1999 (March). An ide-

Inlining as Staged Computation 29

alized MetaML: simpler, and more expressive. Pages 193–207 of: Proceedings of the european symposium on programming.

Monnier, Stefan, Blume, Matthias, & Shao, Zhong. 1999 (March). Cross-functor inlining in FLINT.

Tech. rept. YALEU/DCS/TR-1189. Dept. of Computer Science, Yale University, New Haven, CT. Nielson, Flemming, & Nielson, Hanne Riis. (1992). Two-level functional languages. New York:

Cambridge University Press. Peyton Jones, Simon, & Marlow, Simon. 1999 (September). Secrets of the Glasgow Haskell Com-

piler inliner. Proceedings of the international workshop on implementation of declarative languages.

PLDI’96. (1996). Symposium on programming languages design and implementation. ACM Press. PLDI’99. (1999). Symposium on programming languages design and implementation. ACM Press. POPL’96. (1996). Symposium on principles of programming languages. ACM Press. Reynolds, John C. (1974). Towards a theory of type structure. Pages 408–425 of: Proceedings,

colloque sur la programmation, lecture notes in computer science, volume 19. Springer-Verlag, Berlin.

Saha, Bratin, & Shao, Zhong. 1998 (Mar.). Optimal type lifting. International workshop on types in

compilation. Shao, Zhong. (1997a). Flexible representation analysis. In: (ICFP’97, 1997). Shao, Zhong. (1997b). An overview of the FLINT/ML compiler. Proc. 1997 acm sigplan workshop

on types in compilation. Published as Boston College Computer Science Dept. Technical Report BCCS-97-03.

Shao, Zhong. (1998). Typed cross-module compilation. Pages 141–152 of: Proc. 1998 acm sigplan

international conference on functional programming. ACM Press. Shao, Zhong. (1999). Transparent modules with fully syntactic signatures. Pages 220–232 of: Proc.

1999 acm sigplan international conference on functional programming (icfp’99). ACM Press. Shao, Zhong, League, Christopher, & Monnier, Stefan. (1998). Implementing typed intermediate

languages. Pages 313–323 of: Proc. 1998 acm sigplan international conference on functional programming (icfp’98). ACM Press.

Shivers, Olin. 1991 (May). Control-flow analysis of higher-order languages. Ph.D. thesis, Carnegie

Mellon University. CMU-CS-91-145. Sperber, Michael, & Thiemann, Peter. (1996). Realistic compilation by partial evaluation. In:

(PLDI’96, 1996). Sperber, Michael, & Thiemann, Peter. (1997). Two for the price of one: Composing partial eval-

uation and compilation. Pages 215–225 of: Symposium on programming languages design and implementation. ACM Press.

Taha, Walid. 1999 (November). Multi-stage programming: Its theory and applications. Ph.D. thesis,

Oregon Graduate Institute, Beaverton, Oregon. Taha, Walid, & Sheard, Tim. 1997 (June). Multi-stage programming with explicit annotations. Pages

203–217 of: Symposium on partial evaluation and semantics-based program manipulation. Tarditi, David. 1996 (Dec.). Design and implementation of code optimizations for a type-directed

compiler for standard ml. Ph.D. thesis, Carnegie Mellon University. CMU-CS-97-108. Wadler, Philip, & Blott, Stephen. 1989 (Jan.). How to make ad-hoc polymorphism less ad hoc.

Symposium on principles of programming languages.