Multi-stage Programming with
Generative and Analytical Macros
Nicolas Stucki
EPFL
Lausanne, Switzerland
nicolas.stucki@epfl.ch

Jonathan ImmanuelBrachthäuser
EPFL
Lausanne, Switzerland
jonathan.brachthauser@epfl.ch

Martin Odersky
EPFL
Lausanne, Switzerland
martin.odersky@epfl.ch

Abstract

1

In metaprogramming, code generation and code analysis arecomplementary. Traditionally, principled metaprogramming
extensions for programming languages, like MetaML and
BER MetaOCaml, offer strong foundations for code generation but lack equivalent support for code analysis. Similarly,
existing macro systems are biased towards the code generation aspect.
In this work, we present a calculus for macros featuring
both code generation and code analysis. The calculus directlymodels separate compilation of macros, internalizing a commonly neglected aspect of macros. The system ensures thatthe generated code is well-typed and hygienic.
We implement our system in Scala 3, provide a formalization, and prove its soundness.

Generative programming [5] is used in scenarios such ascode configuration of libraries, code optimizations [28], andDSL implementations [4, 26]. There are various kinds of program generation systems ranging from syntax-based andunhygienic, to fully typed [14, 21]. Modern macro systems,
like Racket’s, can extend the syntax of the language [8] tocreate hierarchies of domain-specific languages [1]. In thispaper, we are not concerned with Racket-like language extensibility, but rather macros that can generate/analize codeof expressions at compile-time.
Principled approaches to metaprogramming, such as
MetaML [25] and BER MetaOCaml [3, 11–13], offer strong
foundations for expression code generation. These systems
focus on runtime code generation and ensure static-safety(well-typed and hygienic) and cross-stage safety. They usually provide cross-stage persistence (CSP), the ability to referto values from previous stages, at the cost of not supporting
cross-platform portability [25]. Cross-platform portability,
as defined by Taha and Sheard [25], describes the ability tomove code, generated on one machine, to a (potentially different) machine to compile and execute it there. This ability
is necessary for multi-stage macros in compiled languages
with separate compilation. To move code from one machine
to the next, cross-platform portability requires code serialization, either in the form of source code or as a serializedintermediate representation. Multi-stage systems that support portability usually need to make some compromises.
Some miss analytical capabilities while others allow bothgenerative and analytical macros by resorting to advanced
type system machinery.
MacroML [9] extended MetaML to provide a multi-stage
macro system showing that “multi-stage programming languages are a good foundation for the semantics based designof macro systems” [9]. By design, MacroML took a conservative approach not to blur the distinction between code anddata, explicitly avoids dynamic scoping, and lacks analytical macros. Squid [16–18] provides a multi-stage system forgenerative and analytical macros. Unlike MacroML, Squid
uses statically typed dynamic scoping, tracking free term
variables in types, to provide type-safe analytical macros.

CCS Concepts: • Software and its engineering → Macrolanguages; Semantics; Patterns.
Keywords: multi-stage programming, metaprogramming,
macro systems, formalization
ACM Reference Format:
Nicolas Stucki, Jonathan Immanuel Brachthäuser, and Martin Odersky. 2021. Multi-stage Programming with Generative and Analytical
Macros. In Proceedings of the 20th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (GPCE’21), October 17–18, 2021, Chicago, IL, USA. ACM, New York, NY,
USA, 13 pages. https://doi.org/10.1145/3486609.3487203

Permission to make digital or hard copies of all or part of this work forpersonal or classroom use is granted without fee provided that copies are notmade or distributed for profit or commercial advantage and that copies bear
this notice and the full citation on the first page. Copyrights for componentsof this work owned by others than ACM must be honored. Abstracting withcredit is permitted. To copy otherwise, or republish, to post on servers or toredistribute to lists, requires prior specific permission and/or a fee. Request
permissions from permissions@acm.org.
GPCE ’21, October 17–18, 2021, Chicago, IL, USA© 2021 Association for Computing Machinery.
ACM ISBN 978-1-4503-9112-2/21/10. . . $15.00
https://doi.org/10.1145/3486609.3487203

110

Introduction

GPCE ’21, October 17–18, 2021, Chicago, IL, USA

Nicolas Stucki, Jonathan Immanuel Brachthäuser, Martin Odersky

Requirements. We identify the following requirementsthat a design of a multi-stage macro system for compiled
languages should meet.

As shown in the example, our implementation provides theExpr operation that lifts a value into a quoted expression.

• Cross-platform portability. It should be possible to use
generated code on different machines.
• Static-safety. Generated code should be hygienic andwell-typed.
• Cross-stage safety. Access to variables should only beallowed at stages where they are available.
• Generative/Analytical. Programmers should be able togenerate as well as analyze and decompose code.

