Graph IRs for Impure Higher-Order Languages
Making Aggressive Optimizations Affordable with Precise Effect Dependencies

OLIVER BRAČEVAC∗ , Purdue University, USA and Galois, Inc., USA
GUANNAN WEI, Purdue University, USA
SONGLIN JIA, Purdue University, USA
SUPUN ABEYSINGHE, Purdue University, USA
YUXUAN JIANG, Purdue University, USA
YUYAN BAO, Augusta University, USA
TIARK ROMPF, Purdue University, USA
Graph-based intermediate representations (IRs) are widely used for powerful compiler optimizations, either
interprocedurally in pure functional languages, or intraprocedurally in imperative languages. Yet so far, nosuitable graph IR exists for aggressive global optimizations in languages with both effects and higher-orderfunctions: aliasing and indirect control transfers make it difficult to maintain sufficiently granular dependency
information for optimizations to be effective. To close this long-standing gap, we propose a novel typed graphIR combining a notion of reachability types to track aliasing with an expressive effect system to compute precise
and granular effect dependencies, while supporting local reasoning and separate compilation. Our high-levelgraph IR imposes lexical structure to represent structured control flow and nesting, enabling aggressive andyet inexpensive code motion, instruction selection, and other optimizations for impure higher-order programs.
We formalize the new graph IR based on a 𝜆-calculus with a reachability type-and-effect system along with a
specification of various optimizations. We present performance case studies for CUDA tensor kernel fusion,
symbolic execution of LLVM IR, and SQL query compilation in the Scala LMS compiler framework using the
new graph IR. We observe significant speedups of up to 21𝑥.
CCS Concepts: • Software and its engineering → Compilers; Semantics; Functional languages;
Additional Key Words and Phrases: intermediate representations, higher-order languages, effects, compilers
ACM Reference Format:
Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf.
2023. Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with
Precise Effect Dependencies. Proc. ACM Program. Lang. 7, OOPSLA2, Article 236 (October 2023), 31 pages.
https://doi.org/10.1145/3622813

1 INTRODUCTION
Graph-based intermediate representations (IRs) are an attractive alternative to simpler tree-based
IRs (such as abstract syntax trees, ASTs) for program optimizations. Graphs are sparse in nature,∗ Work completed while at Purdue University

Authors’ addresses: Oliver Bračevac, Purdue University, West Lafayette, IN, USA and Galois, Inc., Portland, OR, USA,oliver@galois.com; Guannan Wei, Purdue University, West Lafayette, IN, USA, guannanwei@purdue.edu; Songlin Jia, Purdue
University, West Lafayette, IN, USA, jia137@purdue.edu; Supun Abeysinghe, Purdue University, USA, tabeysin@purdue.edu;
Yuxuan Jiang, Purdue University, USA, jiang700@purdue.edu; Yuyan Bao, Augusta University, USA, yubao@augusta.edu;
Tiark Rompf, Purdue University, USA, tiark@purdue.edu.

This work is licensed under a Creative Commons Attribution 4.0 International License.
© 2023 Copyright held by the owner/author(s).
2475-1421/2023/10-ART236
https://doi.org/10.1145/3622813

Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

236

236:2

Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf

eliminate redundancy, and exhibit greater locality of information compared to syntax trees. Thisavoids ad-hoc reconstruction of non-local information, (e.g., def-use chains), and facilitates implementations of powerful code motion algorithms and other optimizations. In essence, many forms
of non-local reasoning in the space of program terms map to local reasoning in the space of dependencies between such terms. For instance, common subexpression elimination (CSE) reduces tohash consing, and dead code elimination (DCE) to graph reachability. Most algebraic optimizations
are also just a matter of local “peephole-style” rewrites on nodes and their immediate neighbors.
Impure vs. Higher-Order: Pick One? Graph IRs are widely used in implementations of purefunctional languages [Elliott et al. 2003; Henriksen et al. 2017; Peyton-Jones 1987; Peyton-Jonesand Salkild 1989; Steuwer et al. 2017]. Pure computation induces only data dependencies, thus
granting high degrees of freedom for moving and rewriting code, and enabling aggressive global andinterprocedural optimizations. Graph IRs are also widely used for intraprocedural optimizations1 inimperative language implementations, e.g., “Sea-of-Nodes” IRs [Click and Paleczny 1995] in VMs forJava [Paleczny et al. 2001] and JavaScript [Titzer 2015]. The presence of effects (e.g., heap accesses)
in those languages limits the scope of optimizations to single functions/methods. To achieve any
kind of non-local optimization, imperative languages rely on aggressive inlining and code duplication [Stadler et al. 2014]. Thus, to reap the benefits of graph IRs, language designers/implementerscurrently have to choose between two extremes: (1) higher-order purely functional languages with(truly) global optimizations, or (2) imperative languages with limited local optimizations. But what
about the combination? So far, no suitable graph IRs for global, interprocedural optimization exist
in compilers for languages that combine effects and higher-order functions.
Indirection: The Enemy of Local Reasoning. The main reasons for this significant gap are as
follows: (1) higher-order functions introduce imprecise control transfers, (2) aliasing of mutablereferences introduces imprecise data dependencies, and (3) combinations, such as heap-allocatedfunction values, exacerbate these issues. Consequently, it is hard to extract the sufficiently precise
local dependency information that makes graphs useful. Precise dependency extraction is inherently
context sensitive, so one might consider higher-order flow analyses [Midtgaard 2012; Might 2007;
Shivers 1988] as a natural choice to enhance precision. However, analyses like 0-CFA, while tractable,
are imprecise and yield only coarse-grained dependencies. Analyses like 𝑘-CFA, which simulate
execution up to certain context depth 𝑘 > 0, provide improved precision, but can be prohibitively
expensive in practice [Horn and Mairson 2008; Shivers 2004]. Even considering tractable versions[Might et al. 2010], these analyses are whole-program (i.e., non-modular), propagating information
through iterative fixpoint computations. Thus, it seems that obtaining precise local reasoning firstrequires costly non-local reasoning.
The Key: Typed Graphs Tracking Ownership, Separation, and Effects. Fortunately, typesystems, specifically polymorphic and dependent types, provide an alternative approach to tracking
non-local information, replacing propagation via fixpoint iteration with substitution. Hence, we
propose using types to track dependency information, reducing analysis cost and improving modularity. Type inference algorithms are widely available (e.g., [Dolan and Mycroft 2017; Dunfield andKrishnaswami 2022; Odersky et al. 1999, 2001; Parreaux 2020; Pierce and Turner 2000]), propagate
non-local information effectively, and improve with increased type annotations [Odersky and
Läufer 1996]. Although type inference may have exponential complexity in the worst case, it isefficient in practice. Unlike 𝑘-CFA, type inference does not require simulating execution up to acertain context depth 𝑘 but relies on substitution to propagate non-local information and thus
1 Perhaps confusingly, function-level optimizations are sometimes called “global” in the compiler literature in contrast to“local” block-level optimizations.

Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

Graph IRs for Impure Higher-Order Languages

236:3

avoids many of the challenges associated with maintaining fine-grained dependency information
for aggressive global optimizations.
Based on these insights, we propose a typed graph IR that strikes a balance between affordable
analysis cost and precision. We build on reachability types [Bao et al. 2021], a dependent type system
tracking sets of reachable term variables. It combines ideas from ownership types [Clarke et al.
2013; Noble et al. 1998] and separation logic [Reynolds 2002]. An additional effect system (inspired
by Gordon [2021]) infers how variables are used (e.g., reads, writes, etc.). Combining reachability
and effects allows for precise, local dependency calculations between graph nodes, including true(i.e., read-after-write) and anti-dependencies (i.e., write-after-write, write-after-read).
Our graph IR employs (local) type inference for propagating reachability and effects, and serves as(1) a compilation target of direct-style surface languages, or (2) as part of domain-specific languages(DSLs). In the first case, user annotations guide inference, following the usual credo that someannotations are valuable as documentation, and redundant annotations can be avoided. The amountof required user annotations is reasonable and in the ballpark of Rust [Jung et al. 2021; Matsakis
and Klock 2014]. In the second case, DSL authors leverage the constructive properties and theconstrained nature of DSLs to determine annotations on primitives, which largely eliminates theneed for reachability or effect annotations in user code.
Lexical Structure for Seamless Code Motion and Progressive Lowering. Notably, the newgraph IR features variable binders within nodes, creating a high-level representation of structured
statements with internal control-flow and nesting (e.g., nested functions, conditionals, loops), as
opposed to low-level conditional jumps, and explicit control edges found in traditional “Sea ofNodes” IRs. This approach offers two main advantages: (1) seamless code motion, allowing forflexible movement of conditionals, loops, and lambdas, and (2) progressive lowering, enablingcompilers to translate high-level code into successive lower-level representations within the same
IR. For example, early-stage loops can have implicitly parallel semantics without committing to a
specific behavior, enabling later translations to potentially parallelized and vectorized imperative
loop nests. This nesting structure aligns with contemporary IR frameworks such as MLIR [Lattner
et al. 2021], as opposed to earlier platforms like LLVM [Lattner and Adve 2004].
Contributions. In summary, we show that reachability types, effects, and lexical structure
are a key step toward unlocking the potential of graph IRs for impure functional languages. We
present a formal model of the new graph IR, 𝜆G∗ , which enjoys key soundness properties, including
safety of dependencies. We have also implemented the new graph IR in the Scala LMS compiler
framework [Rompf and Odersky 2010; Rompf et al. 2013], where we demonstrate its effectivenessin optimizing impure higher-order programs, yielding significant speedups. We make the following
specific contributions:• Section 2 motivates graph-based global optimizations for impure higher-order functional languages and shows how they can be realized using our graph IR.
• Section 3 formalizes the graph IR in the 𝜆G∗ -calculus, a version of Bao et al.’s 𝜆 ∗ -calculus in monadic
normal form (MNF) with reachability types and effects, and extends the calculus with a novel
type-and-effect-directed synthesis of precise effect dependencies. We prove type-and-dependency
safety of 𝜆G∗ , i.e., that synthesized dependencies respect the order of runtime effects.
• Section 4 discusses extensions, such as additional forms of structured nodes (e.g., conditionals),
soft dependencies which lead to improved dead-code elimination (DCE), and destructive effects
which enforce policies such as affine uses.
• Section 5 covers middle-tier optimizations at the graph level, such as DCE, CSE, and 𝜆-hoisting, allbacked by the underlying equational theory of 𝜆G∗ . We also showcase how the graph IR supports
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

236:4

Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf

restricted cases of classic higher-order optimizations (e.g., lambda lifting, super-𝛽 inlining), which
can optionally be complemented with fixpoint-based flow analyses.
• Section 6 discusses efficient scheduling and code generation algorithms to transform IR graphsback into trees and perform backend optimizations. We showcase various optimizations includingcode motion, which uses a cheap frequency-estimation heuristic instead of costly flow analyses.
• Section 7 evaluates our graph IR design through detailed case studies and experiments: (1) loop
fusion and kernel fusion [Wang et al. 2019a,b] on CPUs/GPUs, (2) symbolic execution of LLVM
IR [Wei et al. 2020, 2023b], and (3) SQL query compilation [Essertel et al. 2018; Rompf and Amin
2015; Tahboub et al. 2018]. We achieve significant speedups of up to 21𝑥.
Section 8 discusses related work and Section 9 offers concluding remarks.
2

OVERVIEW: FROM TYPES AND EFFECTS TO GRAPHS AND DEPENDENCIESIn this section, we discuss the challenges of optimizing higher-order languages with effects (such as
Scala and OCaml) and motivate the design of our graph IR. Throughout the paper, we use Scala-like
syntax, but the presented ideas easily map to other impure functional languages.
2.1

Motivating Examples: Optimizing with Graph IRs

Consider a program that creates an array of complex numbers on the unit circle and transforms
them to their conjugates, i.e., maps each complex number 𝑎 + 𝑏𝑖 to 𝑎 − 𝑏𝑖:case class Complex(re: Double, im: Double)
val compNums = (0 until 100).map { th => Complex(cos(th), sin(th)) }val conjNums = compNums.map { c => Complex(c.re, -c.im) }/* : Array[Complex] *//* : Array[Complex] */Fusion and Other Simplifications Using Rewriting. Many compilers for functional highperformance DSLs [Henriksen et al. 2017; Roesch et al. 2018; Rompf and Odersky 2010; Rompf et al.
2013; Shaikhha et al. 2019; Steuwer et al. 2017] would apply clever optimizations (such as vertical
map fusion: map f ◦ map g = map (f ◦ g), to avoid creating and immediately traversing an array ofheap-allocated Complex objects. Graph IRs represent expressions as nodes, and data dependencies
between expressions as edges. This makes it easy to apply such optimizations, as the two map
operations in the example are immediate neighbors in a dependency graph, irrespective of theintervening variable bindings.
Why Side-Effects? Clearly, it would be nice to have comparable optimizations in a full generalpurpose language with side effects. But even taken in isolation, the pure functional approach ofcontext-free rewriting has clear limitations: (1) supporting other kinds of traversals such as map,
reduce, zip leads to an explosion of fusion rules, and (2) if both compNums and conjNums are used later,
vertical fusion of compNums into conjNums still leaves two loops, where we need horizontal fusion tomerge them. Through a progressive lowering approach, exposing selected side effects and attempting
fusion in the example, e.g.,
val compNums, conjNums = new Array[Complex](100) /* explicit allocation */for (th ← 0 until 100) {val re = cos(th); val im = sin(th)compNums(th) = Complex(re, im)/* explicit assignment */conjNums(th) = Complex(re, -im)}leads to more uniform and generic handling of multiple fusion scenarios compared to pure functional
simplification (cf. Section 7.1). But of course, this requires precise reasoning about effects anddependencies, while still working in a higher-order setting.
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

Graph IRs for Impure Higher-Order Languages

236:5

Changing Data Representation. Many other non-trivial optimizations can be performed locallyby looking at the neighbors of a node, e.g., transforming from an “array-of-struct (AoS)” to “structof-array (SoA)” layout that disentangles the array of complex numbers compNums into two arrays of
the real and imaginary components. This transformation changes the data layout, yielding a better
fit for SIMD or GPU execution. In the transformed code, there are no explicit Complex objects left:
val compRe, compIm, conjRe, conjIm = new Array[Double](100)for (th ← 0 until 100) {val re = cos(th); val im = sin(th)compRe(th) = re; compIm(th) = im/* compNums */conjRe(th) = re; conjIm(th) = -im /* conjNums */}Clearly, care must be taken here to ensure that reordered operations are noninterfering. A compiler
using a graph IR can also recognize that the computation does not change the real parts of thenumbers and altogether eliminate the conjRe array. Downstream uses of conjNums can share the arrayof real components with compNums.
Moving Code Around Freely. Another benefit of using a graph IR is cheap code motion. A code
motion algorithm converts a graph into a tree and decides the hierarchy and ordering according todependencies and heuristics (cf. Section 6). Let us add a conditional selection:
val result = if (cond) { (compRe, compIm) /* compNums */ }else
{ (compRe, conjIm) /* conjNums */ }If the rest of the computation only uses either branch via result, then the previous conjIm computation
is wasteful. Code motion will move it directly into the else-branch:val result = if (cond) { (compRe, compIm) } else {val conjIm = new Array[Double](100)for (th ← 0 until 100) { conjIm(th) = -compIm(th) }(compRe, conjIm)}

On the other hand, for blocks that may be executed multiple times (such as loops and functions), it
is preferable to compute as much as possible before the block, so a code motion algorithm would
attempt to place instructions as little as possible inside these blocks.
2.2

Data and Effect Dependencies

We now switch to informal but thorough explanations of our graph IR. We use A-normal form(ANF) [Flanagan et al. 1993] to represent programs as sequential blocks binding each operation toa unique variable, which permits a straightforward reading as a directed graph. Fundamental tooptimizing impure higher-order programs are dependencies exposing local information at nodes.
Data Dependencies. The first and most obvious kind are data dependencies which coincidewith free-variable occurrences in terms. We draw them as directed dotted edges, connecting nodes
with free occurrences to the respective nodes with binding occurrences. val x1 = 1
x1 : 1
We draw ANF terms (i.e., nodes) as white boxes labeled with their val x2 = 2
x2 : 2(unique) name. These nodes are also labeled with the operand of the val x3 = x1 + x2
x3 : +
term, but we often omit it in examples.
Effect Dependencies. We have further kinds of dependencies that induce a partial ordering overeffectful operations. Such a dependency imposes a strict before-after execu- out out...
tion/scheduling order. Consider the following program that prints a sequence ofoutmessages to standard output (out):x1
val x1 = println(out, "hello")/ {out ↦→ last-use-out}
val x2 = println(out, "changed") / {out ↦→ x1}
val x3 = println(out, "world")/ {out ↦→ x2}

out

x2
out

x3

Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

236:6

Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf

We annotate the variable bindings with effect-dependency mappings. A dependency mapping𝑥 ↦→ 𝑦 indicates an effectful use of the operand 𝑥 by the annotated node, and 𝑦 is the node where𝑥 was last used, or the start of a block (cf. Section 2.3). For example, out ↦→ x1 above denotes that
node x2 prints to out, and the last prior print operation to out happens at node x1, therefore theexecution/scheduling of x2 should happen after x1. We draw effect dependencies as directed solidedges in teal, labeled with the name of the used resource, and connect a node using the resource
to the node that last used it. In the drawing on the right, all prior uses are subsumed under “. . . ”.
Notably, pure expressions are recognizable by having an empty effect-dependency mapping.
Nodes can induce effects on multiple operands/resources, which will each appear in the depenout
dency mapping’s domain. Consider printing to two files out and err:...
x1
val x1 = println(out, "ok 1") / {out ↦→ last-use-out}
val x2 = println(err, "bad") / {err ↦→ last-use-err}
val x3 = println(out, "ok 2") / {out ↦→ x1}
val x4 = println(err, "bad") / {err ↦→ x2}

err

...
err

x2

out

x3
x4

Since node x2 writes to err and only needs to depend on the last node printing to err, node x3 candepend on x1, skipping x2. Optimizations/code motion may use this fact to rearrange x2 after x3.
Hard and Soft Dependencies. Effect dependencies induce an unbreakable “hard” ordering
requirement which is sometimes overly strict, especially in programs involving memory allocations,reads, and writes. Consider the following snippet that consecutively writes numbers to a heapallocated cell and finally reads from that cell:
val x1 = new Ref(0); val x2 = (x1 := 1); val x3 = (x1 := 2); !x1

Note that the assignment to x1 at node x2 is immediately overwritten at node x3, and it is thus
unnecessary to generate code for x2. However, the last use of x1 at x3 points to x2, and the effectdependency notion so far prevents eliminating x2. We solve this issue with soft dependencies(cf. Section 4.2), and by further classifying effectful uses of operands as read or writes. Nodes with
only soft dependencies may be eliminated but still need to be taken into account for ordering.
The above example exposes the “write-after-write” pattern and induces a soft dependency fromx3 to x2. Another pattern inducing soft dependency is “write-after-read”, for example: . . . 𝜔 x1
val x1 = new Ref(0) / {𝜔 ↦→ ...}ℎ {}𝑠val x2 = !x1/ {x1 ↦→ x1}ℎ {}𝑠val x3 = (x1 := 42) / {}ℎ {x1 ↦→ x2}𝑠

x1

x2
x1

x3

Subscripts (ℎ and 𝑠) distinguish the hard from soft dependencies, which are depicted by dashed tealedges. Here, x3 soft-depends on node x2, meaning that x2 can never be executed/scheduled after x3.
However, for x3, it is not necessary to be executed/scheduled after x2. So we could safely eliminate
x2 if it has no further use in the program. Note that reference allocations (e.g., x1) induce a readeffect on the node 𝜔, which represents a global allocation capability. Once a reference is allocated,
it is tracked with hard/soft dependencies, and it may have multiple soft dependencies: . . . 𝜔 x1
val x1 = new Ref(0) / {𝜔 ↦→ ...}ℎ {}𝑠val x2 = (x1 := 21) / {}ℎ {x1 ↦→ x1}𝑠val x3 = !x1/ {x1 ↦→ x2}ℎ {}𝑠val x4 = (x1 := 42) / {}ℎ {x1 ↦→ [x2, x3]}𝑠

x1

x2
x1

x3

x1
x1

x4

Read and Write Effects. A read effect (e.g., at x3) results in a hard dependency on the last write.
In contrast, a write effect (e.g., at x2 and x4) induces soft dependencies on the last write and all reads
after that write. The assignment at x2 is the first effectful use of x1, hence the soft dependency points
to the node declaring x1. It is safe to eliminate x2 and x3, as long as x3 has no further occurrence.
The choice of read/write effects needs to be individually determined for each kind of operation,and our approach supports effect-specific optimizations. Consider the following examples ofdifferent kinds of “read” operations and their effects:
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

Graph IRs for Impure Higher-Order Languages/* file I/O; read is also a write */val f1 = read(fd) / {fd ↦→ last-write-fd}ℎ {}𝑠val f2 = read(fd) / {fd ↦→ f1}ℎ {}𝑠/* memory allocation; reads next store address */val a1 = alloc(4) / {𝜔 ↦→ block-start}ℎ {}𝑠val a2 = alloc(4) / {𝜔 ↦→ block-start}ℎ {}𝑠236:7/* randomness; non-idempotent read */val r1 = random() / {𝜌 ↦→ block-start}ℎ {}𝑠val r2 = random() / {𝜌 ↦→ block-start}ℎ {}𝑠/* references; idempotent reads, permitting CSE */val x1 = !x
/ {x ↦→ last-write-x}ℎ {}𝑠val x2 = !x
/ {x ↦→ last-write-x}ℎ {}𝑠

We categorize file I/O, memory allocation, and randomness differently from mutable references.
File-system reads create hard dependencies and are considered both read and write effects due to theimplicit change in the file cursor’s state. However, soft dependency for files is unsafe, e.g., removing
f1 would change the behavior of the program, even if f1 is never used. Memory allocation involves
heap reads but does not require ordering, allowing removal of unused allocations (cf. Section 7.3).
Reading random numbers alters the generator 𝜌, but is treated as a non-idempotent read since theorder is insignificant. A local CSE rule can be defined for multiple reference reads (cf. Section 5.1),
which is not applicable to the other operations mentioned due to their idempotency.
Aliasing and Reachability. As shown above, the key of dependency tracking is identifying thelast use of effectful resources. This is less straightforward if resources are aliased through multiple
bindings, closed over by first-class functions, or other data structures. It is crucial to track aliasing
to maintain fine-grained dependencies, which would otherwise become useless for optimizations.
We use reachability types [Bao et al. 2021] for tracking sets of aliased variables in types. Consider
the following example of two aliased references:... 𝜔x1/* x1: Ref[Int]{x1} */val x1 = new Ref(0)/ {𝜔 ↦→ ...}ℎ {}𝑠/* x2: Ref[Int]{x1, x2} */val x2 = x1
/ {}ℎ {}𝑠val x3 = (x1 := 1) /* @wr(x1)*/ / {}ℎ {x1 ↦→ x1}𝑠val x4 = (x2 := 2) /* @wr(x1,x2) */ / {}ℎ {x1 ↦→ x3, x2 ↦→ x3}𝑠

x2 x1

x3
x1

x2

x4

The type of x2 is an integer reference. The reachability type system annotates it with a set of variables {x1, x2}, i.e., the aliases of x2. We make use of this fact at x4, inferring dependencies for eachalias of the assignment target, informed by effect types. That is, we assign effects to reachability
sets, e.g., writing x2 induces the @wr(x1,x2) effect on x2 and all its aliases (dually, the @rd(_) effectindicates a read), and effects determine the dependency mappings (cf. Section 3). Dependency
tracking thus remains precise even in the presence of aliasing.
For simplicity, we conflate reachability and aliasing, but the former is actually a stronger relation,e.g., x1’s set remains unaffected by the subsequent alias x2. This is a key aspect of the type system:
if two entities are aliased, then their reachability sets will overlap, which is sufficient for reasoning
about program properties and optimization opportunities, and avoids more complex alias analysis.
2.3

Block Structure

Instructions are implicitly grouped as blocks via their dependencies. In contrast to traditional “Seaof-Nodes” IRs (e.g., Graal [Duboscq et al. 2013] and V8), our IR’s blocks have bound variables, sothat we can directly represent nested blocks and function definitions without a known control-flow
predecessor. “Sea-of-Nodes” IRs do not support these features.
A block ends with the return variable and summary of the effect dependencies at the block’s
return position, including their last effectful use. Here is an example block labeled 𝜆z.x3/𝛿:out𝑧{ /* z => block with implicit binder */val x1 = println(out, "str1") / {out ↦→ z}
val x2 = println(out, "str2") / {out ↦→ x1}
val x3 = 42 / {}x3 / {out ↦→ x2}
}

out

x1
out

x2
x3

out

𝜆 •.•/•

Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

236:8

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf
val c = new Ref(0)/* inc : (Int => Int @rd(c)@wr(c)){c} */def inc(x0: Int) = {val x1 = !c
/ {c ↦→ x0}
val x2 = c := x1 + x0 / {c ↦→ x1}
val x3 = !c
/ {c ↦→ x2}x3/ {c ↦→ x3}} / {}x0c

Call Site (After Inlining)

c

c

c

x1

𝜆inc(x0)

c

u

c

c

u

x2

x1

c
c

c

42

c

𝜆 •.•/•

c

x3

c

a

out

a

val a = (c := 0) / {c ↦→ r}
val p = println(out, r) / {out ↦→ ...}
p

42

x2

r

/* function call to be inlined */val r = inc(42)/ {c ↦→ u}c𝜆inc(x0)

x3

val u = (c := 21) / {c ↦→ c}⇒Call Site

Function Definition

out

p

...

c

out
out

...

Fig. 1. Example: Function inlining and dependency rewiring. Left: Function definition using blocks withbinders. Middle: Dependency of a function application. Right: Inlining the function at node r rewires thecaller and callee dependencies (highlighted in red). The type of function inc indicates that it closes over thereference c and induces read/write effects on it. This effect informs the dependency on c at the call site r.

The return variable x3 of the block includes the dependency on out at node x2. Transitively, this will
also include the println effect on out at node x1. The first effectful operation in a block depends on
the bound variable provided by the enclosing structure, e.g., a function’s formal parameter.
Crucially, unlike traditional SSA/CFG IRs that use jump instructions at the terminal position torepresent control transfer, our IR directly supports nesting and bindings, thus retaining a more direct
representation of higher-order programs in the graph. This design choice allows us to efficiently
perform frequency estimation and code motion (cf. Section 6.2).
Blocks can be used to compose larger elements, such as conditionals, loops, and function abstractions. Conditional nodes consist of a symbol referring to the conditional expression, and two nested
blocks representing the two branches. Similarly, a loop node has a single symbol and a single block:
val x1 = if (cond ) 𝑏 1 else 𝑏 2
val x2 = while (cond ) 𝑏

z1
..
.
cond

b1 : 𝜆 •.•/•

z
..
.

z2
..
.
b2 : 𝜆 •.•/•

x1 : if (•) • else •b : 𝜆 •.•/•

condx2 : while (•) •Using the block structure, a potentially recursive function abstraction can be syntactically represented as a self-reference symbol 𝑓 , a formal parameter 𝑥, and a block 𝑏, i.e., 𝜆𝑓 (𝑥).𝑏.
2.4

Function Abstraction

Typing Functions with Latent Effects. Free variables captured by functions are consideredreachable by the function and hence occur in the function type’s reachability qualifier. The following
example shows a heap-allocated cell and a function that increments it and returns the new value:
val c = new Ref(0) /* c: Ref[Int]{c} *//* inc: (Int => Int @rd(c)@wr(c)){c} */def inc(y: Int) = { val old = !c; c := old + y; val res = !c; res }The comments precisely describe the type of c and inc. The function type of inc has a qualifier {c},which is the combined reachable set of all its free variables, and @rd(c)@wr(c) indicates the function’s
latent effects: inc can read and write reference c.
Dependency Abstraction. Figure 1 (left) shows the ANF version of function inc with dependencies (Line 3-9). A function definition is pure and hence has no effect dependency (Line 9). However,inside the function, the formal parameter x0 is not only a placeholder for an unknown value, but
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

Graph IRs for Impure Higher-Order Languages

236:9

Graph IR Syntax
𝜆G∗x, y, z ::= 𝑥 | ℓName𝑔 ::= x | let 𝑥 = 𝑏 • 𝛿 in 𝑔Graph𝑣 ::= ℓValue𝑏 ::= 𝑛 | 𝑔
Binding
Qualifier/Effect𝑛 ::= 𝜄 | x x | ref x x | ! x | x B x Graph Node 𝑝, 𝑞, 𝜺, 𝜑 ∈ Pfin (Var ⊎ Loc)
𝑆,𝑇 , 𝑈 ::= 𝐵 | (𝑥 : 𝑇 𝑞 ) →𝜺 𝑇 𝑞 | Ref 𝑇 Type
𝜄 ::= 𝑐 | 𝜆𝑥 .(𝑔 • 𝛿) | ref ℓ ℓ
IntroductionΓ ::= ∅ | Γ, 𝑥 : 𝑇 𝑞
Typing Context
Δ, 𝛿 ::= x ↦→ x
Dependency
Σ ::= ∅ | Σ, ℓ : 𝑇 𝑞
Store Typing
𝑥, 𝑦, 𝑧 ∈ Var
Variable𝜺1 ▷ 𝜺2 := 𝜺1 ∪ 𝜺2
Sequential Compositionℓ, 𝑤 ∈ Loc
LocationFig. 2. Term and type syntax of the graph IR 𝜆G∗ .

also a placeholder for unknown dependencies at call sites. In this example, the node that first reads
c depends on the parameter x0 (Line 5), hence it will be scheduled at the block’s start.

There are two abstractions here: (1) The function parameter can be a dependency for operationsin the function’s body; (2) functions need to return a dependency mapping that summarizes last-use
information. Using them together enables a modular, context-insensitive way to specify dependency
for functions. Next, we discuss how dependencies are instantiated at call sites.
Connecting and Rewiring Dependencies. Consider the call site at Line 11-17 in Figure 1, which
has an application of inc in-between two operations over c (Line 14). From the type of inc (Line 3)
we know that it performs effects over its captured resource c. Hence, call sites of inc should include
dependencies of c, which is {c ↦→ u} in this example. In the rest of the block, the next operation of c(Line 16) also depends on the application (i.e., {c ↦→ r}).
Figure 1 (right) shows the graphs of inc’s definition, and the call site before and after inlining inc.
We can observe the following difference (highlighted in red): (1) the function body replaces r, andthe parameter in the body has been replaced with the call’s argument 42; (2) the dependency ofthe body’s first node pointing to the formal parameter x0 is rewired to the upstream node u at thecall site; (3) any downstream dependency to the function application r is rewired with the actual
last effectful operation in the function body (using the information from the function’s return
dependency). We call the second and third changes “dependency rewiring”.
3

CORE GRAPH IR

We sketch the formal theory and metatheory of the typed graph IR 𝜆G∗ ,2 proving syntactic typesoundness and correctness properties of effect-dependency synthesis. The core system presented
here supports only “hard” dependencies, with soft dependencies being covered in Section 4.2.
We also omit other non-essential features like untracked values, recursive 𝜆-abstractions, higherorder mutable references, and type polymorphism. Those can be supported by basing the 𝜆G∗ IR on
polymorphic reachability types [Wei et al. 2023a].
From ANF to MNF. So far, we motivated the 𝜆G∗ IR in Section 2 informally in ANF (i.e., flat
sequences of named atomic expressions), which is also used by our Scala LMS implementation.
Now we generalize from ANF to monadic normalform (MNF) [Hatcliff and Danvy 1994], allowing
nested let bindings. This permits decomposing complex transformations into more elementary
steps, simplifying reasoning in 𝜆G∗ ’s metatheory. For instance, function inlining in LMS (Figure 1)
while straightforward in its implementation is quite involved when viewed syntactically becauseof the need to maintain the “flat” ANF syntax, and requires simultaneous substitution, flattening,and dependency rewiring of the function body. So, using evaluation contexts, an atomic formal
2 The full details, including soundness proofs are in the supplementary material [Bračevac et al. 2023].

Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

236:10

Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf[Σ | Γ] 𝜑 • Δ ⊢ (𝑛 | 𝑔) : 𝑇 𝑞 𝜺 { (𝒏 | 𝒈) • 𝛿

Dependency Synthesisx : (Ref 𝐵) 𝑞 ∈ [Σ | Γ] 𝜑𝑐∈𝐵[Σ | Γ] 𝜑 • Δ ⊢ 𝑐 : 𝐵 ∅ ∅ { 𝑐 • ∅({-cst)[Σ | Γ , 𝑥 : 𝑇 𝑝 ] 𝑞,𝑥 • ↦→𝑥 ⊢ 𝑔 : 𝑈 𝑟 𝜺 { 𝒈 • 𝛿𝑞⊆𝜑y : 𝐵 ∅ ∈ [Σ | Γ] 𝜑

[Σ | Γ] 𝜑 • Δ ⊢ x B y : Unit ∅ x{ x B y • Δ| x∗({-:=)

x : 𝑇 𝑞 ∈ [Σ | Γ] 𝜑
[Σ | Γ] 𝜑 • Δ ⊢ 𝜆𝑥 .𝑔 : ((𝑥 : 𝑇 𝑝 ) →𝜺 𝑈 𝑟 ) 𝑞 ∅({-ret){ (𝜆𝑥 .𝒈 • 𝛿) • ∅[Σ | Γ] 𝜑 • Δ ⊢ x : 𝑇 x ∅ { x • ∅({-abs)𝑞x : (𝑧 : 𝑇 𝑝∗∩𝑞∗ ) →𝜺 𝑈 𝑟 ∈ [Σ | Γ] 𝜑
[Σ | Γ] 𝜑 • Δ ⊢ 𝑏 : 𝑆 𝑝 𝜺1 { 𝒃 • 𝛿 1
y : 𝑇 𝑝 ∈ [Σ | Γ] 𝜑
𝜃 = [𝑝/𝑧][Σ | Γ , 𝑥 : 𝑆 𝑝∗∩𝜑∗ ] 𝜑,𝑥 • Δ, (𝜺1 ∗, 𝑥) ↦→ 𝑥 ⊢ 𝑔 : 𝑇 𝑞 𝜺2𝑧 ∉ fv(𝑈 )𝜺 ⊆ 𝑞, 𝑧𝑟 ⊆ 𝜑, 𝑧{ 𝒈 • 𝛿2({-app)
𝜑
𝑟
𝜃
=
[𝑝/𝑥]
𝑥 ∉ fv (𝑇 )[Σ | Γ] • Δ ⊢ x y : (𝑈 𝜺)𝜃
𝜑{ x y • Δ| (𝜺𝜃 )∗[Σ | Γ] • Δ ⊢ let 𝑥 = 𝑏 in 𝑔 : (𝑇 𝑞 𝜺1 ▷ 𝜺2 )𝜃
{ (let 𝑥 = 𝒃 • 𝛿 1 in 𝒈) • 𝛿 1, 𝛿 2 [𝑥 { Δ|𝑝 ∗]x : Alloc 𝑞 ∈ [Σ | Γ] 𝜑 y : 𝐵 ∅ ∈ [Σ | Γ] 𝜑({-let)({-ref)[Σ | Γ] 𝜑 • Δ ⊢ ref x y : (Ref 𝐵) ∅ x{ ref x y • Δ| x∗[Σ | Γ] 𝜑 • Δ ⊢ 𝑏 : 𝑆 𝑝 𝜺1 { 𝒃 • 𝛿 1
Σ | Γ ⊢ 𝑆 𝑝 𝜺1 <: 𝑇 𝑞 𝜺2
x : (Ref 𝐵) 𝑞 ∈ [Σ | Γ] 𝜑({-!)
𝑞, 𝜺2 ⊆ 𝜑[Σ | Γ] 𝜑 • Δ ⊢ ! x : 𝐵 ∅ x { ! x • Δ| x∗({-sub)[Σ | Γ] 𝜑 • Δ ⊢ 𝑏 : 𝑇 𝑞 𝜺2 { 𝒃 • Δ| 𝜺2
x : 𝑇 𝑞 ∈ [Σ | Γ] 𝜑Name Lookup
𝑥 :𝑇𝑞 ∈ Γℓ :𝑇𝑞 ∈ Σ𝑞, 𝑥 ⊆ 𝜑(l-var)𝑥 : 𝑇 𝑞 ∈ [Σ | Γ] 𝜑𝑞, ℓ ⊆ 𝜑(l-loc)ℓ : 𝑇 𝑞 ∈ [Σ | Γ] 𝜑

Fig. 3. Dependency synthesis and select type checking rules of the graph IR 𝜆G∗ . The remaining type checking
rules coincide with the synthesis rules when ignoring the output to the right of {.

inlining step on ANF would look like
(𝑓 = 𝜆𝑦.𝐴2 [ 𝑧/𝛿 2 ]) ∈ 𝐴1

𝜃 1 = [𝑢/𝑦]𝜃 2 = [𝑧/𝑥]𝜌 1 = [𝑦 { 𝛿 1 ]𝜌 2 = [𝑥 { 𝛿 2 ]𝐴1 [ let 𝑥 = 𝑓 𝑢/𝛿 1 in 𝑎 ] −→ 𝐴1 [ 𝐴2 [ 𝑎𝜃 2 𝜌 2 ]𝜃 1 𝜌 1 ]where we are careful to replace the function call at 𝑥 with the entire function body, plugging thecontinuation 𝑎 into function block 𝐴2 ’s return position, before plugging the inlined result backinto the calling context 𝐴1 . Plus, we need to patch up the formal parameter and block return by
substitution and dependency rewiring (cf. Section 3.3).
Formally proving the soundness of such a rule within the constraints of ANF is tedious, and one
is better off with more fine-grained reductions. MNF enables modeling function inlining by a formof 𝛽-reduction, simply replacing the call 𝑓 𝑢 with an instance of the function’s body at the binding
𝑥 above. We can further “flatten” the nested term by separate administrative liftings.
3.1

SyntaxWe represent programs in the MNF syntax (Figure 2) as terms 𝑔, where let bindings denote named
nodes or nested graphs, variable occurrences indicate edges for data dependencies, and 𝛿 maps
indicate edges for effect dependencies. A node 𝑛 is either an introduction form (i.e., constants,functions, allocations), or an operation on let-bound names, i.e., applications, reference allocations,
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

Graph IRs for Impure Higher-Order Languages

236:11

Store Terms, Graph Term Contexts, Binding Contexts
𝜎 ::= ∅ | 𝜎, lets ℓ = 𝜄

𝐺 ::= □ • 𝛿 | (let 𝑥 = 𝐺 in 𝑔) • 𝛿

𝐵 ::= (let 𝑥 = □ in 𝑔) • 𝛿 | (let 𝑥 = 𝐵 in 𝑔) • 𝛿
𝜎 | 𝑧.𝑔 • 𝛿 −→G 𝜎 | 𝑧.𝑔 • 𝛿Reduction Rules
𝜎 | 𝑧.𝐵 [ ℓ1 ℓ2 • 𝛿 1 ]−→G

𝜎 | 𝑧.𝐵 [ (𝑔 • 𝛿 2 ) [𝑥 { 𝛿 1 ] [ℓ2 /𝑥] ]𝜎 = 𝜎1, lets ℓ1 = 𝜆𝑥 .𝑔 • 𝛿 2, 𝜎2dom(𝛿 1 ) ⊆ dom(𝜎), cod(𝛿 1 ) ⊆ {𝑧}(𝛽)𝜎 | 𝑧.𝐺 [ let 𝑥 = ℓ • 𝛿 in 𝑔 ]−→G

𝜎 | 𝑧.𝐺 [ 𝑔[𝑥 { 𝛿] [ℓ/𝑥] ]dom(𝛿) ⊆ dom(𝜎), cod(𝛿) ⊆ {𝑧}(let)

𝜎 | 𝑧.𝐺 [ let 𝑥 = 𝜄 • 𝛿 in 𝑔 ]−→G𝜎, lets ℓ = 𝜄 | 𝑧.𝐺 ′ [ 𝑔[𝑥 { 𝛿] [ℓ/𝑥] ]ℓ ∉ dom(𝜎), cod(𝛿) ⊆ {𝑧}, 𝐺 ′ = 𝐺 ⟨𝜄 : 𝑧.ℓ⟩

(intro)𝜎, lets ℓ = ref 𝑤 ℓ ′, 𝜎 ′ | 𝑧.𝐵 [ !ℓ • 𝛿 ]−→G𝜎, lets ℓ = ref 𝑤 ℓ ′, 𝜎 ′ | 𝑧.𝐵 [ ℓ ′ • 𝛿 ]dom(𝛿) ⊆ dom(𝜎), cod(𝛿) ⊆ {𝑧}(deref)𝜎, lets ℓ = ref 𝑤 ℓ ′, 𝜎 ′ | 𝑧.𝐵 [ ℓ := ℓ ′′ • 𝛿 ]−→G𝜎, lets ℓ = ref 𝑤 ℓ ′′, 𝜎 ′ | 𝑧.𝐵 [ unit • 𝛿 ]dom(𝛿) ⊆ dom(𝜎), cod(𝛿) ⊆ {𝑧}(assign)Contextual Effect Propagation

𝐺 ⟨𝜄 : 𝑧.ℓ⟩𝐺 ⟨𝑐 : 𝑧.ℓ⟩
= 𝐺𝐺 ⟨𝜆𝑥 .𝑔 • 𝛿 : 𝑧.ℓ⟩= 𝐺(□ • 𝛿)⟨ref 𝑤 ℓ1 : 𝑧.ℓ2 ⟩= □ • 𝛿, ℓ2 ↦→ 𝑧((let 𝑥 = 𝐺 in 𝑔) • 𝛿)⟨ref 𝑤 ℓ1 : 𝑧.ℓ2 ⟩ = (let 𝑥 = 𝐺 ⟨ref 𝑤 ℓ1 : 𝑧.ℓ2 ⟩ in 𝑔) • 𝛿, ℓ2 ↦→ 𝑧
Fig. 4. Call-by-value reduction for 𝜆G∗ with runtime dependency checking.

dereferences, or assignments. Operands can either be store locations or term variables, and we
use the category of names to refer to either. For a uniform treatment of effect introductions, we
let allocations ref x y take an explicit capability parameter x granting permission to allocate. We
consider only store locations as values, because the operational semantics (Section 3.5) retains both
immutable and mutable variables, so that term substitution becomes renaming.
3.2

Reachability Types, Aliasing and Separation

The 𝜆G∗ type system tracks reachability qualifiers 𝑞 and effects 𝜺 (Figure 2), which are both sets
of variables and store locations. Qualifiers track which other values are reachable/aliased from acomputation’s result, whereas effects indicate which variables/node names are the target of aneffect. Tracking reachable variables in types enables reasoning about many useful properties ofhigher-order programs (cf. [Bao et al. 2021]).
Observable Separation. In the case of function types ((𝑥 : 𝑆 𝑝 ) →𝜺 𝑇 𝑞 ) 𝑟 , the attached qualifier𝑟 includes the free variables. Function types are dependent in their argument 𝑥, which may appear
free in the latent effect 𝜺, codomain type 𝑇 , and codomain qualifier 𝑞 and refers to the qualifierof arguments at call sites. The reachability type system guarantees observable separation, i.e., thequalifier 𝑟 above certifies that functions of this type do not observe any reachable names beyond 𝑟
in the context. That limits variables/node names in effects, and thus potential effect dependencies.
More generally, we assign a filter 𝜑 to typing judgments (Figure 3) which restricts access to thecontext, akin to substructural type systems, i.e., the subject 𝑔 can only observe the names in 𝜑.
On-demand Reachability. Following Wei et al. [2023a], we choose a variant of Bao et al.’ssystem which assigns reachability qualifiers (and effects) in an on-demand manner. That is, typeassignment assigns minimal reachability sets to expressions, e.g., variables initially only reachthemselves in rule ({-ret), as opposed to an “eager” assignment where all reachable aliases inProc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

236:12

Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf

context are immediately assigned. To resolve maximal dependencies, we compute the transitive
reachability closure in the given context, written 𝑞∗ resp. 𝜺∗, when appropriate. Its formal definition
is in the supplementary material ([Bračevac et al. 2023], Figure 3).
3.3

Dependencies

Effect dependencies are finite maps 𝛿 from names to names attached to let bindings and function
bodies. Dependencies come with the standard "update" operator which is associative:(𝛿 1, 𝛿 2 ) (x) = 𝛿 2 (x), x ∈ dom(𝛿 2 )(𝛿 1, 𝛿 2 ) (x) = 𝛿 1 (x), x ∉ dom(𝛿 2 )and a restriction operator of the domain to a given set (abusing set notation): 𝛿 |𝛼 := {x ↦→ y ∈𝛿 | x ∈ 𝛼 }, and we also define a removal operator, i.e., 𝛿 − 𝛼 := {x ↦→ y ∈ 𝛿 | y ∉ 𝛼 } removing
all mappings pointing into 𝛼. In symmetry with substitutions on graphs and qualifiers, there is a
notion of substitution (or rewiring, rerouting), over dependencies:
𝛿 1 [x { 𝛿 2 ] := 𝛿 1 − {x}, {y ↦→ z ∈ 𝛿 2 | y ↦→ x ∈ 𝛿 1 },which is rerouting the dependency target x via 𝛿 2 . That is, we substitute some of the targets independency mappings, which happens when the name x is replaced, e.g., when x is the formal
parameter of a function at a call site.
3.4

Type-Effect-Dependency System

From reachability qualifiers and effects, we can extract precise effect dependencies, as motivated in
Section 2.2, and formalized by type-directed dependency synthesis (Figure 3).
The judgment [Σ | Γ] 𝜑 • Δ ⊢ 𝑔 : 𝑇 𝑞 𝜺 { 𝒈 • 𝛿 intuitively means: Given a dependency map Δ
recording the ambient last uses of each variable/location bound in Γ and Σ, the graph 𝑔 synthesizes
to the dependency-annotated 𝒈 and has local dependencies 𝛿.
Ignoring the teal parts, we obtain a version of Bao et al.’s type system for MNF, where effects track
those variables/locations and their reachable aliases which are the operand of an effect operation.
Synthesis. Dependency synthesis follows a simple idea: We track in the map Δ attached to thecontext (essentially a coeffect) the last use of each bound name as the target of an effect invocation.
If the graph’s effect is 𝜺, then the generated local dependency 𝛿 is always the projection 𝛿 = Δ| 𝜺∗ ,i.e., we attach the current last uses of the variables in the effect. The last-uses map Δ is updated at
let bindings ({-let), i.e., if the bound subgraph has effect 𝜺1 , then we synthesize the body withΔ, (𝜺1 ∗, 𝑥) → 𝑥, i.e., the last use of the variables in 𝜺1 ∗ is at 𝑥, and 𝑥 points to itself since it is new.
In contrast, synthesizing functions ({-abs) sets all last uses to the parameter 𝑥, abstracting overall possible call sites. The shorthand ↦→𝑥 denotes the map Δ that assigns 𝑥 to all names in context.
Typing nodes and graphs may use subsumption ({-sub) to scale (1) qualifiers (increasing
aliasing), (2) effects, and (3) dependency mappings (remaining consistent with the effect scaling).
The subtyping rules are defined in the supplement [Bračevac et al. 2023]. To summarize, we canprove that synthesis is essentially a function over typing derivations of Bao et al.’s system in MNF:
Lemma 3.1 (Synthesis Properties).
(1) Dependencies mirror effects: [Σ | Γ] 𝜑 • Δ ⊢ 𝑔 : 𝑇 𝑞 𝜺 { 𝒈 • 𝛿, then 𝛿 = Δ| 𝜺∗ .
(2) Synthesis is sound: If [Σ | Γ] 𝜑 • Δ ⊢ 𝑔 : 𝑇 𝑞 𝜺 { 𝒈 • 𝛿, then [Σ | Γ] 𝜑 • Δ ⊢ 𝒈 : 𝑇 𝑞 𝜺.
(3) Synthesis is total: If [Σ | Γ] 𝜑 ⊢M 𝑔 : 𝑇 𝑞 𝜺 then ∀Δ. ∃𝒈. ∃𝛿. [Σ | Γ] 𝜑 • Δ ⊢ 𝑔 : 𝑇 𝑞 𝜺 { 𝒈 • 𝛿.
3.5

Dependency-Checking Operational Semantics

Figure 4 shows the call-by-value operational semantics for 𝜆G∗ . Unlike standard formulations, it
keeps both mutable and immutable values in the store, and static dependencies as part of the terms.
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

Graph IRs for Impure Higher-Order Languages

236:13

Reductions occur over runtime configurations 𝜎 | 𝑧.𝑔 • 𝛿, attaching a block start variable 𝑧 to
the graph term 𝑔 with its dependency 𝛿. 𝑧 is chosen to not be a free variable of 𝑔 and to check if adependency has been evaluated. The next operation’s dependencies will point to 𝑧, ensuring all
current node dependencies are resolved. Well-typed terms do not exhibit dependency violations,meaning dependencies correctly reflect the runtime execution order of effects.
As motivated in Section 2.4, function applications (𝛽) rewire function and call-site dependencies,
similar to let-binding reduction in (let). Rule (intro) commits an introduction form into the store,
allocating a fresh location. For reference introductions, the fresh location is included in an effectand must be inserted/propagated in dependencies along the evaluation context spine. The otherrules for dereference and assignment are standard.
3.6

Metatheory

The 𝜆G∗ graph IR’s type system is sound with respect to the dependency-checking operationalsemantics. We only state the theorems here, their proofs can be found in [Bračevac et al. 2023]:
Theorem 3.2 (Progress). If [Σ | ∅] dom(Σ) ⊢ 𝑧.𝑔 •𝛿 : 𝑇 𝑞 𝜺, then either 𝑔 is a location ℓ ∈ dom(Σ),
or for any store 𝜎 where [Σ | ∅] dom(Σ) ⊢ 𝜎, there exists a graph term 𝑔′ , store 𝜎 ′ , and dependency 𝛿 ′such that 𝜎 | 𝑧.𝑔 • 𝛿 −→G 𝜎 ′ | 𝑧.𝑔′ • 𝛿 ′ .
Theorem 3.3 (Preservation).
[Σ | ∅] dom(Σ) ⊢ 𝑧.𝑔 • 𝛿 : 𝑇 𝑞 𝜺∃Σ′ ⊇ Σ. ∃𝑝 ⊆ dom(Σ′ \ Σ).

Σ | ∅ • ↦→𝑧.𝑧 ok[Σ′ | ∅]

dom(Σ′ )[Σ | ∅] dom(Σ) • ↦→𝑧 ⊢ 𝜎⊢ 𝑧.𝑔′ • 𝛿 ′ : 𝑇 𝑞,𝑝 𝜺, 𝑝

𝜎 | 𝑧.𝑔 • 𝛿 −→G 𝜎 ′ | 𝑧.𝑔′ • 𝛿 ′Σ′ | ∅ • ↦→𝑧.𝑧 ok′[Σ′ | ∅] dom(Σ ) • ↦→𝑧 ⊢ 𝜎 ′Corollary 3.4 (Dependency Safety). Evaluation respects the order of effect dependencies forwell-typed 𝜆G∗ terms, i.e., an operation is executed only if all its dependencies are resolved in the store.
Conclusion. Dependency synthesis is determined entirely by effect typing through modular
and local reasoning. Effect dependencies are term-level witnesses of type-level effects on reachable
variables in the program’s context. Well-typed graphs carry provably correct dependencies. They
have no direct operational meaning, but induce edges when viewing 𝜆G∗ terms as graphs, giving
localized insights into the program’s behavior exploitable by optimizations (Sections 5 and 6).
4

EXTENSIONS

4.1 Structured Expressions
Based on the treatment of 𝜆 abstractions in 𝜆G∗ , conditionals, loops, comprehensions, and otherstructured expressions/nodes become straightforward variations, e.g., we model conditionals as
nodes: 𝑛 ::= · · · | if (x) 𝑔 else 𝑔. Typing and effects for conditionals are standard:[Σ | Γ] 𝜑 • Δ ⊢ 𝑔:𝑇𝑞 𝜺x : Bool ∅ ∈ [Σ | Γ] 𝜑
[Σ | Γ] 𝜑 • Δ ⊢ 𝑔2 : 𝑇 𝑞 𝜺2 { 𝒈2 • 𝛿 2
1 { 𝒈1 • 𝛿 1

1𝜑[Σ | Γ] • Δ ⊢ if (x) 𝑔(if)
1 else 𝑔2 : 𝑇𝑞 𝜺

1 ∪ 𝜺2 { if (x) 𝒈1 else 𝒈2 • 𝛿 1 , 𝛿 2

Branches should have the same type and analogously the same reachability qualifier, which
can be mediated by subtyping. As with most effect systems, the branch effects are composed bya notion of join which is set union in our simple effect system, and that translates to sequential
composition of the branch dependencies in the output, by the properties of dependency calculation(Lemma 3.1).
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

236:14

4.2

Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf

Hard and Soft Dependency

In Section 2.2, we have discussed examples and optimizations enabled by distinguishing hard andsoft dependencies. During code generation, a node that is only soft-depended by other nodes is
considered dead, and therefore is not scheduled (cf. Section 6).
If node 𝐴 hard-depends on node 𝐵, then 𝐵 must be executed (or scheduled) before 𝐴. This is thedefault notion for the base 𝜆G∗ system (Section 3). In contrast, if 𝐴 soft-depends on 𝐵, then 𝐵 should
never be scheduled after 𝐴, but 𝐵 might not be scheduled even if 𝐴 is scheduled. The entire formal
system and reasoning principles of 𝜆G∗ carry over into a system with hard and soft dependencies
as presented in this section. The difference is the change in the effect and dependency structure,i.e., effects are split into reads and writes, which induce hard dependencies (the previous section’s
notion) and soft dependencies, respectively. This is a product composition of structures:
H, h
S, s

::=
::=

x ↦→ xx ↦→ xHard Dependencies
Soft Dependencies

Δ, 𝛿
𝜺

::=
::=

h; s
r:𝑞; w:𝑞

Dependencies
Effects

Hard dependencies h have the same structure as before (assign at most one dependency), whereas
soft dependencies s map variables to sets of variables. By overloading each dependency and effectoperator in the metatheory with versions acting on products, we can reuse the system in Figure 3
with minimal adjustments. Effectful primitives need to label their effects as read or write, i.e.,x : Alloc 𝑞 ∈ [Σ | Γ] 𝜑y : 𝐵 ∅ ∈ [Σ | Γ] 𝜑

[Σ | Γ] 𝜑 • Δ ⊢ ref x y : (Ref 𝐵) ∅ r(x) { ref x y • Δ| r(x)∗({-ref)x : (Ref 𝐵) 𝑞 ∈ [Σ | Γ] 𝜑
[Σ | Γ] 𝜑 • Δ ⊢ ! x : 𝐵 ∅ r(x) { ! x • Δ| r(x)∗x : (Ref 𝐵) 𝑞 ∈ [Σ | Γ] 𝜑({-!)

y : 𝐵 ∅ ∈ [Σ | Γ] 𝜑

[Σ | Γ] 𝜑 • Δ ⊢ x B y : Unit ∅ w(x) { x B y • Δ| w(x)∗({-:=)

where r(𝑞) = (r : 𝑞 ; w : ∅) and w(𝑞) = (r : ∅ ; w : 𝑞). Allocations classify as a “read” on thecapability operand, dereferencing induces a read on the reference itself and its reachable aliases,
and assignment induces a write. Plus, updating the last uses Δ at let bindings and projecting the
local dependency from effects Δ| 𝜺 need changing, to implement the informal policy on read andwrite effects motivated in Section 2.4. We use the hard dependency in Δ to track the last write ofany variable/location in context, whereas its soft dependency tracks all the reads on a variable
since it was last written.
Projections need to merge the hard dependencies of a write effect into its soft dependencies, andproject the hard dependencies for reads, i.e., (h; s)| (r:𝑞 ; w:𝑝 ) := (h|𝑞 ; h|𝑝 ⊔ s|𝑝 ).
Last-use updates at let bindings need to reset the recorded last reads for any written variable,
and add the bound variable to the last reads for any written variable, i.e.,(h; s) ⊕𝑥 (r : 𝑞 ; w : 𝑝) := (h, (𝑝, 𝑥) ↦→ 𝑥 ; (s, (𝑝, 𝑥) ↦→ ∅) ⊕𝑥 𝑞),
where 𝑥 is the let-bound variable and s ⊕𝑥 𝑞 := s, {𝑦 ↦→ s(𝑦), 𝑥 | 𝑦 ∈ 𝑞}.
In future work, we would like to develop a generic theory of graph IRs that is parametric in such
effect and dependency structures. Bao et al. [2021]’s direct style system already proposes one halfof the solution by adopting Gordon [2021]’s effect quantales. While we present a specific instance,
nothing prevents a graph IR definition that is parametric in such structures.
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

Graph IRs for Impure Higher-Order Languages

236:15

def Tensor(shape: Seq, f: Int => Int): Tensor = {val builder = mkTensorBuilder(shape)
val lp = forLoop(shape, i => builderAdd(builder, i, f(i)))
builderRes(builder)}/ {builder ↦→ builder}/ {builder ↦→ lp}(a) The Tensor DSL internally uses mutable builders. The forLoop IR node named lp induces a corresponding
dependency on the builder object. Sum is defined similarly.
def mkTensorBuilder: Seq
def builderAdd: (bld:TensorBuilder)def builderRes: (bld:TensorBuilder)def mkSumBuilder: Int
def sumBuilderAdd : (sbld:SumBuilder)def sumBuilderRes : (sbld:SumBuilder)=> TensorBuilder=> Int => Int => Unit=> Tensor=> SumBuilder=> Int => Int => Unit=> Sum@rd(world)@wr(bld)@kl(bld) @rd(bld)@rd(world)@wr(sbld)@kl(sbld) @rd(sbld)(b) Builder APIs annotated with read/write/kill effects. The destructive “kill” effect (kl, cf. Section 4.3) onbuilderRes and sumBuilderRes signifies that the builder objects are frozen and can no longer be mutated.
Fig. 5. Builder and Tensor APIs.

4.3

Tracking Typestate with Destructive “Kill” Effects

In addition to read/write effects, we can further add destructive “kill” effects as sketched in Bao
et al. [2021]. They can model memory deallocation, ownership transfer, and move semantics. In thecontext of our graph IR, the type system prevents any further dependencies on a killed node. Thisis exemplified in a snippet using the tensor DSL in Figure 5b, where converting a mutable builder
object bld into an immutable result tensor via builderRes(bld) induces the kill effect to disable any
further mutation:
val t1: Tensor = builderRes(bld)/ @kl(bld) {bld ↦→ ...}
forLoop(Seq(100), i => builderAdd(bld, i, 1+2*i)) /* error */The attempt to mutate the tensor builder using builderAdd would not type check, since the write effecton bld induced by builderAdd introduces a dependency to the killed bld. In practice, the DSL developer
needs to properly annotate the kill effects on operations in the DSL of interest. In Section 7.1, we
present a case study of loop fusion using an extended set of tensor APIs with these effects.
5

GRAPH-LEVEL OPTIMIZATIONSIn this section, we examine optimizations that rewrite or transform the dependency structure. We
first study domain-agnostic equational transformation rules over the graph IR that justify the latercode motion and generic optimizations. Then we discuss how to realize several optimizations forhigher-order programs.
5.1

Equational Theory

Figure 6 shows equational rules for 𝜆G∗ with soft and hard dependencies (Section 4.2) specifying anequivalence over graph-IR programs.
The first two rules (comm) and (𝜆-hoist) correspond to code motion. Rule (comm) permits
reordering of two consecutive let-bindings, as long as the second binding has no data/hard/soft
dependency on the first. Rule (𝜆-hoist) permits hoisting a node or nested graph 𝑏 out of the bodyof a function into its outer scope. Since a function’s effects are latent, hoisting is only permissible if
𝑏 is pure. One can determine purity by simply checking that hard and soft dependencies are absent,
since dependency synthesis always results in non-empty dependency mappings for effectful terms.
Furthermore, there should be no data dependency on nodes that are locally bound in the function,i.e., no locally bound variable in the context of the function body appears free in 𝑏.
Other rules allow us to shrink the program in a semantics-preserving way. The dead-code
elimination rule (dce) just needs to determine the absence of downstream data dependencies(𝑥 ∉ fv(𝑔)), and no hard dependencies (𝑥 ∉ FHD(𝑔)). In that case, any soft dependency of theProc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

236:16

Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf

𝐶 ::= □ | let 𝑥 = 𝐶 • 𝛿 in 𝑔 | let 𝑥 = (𝜆𝑦.𝐶 • 𝛿) • 𝛿 in 𝑔 | let 𝑥 = 𝑏 • 𝛿 in 𝐶
(comm)𝑥 ∉ FV(𝑏 2 ) ∪ dom(h′ ) ∪ dom(s′ ) ∪ cod(h′ ) ∪ cod(h′ )dom(h) ∩ dom(h′ ) = dom(s) ∩ dom(s′ ) = ∅𝐶 [ let 𝑥 = 𝑏 1 • h; s in let 𝑦 = 𝑏 2 • h′ ; s′ in 𝑔] ≡ 𝐶 [ let 𝑥 = 𝑏 2 • h′ ; s′ in let 𝑦 = 𝑏 1 • h; s in 𝑔](𝜆-hoist)
fv(𝑏) ∩ (BV(𝐶 2 ) ∪ {𝑥 }) = ∅𝐶 1 [ let 𝑓 = 𝜆𝑥 .𝐶 2 [ let 𝑦 = 𝑏 • ∅; ∅ in 𝑔1 ] in 𝑔2 ] ≡ 𝐶 1 [ let 𝑦 = 𝑏 • ∅; ∅ in let 𝑓 = 𝜆𝑥 .𝐶 2 [ 𝑔1 ] in 𝑔2 ](dce)
𝑥 ∉ fv(𝑔)(cse)𝐶 [ let 𝑥 = 𝑏 • ∅; ∅ in let 𝑦 = 𝑏 • ∅; ∅ in 𝑔 ]≡ 𝐶 [ let 𝑥 = 𝑏 • ∅; ∅ in 𝑔[𝑦/𝑥] ]𝑥 ∉ FHD(𝑔)𝐶 [ let 𝑥 = 𝑏 • h; s in 𝑔 ] ≡ 𝐶 [ 𝑔[𝑥 { s] ](e-cse)𝑏 is idempotent
𝐶 [ let 𝑥 = 𝑏 • h; s in let 𝑦 = 𝑏 • h; s in 𝑔 ] ≡ 𝐶 [ let 𝑥 = 𝑏 • h; s in 𝑔[𝑦/𝑥] ]
.
..
x
y

≡

..
.

f x

y

y

y

f x

x

..
.

u

v

...

b

≡

..
.

u

...

b

a

v

a

x

≡

a

..
.
x:t

y:t

n

m

≡

..
.

..
.

x:t

x:t

y:t

n

m

..
.

≡

x:t

b

..
.

..
.

(a) COMM

𝜆 •(•).•/•𝜆 •(•).•/•(b) 𝜆-HOIST

y

...

z

y

(c) DCE

...

z

n

m

(d) CSEnm(e) E-CSE

Fig. 6. Equational rules and their visualizations for 𝜆G∗ with hard and soft dependencies. Black thick edges
represent either a data, hard, or soft dependency.

eliminated binding has to be rewired downstream to maintain consistency. This rule is powerful in
combination with soft dependencies, and can optimize memory access patterns such as write-afterwrite (Section 2.2). In general compilers, we need a termination analysis to apply DCE, which weomit here in the context of DSLs. The common subexpression elimination rule (cse) removes pure
expressions if the same expression has been defined previously. Additionally, effectful redundant
expressions can be removed if the node/subgraph 𝑏 is idempotent (e-cse), e.g., consecutively readinga reference twice (Section 2.2).
Soundness. We apply the logical type soundness approach [Timany et al. 2022] to support
relational reasoning about contextual equivalence of two programs in the direct-style type-andeffect system 𝜆𝜀∗ ([Bračevac et al. 2023] Sec. 7). We build on a framework for modeling reachability
types with logical relations by Bao et al. [2023].
A key insight is that the proof based on logical relations in the direct-style calculus is sufficient
to argue for contextual equivalence in MNF (supplement Sec. 8) because: (1) MNF is a sublanguageof the direct-style language, and (2) dependencies are entirely determined by effects (Lemma 3.1).
Effect dependencies have no operational meaning beyond asserting that they respect the observed
call-by-value evaluation order of effects (Corollary 3.4). Therefore, we can appeal to the logicalrelations for 𝜆𝜀∗ by dependency erasure and re-synthesis to derive their counterparts for 𝜆G∗ .
We have proved contextual equivalence of the rules in Figure 6 restricted to only hard dependencies. This restriction does not impact most rules in a major way, except for (dce), which requires
forbidding any mention of 𝑥 in the rest of the program 𝑔. To prove contextual equivalence of thefull (dce), the logical relation needs to be extended to support read/write effects, and consequently
soft dependencies. We leave the proofs for 𝜆G∗ with hard/soft dependency as future work.
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

Graph IRs for Impure Higher-Order Languages

5.2

236:17Higher-Order Program Optimizations

Our graph IR enables useful and efficient higher-order optimizations purely from local reasoning
with dependencies and its support for lexical structure. Even without using costly higher-order
flow and environment analyses [Might 2007; Shivers 1988], our graph-based transformations are
already useful for eliminating higher-order functions. Additional fixed-point based analyses could
be integrated to enable more aggressive optimizations.
Lambda Lifting. Lambda lifting [Johnsson 1985] transforms nested functions into top-level
functions, where free variables captured by the function are replaced with newly added function
parameters. Call-sites are also transformed to pass the extra arguments. This avoids creatingclosures at run time, e.g.,// before lambda lifting:def f(x: Int): Int =def g(y: Int): Int = x + y // closureg(42)// after lambda lifting:def g(y: Int, x': Int): Int = x' + y // g lifteddef f(x: Int): Int =g(42, x) // no closure

There are two possible ways to realize lambda lifting in the graph IR: (1) post-scheduling, i.e., first
convert the graph back into a tree (cf. Section 6), which explicates lexical scope, and then apply
classic lambda lifting algorithms. In this way, the resulting program depends on the downstreamscheduling algorithm which decides the scope structure of programs. (2) pre-scheduling, i.e., directlytransform the graph representation before scheduling a tree representation, discussed below:
We compute the set of extra parameters using graph dependencies [Danvy and Schultz 2004;
Leißa et al. 2015; Morazán and Schultz 2007] and express lambda lifting by graph rewriting:• The dependencies to scope-sensitive variables are rewired to the newly introduced parameters.
• Call-sites are transformed to introduce explicit dependencies to lexically scoped variables.
After that, we must instruct the later code motion algorithm (cf. Section 6) to lift functions without
local dependencies to the top level, i.e., those functions should not have a parent scope. Using agraph structure to compute the set of extra parameters also exhibits better asymptotic complexity[Morazán and Schultz 2007] compared to Johnsson’s equation-based algorithm.
Similar to lambda lifting, with additional support of data structures, we can also implement
closure conversion as a graph transformation.
Super-Beta Inlining. Super-𝛽 inlining [Shivers 1991] is an aggressive form of higher-orderfunction inlining across abstraction boundaries, traditionally driven by expensive control-flow
analysis (CFA) [Midtgaard 2012; Shivers 1988, 1991] and environment analysis [Might 2007]. Ourgraph IR does not directly answer global control-flow questions or track the dynamic environment
component of closure values. However, a subset of super-𝛽 inlining can be viewed as a combinationof lambda dropping [Danvy and Schultz 2000] (i.e., the inverse of lambda lifting) and local function
inlining. We show that by taking advantage of the sparsity and locality of graph dependencies, ourgraph IR can already enable super-𝛽 inlining in many cases.
Consider the tail-recursive factorial function written in continuation-passing style (adapted from
Might [2007]). We invoke fact with a continuation that prints the final result.
// before super-𝛽 inlining:def fact[T](n: Int, acc: Int, k: Int => T) =if (n == 0)// after super-𝛽 inlining:def fact[T](n: Int, acc: Int) =if (n == 0)k(acc)

else fact(n - 1, acc * n, k)fact(x, 1, res => println(res))println(acc)else fact(n - 1, acc * n)fact(x, 1)

The highlighted call of k in the body (left) is a super-𝛽 inlinable call-site. In our IR, we immediately
know that fact is called with a continuation, connected by a data-dependency edge. This continuation function as a closure shares no variables with fact from the environment. Moreover, allProc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

236:18

Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf

recursive calls to fact in its body have the same continuation argument k. These facts are enoughto establish the safety condition to perform super-𝛽 inlining in this case. Moreover, they can be
identified without relying on any fix-point analysis but inspecting the graph locally. After super-𝛽
inlining, the call-site of k is replaced with the continuation body. Furthermore, the argument k
becomes useless and is therefore eliminated. To summarize, the resulting program can be obtainedby first dropping the continuation function into the scope of fact and then inlining the function.
Beyond Graph Transformation. We have explored optimizations based on local graph rewritingor transformations, which are practical and cost-effective. However, powerful (and expensive)
analyses based on fixed-point iteration can also be implemented on our IR. For instance, super-𝛽
inlining typically requires sophisticated environment and flow analyses. Implementing a global CFA
on the graph IR would be more efficient compared to tree-like IRs. Instead of iteratively traversing
tree-like ASTs and propagating information, we can directly update the graph and leverage its
sparsity and locality for information propagation.
6

FROM GRAPHS BACK TO TREESThis section covers efficient algorithms and heuristics for code generation, transforming 𝜆G∗ graphs
into trees. These algorithms refine the optimizations presented in Section 5. We discuss the basicscheduling algorithm with dead code elimination (Section 6.1), a lightweight frequency estimation
heuristic for code motion (Section 6.2), and a compact scheduling algorithm for instruction selectionand expression inlining (Section 6.3).
6.1

Basic Scheduling Algorithm with Dead Code Elimination

The block scheduling algorithm traverses a hierarchy of graph-represented blocks based on dependencies and selects the nodes to build tree-represented blocks. Figure 7 shows the vanilla block
scheduling algorithm. Following the dependencies of the final result res, scheduleBlock partitions
the unscheduled nodes scope into two groups: (1) schedule in the current block, and (2) schedule
into some inner block. This process is recursively applied when encountering lambda nodes intraverseNode. Scheduling decisions rely on two properties over nodes, available and reachable:
Nested Scopes. A node is available if all its dependent bound variables have been introduced
under the current path. This is the set of accumulated bound variables (e.g., introduced by lambdas)
down to the current block. We schedule a node in the current block if it is both reachable andavailable; otherwise, it is deferred to some inner block. Consequently, we need to transitively
compute the bound variables depended upon by nodes, which is performed by boundDeps. Both pathand scope need to be maintained through recursive calls to properly handle blocks and nested scopes.
Dead Code Elimination. A node is reachable if it can be traced back from the current result
node through effect or data dependencies. Only reachable nodes are scheduled, which naturally
eliminates dead code (cf. the dce rule in Figure 6). In Figure 7, reachable is implemented as apriority queue (reachable) to keep track of reachable nodes in topological order, populated withdata and effect dependencies during the iteration. As an extension, we discern soft dependencies(Section 4.2) and identify data and hard dependencies as reachableHard . This ensures nodes that are
only reachable via soft dependencies can be eliminated.
Complexity. Given the total number of nodes 𝑛 and the maximal depth of nested scopes 𝑘, theworst-case asymptotic time complexity is 𝑂 (𝑘𝑛 2 ). This is because the algorithm traverses over thereachable nodes in order (𝑂 (𝑛) each), and repeats this process for nested scopes. In practice, thecomplexity is 𝑂 (𝑘𝑛 log 𝑛) due to the decreasing size of nested scopes and the limited degrees ofgraph nodes. For example, our symbolic-execution compiler (Section 7.2) based on the graph IR
schedules 548,976 nodes within 19.3 sec, which is rather efficient.
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

Graph IRs for Impure Higher-Order Languages

236:19/* auxiliary functions to access different sorts of dependencies of a nodeboundDeps: dependencies that are bound variables
dataDeps, effDeps: data- and effect-dependencies
hardDeps ( ⊆ effDeps): hard effect-dependencies */val boundDeps, dataDeps, effDeps, hardDeps : Node => Set[Node]/* obtain estimated frequencies of data-/effect-dependencies of a node: */val depFreq: Node => Map[Node, Double]/* traverse a single node to emit a tree node */def traverseNode(inner: Set[Node], path: Set[Node], n: Node): TreeNode = n matchcase 𝜆 f(x).r =>// schedule nodes into a 𝜆 scope
TreeNode.Scope(𝜆 f(x), scheduleBlock(inner, path ∪ {f, x}, r))...
case "$sym := $op($args)" =>// schedule common nodes as leaves
TreeNode.Leaf(sym, Exp(op, args))/* schedule a block given its final result, producing a scoping tree */def scheduleBlock(scope: Set[Node], path: Set[Node], res: Node): List[TreeNode] =val reachable: PriorityQueue[Node] = {res}// reachable nodes, topologically orderedval reachableHard: Set[Node] = {res}// reachable nodes, required by data/hard deps.

val reachableHot: Set[Node] = {res}val current: List[Node] = ∅val inner:Set[Node] = ∅def available(n: Node): Boolean = boundDeps(n) ⊆ path// reachable nodes, frequently executed// scheduled in current block// scheduled in inner blocks// available: bound vars. in deps. are readyfor n ← reachable doif reachableHard(n) thenif reachableHot(n) ∧ available(n) thencurrent = n :: current
for m ← (dataDeps(n) ∪ effDeps(n)) ∩ scope do// reachable via data/hard dependencies// reachable via hot paths// consider deps. hot if freq > 0.5

if depFreq(n)[m] > 0.5 then reachableHot += {m}// only via cold path, or hot but unavailable

else
inner += {n}if reachableHot(n) then// deps. of unavailable hot nodes are still hot

reachableHot += (dataDeps(n) ∪ effDeps(n)) ∩ scope
reachableHard += (dataDeps(n) ∪ hardDeps(n)) ∩ scope
reachable += (dataDeps(n) ∪ effDeps(n)) ∩ scopefor n ← current yield traverseNode(inner, path, n)// reachable via data and only hard dependencies// reachable via data/effect dependencies// recursively build up the scoping tree

Fig. 7. The pseudocode of the basic scheduling algorithm with the extensions of dead code elimination (Section 6.1) and frequency estimation (Section 6.2). Function scheduleBlock decides which nodes are scheduled
into the current block and recursively schedules inner scopes. To generate code for a graph g, we invokescheduleBlock(g.nodes, ∅, g.result).

6.2

Code Motion with Frequency Estimation

Our basic scheduling algorithm eagerly schedules nodes into their outermost block, following theequational rules (comm) and (𝜆-hoist) in Figure 6. This is a form of code motion with no extra
effort and generally desirable for functions and loops. For instance, consider the following code:
List(1, 2, 3, 4, 5).map(x => x * factorial(N))

Lifting the expensive factorial out of the lambda is feasible since it does not depend on the boundvariable x. However, this does not guarantee generating optimal code. Consider a conditional
expression that transforms an array of complex numbers only in the then-branch,if (cnd) compNums.map(f) else compNums

Since compNums.map(f) has no dependency on the condition cnd, it would be lifted to the outer blockand always be executed, imposing unnecessary runtime overhead when the else-branch is taken.
To avoid this situation, we can statically estimate how frequently a node will be used at runtime
and move less frequent (“cold”) nodes into nested scopes. The results of functions and loops are
assigned frequency 100, indicating that they can be executed multiple times (definitely “hot”). The
results of conditional branches are assigned 0.5 (i.e., cold), assuming each branch is taken withequal probability. All other nodes are assigned 1.0 (i.e., normal). Numbers above are illustrative andProc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

236:20

Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf

context-insensitive. Alternative metrics are possible, while what we present here is beneficial tomost code patterns.
The teal parts in Figure 7 highlight the changes to the basic scheduling algorithm for frequency
estimation. Given a node which is to be scheduled in the current block, we use the function
depFreq to access the frequency estimation of its dependencies. Only those dependencies withfrequencies greater than 0.5 are considered hot-reachable, and thus can be included in current. Other
dependencies are classified as cold, and a node should be deferred to inner blocks if downstream
nodes depend on it only via cold dependencies. For a node which is to be scheduled in some inner
block, its dependencies are considered to have the same “temperature” as the node itself, ensuringconsistent code motion behavior for code with nested scopes.
Our approach is easier to implement and more efficient than sophisticated analyses, such as
lazy code motion [Knoop et al. 1992a], partial redundancy elimination [Kennedy et al. 1999], andwhole-program dataflow analyses. The heuristic associates a constant factor to each traversed node,
keeping the scheduling algorithm’s complexity unchanged.
6.3

Instruction Selection with Compact Traversal

The basic scheduling algorithm binds every intermediate expression, which is not only verbose but
also suboptimal without considering the target-specific primitives. Consider the following tensor
computation snippet,
val X = Matmul(A, B); val C = Add(C, X); C

The unique use of X in Add enables destination-passing style using generalized matrix multiplication
GEMM, which updates C in-place by 𝐶 ← 𝛼𝐴𝐵 + 𝛽𝐶. Thus, we can match the tree structure Add(C,Matmul(A, B)) and generate a single operation, eliminating the intermediate multiplication X:
GEMM(A, B, C, alpha=1.0, beta=1.0); C

This is a form of instruction selection as seen in optimizing compilers. However, it is non-trivial
on computation graphs where all consumers of a value need consideration. While LLVM’s SelectionDAG algorithm [Lattner and Adve 2004] offers a comprehensive solution, our graph IR employs
a simpler, efficient alternative: compact traversal. It converts graph nodes into inlined trees whenpossible, then selects the best primitive using tree-matching algorithms (e.g., maximal munch)while respecting dependencies to preserve the semantics. Consider the following code where inc(x)has an effect dependency on node y, although y is used only once.
if (cond) { val y = !x; inc(x); println(y) }Therefore, inlining y to println breaks the semantics, and our algorithm correctly avoids generating
inlined code for such cases.
Compact traversal works on each current block determined by the basic scheduling algorithm(Figure 7). Initially, all nodes in the block are viewed as individual trees. Three steps are then taken
to build them into a list of inlined trees ready for pattern matching and code emission. We document
the complete pseudocode in the supplementary material [Bračevac et al. 2023].
(1) Track Node Usage. The core concept of compact traversal is to consider inlining only fornodes that are locally defined, used exactly once, and not used in nested scopes. We identify inlining
candidate nodes by tracking local definitions and node usages in the current and inner blocks.
(2) Compute Local Successors. After recording node usage information, we calculate local
successors of a node within the current block. Node 𝑥 is a local successor of node 𝑦 if they arescheduled in the same block and 𝑥 depends on 𝑦. A map is used to store local successors of nodes.
(3) Check Inlining. Finally, the algorithm runs a backward pass for all inlinable nodes, checking
if all successors are emitted after the potential inlining point. If not, inlining the current node isdisabled; otherwise, it is inlined and any node it uses is checked for inlinability.
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

Graph IRs for Impure Higher-Order Languages

236:21

Summary. We demonstrated various optimizations achievable with simple, efficient algorithms
through scheduling graphs back to nested tree representations. Additional optimizations can befurther incorporated, e.g., to exploit instruction-level parallelism, we could use node priority values
reflecting the dependency and timing to perform instruction scheduling. In summary, our graph IR
serves as an efficient and flexible bedrock for generating high-performance code.
7

CASE STUDIESIn this section, we demonstrate optimizations enabled by our approach and evaluate its performance
empirically. We implemented our graph IR in LMS [Rompf and Odersky 2010; Rompf et al. 2013], acompiler framework embedded in Scala. LMS evaluates DSL expressions into the graph IR using
normalization by evaluation [Rompf 2016]. The modified LMS allows DSL authors to annotate
effects for each operation (e.g., Figure 5b), while dependencies are resolved automatically.
7.1

Fusing Tensor Computations on CPU/GPU

In Section 2, we discussed the interaction between loop-fusion transformations and effect dependencies. Here, we present more sophisticated case studies applying loop fusion and kernel fusion
based on graph dependencies to tensor computations on CPUs and GPUs. Consider the mean andvariance in a functional tensor DSL (Figure 5a):def square(d: Int)= d * ddef mean(t: Tensor)= Sum(Seq(t.size), { i => t(i) }) / t.size
def variance(t: Tensor) = Sum(Seq(t.size), { i => square(t(i)) }) / t.size - square(mean(t))

The Tensor and Sum forms are constructors for creating tensors and summations, respectively. Under
the hood, these types represent the computations as loops. Say we computed the mean and varianceof an affine tensor, obtained by pointwise addition of the tensors constant and linear:val constant = Tensor(Seq(100), { i => 1 })val linear= Tensor(Seq(100), { i => 2*i })val affine= Tensor(Seq(100), { i => constant(i) + linear(i) })println(mean(affine))
println(variance(affine))

A compiler without fusion would generate six loops for this program. Utilizing the dependency
information from our graph IR, we can efficiently fuse these loops. In this example, the Tensor
and Sum constructors internally use mutable builder objects during construction, as shown in thedefinitions (Figures 5a and 5b), which greatly reduces the number of fusion rules needed for programtransformations.
Dependency-Guided Fusion. Following Rompf et al. [2013], we consider two fusion types:(1) horizontal fusion, combining loops with the same range, and (2) vertical fusion, fusing data
producers with consumers. To apply fusion, note that the initialization of affine consumes datafrom constant and linear at the same loop index. By applying vertical loop fusion, affine directly
uses this data, eliminating the need for materializing the constant/linear tensor. The resulting loop
representation for computing affine is:
forLoop(Seq(100), i => builderAdd(affBld, i, 1+2∗i)) /* def. for builder affBld omitted */The tensor affine is consumed by the downstream println calls taking three Sum loops introducedby mean/variance. Applying the same vertical fusion transformation, we can continue fusing affine
into its three consumers (i.e., summing loops) and obtain the following code (there are two loops
performing the same computation since variance also calls mean):
forLoop(Seq(100), i => sumBuilderAdd(sumBld1, i, 1 + 2 * i))
forLoop(Seq(100), i => sumBuilderAdd(sumBld2, i, 1 + 2 * i))
forLoop(Seq(100), i => val t = 1 + 2 * i; sumBuilderAdd(sumBld3, i, t * t))

Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

1

Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf

w/ opt
35
30
25
20
15
10
5
0

w/o opten s
nce odmp
rod rEvria
Su
r/Va −PtP DotP mSq 5−Ma inear
2L
3− −Su
6−
4

No.
1
2
3
4
5
6

w/opt
w/o opt
speedupmean std mean std
1.09 1.01 21.0 2.05
19.3
1.79 1.41 27.2 1.45
15.2
0.89 1.04 17.2 1.08
19.3
1.50 1.10 17.4 1.06
11.6
1.09 1.01 21.9 2.89
20.1
0.81 0.97 17.2 1.04
21.2

Running time (ms)Running time (ms)236:22w/ opt
40
30
20
10
0

No.
1
2
3
4

adi

ean
−M

w/o opt

sc
Ca

1−

w/opt
w/o opt
speedupmean std mean std
14.8 0.83 28.2 2.09
1.9
15.4 0.86 29.2 2.50
1.9
15.1 0.46 27.9 1.96
1.8
15.0 0.53 39.7 3.27
2.6

dd
ats
at2
lu
ngA Conc
onc
Re
litC −Add
lit
Sp
Sp
4
3−
2−

(a) Loop fusion of tensor computations.
(b) CUDA kernel fusion with code motion.
Fig. 8. Empirical evaluation of (a) loop fusion and (b) kernel fusion. Bar charts show the median of runningtimes (ms) where whiskers are max/min of samples. Tables show mean and std of the same sample set.

The identical index range of the loops suggests horizontal fusion is possible, but care must be
taken regarding effectful operations, such as destructive mutations via sumBuilderAdd. By analyzing
dependency information in the graph IR, we can tell that builders are separate and loops are
independent, allowing fusion into a single loop. After applying additional lowering transformations,the compiler generates an optimal single-loop program.
CUDA Kernel Fusion. Kernel fusion is another case utilizing dependency information for highlevel optimization. Kernels, executed by GPUs, process tensor inputs and outputs. Naive CUDA
backends in ML compilers may generate excessive intermediate results in the GPU’s global memory,
reducing throughput and efficiency. Kernel fusion [Filipovič et al. 2015] vertically combines asequence of kernels into one, improving performance. We extend the AIRCop compiler [Wanget al. 2019a] on top of our graph IR with kernel fusion and other optimizations (e.g., DCE and CSE).
Consider the following tensor program:it w split
spl
val in1 = Input(Seq(100,100), "input1.data")
val in2 = Input(Seq(100,100), "input2.data")
val w = Tensor(Seq(100,100))
val a = in1 * w
val b = in2 * aprint(b)

w0

w1

spl

cat

it

co
a spli

a1
∗in2

∗in2
ca

t
ca

n

t

co

b1

it

w

spl

it

w0

⇒

t

a0
b0 co
n

spl

∗in1
t a1
nca

∗in1

a0 con

a0

a1
∗in2

∗in2

b0 co
nc

at

nc

at

co

w

it

spl

w1
∗in1

∗in1

spl
i

t

w0

w1

⇒ b c

b1

∗in1 ∗in2∗in1 ∗in2

0

on

ca

nc

co

t

b
at 1

b

b

b

When executing a program on a two-GPU cluster, the weight tensor w can be split and scatteredacross the cluster, using model parallelism. Dependency analysis shows that the intermediate resulta, generated by the first multiplication, is only consumed by the second multiplication. Therefore, tensor a can remain distributed during execution. Kernel fusion combines the two matrix
multiplications, eliminating intermediate results and leading to the optimized dataflow to the right.
Kernel fusion is also used to generate low-level CUDA code for conserving memory in distributedmodel training, by scattering weight gradients across the cluster. The following snippet demonstrates this transformation through kernel fusion. Before t is accumulated, it is collected from otherGPUs’ transient memory using a sequence of add kernels:recv(GPU1, w1, GPU2, w2, GPU3, w3);
cudaMalloc(t1); cudaMalloc(t2);add(t1, w0, w1); add(t2, w2, w3); add(t, t1, t2);
accumulate(t);⇒recv(GPU1, w1, GPU2, w2, GPU3, w3);
addAccumulate(t, w0, w1, w2, w3);

After fusion (right), these add kernels and accumulate kernel are fused into a single one, eliminatingintermediate tensors t1 and t2 which saves memory.
Empirical Evaluation. Figure 8a compares the performance of low-level Scala code with andwithout loop fusion on benchmarks, including the mean/variance example. Using arrays of 106
elements, each benchmark runs 20 times, reporting median/min/max in the bar chart and mean/std
in the table. The large std numbers result from JVM warmup. Our fusion algorithm successfully
combines multiple loops, with fused programs running up to 21x faster than those without fusion.
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

Graph IRs for Impure Higher-Order Languages

236:23Figure 8b compares the execution time of CUDA kernel programs with and without fusion, using
an input size of 300,000 on two NVIDIA GeForce GTX 1080 GPUs. Kernel fusion with code motion
enhances tensor benchmark performance by 1.5x to 2x on average.
7.2

Symbolic-Execution Compiler

Wei et al. [2020, 2023b, 2021] introduce a symbolic-execution (SE) compiler framework built using
LMS. It converts LLVM IR programs into C++ files for SE. The artifact generates purely functional,
easily parallelizable code with domain-specific optimizations for LLVM’s symbolic semantics.
Due to purity and persistence, only data dependencies exist, simplifying the implementation of
optimizations, but potentially negatively impacting single-thread execution performance.
In this case study, we refactor their artifact to generate effectful code with in-place updates,
reducing intermediate structures. In-place operations are effect-annotated, enabling LMS to generate
an effectful IR graph with dependencies. We then apply effect-aware graph rewriting to reproduce
their optimizations and evaluate their effectiveness.
Effect-aware Rewriting and Optimizations. We identify interesting optimizations in the original artifact requiring effect-aware rewriting after refactoring, such as register assignment/lookup
elimination and stack allocation aggregation. Local and effect-free expression simplification is also
important but less relevant to this case study. We use register lookup elimination as an example.
In LLVM IR, local variables within function scope are called “virtual registers” and will be assigned
only once. For example, the following code snippet is the compiled program corresponding to an
LLVM program that assigns register x with value v and then later looks up this register x:
val _ = s.assign(x, v) /* write effect over s.x, where s is a symbolic state */...
/* other effectful operations over s */val t = s.lookup(x)/* read effect over s.x */...
/* later code uses lookup result t */The compiled program operates on a symbolic state s. The unnecessary lookup can be eliminatedsince x is assigned once and its value is locally known. Rewriting the program binds t to v. In
the graph representation, an effect dependency connects the lookup and assign nodes, with lookup
inducing a read effect on s.x and assign inducing a write effect on s.x. The assigned value is foundby locating the last write over s.x and performing substitution on downstream computations, i.e.,in the formal notations from Sections 3 and 5.1:
𝐶 1 [let 𝑛 = 𝑠.assign(𝑥, 𝑣) • h; s in 𝐶 2 [let 𝑦 = 𝑠.lookup(𝑥) • {𝑠.𝑥 ↦→ 𝑛}; s in 𝑔]] ≡𝐶 1 [let 𝑛 = 𝑠.assign(𝑥, 𝑣) • h; s in 𝐶 2 [𝑔[𝑦 { {𝑠.𝑥 ↦→ 𝑛}; s] [𝑣/𝑦]]]After exhaustive elimination of lookups, the corresponding assignments become dead code and will
also be removed during code scheduling.
Experiment. We compare the refactored (Imp) and original (Pure) SE compiler with and without
the optimizations. We record the sizes of generated programs and their running times, which are
divided into solver time and execution time. Each task is repeated 10 times. We use a downstream
C++ compiler g++ 9.2.0 with O3, SMT solver STP, and JDK 8, running on a machine with 4 Xeon 8168
CPUs and 3TB memory.
Empirical Evaluation: Imp w/ opt vs. Imp w/o opt. Figure 9 shows the result of 6 benchmarks.
We first observe that the generated C++ programs are more compact (21.49% smaller on avg.), since
optimizations lead to constructing a smaller graph and program.
Symbolic execution workloads often spend most execution time on constraint solving by an external solver. Compile-time rewriting of symbolic expressions can improve solver-side performance.
For example, KMP considerably benefits from eliminating unnecessary bit-vector extensions.
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

236:24

Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf

Exec. time (s)Imp − w/ opt
0.6

0.4
0.3
0.1
0.0

Imp
Bubble
Sort
Pure
Imp
KMP
Pure
Imp
Knapsack
Pure

0.9

0.4

0.6

0.2

0.2

0.3

0.0

0.0

0.0

bubbleSort

kmp

LOC

Solver Time (s)
mean
std
21.71
0.03
21.42
0.02
21.65
0.04
21.43
0.008
4.11
0.006
8.32
0.03
4.31
0.01
8.37
0.01
126.010.06
130.530.07
134.972.29
129.960.07

Benchmarkw/ optw/o opt
w/ optw/o opt
w/ optw/o opt
w/ optw/o opt
w/ optw/o opt
w/ optw/o opt

198
259
195
241
399
504
400
486
288
360
257
314

Pure − w/ opt

knapsack
Exec. Time (s)mean std speedup
0.24 0.003
1.9
0.26 0.003
1.8
0.27 0.004
1.6
0.45 0.004
1.0
0.33
0.01
1.7
0.41
0.01
1.4
0.38
0.02
1.5
0.57
0.02
1.0
0.35 0.008
2.1
0.41 0.008
1.8
0.51 0.009
1.4
0.73 0.009
1.0

Pure − w/o opt
12
10
8
6
4
2
0

1.2

0.6
0.4

0.2

Imp − w/o opt
0.8

2.0
1.5
1.0
0.5
0.0

mergeSort

nqueenBenchmarkLOC

w/ optw/o opt
w/ optPure
w/o opt
w/ optImp
w/o opt
w/ optPure
w/o opt
w/ optImp
w/o opt
w/ optPure
w/o opt
Imp

Merge
Sort

NQueen

Quick
Sort

459
634
448
582
564
678
563
656
237
297
229
276

quicksort

Solver Time (s)Exec. Time (s)meanstdmean std speedup
47.22
0.03
0.52 0.02
2.2
46.93
0.02
0.83 0.02
1.4
47.82
0.13
0.63 0.02
1.9
47.82
0.05
1.17 0.02
1.0
2.56
0.004
3.93 0.01
3.1
2.57
0.003
4.32 0.01
2.7
3.04
0.02
6.48 0.02
1.8
3.58
0.005
11.81 0.02
1.0
89.93
0.04
1.14 0.02
1.9
90.13
0.19
1.31 0.02
1.7
90.82
0.06
1.49 0.02
1.5
90.42
0.03
2.17 0.02
1.0

Fig. 9. Empirical evaluation: Graph IR optimizations on a symbolic-execution compiler. Bar charts show theexecution time for each benchmark and engine configurations. Table reports the size of the generated code
(LOC), solver running time, execution time, and speedups of execution times (baseline is “Pure w/o opt”).
SELECT SUM(l_extendedprice*l_discount)
FROM lineitem
WHERE l_shipdate >= '1994-01-01'
AND l_shipdate < '1995-01-01'
AND l_discount between 0.05 and 0.07
AND l_quantity < 24.

(b) ColumnarBuffer insert implementation in LB2.

(a) TPC-H Query 6.
int main() {/* allocating memory for columns */int* l_orderkey_buf = (int *) malloc(init_size);
int* l_partkey_buf = (int *) malloc(init_size);... (10 other unused columns)
int* l_shipdate_buf = (int *) malloc(init_size);
double* l_discount_buf = (double *) malloc(...);... (2 other used columns)
while (/* end of source file */) {/* parse the data and insert to buffers */// parse l_orderkey (omitted)
l_orderkey_buf[pos] = new_l_orderkey;// parse l_partkey (omitted)
l_partkey_buf[pos] = new_partkey;... (10 other unused columns)

class ColumnarBuffer(schema: Schema, columns: Map[String, Column], /* elided */) {def insert(rec: Record) =schema map { field =>// enumerate table fields
val column = columns(field.name) // get the column for the fieldcolumn.insert(rec(field.name))// insert the new value}}// parse l_shipdate (omitted)
l_shipdate_buf[pos] = new_shipdate;// parse l_discount (omitted)
l_discount_buf[pos] = new_discount;... (other 2 used columns)/* resize the buffers if full */if (/* buffer is full */) {l_orderkey_buf = (int *) realloc(l_orderkey_buf, new_size);l_partkey_buf = (int *) realloc(l_partkey_buf, new_size);... (resize other 10 unused columnar buffers)
l_shipdate_buf = (int *) realloc(l_shipdate_buf, new_size);l_discount_buf = (double *) realloc(l_discount_buf, new_size);... (resize other 2 used columnar buffers)}/* rest of the query */}(c) Code generated by LB2 for TPC-H Query 6.
Fig. 10. The DCE pass on our graph IR eliminates unused columns (red lines) altogether which generalpurpose compilers (e.g., GCC -O3) are incapable of.

Execution time (i.e., total time minus solver time) is not prominent in most cases due to utilizing inplace updates and avoiding copying. Our graph-IR optimizations still yield significant improvements.
On average, the optimized Imp version is 16.95% faster than the non-optimized version. These
speedups demonstrate the effectiveness of graph-based domain-specific optimizations, particularly
for workloads with dominant concrete execution, such as NQueen in Figure 9.
Empirical Evaluation: Imp vs. Pure. In Figure 9, we also assess the impact of transitioning
from persistent to imperative data structures, enabling effectful in-place updates. The unoptimized
imperative version is sometimes faster than the optimized pure version. When optimizations areenabled for both, the imperative version is 24.30% faster on average than the pure version, because
our optimizations eliminated the creation and storage of intermediate results.
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

Graph IRs for Impure Higher-Order Languages

236:25

Exec. time (s)40w/ optw/o opt

32
24
16
8
0
Q01 Q02 Q03 Q04 Q05 Q06 Q07 Q08 Q09 Q10 Q11 Q12 Q13 Q14 Q15 Q16 Q17 Q18 Q19 Q20 Q21 Q22Time (s)

Q1 Q2

Q3

Q4

Q5

Q6

Q7

Q8

Q9 Q10 Q11 Q12 Q13 Q14 Q15 Q16 Q17 Q18 Q19 Q20 Q21 Q22

w/ opt11.2 4.1 9.9 9.2 10.4 7.0 10.7 11.8 14.2 12.5
w/o opt 14.4 4.6 14.9 19.2 15.9 11.2 15.7 17.0 19.1 17.6
speedup 1.3 1.1 1.5 2.1 1.5 1.6 1.5 1.4 1.3 1.4

2.7 9.6
2.9 14.3
1.1 1.5

5.8 7.4 12.8
6.5 11.9 22.8
1.1 1.6 1.8

3.1 15.0 15.1 9.2 10.1 23.2
3.3 25.8 26.7 13.2 15.0 39.2
1.1 1.7 1.8 1.4 1.5 1.7

2.4
3.3
1.4

Fig. 11. Empirical evaluation of the effect of precise dependency tracking based DCE in graph IR. We run all
22 queries of the TPC-H Benchmark (Scale Factor = 10) with (and without) the DCE pass.

7.3

LB2: Relational Query Compiler

LB2 [Essertel et al. 2018; Rompf and Amin 2015; Tahboub et al. 2018] is a comprehensive SQL querycompiler built with LMS that achieves competitive performance compared to highly optimized
counterparts like HyPer [Neumann 2011]. One of the key optimizations enabled by our graphIR’s dependency tracking is a very precise DCE during code generation that cannot be achieved
with downstream general-purpose compilers (e.g., GCC -O3). The precise DCE prevents redundant
memory allocations, copying, etc., for attributes that are not used in a query.
In Query 6 (Figure 10a) from the TPC-H benchmark [TPC 1999], an aggregate is computedfor the lineitem relation based on specific constraints. The lineitem relation has 16 attributes,
but only four are used for the final result. The query plan includes data loading, filtering, and an
aggregation operator. Figure 10b presents an excerpt of the ColumnarBuffer type, storing tabledata in a columnar format with separate arrays for each column. These high-level abstractions
exist only in the library code and map to native C arrays in the compiled code.
The generic buffer abstraction is easy to use but lacks query-specific information, such as usedcolumns. Without precise DCE, the generated C code for Query 6 would unnecessarily allocate,reallocate, and copy memory for 12 unused columns in lineitem. The downstream compiler,
unaware of these high-level dependencies, cannot eliminate these unneeded operations.
Our graph IR precisely tracks dependencies, such as the creation and usage of individual columns
in each relation through effect and data dependencies. Columns needed for the final output havedata dependencies to the corresponding columnar arrays. Our DCE rule (Section 5.1) eliminates
unreachable columnar arrays, preventing them from being scheduled for code generation, as shownin the highlighted parts of Figure 10c.
Empirical Evaluation. We evaluate the effectiveness of precise DCE on large-scale realistic
queries from the TPC-H benchmark (Scale Factor 10), using the same experimental setup as
Section 7.2. Figure 11 summarizes the results of running the queries with and without DCE. We
observe a maximum speedup of 2.1x and an average speedup of 1.5x across all queries.
8

RELATED WORK

Graph-based IRs for Imperative Languages. Program dependence graphs (PDGs) [Ferrante
et al. 1987] include explicit data and control dependencies which allow many optimizations to run
in a single pass and incrementalize dataflow computations. Our work shares these qualities, e.g., in
the code motion and tree generation phase. Similarly, the graph-based IR by Click and Paleczny[1995] is an enhanced form of static single assignment form (SSA) [Cytron et al. 1991] that has
been used in production and research compilers, such as the Java HotSpot compiler [Paleczny
Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

236:26

Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf

et al. 2001] and Truffle/Graal [Duboscq et al. 2013; Würthinger et al. 2013]. However, these works
target first-order imperative languages, while our IR targets higher-order functional languages witheffects. Notably our IR has a type system based on reachability and effects [Bao et al. 2021], which isnovel in this area. General-purpose typed graph representations are becoming more commonplacein compilers. For instance, MLIR [Lattner et al. 2021] can be classified as an extensible DSL forcompiler infrastructures.
Graph Reduction and Rewriting for 𝜆-Calculi. Pure functional language compilers have aquite different notion of graph IR. Terms in the 𝜆-calculus correspond to terms in combinatory logic
which effectively yields simplified IRs for functional programs in point-free style, i.e., devoid ofvariables and bindings [Turner 1979; Wadsworth 1971]. Due to referential transparency, combinatory
terms can be presented as graphs with zero code duplication, and optimizations apply simultaneously
to all occurrences. Graph reduction techniques later became popular for implementing non-strict
functional languages [Johnsson 1984; Peyton-Jones 1987; Peyton-Jones and Salkild 1989; Turner
1979]. A closely-related notion is term-graph rewriting [Barendregt et al. 1987], and both are interderivable [Danvy and Zerny 2013; Zerny 2013]. Our work deals with impure functional languages
so that referential transparency and the sharing properties of a combinator graph are lost. Moreover,
our reliance on sets of variables and effects on variables is incompatible with the point-free style.
Functional Compilers and High-Performance DSLs. Elliott et al. [2003] propose a framework
for compiling embedded DSLs that contains optimizations including CSE and code motion. Codemotion is implemented by first converting the input program into a directed acyclic graph (DAG).
After let-bindings are introduced for CSE in the DAG, expressions in loop bodies that are notdependent on the loop variable are candidates for code motion. More fine-grained constraints
ensure that it moves the largest such expression that does not incur additional re-computation.
Early LMS [Rompf 2012; Rompf et al. 2011] and Delite [Sujeeth et al. 2014] systems did not allow
sharing between mutable objects or nested mutable references, and rely on DSL writers to manuallyannotate side effects. Thus, they can only perform loop fusion in the phase of code generation. As
shown in Section 7.1, this work allows us to add another abstraction layer into LMS, i.e., translating
a DSL into a typed imperative graph IR, instead of directly translating into low-level code. This
treatment separates optimization from code generation, thus enhances the modularity of LMS byprogressively lowering the level of abstraction.
Futhark [Henriksen et al. 2017] is a functional data-parallel language targeting GPUs, similar to
our work, using types for local reasoning. Lift [Steuwer et al. 2017] employs a 𝜆-calculus IL andgraph IR for array computations on GPU backends. RISE and ELEVATE [Hagedorn et al. 2020],
successors to Lift, feature a DSL for optimization strategies, inspired by Stratego [Visser et al. 1998].
As demonstrated in Section 7.1, our work can lower tensor computations to GPUs with kernel
fusion [Wang et al. 2018, 2019b]. We could potentially support similar user-defined strategy DSLs.
Equality saturation and e-graphs [Nelson and Oppen 1980] have been adopted for compiler
optimization [Tate et al. 2009; Willsey et al. 2021]. However, their scalability in impure higher-orderlanguages is unclear. Integrating them with our graph IR is an interesting research direction.
Thorin [Leißa et al. 2015] is a graph IR for pure higher-order functional programs based on CPS
that tracks data dependencies only, whereas our graph IR supports impurity/effects in direct-stylefunctional programs, including complex usage patterns arising from mutability and higher-orderfunctions. Thorin calculates node dependencies by a transitive reachability analysis, while oursystem uses reachability types to first determine transitively aliased sets as potential dependency
candidates, before further narrowing these down by considering their usage effects.

Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

Graph IRs for Impure Higher-Order Languages

236:27Whole-program Optimization. MLton [Weeks 2006] reduces polymorphic and higher-orderprograms to a first-order SSA-based IR using monomorphization, inlining, and defunctionalization, enabling traditional intraprocedural optimizations but causing code duplication and longer
compilation times due to being whole-program.
In contrast, our approach works directly on unmodified higher-order and potentially polymorphic
program representations, enabling high-level rewriting rules (e.g., map/loop fusion (Sections 2
and 7.1) and modular application to program units, resulting in benefits such as faster compilation
times and late binding against libraries.
Code Motion. Classical code motion algorithms over CFGs aim to eliminate redundant computation based on expensive program analyses identifying unnecessary or loop-invariant computations [Cytron et al. 1986; Knoop et al. 1992b, 1994]. However, loop-invariant code motion isbound to the structure of a pre-existing CFG, thus cannot move code where no block exists. The
lexical structure in our graph IR avoids these problems and has more degrees of freedom whenmoving code. Based on Click [1995]’s work, our code motion algorithms work over graph IRs andschedule instructions. In addition, we take advantage from the dependencies and effects information
provided by our type system. We also consider higher-order functions as a basic ingredient of our
IR and can move entire pure functional blocks, which are not considered by Click’s IR and code
motion algorithm. Barany and Krall [2013] extends Click’s work with a spilling algorithm that
performs global code motion for effectful programs in the phase of machine instruction scheduling.
Our code motion algorithm is applied in the stage of code generation.
Type-and-Effect Systems. Ownership type systems [Clarke et al. 2013; Noble et al. 1998] have along history of structuring memory resources. As a close cousin to those systems, we are the firstto use reachability types [Bao et al. 2021] to extract effect dependencies in an IR and use them toperform optimizations. Benton et al. [2009, 2006] study the use of effect information to identify
valid transformations over higher-order effectful programs. However, computations with write
effects cannot be eliminated even if they are not observed by the rest of the program. We go a stepfurther, and use effects and aliases to derive precise dependencies that track last uses. Therefore,
we are able to soundly remove certain non-observable effectful computations.
9

CONCLUSION

This work bridges a long-standing gap in graph-based compiler optimization, enabling affordable
global optimizations for impure higher-order programs using reachability types, effects, and highlevel IR graphs with lexical structure. We have formalized and proved type-and-dependency safety,
and our experimental evaluation demonstrates competitive performance on a variety of benchmarks.
ACKNOWLEDGMENTS
A large number of people have contributed to the design of the LMS graph IR over the years, and inparticular to the system of effect dependencies: Nada Amin, Thaïs Baudon, Kevin J. Brown, James
M. Decker, Grégory Essertel, Georg Ofenbeck, Alen Stojanov, Arvind K. Sujeeth, Fei Wang, andYushuo Xiao. This work was supported in part by NSF awards 1553471, 1564207, 1918483, 1910216,
DOE award DE-SC0018050, as well as gifts from Meta, Google, Microsoft, and VMware.
REFERENCES
Yuyan Bao, Guannan Wei, Oliver Bračevac, Yuxuan Jiang, Qiyang He, and Tiark Rompf. 2021. Reachability Types: Tracking
Aliasing and Separation in Higher-Order Functional Programs. Proc. ACM Program. Lang. 5, OOPSLA (2021), 139:1–139:32.
Yuyan Bao, Guannan Wei, Oliver Bračevac, and Tiark Rompf. 2023. Modeling Reachability Types with Logical Relations:
Semantic Type Soundness, Termination, and Equational Theory. arXiv:2309.05885 [cs.PL]

Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

236:28

Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf

Gergö Barany and Andreas Krall. 2013. Optimal and Heuristic Global Code Motion for Minimal Spilling. In Compiler
Construction - 22nd International Conference, CC 2013, Held as Part of the European Joint Conferences on Theory andPractice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings (Lecture Notes in Computer Science, Vol. 7791),
Ranjit Jhala and Koen De Bosschere (Eds.). Springer, 21–40.
Hendrik Pieter Barendregt, Marko C. J. D. van Eekelen, John R. W. Glauert, Richard Kennaway, Marinus J. Plasmeijer, and
M. Ronan Sleep. 1987. Term Graph Rewriting. In PARLE, Parallel Architectures and Languages Europe, Volume II: Parallel
Languages, Eindhoven, The Netherlands, June 15-19, 1987, Proceedings (Lecture Notes in Computer Science, Vol. 259), J. W.
de Bakker, A. J. Nijman, and Philip C. Treleaven (Eds.). Springer, 141–158.
Nick Benton, Andrew Kennedy, Lennart Beringer, and Martin Hofmann. 2009. Relational semantics for effect-based programtransformations: higher-order store. In Proceedings of the 11th International ACM SIGPLAN Conference on Principles
and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal, António Porto and Francisco Javier
López-Fraguas (Eds.). ACM, 301–312.
Nick Benton, Andrew Kennedy, Martin Hofmann, and Lennart Beringer. 2006. Reading, Writing and Relations. In Programming Languages and Systems, 4th Asian Symposium, APLAS 2006, Sydney, Australia, November 8-10, 2006, Proceedings(Lecture Notes in Computer Science, Vol. 4279), Naoki Kobayashi (Ed.). Springer, 114–130.
Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf. 2023. Graph
IRs for Impure Higher-Order Languages (Technical Report). arXiv:2309.08118 [cs.PL]
Dave Clarke, Johan Östlund, Ilya Sergey, and Tobias Wrigstad. 2013. Ownership Types: A Survey. In Aliasing in ObjectOriented Programming. Types, Analysis and Verification, Dave Clarke, James Noble, and Tobias Wrigstad (Eds.). Lecture
Notes in Computer Science, Vol. 7850. Springer, 15–58.
Cliff Click. 1995. Global Code Motion / Global Value Numbering. In Proceedings of the ACM SIGPLAN’95 Conference on
Programming Language Design and Implementation (PLDI), La Jolla, California, USA, June 18-21, 1995, David W. Wall
(Ed.). ACM, 246–257.
Cliff Click and Michael Paleczny. 1995. A Simple Graph-Based Intermediate Representation. In Proceedings ACM SIGPLAN
Workshop on Intermediate Representations (IR’95), San Francisco, CA, USA, January 22, 1995, Michael D. Ernst (Ed.). ACM,
35–49.
Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. 1991. Efficiently Computing Static
Single Assignment Form and the Control Dependence Graph. ACM Trans. Program. Lang. Syst. 13, 4 (1991), 451–490.
Ron Cytron, Andy Lowry, and F. Kenneth Zadeck. 1986. Code Motion of Control Structures in High-Level Languages. In
Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, St. Petersburg Beach,
Florida, USA, January 1986. ACM Press, 70–85.
Olivier Danvy and Ulrik Pagh Schultz. 2000. Lambda-dropping: transforming recursive equations into programs with block
structure. Theor. Comput. Sci. 248, 1-2 (2000), 243–287.
Olivier Danvy and Ulrik Pagh Schultz. 2004. Lambda-Lifting in Quadratic Time. J. Funct. Log. Program. 2004 (2004).
Olivier Danvy and Ian Zerny. 2013. Three syntactic theories for combinatory graph reduction. ACM Trans. Comput. Log. 14,
4 (2013), 29:1–29:27.
Stephen Dolan and Alan Mycroft. 2017. Polymorphism, subtyping, and type inference in MLsub. In POPL. ACM, 60–72.
Gilles Duboscq, Lukas Stadler, Thomas Würthinger, Doug Simon, Christian Wimmer, and Hanspeter Mössenböck. 2013.
Graal IR: An extensible declarative intermediate representation. In Proceedings of the Asia-Pacific Programming Languages
and Compilers Workshop.
Jana Dunfield and Neel Krishnaswami. 2022. Bidirectional Typing. ACM Comput. Surv. 54, 5 (2022), 98:1–98:38.
Conal Elliott, Sigbjørn Finne, and Oege de Moor. 2003. Compiling embedded languages. J. Funct. Program. 13, 3 (2003),
455–481.
Grégory M. Essertel, Ruby Y. Tahboub, James M. Decker, Kevin J. Brown, Kunle Olukotun, and Tiark Rompf. 2018. Flare:
Optimizing Apache Spark with Native Compilation for Scale-Up Architectures and Medium-Size Data. In OSDI. USENIX
Association, 799–815.
Jeanne Ferrante, Karl J. Ottenstein, and Joe D. Warren. 1987. The Program Dependence Graph and Its Use in Optimization.
ACM Trans. Program. Lang. Syst. 9, 3 (1987), 319–349.
Jiří Filipovič, Matúš Madzin, Jan Fousek, and Luděk Matyska. 2015. Optimizing CUDA code by kernel fusion: application on
BLAS. The Journal of Supercomputing (2015), 3934–3957.
Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. 1993. The Essence of Compiling with Continuations. In
Proceedings of the ACM SIGPLAN’93 Conference on Programming Language Design and Implementation (PLDI), Albuquerque,
New Mexico, USA, June 23-25, 1993, Robert Cartwright (Ed.). ACM, 237–247.
Colin S. Gordon. 2021. Polymorphic Iterable Sequential Effect Systems. ACM Trans. Program. Lang. Syst. 43, 1, Article 4(April 2021), 79 pages.
Bastian Hagedorn, Johannes Lenfers, Thomas Koehler, Xueying Qin, Sergei Gorlatch, and Michel Steuwer. 2020. Achieving
high-performance the functional way: A functional pearl on expressing high-performance optimizations as rewrite

Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

Graph IRs for Impure Higher-Order Languages

236:29strategies. Proc. ACM Program. Lang. 4, ICFP (2020), 92:1–92:29.
John Hatcliff and Olivier Danvy. 1994. A Generic Account of Continuation-Passing Styles. In POPL. ACM Press, 458–471.
Troels Henriksen, Niels G. W. Serup, Martin Elsman, Fritz Henglein, and Cosmin E. Oancea. 2017. Futhark: Purely functional
GPU-programming with nested parallelism and in-place array updates. In Proceedings of the 38th ACM SIGPLAN Conference
on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017, Albert Cohen andMartin T. Vechev (Eds.). ACM, 556–571.
David Van Horn and Harry G. Mairson. 2008. Deciding kCFA is complete for EXPTIME. In Proceeding of the 13th ACM
SIGPLAN international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008,
James Hook and Peter Thiemann (Eds.). ACM, 275–282.
Thomas Johnsson. 1984. Efficient compilation of lazy evaluation. In Proceedings of the 1984 SIGPLAN Symposium on Compiler
Construction, Montreal, Canada, June 17-22, 1984, Mary S. Van Deusen and Susan L. Graham (Eds.). ACM, 58–69.
Thomas Johnsson. 1985. Lambda Lifting: Treansforming Programs to Recursive Equations. In FPCA (Lecture Notes in
Computer Science, Vol. 201). Springer, 190–203.
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2021. Safe systems programming in Rust. Commun.
ACM 64, 4 (2021), 144–152.
Robert Kennedy, Sun Chan, Shin-Ming Liu, Raymond Lo, Peng Tu, and Fred Chow. 1999. Partial Redundancy Elimination in
SSA Form. ACM Trans. Program. Lang. Syst. 21, 3 (may 1999), 627–676.
Jens Knoop, Oliver Rüthing, and Bernhard Steffen. 1992a. Lazy Code Motion. In Proceedings of the ACM SIGPLAN 1992
Conference on Programming Language Design and Implementation (San Francisco, California, USA) (PLDI ’92). Association
for Computing Machinery, New York, NY, USA, 224–234.
Jens Knoop, Oliver Rüthing, and Bernhard Steffen. 1992b. Lazy Code Motion. In Proceedings of the ACM SIGPLAN’92
Conference on Programming Language Design and Implementation (PLDI), San Francisco, California, USA, June 17-19, 1992,
Stuart I. Feldman and Richard L. Wexelblat (Eds.). ACM, 224–234.
Jens Knoop, Oliver Rüthing, and Bernhard Steffen. 1994. Optimal Code Motion: Theory and Practice. ACM Trans. Program.
Lang. Syst. 16, 4 (1994), 1117–1155.
Chris Lattner and Vikram S. Adve. 2004. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation.
In 2nd IEEE / ACM International Symposium on Code Generation and Optimization (CGO 2004), 20-24 March 2004, San Jose,
CA, USA. IEEE Computer Society, 75–88.
Chris Lattner, Mehdi Amini, Uday Bondhugula, Albert Cohen, Andy Davis, Jacques A. Pienaar, River Riddle, Tatiana
Shpeisman, Nicolas Vasilache, and Oleksandr Zinenko. 2021. MLIR: Scaling Compiler Infrastructure for Domain Specific
Computation. In CGO. IEEE, 2–14.
Roland Leißa, Marcel Köster, and Sebastian Hack. 2015. A graph-based higher-order intermediate representation. In CGO.
IEEE Computer Society, 202–212.
Nicholas D. Matsakis and Felix S. Klock. 2014. The rust language. In Proceedings of the 2014 ACM SIGAda annual conference on
High integrity language technology, HILT 2014, Portland, Oregon, USA, October 18-21, 2014, Michael Feldman and S. Tucker
Taft (Eds.). ACM, 103–104.
Jan Midtgaard. 2012. Control-flow analysis of functional programs. ACM Comput. Surv. 44, 3 (2012), 10:1–10:33.
Matthew Might. 2007. Environment Analysis of Higher-Order Languages. Ph.D. Dissertation. Georgia Institute of Technology,
Atlanta, GA, USA.
Matthew Might, Yannis Smaragdakis, and David Van Horn. 2010. Resolving and exploiting the k-CFA paradox: illuminating
functional vs. object-oriented program analysis. In PLDI. ACM, 305–315.
Marco T. Morazán and Ulrik Pagh Schultz. 2007. Optimal Lambda Lifting in Quadratic Time. In IFL (Lecture Notes in
Computer Science, Vol. 5083). Springer, 37–56.
Greg Nelson and Derek C. Oppen. 1980. Fast Decision Procedures Based on Congruence Closure. J. ACM 27, 2 (1980),
356–364.
Thomas Neumann. 2011. Efficiently Compiling Efficient Query Plans for Modern Hardware. Proc. VLDB Endow. 4, 9 (2011),
539–550.
James Noble, Jan Vitek, and John Potter. 1998. Flexible Alias Protection. In ECOOP’98 - Object-Oriented Programming, 12th
European Conference, Brussels, Belgium, July 20-24, 1998, Proceedings (Lecture Notes in Computer Science, Vol. 1445), Eric
Jul (Ed.). Springer, 158–185.
Martin Odersky and Konstantin Läufer. 1996. Putting Type Annotations to Work. In POPL. ACM Press, 54–67.
Martin Odersky, Martin Sulzmann, and Martin Wehr. 1999. Type Inference with Constrained Types. Theory Pract. Object
Syst. 5, 1 (1999), 35–55.
Martin Odersky, Christoph Zenger, and Matthias Zenger. 2001. Colored local type inference. In POPL. ACM, 41–53.
Michael Paleczny, Christopher Vick, and Cliff Click. 2001. The Java HotSpottm Server Compiler. In Proceedings of the Java
Virtual Machine Research and Technology Symposium, Vol. 1. 1–12.

Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

236:30

Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf

Lionel Parreaux. 2020. The simple essence of algebraic subtyping: principal type inference with subtyping made easy
(functional pearl). Proc. ACM Program. Lang. 4, ICFP (2020), 124:1–124:28.
Simon L. Peyton-Jones. 1987. The Implementation of Functional Programming Languages. Prentice-Hall.
Simon L. Peyton-Jones and Jon Salkild. 1989. The Spineless Tagless G-Machine. In Proceedings of the fourth international
conference on Functional programming languages and computer architecture, FPCA 1989, London, UK, September 11-13,
1989, Joseph E. Stoy (Ed.). ACM, 184–201.
Benjamin C. Pierce and David N. Turner. 2000. Local Type Inference. ACM Trans. Program. Lang. Syst. 22, 1 (2000), 1–44.
John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In 17th IEEE Symposium on Logic in
Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings. IEEE Computer Society, 55–74.
Jared Roesch, Steven Lyubomirsky, Logan Weber, Josh Pollock, Marisa Kirisame, Tianqi Chen, and Zachary Tatlock. 2018.
Relay: a new IR for machine learning frameworks. In Proceedings of the 2nd ACM SIGPLAN International Workshop on
Machine Learning and Programming Languages, MAPL 2018, Justin Gottschlich and Alvin Cheung (Eds.). ACM, 58–68.
Tiark Rompf. 2012. Lightweight modular staging and embedded compilers: Abstraction without regret for high-level highperformance programming. Ph.D. Dissertation. EPFL.
Tiark Rompf. 2016. The Essence of Multi-stage Evaluation in LMS. In A List of Successes That Can Change the World - Essays
Dedicated to Philip Wadler on the Occasion of His 60th Birthday (Lecture Notes in Computer Science, Vol. 9600), Sam Lindley,
Conor McBride, Philip W. Trinder, and Donald Sannella (Eds.). Springer, 318–335.
Tiark Rompf and Nada Amin. 2015. Functional pearl: a SQL to C compiler in 500 lines of code. In ICFP. ACM, 2–9.
Tiark Rompf and Martin Odersky. 2010. Lightweight modular staging: a pragmatic approach to runtime code generation andcompiled DSLs. In Generative Programming And Component Engineering, Proceedings of the Ninth International Conference
on Generative Programming and Component Engineering, GPCE 2010, Eindhoven, The Netherlands, October 10-13, 2010,
Eelco Visser and Jaakko Järvi (Eds.). ACM, 127–136.
Tiark Rompf, Arvind K. Sujeeth, Nada Amin, Kevin J. Brown, Vojin Jovanovic, HyoukJoong Lee, Manohar Jonnalagedda,
Kunle Olukotun, and Martin Odersky. 2013. Optimizing data structures in high-level programs: new directions forextensible compilers based on staging. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL ’13, Rome, Italy - January 23 - 25, 2013, Roberto Giacobazzi and Radhia Cousot (Eds.). ACM, 497–510.
Tiark Rompf, Arvind K. Sujeeth, HyoukJoong Lee, Kevin J. Brown, Hassan Chafi, Martin Odersky, and Kunle Olukotun. 2011.
Building-Blocks for Performance Oriented DSLs. In Proceedings IFIP Working Conference on Domain-Specific Languages,
DSL 2011, Bordeaux, France, 6-8th September 2011 (EPTCS, Vol. 66), Olivier Danvy and Chung-chieh Shan (Eds.). 93–117.
Amir Shaikhha, Andrew W. Fitzgibbon, Dimitrios Vytiniotis, and Simon Peyton Jones. 2019. Efficient differentiable
programming in a functional array-processing language. Proc. ACM Program. Lang. 3, ICFP (2019), 97:1–97:30.
Olin Shivers. 1988. Control-Flow Analysis in Scheme. In Proceedings of the ACM SIGPLAN’88 Conference on Programming
Language Design and Implementation (PLDI), Atlanta, Georgia, USA, June 22-24, 1988, Richard L. Wexelblat (Ed.). ACM,
164–174.
Olin Shivers. 1991. Control-Flow Analysis of Higher-Order Languages or Taming Lambda. Ph.D. Dissertation. Carnegie Mellon
University, PA, USA.
Olin Shivers. 2004. Higher-Order Control-Flow Analysis in Retrospect: Lessons Learned, Lessons Abandoned. In Best of
PLDI. ACM, 257–269.
Lukas Stadler, Thomas Würthinger, and Hanspeter Mössenböck. 2014. Partial Escape Analysis and Scalar Replacement forJava. In 12th Annual IEEE/ACM International Symposium on Code Generation and Optimization, CGO 2014, Orlando, FL,
USA, February 15-19, 2014, David R. Kaeli and Tipp Moseley (Eds.). ACM, 165.
Michel Steuwer, Toomas Remmelg, and Christophe Dubach. 2017. Lift: A functional data-parallel IR for high-performance
GPU code generation. In Proceedings of the 2017 International Symposium on Code Generation and Optimization, CGO
2017, Austin, TX, USA, February 4-8, 2017, Vijay Janapa Reddi, Aaron Smith, and Lingjia Tang (Eds.). ACM, 74–85.
Arvind K. Sujeeth, Kevin J. Brown, HyoukJoong Lee, Tiark Rompf, Hassan Chafi, Martin Odersky, and Kunle Olukotun.
2014. Delite: A Compiler Architecture for Performance-Oriented Embedded Domain-Specific Languages. ACM Trans.
Embed. Comput. Syst. 13, 4s (2014), 134:1–134:25.
Ruby Y. Tahboub, Grégory M. Essertel, and Tiark Rompf. 2018. How to Architect a Query Compiler, Revisited. In SIGMOD
Conference. ACM, 307–322.
Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner. 2009. Equality saturation: A new approach to optimization. In
Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah,
GA, USA, January 21-23, 2009, Zhong Shao and Benjamin C. Pierce (Eds.). ACM, 264–276.
Amin Timany, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. 2022. A Logical Approach to Type Soundness. https://iris-project.org/pdfs/2022-submitted-logical-type-soundness.pdf.
Ben L. Titzer. 2015. Digging into the TurboFan JIT. Retrieved April 14, 2022 from http://web.archive.org/web/20220414155345/
https://v8.dev/blog/turbofan-jit

Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.

Graph IRs for Impure Higher-Order Languages

236:31

TPC. 1999. TPC Benchmark H. Retrieved April 14, 2022 from http://web.archive.org/web/20220407033028/https://www.tpc.
org/tpch/
D. A. Turner. 1979. A new implementation technique for applicative languages. Software: Practice and Experience 9, 1 (1979),
31–49.
Eelco Visser, Zine-El-Abidine Benaissa, and Andrew P. Tolmach. 1998. Building Program Optimizers with Rewriting
Strategies. In Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP ’98),
Baltimore, Maryland, USA, September 27-29, 1998, Matthias Felleisen, Paul Hudak, and Christian Queinnec (Eds.). ACM,
13–26.
Christopher Peter Wadsworth. 1971. Semantics and Pragmatics of the Lambda-Calculus. Ph.D. Dissertation. University of
Oxford.
Fei Wang, Guoyang Chen, Weifeng Zhang, and Tiark Rompf. 2019a. Parallel Training via Computation Graph Transformation.
In 2019 IEEE International Conference on Big Data (Big Data). 3430–3439.
Fei Wang, James M. Decker, Xilun Wu, Grégory M. Essertel, and Tiark Rompf. 2018. Backpropagation with Callbacks:
Foundations for Efficient and Expressive Differentiable Programming. In Advances in Neural Information Processing
Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal,
Canada, Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi, and Roman Garnett(Eds.). 10201–10212.
Fei Wang, Daniel Zheng, James M. Decker, Xilun Wu, Grégory M. Essertel, and Tiark Rompf. 2019b. Demystifying
differentiable programming: shift/reset the penultimate backpropagator. Proc. ACM Program. Lang. 3, ICFP (2019),
96:1–96:31.
Stephen Weeks. 2006. Whole-program compilation in MLton. In Proceedings of the ACM Workshop on ML, 2006, Portland,
Oregon, USA, September 16, 2006, Andrew Kennedy and François Pottier (Eds.). ACM, 1.
Guannan Wei, Oliver Bračevac, Shangyin Tan, and Tiark Rompf. 2020. Compiling symbolic execution with staging andalgebraic effects. Proc. ACM Program. Lang. 4, OOPSLA (2020), 164:1–164:33.
Guannan Wei, Oliver Bračevac, Songlin Jia, Yuyan Bao, and Tiark Rompf. 2023a. Polymorphic Reachability Types: Tracking
Freshness, Aliasing, and Separation in Higher-Order Generic Programs. arXiv:2307.13844 [cs.PL]
Guannan Wei, Songlin Jia, Ruiqi Gao, Haotian Deng, Shangyin Tan, Oliver Bračevac, and Tiark Rompf. 2023b. Compiling
Parallel Symbolic Execution with Continuations. In ICSE. IEEE, 1316–1328.
Guannan Wei, Shangyin Tan, Oliver Bračevac, and Tiark Rompf. 2021. LLSC: a parallel symbolic execution compiler for
LLVM IR. In ESEC/SIGSOFT FSE. ACM, 1495–1499.
Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021. egg: Fastand extensible equality saturation. Proc. ACM Program. Lang. 5, POPL (2021), 1–29.
Thomas Würthinger, Christian Wimmer, Andreas Wöß, Lukas Stadler, Gilles Duboscq, Christian Humer, Gregor Richards,
Doug Simon, and Mario Wolczko. 2013. One VM to rule them all. In ACM Symposium on New Ideas in Programming andReflections on Software, Onward! 2013, part of SPLASH ’13, Indianapolis, IN, USA, October 26-31, 2013, Antony L. Hosking,
Patrick Th. Eugster, and Robert Hirschfeld (Eds.). ACM, 187–204.
Ian Zerny. 2013. On graph rewriting, reduction, and evaluation in the presence of cycles. High. Order Symb. Comput. 26, 1-4(2013), 63–84.

Received 2023-04-14; accepted 2023-08-27

Proc. ACM Program. Lang., Vol. 7, No. OOPSLA2, Article 236. Publication date: October 2023.