Macros. We can use the same splicing abstraction to express macros. In our system, a macro consists of top-level
splices (not nested in any quote). Conceptually, the contentsof the splice are evaluated one stage earlier than the program. Or, in other words, the contents are evaluated while
compiling the program. The generated code resulting fromthe macro replaces the splice in the program.
def power2(x: Int): Int =${ powCode('x, 2) } // x * x * 1

We present a formal calculus that captures the fundamental aspects of the Scala 3 multi-stage macro system. The
formalization and implementation advance the state of theart, satisfying the requirements listed above.

Stage consistency. We define the staging level of somecode as the number of quotes minus the number of splices
surrounding said code. In general, it is never possible toaccess a local variable from a lower staging level as it does
not yet exist.

Contributions. In particular, this paper makes the following contributions.
• We introduce a calculus (𝜆 ▲ ) for well-typed and hygienic
multi-stage metaprogramming that allows both generative and analytical macros (Section 3). The calculus supports quotes and splices (Section 3.1), cross-platform
portability (Section 3.2), and analytical macros via pattern matching (Section 3.3).
• We prove soundness of 𝜆 ▲ in terms of the standard
theorems for progress (Theorems 3.5 and 3.14) andpreservation (Theorems 3.6 and 3.15).
• We fully implement 𝜆 ▲ as a production-ready systemin the Scala 3 programming language (Section 4).

2

def badPower(x: Int, n: Int): Int =${ powCode('x, n) } // ERROR value of `n` not known yet

In the context of macros and cross-platform portability, thatis, macros compiled on one machine but potentially executedon another, we cannot support cross-stage persistence of
local variables.
def badPowCode(x: Expr[Int], n: Int)(using Quotes) =// ERROR `n` potentially not available in the next machine'{ power($x, n) }Multi-Stage Macros in Scala 3

def power(x: Int, n: Int): Int =if n == 0 then 1
else power(x, n-1)

In this section, we offer an informal overview of the featuresthat our calculus provides and discuss how they relate to
the design requirements stated in the previous section. All
examples in this section are expressed in Scala 3, using our
implementation. In Section 3, we present 𝜆 ▲ formally.
2.1

Therefore, in our system, local variables can only be accessedat precisely the same staging level. For global definitions,such as powCode, the rules are slightly different. It is possible togenerate code that contains a reference to a global definition
such as in '{ power(2, 4) }. This is a limited form of crossstage persistence, where we refer to the already compiled
code for power. Each compilation step will lower the staging
level by 1 while keeping global definitions. In consequence,
we can refer to compiled definitions in macros such as powCodein ${ powCode('x, 2) }. We disallow splices within top-level
splices.

Generative Multi-Stage Programming

Our implementation in Scala 3 supports generative multistage programming. Here we give an overview of the various
features that together constitute the meta-programming API.
Quotes and Splices. Multi-stage programming in Scala
3 uses quotes '{..} to delay/stage execution of code andsplices ${..} to evaluate and insert code into quotes. Quoted
expressions are typed as Expr[T] with a covariant type parameter T. With these two concepts, it is easy to write staticallysafe code generators. The following examples shows naive
implementation of the 𝑥 𝑛 mathematical operation.

Inlining. Since using the splices in the middle of a program is not as ergonomic as calling a function, we hide thestaging mechanism from end-users of macros and have auniform way of calling macros and normal functions. For
this, we restrict the use of top-level splices to only appear in
so-called inline methods [22]. This mechanism is not part of
the formalization of the present paper but helps to see howmacros will be used in practice.

import scala.quoted.*def powCode(x: Expr[Int], n: Int)(using Quotes): Expr[Int] =if n == 0 then Expr(1) // lift 1 into '{ 1 }else '{ $x * ${ powCode(x, n-1) } }111

Multi-stage Programming with Generative and Analytical Macros

GPCE ’21, October 17–18, 2021, Chicago, IL, USA

Patterns may contain two kinds of references, global reference such as power in '{ power(...) } or references to bindings
defined in the pattern such as x in case '{ (x: Int) ⇒ x }.

// inline macro definition
inline def inlinePower(x: Int, n: Int): Int =${ powCodeFor('x, 'n) }// `powCodeFor` defined in next section

Closed patterns. When extracting an expression from aquote, we need to make sure that we do not extrude any
variables from the scope where they are defined.

// user codedef power2(x: Int): Int =inlinePower(x, 2) // x * x * 1'{ (x: Int) ⇒ x + 1 } matchcase '{ (y: Int) ⇒ $z } ⇒// should not match, otherwise: z = '{ x + 1 }The evaluation of the macro will only happen when the code
is inlined into power2. When inlined, the code is equivalent to
the previous definition of power2. An important consequenceis that none of the arguments or the return type of the macro
will have to mention the Expr types, encapsulating all aspectsof metaprogramming from the end users.
2.2

In this example, we see that the pattern should not match.
Otherwise, any use of the expression z would contain an
unbound reference to x. To avoid any such extrusion, weonly match on a ${..} if its expression is closed under thedefinitions within the pattern.

Analytical Multi-Stage Programming

HOAS patterns. To allow extracting expression that may
have extruded references we offer a higher-order abstract syntax (HOAS) [19] pattern $f(y) (or $f(y1, ...)). This pattern
will 𝜂-expand the sub-expression with respect to 𝑦 and bindit to 𝑓 . The variables that might have been extruded will be
replaced by the arguments of the lambda.

By nature, macros consume and produce program fragmentsof type Expr. Analytical macros inspect the code they receive
as arguments to perform some analysis or transformation.
Value analysis. To be able to generate optimized codeusing powCode, the macro implementation powCodeFor needs tofirst determine whether the argument passed as parameter n
is a constant value. This can be achieved via unlifting using
the Expr extractor from our library implementation that will
only match if n is a quoted constant and extracts its value.

'{ ((x: Int) ⇒ x + 1).apply(2) } matchcase '{ ((y: Int) ⇒ $f(y)).apply($z: Int) } ⇒// f may contain references to x// f = (y: Expr[Int]) ⇒ '{ $y + 1 }f(z) // generates '{ 2 + 1 }def powCodeFor(x: Expr[Int], n: Expr[Int])(using Quotes) =n match// it is a constant: unlift code n='{m} into number mcase Expr(m) ⇒ powCode(x, m)// not known: call power at runtime
case _ ⇒ '{ power($x, $n) }This approach was also used in earlier Squid [17] versions.
The use of HOAS allows us to keep the involved types simple. The 𝜂-expanded sub-expression can be typed with asimple function type. This way we can avoid scope extrusion without resorting to involved type-level machinery of
tracking free variables. HOAS patterns without parameters
are considered closed patterns.

Structural analysis. It is sometimes necessary to analyze the structure of the code or decompose the code into
its parts. A classic example is an embedded DSL, where amacro knows a set of definitions that it can reinterpret while
compiling the code using a macro (for instance, to perform
optimizations). In the following example, we extend our previous implementation of powCode with the ability to look into
x to provide further optimizations.

Summary. We showed the features of our system that
support generative and analytical multi-stage programming.
We showed how cross-platform portability relates to macrosand how it influences the design of cross-stage safety. We
showed how we guarantee cross-stage safety with stage
consistency and HOAS patterns.

3

Multi-Stage Macros Calculus

In this section, we present the 𝜆 ▲ multi-stage macros calculus. The presentation is organized into four parts. We first
introduce the core calculus, which extends the simply-typed
lambda calculus with support for quotes and splices. The
two abstractions are at the core of cross-stage safety andstatic-safety. In a second step, we extend the calculus to capture the semantics of compilation of macros. An abstractionthat supports cross-platform portability. Then we extend thecore calculus with quote analysis by adding quoted patternmatching. In a final extension, we combine compilation anddef powCode(x: Expr[Int], n: Int)(using Quotes) =x matchcase '{ power($y, ${Expr(m)}) } ⇒ // we have (y^m)^n
powCode(y, n * m) // generate code for y^(n*m)
case _ ⇒if n == 0 then '{ 1 }else '{ $x * ${ powCode(x, n-1) } }The pattern ${..} extracts code as an expression, and it iseither bound as $y or matched against a nested pattern as in${Expr(m)}.

112

GPCE ’21, October 17–18, 2021, Chicago, IL, USA

Nicolas Stucki, Jonathan Immanuel Brachthäuser, Martin Odersky

macros with the pattern matching extension. We show thesoundness of individual extensions and their combination.
3.1

starts at 0, increases each time we encounter a quote (TQuote), and decreases each time we encounter a splice (TSplice). All other typing rules maintain the same level in
their premises. Splices cannot be typed at level 0 to avoid
negative staging levels. As can be seen in rule T-Abs, bindings
are added to the environment with the level at which they
are defined. Similarly, a variable can only be typed if it isreferenced at the same level it was defined in (T-Var).

Core Calculus: Quotes and Splices

This first core calculus captures the fundamental semantics
of programs that operate on and produce code. To this end,
it extends STLC with the ability to delay the computation
by quoting the code and the ability to compose delayedcomputations by splicing.
Figure 1 defines the syntax and semantics of this calculus. We use the notation [𝑥 ↦→ 𝑡 2 ]𝑡 1 to denote the standard
capture-avoiding substitution of 𝑡 2 for 𝑥 within 𝑡 1 . As usual,
we follow Barendregt [2] and require that all variable names
are globally unique. We also only distinguish terms up torenaming.

Example 3.3. Tracking of levels ensures cross-stage safetyof variables. Both type derivations below fail.
Fail3.1.1 Syntax. The calculus features the standard forms of
simply-typed lambda calculus, that is, constants 𝑐, variables
𝑥, abstraction 𝜆𝑥:𝑇 .𝑡, and application 𝑡 𝑡. In order to express
the introductory examples, we also add support for fixpointcomputation fix 𝑡. The two most important additions to theterm syntax are quotation ⌈𝑡⌉ (instead of '{t}) and splicing⌊𝑡⌋ (instead of ${t}). The syntax of types includes built-in
types 𝐶, function types of the form 𝑇 →𝑇 , and the type ofquoted terms ⌈𝑇 ⌉ (corresponds to Expr[T]). That is, for a term𝑡 of type 𝑇 , the quoted term ⌈𝑡⌉ has type ⌈𝑇 ⌉.

Fail𝑥 :1 𝑇 ∈ ∅, 𝑥 :0 𝑇

𝑥 :0 ⌈𝑇 ⌉ ∈ ∅, 𝑥 :1 ⌈𝑇 ⌉∅, 𝑥 :0 𝑇 ⊢1 𝑥 : 𝑇∅, 𝑥 :1 ⌈𝑇 ⌉ ⊢0 𝑥 : ⌈𝑇 ⌉∅, 𝑥 :0 𝑇 ⊢0 ⌈𝑥⌉ : ⌈𝑇 ⌉∅, 𝑥 :1 ⌈𝑇 ⌉ ⊢1 ⌊𝑥⌋ : 𝑇∅ ⊢0 𝜆𝑥:𝑇 .⌈𝑥⌉ : 𝑇 →⌈𝑇 ⌉∅ ⊢1 𝜆𝑥:⌈𝑇 ⌉.⌊𝑥⌋ : ⌈𝑇 ⌉→𝑇

3.1.4 Evaluation. We present the semantics of our calculus in terms of a small-step operational semantics (Figure 1).
Like the typing judgments, the evaluation relation is also
indexed by a staging level 𝑖. Also similar to typing, the index
starts at 0, increases each time it goes in a quote (E-Quote),and decreases each time it goes into a splice (E-Splice). At
level 0, the semantics follow the usual STLC semantics andwe perform 𝛽-reduction (E-Beta) and fix-point computation(E-Fix-Red). The rules E-App-1, E-App-2, and E-Fix express
the usual congruences. The congruences E-Quote and ESplice modify the levels accordingly. Intuitively, the calculus
not only performs 𝛽-reduction on level 0, but also seeks to
reduce all splices at level 1 (E-Splice-Red). To achieve this,at levels greater than 0, we need to evaluate under lambdas(E-Abs) in case it contains a level 1 splice.

Example 3.1. Within the core calculus, we can easily write
a function that can generate complex code. The def powCodeof Section 2 can be encoded in this calculus for a numericaltype N as follows:
fix 𝜆rec:⌈N⌉→N→⌈N⌉.
𝜆𝑥:⌈N⌉.𝜆𝑛:N.ifIsZero 𝑛 ⌈1⌉ ⌈mult ⌊𝑥⌋ ⌊rec 𝑥 (𝑛−1)⌋⌉

Example 3.4. The specifics of the operational semantics
are illustrated by the following example, which makes use ofboth reductions rules E-Beta and E-Splice-Red. The resulting expression is a value according to our definition since itdoes not contain any level-1 splice.

3.1.2 Environments. As usual, environments Γ are listsof bindings 𝑥 :𝑖 𝑇 . However, they do not only track the typeof each binding 𝑇 , but also at which staging level 𝑖 a variable has been introduced. The staging level 𝑖 is a number in
N0 = {0, 1, 2, . . . }. We consider bindings at different levels
as disjoint. That is, looking up the binding for 𝑥 at level 𝑗in environment Γ = Γ1, 𝑥 :𝑖 𝑇 , Γ2 only succeeds, if 𝑖 = 𝑗. For
simplicity, we require well-formedness to establish that environments contain a single binding of each name 𝑥, rulingout Γ, 𝑥 :𝑖 𝑇 , 𝑥 : 𝑗 𝑇 by construction. By definition, the environment guarantees cross-stage safety. Notably, this implies
that there is no cross-stage persistence of local variables.

⌈𝜆𝑥:𝑇 .⌊(𝜆𝑦:⌈𝑇 ⌉.𝑦) ⌈𝑓 𝑥⌉⌋⌉−→⌈𝜆𝑥:𝑇 .⌊⌈𝑓 𝑥⌉⌋⌉−→⌈𝜆𝑥:𝑇 .𝑓 𝑥⌉

E-BetaE-Splice-Red

3.1.5 Values. While it may appear non-standard, the definition of values follows directly from the operational semantics. Intuitively, a term is a value, if it is a constant (V-Const),
an abstraction (V-Abs-0), or a quote (V-Quote) that does notcontain any level-1 splices.

Example 3.2. Though the calculus itself does not support
CSP, it is possible to use values in later stages by liftingand splicing. In the following example, we lift a boolean (B)constant into a quote containing the constant.

3.1.6 Soundness. We show the soundness of the calculus
by proving the standard progress and preservation theorems.
Theorem 3.5 (Progress for Terms). If ∅ ⊢𝑖 𝑡 : 𝑇 , then 𝑡 is avalue ⊢𝑖 𝑡 vl or there exists 𝑡 ′ such 𝑡 −→𝑖 𝑡 ′.

𝜆𝑥:B.ifIsTrue 𝑥 ⌈true⌉ ⌈false⌉

3.1.3 Typing. Typing judgments take the form Γ ⊢𝑖 𝑡 :𝑇 and assign a term 𝑡 the type 𝑇 . However, they are also
parameterized by the staging level 𝑖. Conceptually, the level

Theorem 3.6 (Preservation for Terms). If Γ ⊢𝑖 𝑡 : 𝑇 and𝑡 −→𝑖 𝑡 ′, then Γ ⊢𝑖 𝑡 ′ : 𝑇 .

113

Multi-stage Programming with Generative and Analytical Macros

GPCE ’21, October 17–18, 2021, Chicago, IL, USA

SyntaxTerm𝑡F𝑐 | 𝑥 | 𝜆𝑥:𝑇 .𝑡 | 𝑡 𝑡 | fix 𝑡 | ⌈𝑡⌉ | ⌊𝑡⌋

Type

𝑇

F

𝐶 | 𝑇 →𝑇 | ⌈𝑇 ⌉Environment
Typing environmentΓF∅ | Γ, 𝑥 :𝑖 𝑇

Level

𝑖

∈

N0

Typing Rules
𝑥 :𝑖 𝑇 ∈ ΓΓ, 𝑥 :𝑖 𝑇1 ⊢𝑖 𝑡 2 : 𝑇2

Γ ⊢𝑖 𝑥 : 𝑇(T-Var)Γ ⊢𝑖 𝜆𝑥:𝑇1 .𝑡 2 : 𝑇1 →𝑇2(T-Abs)Γ ⊢𝑖 𝑡 : 𝑇 →𝑇

Γ ⊢𝑖+1 𝑡 : 𝑇Γ ⊢𝑖−1 𝑡 : ⌈𝑇 ⌉

Γ ⊢𝑖 fix 𝑡 : 𝑇(T-Fix)Γ ⊢𝑖 ⌈𝑡⌉ : ⌈𝑇 ⌉(T-Quote)Γ ⊢𝑖 𝑐 : 𝐶(T-Const)

Γ ⊢𝑖 𝑡 1 : 𝑇1 →𝑇2Γ ⊢𝑖 𝑡 2 : 𝑇1

Γ ⊢𝑖 𝑡 1 𝑡 2 : 𝑇2
(T-App)𝑖≥1

Γ ⊢𝑖 ⌊𝑡⌋ : 𝑇(T-Splice)

Operational Semantics
𝑡 1 −→𝑖 𝑡 1′

𝑡 −→𝑖 𝑡 ′𝑡 1 𝑡 2 −→𝑖 𝑡 1′ 𝑡 2(E-App-1)

𝜆𝑥:𝑇 .𝑡 −→𝑖 𝜆𝑥:𝑇 .𝑡 ′(E-Abs)(𝜆𝑥:𝑇1 .𝑡 1 ) 𝑡 2 −→0 [𝑥 ↦→ 𝑡 2 ]𝑡 1
(E-Beta)𝑡 −→𝑖 𝑡 ′𝑡 2 −→𝑖 𝑡 2′⊢𝑖 𝑡 1 vl⊢0 𝑡 2 vl

𝑖≥1𝑡 1 𝑡 2 −→𝑖 𝑡 1 𝑡 2′
(E-App-2)

fix 𝜆𝑥:𝑇 .𝑡 −→0 [𝑥 ↦→ fix 𝜆𝑥:𝑇 .𝑡]𝑡
(E-Fix-Red)

fix 𝑡 −→𝑖 fix 𝑡 ′(E-Fix)𝑡 −→𝑖+1 𝑡 ′𝑡 −→𝑖−1 𝑡 ′⌈𝑡⌉ −→𝑖 ⌈𝑡 ′ ⌉(E-Quote)⊢1 𝑡 vl𝑖≥1⌊𝑡⌋ −→𝑖 ⌊𝑡 ′ ⌋(E-Splice)⌊⌈𝑡⌉⌋ −→1 𝑡(E-Splice-Red)

Values⊢0 𝜆𝑥:𝑇 .𝑡 vl(V-Abs-0)⊢𝑖 𝑐 vl(V-Const)⊢𝑖 𝑡 vl𝑖≥1⊢𝑖 𝑡 vl𝑖≥1⊢𝑖 fix 𝑡 vl⊢𝑖 𝜆𝑥:𝑇 .𝑡 vl(V-Fix)(V-Abs)⊢𝑖+1 𝑡 vl𝑖≥1⊢𝑖 ⌈𝑡⌉ vl(V-Quote)⊢𝑖 𝑥 vl(V-Var)⊢𝑖 𝑡 1 vl⊢𝑖 𝑡 2 vl⊢𝑖 𝑡

1 𝑡 2 vl
(V-App)𝑖≥1⊢𝑖−1 𝑡 vl𝑖≥2⊢𝑖 ⌊𝑡⌋ vl(V-Splice)

Figure 1. Core Calculus
The full proofs can be found in Appendix A [24], here we
only point out the structure and define key lemmas.
As usual, progress requires us to show that values takecanonical forms. This standard lemma trivially extends toour non-standard definition of values.

Using the restricted context, we define the generalized version of progress as:

Lemma 3.7 (Canonical Forms).
If ⊢0 𝑡 vl and• 𝑡 : 𝐶, then 𝑡 = 𝑐 for some 𝑐.
• 𝑡 : 𝑇1 →𝑇2 , then 𝑡 = 𝜆𝑥:𝑇1 .𝑡 1 for some 𝑥 and 𝑡 1 .
• 𝑡 : ⌈𝑇 ⌉, then 𝑡 = ⌈𝑡 1 ⌉ for some 𝑡 1 .

Proof (of Theorem 3.5). The proof of progress trivially follows from Lemma 3.9, by choosing Γ ≥1 = ∅.
□Lemma 3.9 (Extended Progress for Terms). If Γ ≥1 ⊢𝑖 𝑡 : 𝑇 ,then 𝑡 is a value ⊢𝑖 𝑡 vl or there exists 𝑡 ′ such 𝑡 −→𝑖 𝑡 ′For the proof of preservation, we need to adjust the standard substitution lemma to our setting with levels.
Lemma 3.10 (Substitution). ∀𝑖, 𝑗 ∈ N0 , if Γ ⊢ 𝑗 𝑡 1 : 𝑇1 andΓ, 𝑥 : 𝑗 𝑇1 ⊢𝑖 𝑡 2 : 𝑇2 then Γ ⊢𝑖 [𝑥 ↦→ 𝑡 1 ]𝑡 2 : 𝑇2 .

Proof (of Lemma 3.7). By case analysis on the value definition ⊢0 𝑡 vl.
□

Proof of Preservation (Theorem 3.6). Induction over the typing derivation, using the substitution lemma (Lemma 3.10).
□

To prove progress, we also need to prove a more general variant allowing the typing context Γ to only contain bindings
on a level greater than 0. To capture this property, we defineΓ ≥1 as a restricted typing context:

3.2

Definition 3.8 (Restricted Typing Context).
Γ ≥1F∅ | Γ ≥1, 𝑥 :𝑖 𝑇

Macros Extension: Cross-Platform Portability

The calculus from the previous section allowed us to write
programs that generate code using quotes and splices.

for 𝑖 ≥ 1

114

GPCE ’21, October 17–18, 2021, Chicago, IL, USA

Nicolas Stucki, Jonathan Immanuel Brachthäuser, Martin Odersky

Extended Syntax
ProgramLibraries𝑝

F

Library typingΣF∅ | Σ, 𝑥:𝑇

Runtime libraryΩF∅ | Ω, 𝑥=𝑡

def 𝑥 = ⌈𝑡⌉ in 𝑝 | eval 𝑡

Extended Typing Rules
𝑥:𝑇 ∈ Σ∅ | Σ ⊢0 𝑡 : 𝑇

Γ | Σ ⊢𝑖 𝑥 : 𝑇(T-Link)Σ ⊢ eval 𝑡 : 𝑇(T-Eval)∅ | Σ ⊢1 𝑡 : 𝑇1

Extended Values⊢0 𝑡 vl

Σ, 𝑥:𝑇1 ⊢ 𝑝 : 𝑇2

Σ ⊢ def 𝑥 = ⌈𝑡⌉ in 𝑝 : 𝑇2
(T-Def)⊢ eval 𝑡 vl
(V-Eval)Extended Operational Semantics
𝑥=𝑡 ∈ Ω𝑡 −→0Ω 𝑡 ′𝑡 −→1Ω 𝑡 ′⊢1 𝑡 vl

𝑥 −→0Ω 𝑡(E-Link)eval 𝑡 | Ω −→ eval 𝑡 ′ | Ω(E-Eval)def 𝑥 = ⌈𝑡⌉ in 𝑝 | Ω −→ def 𝑥 = ⌈𝑡 ′ ⌉ in 𝑝 | Ω(E-Macro)def 𝑥 = ⌈𝑡⌉ in 𝑝 | Ω −→ 𝑝 | Ω, 𝑥=𝑡(E-Compile)

Figure 2. Macros Extension
3.2.3 Typing. The typing judgements in Figure 2 extend
the ones presented in Figure 1. We modify the judgement
form Γ ⊢𝑖 𝑡 : 𝑇 to also track the library typing Σ as Γ | Σ ⊢𝑖𝑡 : 𝑇 . All existing rules simply pass Σ unmodified to theirpremises. To type programs, we add a new typing judgmentΣ ⊢ 𝑝 : 𝑇 where Σ tracks the library bindings. When typing alibrary definition def 𝑥 = ⌈𝑡⌉ in 𝑝 (T-Def), we type the term𝑡 at level 1. This way the term 𝑡 can contain splices, which inturn allows us to model macros. The rest of the program is
typed adding 𝑥 to the library environment Σ. Typing eval 𝑡(T-Eval) simply types 𝑡 at level 0 (like in Section 3.1) but
adds the Σ, which will not change in the remainder of thederivation. To be able to access library functions, we add rule
T-Link, which looks up the signature of a free variable 𝑥 in Σ.
We assume that dom(Σ) and dom(Γ) are disjoint and hence
there cannot be any ambiguity with (T-Var). Note that, unlike
rule T-Var, variables in Σ are stage polymorphic, therefore
library functions display a form of cross-stage persistence.

In realistic compiled languages, code is first compiled onsome machine and then used on a (potentially) different machine. If a macro is executed when compiling, the code it
generates will also be compiled and then used on another machine. This implies that we need cross-platform portability
to compile the generated code. If a macro definition is itself
compiled, we need to compile a program containing quoted
code. This requires a form of serialization in practice, but forthis to be sound it also requires cross-platform portability.
To capture the semantics of compiling programs, we extend the previous calculus with library function definitions.
These definitions will be compiled before they are used. The
calculus also adds a restricted notion of CSP that is compatible with cross-platform portability. Figure 2 defines thesyntax and semantics of the extended 𝜆 ▲ calculus.
3.2.1 Syntax. The macro calculus extends the syntax of
Figure 1 adding a syntactic form for programs 𝑝. Programs
are lists of library bindings def 𝑥 = ⌈𝑡⌉ in 𝑝 ending in asingle term eval 𝑡 that will be evaluated after all library bindings have been compiled. Here, def 𝑥 = ⌈𝑡⌉ in 𝑝 represents
the definition of a library function that is made available as
𝑥 in the remaining program. The implementation 𝑡, which
is given as code, is compiled and then added to a simplified
store, which we use to model the set of compiled functions
loaded in the program. In this program, a macro is a splice
within 𝑡. The syntactic form eval 𝑡 represents a programthat will be evaluated without being compiled. In practice,eval 𝑡 would be an interpreted call to the main method.

Example 3.11. Library functions in Σ can be used at any
level after they are compiled. This is illustrated by the typing
derivation below, where 𝑓 is used at staging levels 0 and 1.
Assuming that 𝑓 :⌈𝐶⌉→𝐶 ∈ Σ, we can see that all premises
are satisfiable with 𝑇1 = 𝑇3 = ⌈𝐶⌉ and 𝑇2 = 𝐶.
∅ | Σ ⊢0 𝑐 : 𝐶
𝑇3 = ⌈𝐶⌉

𝑓 :𝑇3 →𝑇2 ∈ Σ∅ | Σ ⊢1 𝑓 :𝑇3 →𝑇2∅ | Σ ⊢1 ⌈𝑐⌉ : 𝑇3

𝑓 :𝑇1 →𝐶 ∈ Σ∅ | Σ ⊢ 𝑓 ⌈𝑐⌉ : 𝑇2
𝑇1 = ⌈𝑇2 ⌉∅ | Σ ⊢0 𝑓 : 𝑇1 →𝐶∅ | Σ ⊢0 ⌈𝑓 ⌈𝑐⌉⌉ : 𝑇1

1

3.2.2 Libraries. Figure 2 introduces store-like runtime libraries Ω that map library function names 𝑥 to their implementation. It also adds a new typing environment Σ, whichtypes libraries Ω and allows us to track references to compiled programs. Values will only ever be added to the libraryΩ but never updated. Importantly, the bindings in Σ (and Ω)are not annotated with staging levels and are thus staginglevel agnostic.

∅ | Σ ⊢0 𝑓 ⌈𝑓 ⌈𝑐⌉⌉ : 𝐶Σ ⊢ eval 𝑓 ⌈𝑓 ⌈𝑐⌉⌉ : 𝐶

3.2.4 Evaluation. Like in the case of typing, the operational semantics in Figure 2 extends the one presented in
Figure 1 by modifying the relation 𝑡 −→𝑖 𝑡 ′ to be indexedwith a runtime library Ω as 𝑡 −→𝑖Ω 𝑡 ′. Also, like in typing, allexisting rules simply pass on Ω to their premises. To specify

115

Multi-stage Programming with Generative and Analytical Macros

GPCE ’21, October 17–18, 2021, Chicago, IL, USAΩ

the evaluation of programs, we introduce a new relation𝑝 | Ω −→ 𝑝 ′ | Ω ′, where a program 𝑝 with a library Ω evaluates to a program 𝑝 ′ with a potentially extended library Ω ′.
For a library definition def 𝑥 = ⌈𝑡⌉ in 𝑝, where 𝑡 is a value(i.e., does not contain macros), the library store is updatedwith a binding 𝑥=𝑡 and the definition is removed (E-Compile).
Importantly, in this process we are taking a 𝑡 at staging level1 and compile it, making it available as a runtime dependency
in the rest of the program; the compiled library function 𝑡 canbe used on arbitrary levels, including level 0. If the libraryfunction 𝑡 in a definition def 𝑥 = ⌈𝑡⌉ in 𝑝 still contains
splices at staging level 1 (macros), we first need to evaluate
them (E-Macro). Using the reduction of the core calculus
from Section 3.1, the contents of the macros will be evaluatedat that point. This will produce a quote value that is then canceled with the splice. To evaluate the final expression eval 𝑡,
we simply reduce the term 𝑡 using the runtime dependencies
in Ω (E-Eval). At this point, Ω is fixed and will not change,
and it will just propagate down to allow E-Link to use Ω. A
reference 𝑥 to a library function typed with T-Link at level
0 will lead to 𝑥 being replaced by the compiled code fromΩ (E-Macro). We say that we “link the reference with thecompiled function”. At any other level 𝑖 ≥ 1, we simply keep
the reference to 𝑥, since it is considered a value.

∅, powCode=..., power2 =𝜆𝑥:N.𝑥∗𝑥∗1

eval power2 3Finally, we evaluate the main program:Ω∅, powCode=..., power2 =...

eval 93.2.6 Soundness. To state the progress and preservation
theorems for the 𝜆 ▲ calculus, we introduce an auxiliary relation Σ ⊩ Ω, which means that Ω is well-typed under environment Σ.
Definition 3.13. (Library Typing) Σ ⊩ Ω if and only ifdom(Σ) = dom(Ω) ∧∅ | Σ ⊢ Ω(𝑥) : Σ(𝑥) for all 𝑥 ∈ dom(Ω) and all 𝑖 ∈ N0𝑖

Using this definition, we state the soundness of the calculus
in terms of progress and preservation for programs. Again,
the full proofs can be found in Appendix B [24].
Theorem 3.14 (Progress for Programs). If Σ ⊢ 𝑝 : 𝑇 , then𝑝 is a value ⊢ 𝑝 vl or, for any Ω such that Σ ⊩ Ω, there exists
𝑝 ′ and Ω ′ such 𝑝 | Ω −→ 𝑝 ′ | Ω ′.
Theorem 3.15 (Preservation for Programs). If Σ ⊢ 𝑝 : 𝑇 ,Σ ⊩ Ω and 𝑝 | Ω −→ 𝑝 ′ | Ω ′, then for some Σ ′ ⊇ Σ, Σ ′ ⊢ 𝑝 ′ : 𝑇and Σ ′ ⊩ Ω ′.

3.2.5 Values. The definition of values in Figure 2 is kept
unchanged. We merely also add a value definition for programs ⊢ 𝑝 vl . The only program value is eval 𝑡 where 𝑡 isrequired to be a value (V-Eval).

Since we added rule T-Link, we need to revisit the lemmas
from the previous section. The Canonical Forms (Lemma 3.7)
still holds because there was no change in value definitions.
We also need to restate the various theorems and lemmas
for terms to account for libraries and library typing.

Example 3.12. The following example illustrates evaluation in the calculus. We define a library function 𝑝𝑜𝑤𝐶𝑜𝑑𝑒(implemented as in Example 3.1) as a macro taking a quoted
base 𝑥 and an exponent 𝑛 of numeric type (N); and a libraryfunction power2 using the macro with 2 as the exponent.

Theorem 3.16 (Progress for Terms). If ∅ | Σ ⊢𝑖 𝑡 : 𝑇 andΣ ⊩ Ω, then 𝑡 is a value ⊢𝑖 𝑡 vl or there exists 𝑡 ′ such 𝑡 −→𝑖Ω 𝑡 ′.

Ω

Lemma 3.17 (Extended Progress for Terms). If Γ ≥1 | Σ ⊢𝑖𝑡 : 𝑇 and Σ ⊩ Ω, then 𝑡 is a value ⊢𝑖 𝑡 vl or there exists 𝑡 ′ such𝑡 −→𝑖Ω 𝑡 ′.

∅Theorem 3.18 (Preservation for Terms). If Γ | Σ ⊢𝑖 𝑡 : 𝑇 ,𝑡 −→𝑖Ω 𝑡 ′ and Σ ⊩ Ω, then Γ | Σ ⊢𝑖 𝑡 ′ : 𝑇 .

def powCode = ⌈fix 𝜆rec:⌈N⌉→N→⌈N⌉. . . .⌉ indef power2 = ⌈𝜆𝑥:N.⌊powCode ⌈𝑥⌉ 2⌋⌉ in eval power2 3

Lemma 3.19 (Substitution). ∀𝑖, 𝑗 ∈ N0 , if Γ | Σ ⊢ 𝑗 𝑡 1 : 𝑇1
and Γ, 𝑥 : 𝑗 𝑇1 | Σ ⊢𝑖 𝑡 2 : 𝑇2 then Γ | Σ ⊢𝑖 [𝑥 ↦→ 𝑡 1 ]𝑡 2 : 𝑇2 .

First, we compile the macro definition powCode since it does
not contain any splices at level 1, storing it in Ω.
Ω∅, powCode=fix 𝜆rec: ⌈N⌉→N→ ⌈N⌉....

Most of the proofs carry through unchanged. To showpreservation we additionally need the following lemma.

def power2 = ⌈𝜆𝑥:N.⌊powCode ⌈𝑥⌉ 2⌋⌉ in eval power2 3

Lemma 3.20 (Σ-Weakening). If Σ ⊢ 𝑝 : 𝑇 and Σ ′ ⊇ Σ, thenΣ′ ⊢ 𝑝 : 𝑇

Next, we perform macro expansion and evaluate the code in
the splice of power2 .
Ω∅, powCode=fix 𝜆rec: ⌈N⌉→N→ ⌈N⌉....

3.3

def power2 = ⌈𝜆𝑥:N.⌊⌈𝑥 ∗ 𝑥 ∗ 1⌉⌋⌉ in eval power2 3

Performing splice canceling results in:ΩAnalytical Extension: Quote Matching

We now extend the calculus of Section 3.1 with support foranalytical macros. To this end, we add a pattern matching
construct that can deconstruct a piece of code into its components. Subexpressions of the code can be selectively extractedusing a bind pattern. Importantly, patterns can only matchon a subset of the language, specifically STLC+Fix. Figure 3
contains the syntax and semantics of this calculus.

∅, powCode=fix 𝜆rec: ⌈N⌉→N→ ⌈N⌉....

def power2 = ⌈𝜆𝑥:N.𝑥 ∗ 𝑥 ∗ 1⌉ in eval power2 3

As before, we compile power2 , which now does not containsplices at level 0.

116

GPCE ’21, October 17–18, 2021, Chicago, IL, USA

Nicolas Stucki, Jonathan Immanuel Brachthäuser, Martin Odersky

Extended Syntax
Terms

F

𝑡

Extended Environment
Pattern bindings. . . | 𝑡 match ⌈𝑡⌉ then 𝑡 else 𝑡 | T𝑥U𝑇𝑥𝑘 :𝑇𝐾ΦF∅ | Φ, 𝑥 ↦→ 𝑥

Extended Typing RulesΓ ⊢𝑖 𝑡𝑠 : ⌈𝑇𝑝 ⌉∅ ⊢𝑖+1 𝑡𝑝 : 𝑇𝑝 ⊣ Γ𝑡
Γ ⊢𝑖 𝑡Γ; Γ𝑡 ⊢𝑖 𝑡𝑡 : 𝑇Γ ⊢𝑖 𝑡𝑒 : 𝑇

𝑠 match ⌈𝑡𝑝 ⌉ then 𝑡𝑡 else 𝑡𝑒 : 𝑇(T-Match)Γ𝑝 ⊢𝑖 𝑐 : 𝐶 ⊣ ∅(T-Pat-Const)
Γ𝑝 ⊢𝑖 𝑡 1 : 𝑇1 →𝑇2 ⊣ Γ𝑡1

Γ𝑝 ⊢𝑖 𝑡 2 : 𝑇1 ⊣ Γ𝑡2

Γ𝑝 ⊢𝑖 𝑡 1 𝑡 2 : 𝑇2 ⊣ Γ𝑡1 ; Γ𝑡2(T-Pat-App)𝑥 :𝑖 𝑇 ∈ Γ𝑝Γ𝑝 , 𝑥 :𝑖 𝑇1 ⊢𝑖 𝑡 : 𝑇2 ⊣ Γ𝑡⊢𝑖 𝑥 : 𝑇 ⊣ ∅Γ𝑝(T-Pat-Var)Γ𝑝 ⊢𝑖 𝜆𝑥:𝑇1 .𝑡 : 𝑇1 →𝑇2 ⊣ Γ𝑡
(T-Pat-Abs)Γ𝑝 ⊢𝑖 𝑡 : 𝑇 →𝑇 ⊣ Γ𝑡

𝑥𝑘 :𝑖 𝑇𝑘 ∈ Γ𝑝

Γ𝑝 ⊢𝑖 fix 𝑡 : 𝑇 ⊣ Γ𝑡
(T-Pat-Fix)Γ𝑝 ⊢𝑖 T𝑥U𝑇𝑥𝑘 :𝑇𝐾 : 𝑇 ⊣ ∅, 𝑥 :𝑖−1 ⌈𝑇𝑘 ⌉→⌈𝑇 ⌉(T-Pat-Bind)

Extended Operational Semantics⊢1 𝑡𝑠 vl

𝑡𝑠 −→0 𝑡𝑠′

𝑡𝑠  𝑡𝑝 / 𝑡𝑡 =⇒ ∅ 𝑡𝑡′

𝑡𝑠 match ⌈𝑡𝑝 ⌉ then 𝑡𝑡 else 𝑡𝑒 −→0 𝑡𝑠′ match ⌈𝑡𝑝 ⌉ then 𝑡𝑡 else 𝑡𝑒(E-Match-Scrut)⌈𝑡𝑠 ⌉ match ⌈𝑡𝑝 ⌉ then 𝑡𝑡 else 𝑡𝑒 −→0 𝑡𝑡′(E-Match-Succ)⊢1 𝑡𝑠 vl𝑡𝑠  𝑡𝑝 / 𝑡𝑡 =⇏ ∅ 𝑡𝑡′⌈𝑡𝑠 ⌉ match ⌈𝑡𝑝 ⌉ then 𝑡𝑡 else 𝑡𝑒(E-Match-Fail)−→0 𝑡

𝑡𝑡 −→𝑖 𝑡𝑡′⊢0 𝑡𝑠 vl𝑖≥1′
𝑡𝑠 match ⌈𝑡𝑝 ⌉ then 𝑡𝑡 else 𝑡𝑒𝑠 match ⌈𝑡𝑝 ⌉ then 𝑡𝑡 else 𝑡𝑒(E-Match-Then)

−→𝑖 𝑡

𝑒

⊢0 𝑡𝑠 vl

⊢0 𝑡𝑡 vl𝑡𝑒 −→𝑖 𝑡𝑒′

𝑖≥1′
𝑡𝑠 match ⌈𝑡𝑝 ⌉ then 𝑡𝑡 else 𝑡𝑒𝑠 match ⌈𝑡𝑝 ⌉ then 𝑡𝑡 else 𝑡𝑒(E-Match-Else)−→𝑖 𝑡

𝑡𝑠1  𝑡𝑝1 / 𝑡𝑡 1 =⇒Φ 𝑡𝑡 2𝑐  𝑐 / 𝑡𝑡 =⇒Φ 𝑡𝑡(E-Pat-Const)

𝑡𝑠2  𝑡𝑝2 / 𝑡𝑡 2 =⇒Φ 𝑡𝑡 3

𝑡𝑠1 𝑡𝑠2  𝑡𝑝1 𝑡𝑝2 / 𝑡𝑡 1 =⇒Φ 𝑡𝑡 3
(E-Pat-App)

𝑡𝑠  𝑡𝑝 / 𝑡𝑡 =⇒Φ 𝑡𝑡′

𝑡𝑠  𝑡𝑝 / 𝑡𝑡 =⇒Φ,𝑥𝑝 ↦→𝑥𝑠 𝑡𝑡′

Φ(𝑥𝑝 )  𝑥𝑝 / 𝑡𝑡 =⇒Φ 𝑡𝑡(E-Pat-Var)

fix 𝑡𝑠  fix 𝑡𝑝 / 𝑡𝑡 =⇒Φ 𝑡𝑡′(E-Pat-Fix)

𝐹𝑉 (𝑡𝑠 ) ∩ range(Φ) ⊆ {Φ(𝑥𝑘 )}𝜆𝑥𝑠 :𝑇 .𝑡𝑠  𝜆𝑥𝑝 :𝑇 .𝑡𝑝 / 𝑡𝑡 =⇒Φ 𝑡𝑡′(E-Pat-Abs)𝑡𝑠′ = 𝜆𝑥𝑘′ :⌈𝑇𝑘 ⌉. [Φ(𝑥𝑘 ) ↦→ ⌊𝑥𝑘′ ⌋] ⌈𝑡𝑠 ⌉𝑡𝑠  T𝑥U𝑇𝑥𝑘 :𝑇𝐾 / 𝑡𝑡 =⇒Φ [𝑥 ↦→ 𝑡𝑠′ ]𝑡𝑡(E-Pat-Bind)
Extended Values⊢𝑖 𝑡𝑠 vl⊢𝑖 𝑡

⊢𝑖 𝑡𝑡 vl⊢𝑖 𝑡𝑒 vl𝑖≥1𝑠 match ⌈𝑡𝑝 ⌉ then 𝑡𝑡 else 𝑡𝑒 vl(V-Match)

Figure 3. Quote Pattern Match Extension
3.3.1 Syntax. The syntax of our extension is defined in
Figure 3. It extends the calculus presented in Figure 1 with
two new syntactic constructs: a pattern matching operation
𝑡𝑠 match ⌈𝑡𝑝 ⌉ then 𝑡𝑡 else 𝑡𝑒 , and a bind pattern T𝑥U𝑇𝑥𝑘 :𝑇𝐾 .
The former matches a scrutinee 𝑡𝑠 against a pattern 𝑡𝑝 . If thematch succeeds the then branch 𝑡𝑡 is evaluated, otherwise
the else branch 𝑡𝑒 is evaluated. A pattern 𝑡𝑝 may contain anyof the following language constructs: constants, references,lambdas, application, and fix operator. In addition, 𝑡𝑝 may
contain a bind pattern T𝑥U𝑇𝑥𝑘 :𝑇𝐾 , which will extract a subexpression of type 𝑇 from the quote and bind it to 𝑥. The
extracted sub-expression is locally closed under 𝑥𝑘 :𝑇𝐾 , thatis, it can only contain any of the 𝑥𝑘 as free variables. We say
the sub-expression is locally closed, since in addition to free117

Multi-stage Programming with Generative and Analytical Macros

GPCE ’21, October 17–18, 2021, Chicago, IL, USAvariables 𝑥𝑘 :𝑇𝐾 bound in the pattern, it can contain free variables defined outside of the pattern. Bind is commonly usedwithout any 𝑥𝑘 :𝑇𝐾 as T𝑥U𝑇 to match a closed subexpression.

Exactly as in pattern typing, sub-pattern matching 𝑡𝑠 
𝑡𝑝 / 𝑡𝑡 =⇒Φ 𝑡𝑡′ can match the syntactic form of STLC+Fix,
as well as bind sub-terms. Rules that do not introduce bindings in the then branch will not modify the 𝑡𝑡 /𝑡𝑡′, they will
only propagate the results from sub-evaluation. Rules E-PatConst, E-Pat-Fix, and E-Pat-App are straightforward. Interestingly, when matching a lambda, the substitution Φ will
track the relationship between the binding in the pattern andin the scrutinee (E-Pat-Abs). When matching a reference toa binding defined in the pattern, we use Φ to know the nameof the equivalent binding in the scrutinee (E-Pat-Var). We
only match if those references are equivalent under the Φ
mapping.
Finally, we have the bind pattern (E-Pat-Bind), which may
match any sub-term as long as it has the correct type andthe correct free variables. First, consider reduction, of thesimplified T𝑥U𝑇 pattern using E-Pat-Bind.

3.3.2 Typing. Typing a pattern match (T-Match) requiresthat the scrutinee of type ⌈𝑇𝑝 ⌉ will be matched against apattern of type 𝑇𝑝 . Patterns themselves are typed under adifferent typing judgment Γ𝑝 ⊢𝑖 𝑡 : 𝑇 ⊣ Γ𝑡 . Here Γ𝑝 represents
an input and contains the bindings defined within the pattern.
In contrast, Γ𝑡 represents an output and contains binding
introduced by the pattern, which is then made available in
the then branch. The pattern is typed at level 𝑖 + 1 as if it wasin a quote (as reflected by the syntax).
The rules for pattern typing mostly coincide with theirtyping counterparts. They only differ in their treatment ofenvironments. First, the Γ𝑝 environment tracks any binding
added by a lambda pattern (T-Pat-Abs). It is used to lookup
references in (T-Pat-Var) and to determine the types of freevariables in a bind pattern (T-Pat-Bind). Second, the Γ𝑡 environment collects 𝑥 bindings added by T𝑥U𝑇𝑥𝑘 :𝑇𝐾 , which will
be made available in the then branch.
The bind pattern T𝑥U𝑇𝑥𝑘 :𝑇𝐾 matches against an arbitrary
expression locally closed under 𝑥𝑘 :𝑇𝐾 . We represent thisclosed term as a curried function taking arguments of thecorresponding types 𝑇𝑘 (T-Pat-Bind). Hence, in the output
environment, we bind 𝑥 to a value of type ⌈𝑇𝑘 ⌉→⌈𝑇 ⌉. As a
special case of rule T-Pat-Bind, we match on a locally closed
sub-expression where 𝑥𝑘 :𝑇𝐾 is empty, and therefore the typeof 𝑥 is simply ⌈𝑇 ⌉. Note that the 𝑖 in this typing judgment isonly present to inform at which level 𝑥 must be added in Γ𝑡 .

𝐹𝑉 (𝑡𝑠 ) ∩ range(Φ) ⊆ ∅𝑡𝑠′ = ⌈𝑡𝑠 ⌉𝑡𝑠  T𝑥U𝑇 / 𝑡𝑡 =⇒Φ [𝑥 ↦→ 𝑡𝑠′]𝑡𝑡
In this case, the premise requires us to show that the intersection of the free variables of 𝑡𝑠 and the range of Φ is empty.
In other words, it means that 𝑡𝑠 does not contain a reference
to a binding that was defined in the scrutinee. Since it is
only locally closed, it may still have references to binding
defined outside of the pattern match as those will be valid
when inserted in the then branch (cf., rule T-Match). If thematch succeeds, rule E-Pat-Bind reduces to [𝑥 ↦→ ⌈𝑡𝑠 ⌉]𝑡𝑡 .
Now, consider the case where 𝑥𝑘 :𝑇𝐾 is not empty. This implies that we will match a 𝑡𝑠 that might contain references
to bindings defined in the pattern. In this case, we cannot
simply substitute 𝑡𝑠 for 𝑥, we first need to bind all free variables. In particular, for each free variable Φ(𝑥𝑘 ) defined in
the pattern we 𝜂-expand by creating a lambda that receives astaged argument of type 𝑥𝑘′ :⌈𝑇𝑘 ⌉. In the body of that lambda
we substitute Φ(𝑥𝑘 ) with the ⌊𝑥𝑘′ ⌋. This process results in acurried lambda of the type ⌈𝑇𝑘 ⌉→⌈𝑇 ⌉.

3.3.3 Evaluation. Once more, the operational semantics
in Figure 3 extends the operational semantics in Figure 1.
First of all, to handle quoted pattern matching, we extend
the reduction relation 𝑡 −→𝑖 𝑡 ′ with additional rules. At
staging level 0, we first evaluate the scrutinee until it is avalue (E-Match-Scrut). At all other levels, we also continue
to reduce the then (E-Match-Then) and else branches (EMatch-Else).
To model the semantics of nested patterns, we introduce
an additional reduction relation 𝑡𝑠  𝑡𝑝 / 𝑡𝑡 =⇒Φ 𝑡𝑡′. It statesthat the sub-term 𝑡𝑠 matches the sub-pattern 𝑡𝑝 with a substitution map Φ, which provides a mapping from a variable
defined in the scrutinee to one defined in the pattern. In
addition to matching, the relation also transforms the thenpart of the match 𝑡𝑡 into a 𝑡𝑡′ where all bindings defined in
the pattern are substituted.
To reduce a match operation, if the pattern matched, we
will evaluate it into 𝑡𝑡′ (E-Match-Succ) where 𝑡𝑡′ does notcontain any of the bindings defined in the pattern. We saythat a pattern (or sub-pattern) did not match if 𝑡𝑠 𝑡𝑡 / 𝑡𝑒 =⇏Φ 𝑡 ′ , that is we cannot derive a match. Therefore, if the𝑡pattern did not match we evaluate to the else branch 𝑡𝑒 (EMatch-Fail).

Example 3.21. In the following example, we show how to
perform 𝛽-reduction at level 1 using quote matching. The
code below is an encoding the HOAS pattern example ofSection 2 for a numerical type N.
𝑦:N

𝜆𝑥:⌈N⌉.𝑥 match ⌈(𝜆𝑦:N.T𝑓 UN ) T𝑧UN ⌉ then 𝑓 𝑧 else 𝑥

3.3.4 Values. The value definition in Figure 3 extends thevalue definition in Figure 1. At level 0, the pattern match
operations are evaluated away. At any other level, we need toensure transitively that sub-terms do not have any splices atlevel 1. As the pattern is not evaluated by itself it is considereda value of its own.
Example 3.22. The ability to match individually quoted
constants allows us to unlift quoted value into a value known
in the current stage. In the example, we unlift a boolean (B)118

GPCE ’21, October 17–18, 2021, Chicago, IL, USA

Nicolas Stucki, Jonathan Immanuel Brachthäuser, Martin Odersky

constant returning the value applied to succ or fail if it is nota constant.

global definitions (Section 3.2), and analytical macros (Section 3.3). From the combination of the different extensions
emerges one additional feature: the ability to pattern matchagainst global definitions. This becomes visible in Figure 4,
which adds additional typing and reduction rules for thecomposed calculus.

𝜆𝑥:B.𝜆succ:B→𝑇 .𝜆fail:𝑇 .
𝑥 match ⌈true⌉ then succ true else
𝑥 match ⌈false⌉ then succ false else fail3.3.5 Substitution. To handle the new syntactic form of
pattern matching substitution is extended to homomorphically apply substitution to its sub-terms. As patterns can only
refer to bindings defined in the pattern itself, as ensured by
Γ𝑝 , substitution does not need to go into the pattern.

3.4.1 Syntax. The syntax is simply the composition of thesyntax of the base calculus (Figure 1), of the macro extension(Figure 2), and the pattern matching extension (Figure 3).
3.4.2 Typing. Figure 4 extends the typing judgement with
one additional rule T-Pat-Link. This rule allows references
to library functions to be typed in patterns. As usual withlibrary functions, the reference can be at any level. Like in
Section 3.2, we assume that all rules are modified to pass thelibrary environment Σ through all rules of term and pattern
typing.

3.3.6 Soundness. The statements of the progress and preservation theorems carry over unchanged from Section 3.1.
Full proofs can be found in Appendix C [24]. Extending theproof of progress with a case for pattern matching is trivial;
depending on the pattern reduction, we simply invoke EMatch-Succ or E-Match-Fail. The proof of preservation
requires a few additional definitions and lemmas. First of all,we extend the substitution lemma to parallel substitutions:3.4.3 Evaluation. The operational semantics in Figure 4
extends the combined operational semantics of calculi in
Figure 2 and Figure 3. When matching a library function reference (E-Pat-Link) we match if the scrutinee is a reference
to the same library function. This pattern does not change or
use Φ in any way as it only needs to handle local variables.
All other rules are modified to add the same Ω to all terms
evaluation as previously done for terms in Section 3.2, patterns are not changed. Thus, reduction rules are of the forms
𝑡 −→𝑖Ω 𝑡 ′ for term reduction, 𝑝 | Ω −→ 𝑝 ′ | Ω ′ for program
reduction, and 𝑡𝑠  𝑡𝑝 / 𝑡𝑡 =⇒Φ 𝑡𝑡′ for pattern reduction. The
definition of values and substitution immediately arises fromthe combination of the different extensions.

Lemma 3.23 (Multi-Substitution). ∀𝑖, 𝑗 ∈ N0 , if Γ ⊢ 𝑗 𝑡𝑘 : 𝑇𝑘
and Γ, 𝑥 : 𝑗 𝑇𝑘 ⊢𝑖 𝑡 : 𝑇 then Γ ⊢𝑖 [𝑥𝑘 ↦→ 𝑡𝑘 ]𝑡 : 𝑇
Next, we state well-formedness of the substitution Φ withrespect to environments Γ𝑝 and Γ𝛿 .
Definition 3.24 (Well-formedness of Φ). Γ𝑝 | Γ𝛿 ⊩ Φ
We say Φ is well-formed with respect to Γ𝑝 and Γ𝛿 , written
Γ𝑝 | Γ𝛿 ⊩ Φ, if and only if Φ is a bijection between dom(Γ𝑝 )and dom(Γ𝛿 ), such that dom(Γ𝑝 ) ∩ dom(Γ𝛿 ) = ∅ and∀𝑥 𝑝 :1 𝑇 ∈ Γ𝑝 . Φ(𝑥 𝑝 ) :1 𝑇 ∈ Γ𝛿 .
Using Definition 3.24, we can state type preservation of
the pattern reduction. That is, reducing a well typed match𝑡𝑠  𝑝 / 𝑡 =⇒Φ 𝑡 ′ results in a well-typed term 𝑡 ′.

Example 3.27. In the following example, we show how the
combined calculus can be used to describe an optimizationof our “DSL for mathematical operations”. We match a numeric expression and check whether it is a call to our global
power DSL function defined in a library. We then unlift thequoted number using an unlift function similar to the one
in Example 3.22. The code below is an encoding of the lastversion of def powCode of Section 2 for a numerical type N.

Theorem 3.25 (Preservation of Pattern Reduction).
If (1), (2), (3), (4), (5) then Γ ⊢0 𝑡 ′ : 𝑇 .
Γ; Γ𝛿 ⊢1 𝑡𝑠 : 𝑇1

(1)

Γ𝑝 ⊢ 𝑡𝑝 : 𝑇1 ⊣ Γ𝑡

(2)

Γ; Γ𝑡 ⊢ 𝑡 : 𝑇

(3)

Φ ′

(4)

Γ𝑝 | Γ𝛿 ⊩ Φ

(5)

1

0

𝑡𝑠  𝑡𝑝 / 𝑡 =⇒ 𝑡

def powCode = ⌈fix 𝜆rec:⌈N⌉→N→⌈N⌉.
𝜆𝑒:⌈N⌉.𝜆𝑛:N.
𝑒 match ⌈power T𝑥UN T𝑚 1 UN ⌉then unlift 𝑚 1 (𝜆𝑚:N.rec 𝑥 (𝑛 + 𝑚)) 𝑒else ... // generate code
⌉ in def power4 = ⌈𝜆𝑥:N.⌊powCode ⌈power 𝑥 2⌉ 2⌋⌉ in 𝑝Here, premises (1) to (3) correspond to premises of rule TMatch. Finally, the match case in the proof of preservation
follows as a corollary from Theorem 3.25:
Corollary 3.26 (Preservation for Match).
If Γ ⊢0 ⌈𝑡𝑠 ⌉ match ⌈𝑡𝑝 ⌉ then 𝑡𝑡 else 𝑡𝑒 : 𝑇 , ⊢1 𝑡𝑠 vl and𝑡𝑠  𝑡𝑝 / 𝑡𝑡 =⇒ ∅ 𝑡𝑡′, then Γ ⊢0 𝑡𝑡′ : 𝑇 .
3.4

Full Calculus: Cross-Platform Quote Matching

3.4.4 Soundness. The proofs of progress and preservation
carry over mostly unchanged. Full proofs can be found in
Appendix D [24].

We are now ready to connect all pieces in a final calculusthat combines quotes and splices (Section 3.1), cross-platform

119

Multi-stage Programming with Generative and Analytical Macros

GPCE ’21, October 17–18, 2021, Chicago, IL, USA

Extended Typing Rules

Extended Operational Semantics
𝑥:𝑇 ∈ Σ𝑥  𝑥 / 𝑡 =⇒Φ 𝑡(E-Pat-Link)

Γ𝑝 | Σ ⊢𝑖 𝑥 : 𝑇 ⊣ ∅(T-Pat-Link)

Figure 4. Global Definition Matching Extension

4

Implementation

can be expressed in Scala as

We scaled our calculus to a practical, industrial-strength
implementation of a multi-stage macro system in the programming language Scala 3 [23].
4.1

s match { case '{ ($f: Int⇒ Int)(3) } ⇒ t; case _ ⇒ e }4.2

Relation to the Calculus

Additional Features

In addition, the implementation also supports type polymorphism, existential types in patterns, and runtime multi-stage
programming.

The static checks as performed by the type checker closely
follow the rules of the calculus as described in this paper.
The choice of syntax for quotes '{t} and for splices ${t} follows the standard syntax rules of Scala’s string interpolatorss"hello $word" or s"hello ${word}" where world is spliced in
the string. To lift or unlift values, we use the Expr(x) syntax
which corresponds to Expr.apply in expression position andto Expr.unapply in pattern position. Global library function
definition such as

Type polymorphism. Type polymorphism is expressedby using the type-class T:Type.
def one[T: Type](e: Expr[T])(using Quotes): Expr[List[T]] ='{ List($e) }The typeclass Type is necessary to know the non-erased typeof T at runtime.

def 𝑥 = ⌈𝑓 3⌉ indef 𝑦 = ⌈𝜆𝑎:N.𝑎⌉ indef 𝑧 = ⌈fix 𝜆rec:N.rec⌉ in . . .

Existential types. Existential types in patterns allow theextraction and use of types that are not statically known.

can be expressed in Scala asdef fuseMap(e: Expr[List[Int]])(using Quotes) =e matchcase '{ ($ls: List[u]).map[v]($f).map[Int]($g) } ⇒'{ $ls.map(x ⇒ $g($f(x))) }case _ ⇒ e

def x: Int = f(3)def y: Int ⇒ Int = (a: Int) ⇒ a
def z: Int = z

To support quoted pattern matching, we extend the pattern syntax to allow the pattern '{pat}. For example, theexpression
𝑠 match ⌈𝑓 T𝑥UN ⌉ then 𝑡 else 𝑒

In the example, the pattern and uses of the extracted types(u and v) can be statically checked. In general, we use lower
case letters for existential type bindings.
Runtime multi-staging. The library function run compiles and executes quoted code at runtime. This allows programmers to perform runtime multi-stage programming.

can be expressed in Scala ass match { case '{ f($x: Int) } ⇒ t; case _ ⇒ e }import scala.quoted.staging.*
given Compiler = ...
val power2 = run('{ (x: Int) ⇒ ${powCode('x, 2)} })where f is a global library reference and $x represents a
locally closed bind pattern. Free variables in bind patterns,
𝑦:N
as in T𝑥UN , can be specified as $x(y):Int. The following
term in 𝜆 ▲ that binds the body of a lambda to 𝑥 and might
have 𝑦 as a free variable

Scope extrusion detection. As Scala is not a pure functional language, we need to make sure that the expressions
are not extruded from their scope through side channels
such as mutable state, exceptions, or even into a run. For
example, we can abuse mutable state to extrude a quoted
local variable follows:𝑦:N𝑠 match ⌈𝜆𝑦:N.T𝑥UN ⌉ then 𝑡 else 𝑒

can be expressed in Scala ass matchcase '{ (y: Int) ⇒ $x(y):Int } ⇒ tcase _ ⇒ evar z: Expr[Int] = null'{ val x = 7; ${ z = '{x}; ... } }// z now contains '{x} and x will never be in scope anymore

Finally, binding an applied function in a pattern𝑠 match ⌈T𝑓 UN→N 3⌉ then 𝑡 else 𝑒

120

GPCE ’21, October 17–18, 2021, Chicago, IL, USA

Nicolas Stucki, Jonathan Immanuel Brachthäuser, Martin Odersky

Squid. Squid [16, 18], a metaprogramming library for
Scala, advances the state of the art of staging systems andputs quasiquotes at the center of user-defined optimizations.
The user can pattern match over existing code and implement retroactive optimizations modularly. To the best of ourknowledge, in an earlier version of Squid, Parreaux et al.
[16] were the first to represent locally closed terms as HOAS
functions. However, they later revisited the approach andinstead track free variables in the type. While expressive, thisapproach requires advanced typing features such as pathdependent types, singleton types, and intersection types.

To avoid this, we add runtime checks that track the stackof nested splices we are in when we create a quote. To know
if an expression is extruded from its scope, we compare thestack of the creation site with the one at the call site andreport a runtime error, if the two are not compatible. In our
implementation, all quotation functionality is provided bymeans of an implicit/contextual instance of the type Quotes,
which also serves as a representation of a persistent stack ofscopes. Each quote will use the instance that is currently inscope and each splice will introduce a new instance.

5

Discussion and Related Work

LISP. LISP has a very simple way to treat programs asdata based on the uniform representation of programs aslists. Quotation turns fragments of (unevaluated) code into
data: '42 is a number, 'a is a symbol, '(+ 3 4) is a list of thequoted constituents. Quasiquotation—with a backquote—lets
us escape inside a program fragment of e.g., a whole list witha comma operator that can unquote and evaluate a part of
the quasiquoted expression e.g., `(1 2 ,(+ 3 4)).

Modal logic. Our calculus is closely related to 𝜆 ◦ [6] and𝜆 [7]. These calculi capture the temporal/modal logic essence of multistage programming. They only support code
generation but not code analysis.
2

6

Future Work

While the calculus models separate compilation, as well as
generative and analytical macros, it does not yet fully cover
all features of our implementation in Scala 3. In particular,
two important features are type polymorphism and existential pattern types. It would be interesting to extend the calculus in future work to account for these features. However,adding them will most likely result in additional complexity
since it will require some kind of type unification.
The calculus assumes the lack of side channels, for which
we use dynamic scope extrusion detection. It is worth formalizing this mechanism and precisely describe how it canbe implemented at runtime or expressed as a static check.
Another way to extend the system would be to investigate the possibility to also allow matching on programs thatuse quotes, splices, and matches themselves. Adding patternmatching on quotes and splices seems to involve a moregeneral notion of staged eta-expansion. In order to add support for matching on the match itself is less clear and would
require some form of meta-pattern. While both extensions
are interesting, we expect the metatheory to be significantly
more involved, and thus neither of the two features is implemented in Scala 3.

Racket. Racket has a sophisticated macro system. On one
hand, contrary to Scala, Racket is dynamically-typed andon the other, Typed Racket will type-check all expressions
at the run-time phase of the given module [27]. Despite
these fundamental differences, it is worth noting that Racket
supports pattern matching with quasiquotes (quasipatterns).
Interestingly, Racket takes one step further and much like thequasiquote expression form, unquote and unquote-splicing
escape back to normal patterns which is something that we
do not support.
Multi-Stage-Programming. Multi-Stage Programming(MSP) transfers the concepts of quotes, quasiquotes, unquotes and staged evaluation [7, 10] in a statically-scoped,
modularly-type safe environment [21]. MSP, popularised
by MetaML [25] and MetaOCaml [3, 12, 13], made generative programming easier [5], effectively narrowing the gapof writing complex solutions of code manipulation such as:code optimizations [28] and DSL implementations [4, 26].
Fred McBride [15] highlights the need to bridge the gap ofexpressing computer-aided manipulation of symbols. Arguingthat it is important to lower the cognitive barrier of reading
and writing algebraic manipulators such as algebraic simplificators and integrators, he develops the first pattern matchingfacility for LISP; a form that provides a natural description toincrease the user’s problem solving potential. MacroML [9]used the quotation system of MetaML to define macros. The
two fundamental quasiquotation operators in Scala 3 were
inspired by MetaML/MacroML and BER MetaOCaml.

7

Conclusion

We introduced a calculus (𝜆 ▲ ) for well-typed and hygienic
multi-stage metaprogramming that allows both generative
and analytical macros. We proved soundness of 𝜆 ▲ and implemented it in Scala 3.

Acknowledgments

Template Haskell. Haskell was introduces to metaprogramming using quasiquotes with Template Haskell [20].
Neither MetaOCaml, MetaML, or Template Haskell support
pattern matching with quasiquotes.

We gratefully acknowledge funding by the Swiss National
Science Foundation under grant 407540_167213 (Programming Language Abstractions for Big Data).

121

Multi-stage Programming with Generative and Analytical Macros

GPCE ’21, October 17–18, 2021, Chicago, IL, USA

References[16] Lionel Parreaux, Amir Shaikhha, and Christoph E. Koch. 2017. Quoted
Staged Rewriting: A Practical Approach to Library-Defined Optimizations. SIGPLAN Not. 52, 12 (Oct. 2017), 131–145. https://doi.org/10.
1145/3170492.3136043[17] Lionel Parreaux, Amir Shaikhha, and Christoph E. Koch. 2017. Squid:Type-Safe, Hygienic, and Reusable Quasiquotes. In Proceedings of the
8th ACM SIGPLAN International Symposium on Scala (Vancouver, BC,
Canada) (SCALA 2017). Association for Computing Machinery, New
York, NY, USA, 56–66. https://doi.org/10.1145/3136000.3136005[18] Lionel Parreaux, Antoine Voizard, Amir Shaikhha, and Christoph E.
Koch. 2017. Unifying Analytic and Statically-Typed Quasiquotes. Proc.
ACM Program. Lang. 2, POPL, Article 13 (Dec. 2017), 33 pages. https://doi.org/10.1145/3158101[19] F. Pfenning and C. Elliott. 1988. Higher-Order Abstract Syntax. SIGPLAN Not. 23, 7 (June 1988), 199–208. https://doi.org/10.1145/960116.
54010[20] Tim Sheard and Simon Peyton Jones. 2002.
Template MetaProgramming for Haskell. In Proceedings of the 2002 ACM SIGPLAN
Workshop on Haskell (Pittsburgh, Pennsylvania) (Haskell ’02). Association for Computing Machinery, New York, NY, USA, 1–16. https://doi.org/10.1145/581690.581691[21] Yannis Smaragdakis, Aggelos Biboudis, and George Fourtounis. 2017.
Structured Program Generation Techniques. In Grand Timely Topics in
Software Engineering, Jácome Cunha, João P. Fernandes, Ralf Lämmel,João Saraiva, and Vadim Zaytsev (Eds.). Springer International Publishing, Cham, 154–178. https://doi.org/10.1007/978-3-319-60074-1_7[22] Nicolas Stucki, Aggelos Biboudis, Sébastien Doeraene, and Martin
Odersky. 2020. Semantics-Preserving Inlining for Metaprogramming.
In Proceedings of the 11th ACM SIGPLAN International Symposium on
Scala (Virtual, USA) (SCALA 2020). Association for Computing Machinery, New York, NY, USA, 14–24. https://doi.org/10.1145/3426426.
3428486[23] Nicolas Stucki, Aggelos Biboudis, and Martin Odersky. 2018. A Practical Unification of Multi-Stage Programming and Macros. In Proceedingsof the 17th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (Boston, MA, USA) (GPCE 2018).
Association for Computing Machinery, New York, NY, USA, 14–27.
https://doi.org/10.1145/3278122.3278139[24] Nicolas Stucki, Jonathan Immanuel Brachthäuser, and Martin Odersky.
2021. Proof of Multi-Stage Programming with Generative and Analytical
Macros. Technical Report. EPFL.
[25] Walid Taha and Tim Sheard. 1997. Multi-Stage Programming with
Explicit Annotations. SIGPLAN Not. 32, 12 (Dec. 1997), 203–217. https://doi.org/10.1145/258994.259019[26] Sam Tobin-Hochstadt, Vincent St-Amour, Ryan Culpepper, Matthew
Flatt, and Matthias Felleisen. 2011. Languages as Libraries. SIGPLAN Not. 46, 6 (June 2011), 132–141. https://doi.org/10.1145/1993316.
1993514[27] Sam Tobin-Hochstadt, Vincent St-Amour, Eric Dobson, and Asumu
Takikawa. 2021. The Typed Racket Guide - Caveats and Limitations.
[28] T Veldhuizen and E Gannon. 1998. Active libraries: Rethinking theroles of compilers and libraries. In Proc. of the 1998 SIAM Workshop:
Object Oriented Methods for Interoperable Scientific and Engineering
Computing. 286–295.

[1] Leif Andersen, Stephen Chang, and Matthias Felleisen. 2017. Super 8
Languages for Making Movies (Functional Pearl). Proc. ACM Program.
Lang. 1, ICFP, Article 30 (Aug. 2017), 29 pages. https://doi.org/10.1145/
3110274[2] Henk P. Barendregt. 1992. Lambda Calculi with Types. 117–309 pages.
[3] Cristiano Calcagno, Walid Taha, Liwen Huang, and Xavier Leroy. 2003.
Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection. In Proc. of the 2nd International Conference on Generative
Programming and Component Engineering (Erfurt, Germany) (GPCE’03). Springer-Verlag, Berlin, Heidelberg, 57–76. https://doi.org/10.
1007/978-3-540-39815-8_4[4] Krzysztof Czarnecki, John T. O’Donnell, Jörg Striegnitz, and Walid
Taha. 2004. DSL Implementation in MetaOCaml, Template Haskell, andC++. Springer Berlin Heidelberg, Berlin, Heidelberg, 51–72. https://doi.org/10.1007/978-3-540-25935-0_4[5] Krzysztof Czarnecki, Kasper Østerbye, and Markus Völter. 2002. Generative Programming. In Object-Oriented Technology ECOOP 2002 Workshop Reader, Juan Hernández and Ana Moreira (Eds.). Springer Berlin
Heidelberg, Berlin, Heidelberg, 15–29. https://doi.org/10.1007/3-54036208-8_2[6] Rowan Davies. 2017. A Temporal Logic Approach to Binding-Time
Analysis. J. ACM 64, 1, Article 1 (March 2017), 45 pages. https://doi.org/10.1145/3011069[7] Rowan Davies and Frank Pfenning. 2001. A Modal Analysis of Staged
Computation. J. ACM 48, 3 (May 2001), 555–604. https://doi.org/10.
1145/382780.382785[8] Matthew Flatt. 2002. Composable and Compilable Macros: You Want
It When? SIGPLAN Not. 37, 9 (Sept. 2002), 72–83. https://doi.org/10.
1145/583852.581486[9] Steven E. Ganz, Amr Sabry, and Walid Taha. 2001. Macros as
Multi-Stage Computations: Type-Safe, Generative, Binding Macros in
MacroML. SIGPLAN Not. 36, 10 (Oct. 2001), 74–85. https://doi.org/10.
1145/507669.507646[10] Ulrik Jørring and William L. Scherlis. 1986. Compilers and Staging
Transformations. Association for Computing Machinery, New York,NY, USA, 86–96. https://doi.org/10.1145/512644.512652[11] Oleg Kiselyov. 2014. The Design and Implementation of BER MetaOCaml. In Functional and Logic Programming, Michael Codish and Eijiro Sumii (Eds.). Springer International Publishing, Cham, 86–102.
https://doi.org/10.1007/978-3-319-07151-0_6[12] Oleg Kiselyov. 2018. Reconciling Abstraction with High Performance:
A MetaOCaml approach. Foundations and Trends® in Programming
Languages 5, 1 (2018), 1–101. https://doi.org/10.1561/2500000038[13] Oleg Kiselyov and Chung-chieh Shan. 2010. The MetaOCaml files Status report and research proposal. In ACM SIGPLAN Workshop on
ML.
[14] Yannis Lilis and Anthony Savidis. 2019. A Survey of Metaprogramming
Languages. ACM Comput. Surv. 52, 6, Article 113 (Oct. 2019), 39 pages.
https://doi.org/10.1145/3354584[15] Fred McBride. 1970. Computer Aided Manipulation of Symbols. Ph.D.
Dissertation. Queen’s University of Belfast.

122