Proto-Quipper with Dynamic Lifting
PENG FU, Dalhousie University, Canada
KOHEI KISHIDA, University of Illinois at Urbana-Champaign, USA
NEIL J. ROSS, Dalhousie University, Canada
PETER SELINGER, Dalhousie University, Canada
Quipper is a functional programming language for quantum computing. Proto-Quipper is a family of languages
aiming to provide a formal foundation for Quipper. In this paper, we extend Proto-Quipper-M with a constructcalled dynamic lifting, which is present in Quipper. By virtue of being a circuit description language, ProtoQuipper has two separate runtimes: circuit generation time and circuit execution time. Values that are known
at circuit generation time are called parameters, and values that are known at circuit execution time are calledstates. Dynamic lifting is an operation that enables a state, such as the result of a measurement, to be liftedto a parameter, where it can influence the generation of the next portion of the circuit. As a result, dynamic
lifting enables Proto-Quipper programs to interleave classical and quantum computation. We describe thesyntax of a language we call Proto-Quipper-Dyn. Its type system uses a system of modalities to keep trackof the use of dynamic lifting. We also provide an operational semantics, as well as an abstract categoricalsemantics for dynamic lifting based on enriched category theory. We prove that both the type system and theoperational semantics are sound with respect to our categorical semantics. Finally, we give some examples ofProto-Quipper-Dyn programs that make essential use of dynamic lifting.
CCS Concepts: • Theory of computation → Type theory; Program semantics.
Additional Key Words and Phrases: Quipper, Proto-Quipper, quantum programming languages, dynamic
lifting, categorical semantics
ACM Reference Format:
Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger. 2023. Proto-Quipper with Dynamic Lifting. Proc. ACM
Program. Lang. 7, POPL, Article 11 (January 2023), 26 pages. https://doi.org/10.1145/3571204

1 INTRODUCTION
1.1 Quipper and Proto-Quipper
Quipper is a functional programming language for quantum computing [Green et al. 2013a,b]. The
overall aim of Quipper is to allow quantum algorithms to be specified at a level of abstraction thatis similar to how the algorithm might be described in a research paper, and to compile this down
to the level of individual quantum gates, producing a logical quantum circuit. Quipper has beenused to program a set of nontrivial algorithms from the quantum computing literature, and it has
been used to generate quantum circuits consisting of trillions of gates. As a circuit description
language, Quipper shares some of the traits of hardware description languages. In particular, it
has two notions of runtime: The first of these is circuit generation time. This is when a Quipper
program is run to generate a quantum circuit. The second is circuit execution time. This is when aquantum circuit is executed by a quantum computer or a simulator.
Authors’ addresses: Peng Fu, Dalhousie University, Canada, frank-fu@dal.ca; Kohei Kishida, University of Illinois at UrbanaChampaign, USA, kkishida@illinois.edu; Neil J. Ross, Dalhousie University, Canada, neil.jr.ross@dal.ca; Peter Selinger,
Dalhousie University, Canada, selinger@mathstat.dal.ca.

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
© 2023 Copyright held by the owner/author(s).
2475-1421/2023/1-ART11
https://doi.org/10.1145/3571204
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

11

11:2

Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger

Quipper is a practical language, implemented as an embedded language in Haskell. As such,it lacks formal foundations such as operational and denotational semantics. This motivates thedevelopment of Proto-Quipper, a family of experimental languages that aim to provide formal
semantics for fragments of Quipper. Proto-Quipper-S features a linear type system with subtyping
as well as an operational semantics [Ross 2015]. Proto-Quipper-M has a linear type system without
subtyping, but with a sound categorical semantics in addition to its operation semantics [Rios andSelinger 2018]. More recently, Proto-Quipper-D was introduced, which features a type system withlinear dependent types as well as a fibrational categorical semantics [Fu et al. 2020b,a].
1.2 Dynamic Lifting and the Interaction of the Two Runtimes
Proto-Quipper, like Quipper, distinguishes two runtimes. Moreover, Proto-Quipper gives a formal
account of parameters and states. A parameter is a value that is known at circuit generation time,such as a boolean value for an if-then-else expression. A state is a value that is only known at circuit
execution time, such as the actual state of a qubit or classical bit in a circuit. The type system ofProto-Quipper reflects this distinction. Among the types, there is a subset of parameter types, suchas Nat and Bool, whose elements can be duplicated and discarded. There is also a subset of statetypes, such as Qubit and Bit, which are linear so that their elements cannot in general be duplicatedor discarded. One of the fundamental design decisions of Proto-Quipper is that parameter types
and state types belong to the same universe of types, so that one can form compound types thatare part parameter and part state. An example of this is the type Bool ⊗ Qubit, whose elements arepairs of a boolean (a parameter) and a qubit (a state). Another example is the type of lists of qubits.
Here, the length of the list is a parameter (known at circuit generation time), but the actual qubits
in the list are states (known at circuit execution time). In this way, Proto-Quipper differs, e.g., from
QWire, an embedded quantum circuit description language in which parameters and states belong
to separate universes [Paykin et al. 2017].
In Quipper, the two runtimes can interact with each other. A priori, it is clear that states candepend on parameters. For example, we can initialize a qubit based on a boolean parameter, simply
by inserting a gate at circuit generation time to initialize the qubit in one state or another. The
opposite direction is more complicated. Usually, circuit execution happens after circuit generation,and in this case, it is clear that a state cannot be converted to a parameter. However, there are somequantum algorithms that require circuit generation and circuit execution to be interleaved. Here, astate, such as the outcome of a measurement in a circuit, may be used to inform the generationof the next part of the circuit. To enable such interleaving, Quipper provides a construct called
dynamic lifting, which enables a state to be lifted to a parameter in certain situations. For example,
dynamic lifting permits the result of a measurement, which is a state of type Bit, to be lifted to aparameter of type Bool. It is important to note that dynamic lifting is an expensive operation, as it
requires control to pass from circuit evaluation time back to circuit generation time. This requires
the real-time quantum computer to put all of its active qubits into long-term storage while spending
an indeterminate amount of time awaiting further instructions from the classical computer incharge of circuit generation.
Dynamic lifting is important because it can be used to express quantum algorithms that requireinterleaving circuit execution time and circuit generation time. While there are many quantum
algorithms that do not require such interleaving, there are some that do. An example is magic state
distillation [Bravyi and Kitaev 2005]. Here, the goal is to prepare a qubit in some target state. We
start with a large number of qubits, say 𝑛 of them, each of which is a rough approximation of thetarget state. We then apply a probabilistic łdistillationž procedure which yields on average, say,𝑛/4 qubits that are better approximations of the target state; the remaining qubits are wasted. By
repeated distillation steps, we eventually wind up with a small number of qubits that are excellent
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

Proto-Quipper with Dynamic Lifting

11:3

approximations of the target state. In such a situation, dynamic lifting is essential because after
each distillation step, we must throw away the wasted qubits, but we do not know ahead of time
which ones (or indeed, how many) there will be. Thus which future gates will be applied depends
on the outcomes of previous measurements. With the help of dynamic lifting, these algorithms canbe naturally expressed as functions in the programming language.
The concept of dynamic lifting is different from measurement, and the two should not be confused.
Measurement is merely a gate in a circuit, turning a quantum bit (a state) into a classical bit (also astate). Dynamic lifting is an operation of the programming language, turning a classical bit (a state)
into a boolean (a parameter).
1.3

A Type System for Dynamic Lifting

Previous versions of Proto-Quipper lacked dynamic lifting. Modeling dynamic lifting is a challenging
problem. To better understand the issues involved, it is useful to know that there are two things
that can be done with circuits in Proto-Quipper. On the one hand, circuits can be run on a quantum
device. On the other hand, circuits can be boxed. A boxed circuit is a data structure that contains acircuit that has already been generated, i.e., an actual list of gates, rather than merely instructions for
how to generate such a list. As a result, a boxed circuit can be used as a building block for all kinds ofthings. In the simplest case, it can be re-used in the construction of other circuits. But it can also beinspected and manipulated in other ways, such as by applying gate transformations (systematicallyreplacing gates by other gates), by adding things like error correction, or by rewriting the circuit tosimplify it, among many other possibilities. Boxed circuits can also be reversed, which is used inmany quantum algorithms, for example to uncompute ancillas. The ability to box circuits is crucial
to Quipper’s ability to express algorithms at a natural level of abstraction, because algorithms areoften described in terms of meta-operations on circuits.
Now it is clear that dynamic lifting only makes sense in the context of a circuit that is actually
being executed, rather than one that is merely being boxed. We will keep track of this in the
programming language by adding a modality to the type system and a corresponding monad to thesemantics. The modality should be thought of as denoting łboxabilityž. For example, a functionof type Qubit ⊸1 Qubit represents a circuit that can be boxed or executed, i.e., that does not use
dynamic lifting, whereas a function of type Qubit ⊸0 Qubit represents a quantum operation thatcan only be executed but not boxed.
Before we can describe the operational or denotational semantics of Proto-Quipper-Dyn, wemust be more precise about what we mean by a łcircuitž. We must also specify what it means tołexecutež a circuit. There are many different notions of circuits, differing, for example, in whichcollection of gates is provided. Rather than specializing to one of these, we take a more generalpoint of view: a circuit is simply a morphism in a small symmetric monoidal category M, which we
assume to be given ahead of time, but otherwise arbitrary (subject to some properties). Similarly,
for the execution of circuits, we assume given another small symmetric monoidal category Q ofquantum operations. Conceptually, the morphisms of M are syntactic entities; thus, M is typically acategory that is free generated (say by a collection of gates). On the other hand, we think of themorphisms of Q as physical operations, which can be performed on a quantum computer. The
categories M and Q have the same objects, and there is a symmetric monoidal interpretation functor
𝐽 : M → Q.
Operationally, dynamic lifting is an operation that reads the state of a bit in Q, and returns aboolean value. Since a bit state can be the result of a measurement, the read operation for dynamic
lifting is nondeterministic, i.e., it can return different boolean values with probabilities governedby measurements. The nondeterministic nature of the dynamic lifting suggests that it should bemodeled as a monadic operation [Moggi 1991].
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

11:4

Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger

We therefore conceptualize the types of Proto-Quipper-Dyn as the objects of a single category
A, with a monad 𝑇 : A → A, called the dynamic lifting monad. This will be done in such a way that
M is fully embedded in A, and Q is fully embedded in the Kleisli category 𝐾𝑙𝑇 (A), in a way thatmakes the following diagram commute.
𝜓

M
𝐽

Q

A
𝐸

𝜙

𝐾𝑙𝑇 (A)

Here, 𝐽 is the given interpretation functor, and 𝐸 is the canonical functor from A to 𝐾𝑙𝑇 (A). We
then model dynamic lifting as a map dynlift : Bit → 𝑇 Bool ∈ 𝐾𝑙𝑇 (A) such that the following
diagram commutes.
Bit
init

dynlift𝜂Bool
𝑇 BoolNote that dynamic lifting is a morphism of the Kleisli category; this makes sense because it isessentially a side-effecting read operation. More generally, any computation that potentially uses
dynamic lifting will have type 𝐴 → 𝑇 𝐵.
As mentioned above, our type system must also distinguish quantum circuits that are being
executed from quantum circuits that are being boxed. Naturally, since the latter may not use
dynamic lifting, they are maps in the category A while the former are maps in the Kleisli category
𝐾𝑙𝑇 (A). As a practical matter for programmer convenience, it would be awkward to have 𝑇 as an
explicit type constructor that must be mentioned everywhere in the program. Instead, we use asystem of modalities to keep track of the dynamic lifting monad 𝑇 . More specifically, we annotatea typing judgment with a modality, i.e., Γ ⊢𝛼 𝑀 : 𝐴, where 𝛼 ∈ {0, 1}. When 𝛼 = 0, it means thatthe term 𝑀 represents a morphism JΓK → 𝑇 J𝐴K in the Kleisli category 𝐾𝑙𝑇 (A). When 𝛼 = 1, itmeans that the term 𝑀 represents a morphism JΓK → J𝐴K in A. An example of the typing rule fordynamic lifting is the following (where Meas : Qubit → Bit represents the measurement gate).
ℓ : Qubit ⊢1 Meas(ℓ) : Bitℓ : Qubit ⊢0 dynlift(Meas(ℓ)) : BoolIf we have a quantum circuit Qubit → Bit, it can be run by a quantum computer and the measurement result of type Bit will be lifted to a parameter of type Bool. Note that the dynlift operation
sets the modality of the typing judgment to 0, and as a result, we have a map Qubit → 𝑇 Bool in
the Kleisli category. The use of modalities in our type system ensures that the term Meas(ℓ) can beturned into a boxed circuit, whereas it will be a compile time typing error to try to box the term
dynlift(Meas(ℓ)).
1.4

Operational Semantics

Next, let us take a look at the operational semantics of Proto-Quipper-Dyn. In previous versions ofProto-Quipper, the operational semantics used configurations of the form (C, 𝑀), where C is thecircuit being currently constructed, and 𝑀 is a term. On the other hand, in the quantum lambda
calculus [Selinger and Valiron 2009], which is not a circuit construction language but intended torun directly on a quantum computer, the operational semantics used configurations of the form
(𝑄, 𝑀), where 𝑄 is the current quantum state and 𝑀 is a term.
In a sense, Proto-Quipper-Dyn is a combination of these prior languages: it is a language for circuit
construction (via the boxing operation), but it is also a language for running quantum operations
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

Proto-Quipper with Dynamic Lifting

11:5(as otherwise dynamic lifting would not be possible). Consequently, our operational semantics uses
both kinds of configurations: those of the form (𝑄, 𝑀) are only used for top-level computations
that actually run on a quantum device, and those of the form (C, 𝑀) are used during boxing. These
two kinds of configurations correspond closely to the two runtimes, since configuration of the form
(C, 𝑀) are used for circuit construction and those of the form (𝑄, 𝑀) are used for circuit execution.
They also correspond to the two categories M and Q.
Consequently, the evaluation rules take two different forms. Evaluation at circuit generation
time takes the form (C, 𝑀) ⇓ (C ′, 𝑉 ), where C is a circuit. The type system ensures that such anevaluation does not involve dynamic lifting, so it can be done entirely with a classical computer
and the evaluation Í
is deterministic. On the other hand, evaluation at circuit execution time takes
the form (𝑄, 𝑀) ⇓ 𝑖 𝑝𝑖 (𝑄𝑖 , 𝑉𝑖 ), where 𝑄 represents a quantum state. Since 𝑀 can use dynamic
lifting, the result of such an evaluation rule is probabilistic, with outcome (𝑄𝑖 , 𝑉𝑖 ) happening withprobability 𝑝𝑖 .
1.5

Related Work

A common misunderstanding is that dynamic lifting means performing measurements during theexecution of a quantum program. That would not be a new feature; indeed, the ability to perform
on-the-fly measurements was already present in the earliest quantum programming languages, suchas [Ömer 1998; Selinger 2004; Selinger and Valiron 2009]. Rather, dynamic lifting is an operationthat only makes sense in the context of a circuit description language, where circuits are not executedduring the circuit generation phase. Dynamic lifting is the transfer of information from the circuit
execution environment back to the circuit generation environment. Therefore, in the following
discussion of related work, we do not include comparisons with most papers on languages that
include measurement but do not have separate circuit generation and circuit execution times.
One of the features of the present work, and of Proto-Quipper in general, is that it works with thestandard notion of quantum circuits [Nielsen and Chuang 2002], which are basically lists of gates,or more precisely, gates that have been composed using the laws of symmetric monoidal categories.
By contrast, some of the other notions of dynamic lifting that appear in the literature not only add
features to the programming language, but also to the generated circuits themselves. Relatedly,
one of the features that makes boxed circuits useful in Proto-Quipper is that they are actual data
structures. Here, by a łdata structurež, we mean data that can be queried, for example via a casedistinction or pattern matching. This is different from a łthunkž, such as a lambda abstraction,
which represents a suspended computation. Some of the alternative notions of dynamic liftingthat appear in the literature make dynamic lifting part of the circuit language, allowing circuits
containing dynamic lifting to be boxed. This turns circuits into thunks.
In recent work, [Lee et al. 2021] extended Proto-Quipper with a version of dynamic lifting. They
work with a single runtime modeled by a category of quantum channels, which are generalizationsof quantum circuits with a notion of branching for measurement results. A quantum channel is
a list of gates like a quantum circuit, with the important exception that if the current gate is ameasurement, the list has two tails, one for each possible measurement outcome. Consequently,
the channels of Lee et al. must either be implemented as thunks, or as data structures that are
exponentially large. The main difference with our work is that in our setting, dynamic lifting
ensures that boxed circuits are data structures that contain only one branch (namely, the one
corresponding to the actual measurement result when the circuit is run), whereas in Lee et al.’ssetting, either all branches are evaluated, or the circuit is a thunk.
Another version of Proto-Quipper incorporating a form of dynamic lifting was proposed by[Colledan and Dal Lago 2022]. Their language uses a very general version of dynamic lifting, whichis even more general than the one present in the Quipper language, and allows for measurements
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

11:6

Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger

to be conditional on the outcomes of prior measurements. As a consequence, the output typeof their circuit can depend on the outcomes of the measurements specified in the computation.
They also work with a single runtime where dynamic lifting is part of their generalized notion ofquantum circuits. While this alternative notion of dynamic lifting is interesting in its own right,
their language does not come equipped with a denotational semantics.
QWire [Paykin et al. 2017] is a quantum programming language that also supports dynamic lifting.
QWire has a host language and a circuit language. The host language describes the computationof the classical computer, while the circuit language describes the computation of the quantum
computer. QWire has a denotational semantics for the circuit language, but not for the host language.
Dynamic lifting is part of the syntax in the circuit language. Therefore QWire’s notion of quantum
circuits differs from Proto-Quipper’s notion. Besides dynamic lifting, QWire also has a notionof static lifting in the form of a łrunž function. This allows measuring all the qubits in a circuit,returning boolean values to the host language, without leaving any unmeasured quantum state. By
contrast, Proto-Quipper-Dyn does not require a run function, since it does not have separate hostand circuit languages. All circuits that are not constructed inside a box are automatically executed,
and dynamic lifting can be used to bring measurement results into the control flow of the language.
We use enriched category theory to describe our categorical model for dynamic lifting. There
are some existing works that also use enriched categories in the context of quantum programming
languages. For example, [Lindenhovius et al. 2018] use CPO-enrichment to model a version ofProto-Quipper-M with recursion. The main difference between our model and that of Lindenhovius
et al. is that our model accounts for dynamic lifting while their model accounts for recursion.
[Rennela and Staton 2020] give a categorical model for a QWire-like language that also uses
enriched categories. Their language allows boxing a circuit that uses dynamic lifting, which is quite
different from how boxing works in Proto-Quipper. As a result, circuits in their setting are thunks
and not data structures. Also, in Rennela and Staton’s EWire language, the host language does notinclude wire types such as a type of qubits, whereas Proto-Quipper does not have separate hostand circuit languages, and includes all types in a single language. Consequently, Proto-Quipper hasa linear type system, whereas the EWire host language does not. This difference is also reflectedin the model: in Rennela and Staton’s semantics, programs are interpreted in a cartesian-closed
category, whereas in our model, they are interpreted in a monoidal category.
The fact that Proto-Quipper has two distinct runtimes (circuit generation time and circuit
execution time) suggests a possible connection to another computational paradigm that also has
multiple runtimes, namely multi-staged computation [MetaOCaml 2020; Taha and Sheard 2000].
However, there are some important differences. One of them is that multi-staged computation,such as in MetaML [Taha and Sheard 2000], deals with potentially many levels, but all of the levels
share the same operations and the same hardware; the primary purpose of staging is to precisely
orchestrate the order in which operations are evaluated. On the other hand, the main purpose of
dynamic lifting in Proto-Quipper is to interleave computations from two different hardware models.
The łmeta-languagež of Proto-Quipper terms has almost nothing in common with the łobject
languagež of circuits. Each of the two stages has its own distinct operations: classical expressions
and control flow for the meta-language, and gates and measurements for the object language. In
particular, quantum circuits are not just code for expressions of the meta-language.
Finally, we will mention the quantum programming language Silq [Bichsel et al. 2020]. Like
Proto-Quipper-Dyn, Silq also uses modalities to keep track of the use of certain operations. For
example, the modality łmfreež in Silq is used to indicate whether a computation uses measurement.
The difference is that Silq is not a circuit description language, so it does not have a notion of boxed
circuits or dynamic lifting.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

Proto-Quipper with Dynamic Lifting

1.6

11:7

Contributions

In this paper, we describe the syntax and type system of an extension of Proto-Quipper withdynamic lifting, called Proto-Quipper-Dyn. The type system uses a system of modalities to keep
track of the use of dynamic lifting. We also provide an operational semantics, using two different
kinds of configurations to model circuit generation time and circuit execution time. We further
provide an abstract categorical semantics for this language, in which dynamic lifting is modeledby a map Bit → 𝑇 Bool, where 𝑇 is a monad encapsulating circuit execution. By an łabstractž
categorical semantics, we mean that we only state the properties that a categorical model mustsatisfy to give a sound interpretation of the language, without constructing an actual concrete
example of such a model. We give such a concrete model in a companion paper [Fu et al. 2022a].
The rest of the paper is organized as follows: In Section 2, we briefly recall the basics of enrichedcategory theory, and then we give an axiomatization of a general categorical semantics for dynamic
lifting. In Section 3, we define a type system for dynamic lifting that uses a system of modalities. We
then show how a typing judgment with modalities is interpreted as a morphism in our categoricalmodel. In Section 4, we define a call-by-value big-step operational semantics for our language.
We show that the operational semantics satisfies type preservation and that the type systemguarantees error freeness. We also show that the operational semantics is sound with respect tothe enriched categorical semantics. In Section 5, we give some applications of dynamic lifting inProto-Quipper-Dyn. We finish the paper with some concluding remarks in Section 6.
2 AN ENRICHED CATEGORICAL SEMANTICS FOR DYNAMIC LIFTING
In this section we will give a general categorical semantics for dynamic lifting. Our categoricalsemantics is based on enriched categories, which are generalizations of ordinary categories. In
enriched categories, instead of hom-sets, one works with hom-objects, which are objects in a
monoidal category.
Definition 2.1. Let V be a monoidal category. A V-enriched category A (or V-category for short)
is given by the following:• A class of objects, also denoted A.
• For any 𝐴, 𝐵 ∈ A, an object A(𝐴, 𝐵) in V.
• For any 𝐴 ∈ A, a morphism in 𝑢𝐴 : 𝐼 → A(𝐴, 𝐴) in V, called the identity on 𝐴.
• For any 𝐴, 𝐵, 𝐶 ∈ A, a morphism 𝑐 𝐴,𝐵,𝐶 : A(𝐴, 𝐵) ⊗ A(𝐵, 𝐶) → A(𝐴, 𝐶) in V, called composition.
• The composition and identity morphisms must satisfy suitable diagrams in V (see [Borceux
1994; Kelly 1982]).
Remarks.
• Many concepts from non-enriched category theory can be generalized to theenriched setting. For example, V-functors, V-natural transformations, V-adjunctions andthe V-Yoneda embedding are all straightforward generalizations of their non-enrichedcounterparts. We refer to [Borceux 1994; Kelly 1982] for comprehensive introductions.
• In the rest of this paper, when we speak of a map 𝑓 : 𝐴 → 𝐵 in a V-enriched category A,
we mean a morphism of the form 𝑓 : 𝐼 → A(𝐴, 𝐵) in V. Furthermore, when 𝑔 : 𝐵 → 𝐶 is
another map in A, we write 𝑔 ◦ 𝑓 : 𝐴 → 𝐶 as a shorthand for𝑓 ⊗𝑔𝑐

𝐼 −−−→ A(𝐴, 𝐵) ⊗ A(𝐵, 𝐶) →− A(𝐴, 𝐶).

• A V-enriched category A gives rise to an ordinary category 𝑉 (A), called the underlying
category 1 of A, where the objects of 𝑉 (A) are objects of A and a hom-set is defined as

1𝑉 stands for łunderlyingž because the letter 𝑈 serves another purpose in this paper.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

11:8

Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger

𝑉 (A)(𝐴, 𝐵) := V (𝐼, A(𝐴, 𝐵)) for any 𝐴, 𝐵 ∈ 𝑉 (A). Similarly, a V-functor 𝐹 : A → B gives
rise to an ordinary functor 𝑉 𝐹 : 𝑉 (A) → 𝑉 (B) and a V-natural transformation 𝛼 : 𝐹 → 𝐺
gives rise to an ordinary natural transformation 𝑉 𝛼 : 𝑉 𝐹 → 𝑉 𝐺.
Ordinary symmetric monoidal categories can be generalized to enriched categories as well.
Definition 2.2. Let V be a symmetric monoidal category. A V-category A is symmetric monoidal
if it is equipped with the following:• There is an object 𝐼 ∈ A called the tensor unit. For any 𝐴, 𝐵 ∈ A, there is an object 𝐴 ⊗ 𝐵 ∈ A.
Moreover, for any 𝐴1, 𝐴2, 𝐵 1, 𝐵 2 ∈ A, there is a morphism
Tensor : A(𝐴1, 𝐵 1 ) ⊗ A(𝐴2, 𝐵 2 ) → A(𝐴1 ⊗ 𝐴2, 𝐵 1 ⊗ 𝐵 2 )in V. The tensor product is a bifunctor in the sense that Tensor◦ (𝑢𝐴 ⊗𝑢𝐵 ) = 𝑢𝐴⊗𝐵 for the identity maps 𝑢𝐴 , 𝑢𝐵 , 𝑢𝐴⊗𝐵 , and the following diagram commutes for any 𝐴1, 𝐴2, 𝐵 1, 𝐵 2, 𝐶 1, 𝐶 2 ∈ A.
A(𝐴1, 𝐵 1 ) ⊗ A(𝐴2, 𝐵 2 ) ⊗ A(𝐵 1, 𝐶 1 ) ⊗ A(𝐵 2, 𝐶 2 )𝑐 ⊗𝑐A(𝐴1, 𝐶 1 ) ⊗ A(𝐴2, 𝐶 2 )Tensor⊗Tensor

TensorA(𝐴1 ⊗ 𝐴2, 𝐵 1 ⊗ 𝐵 2 ) ⊗ A(𝐵 1 ⊗ 𝐵 2, 𝐶 1 ⊗ 𝐶 2 )𝑐

A(𝐴1 ⊗ 𝐴2, 𝐶 1 ⊗ 𝐶 2 )• There are the following V-natural isomorphisms in A and they satisfy the same coherence
diagrams for symmetric monoidal categories.
𝑙𝐴 : 𝐼 ⊗ 𝐴 → 𝐴
𝑟𝐴 : 𝐴 ⊗ 𝐼 → 𝐴

𝛾𝐴,𝐵 : 𝐴 ⊗ 𝐵 → 𝐵 ⊗ 𝐴

𝛼𝐴,𝐵,𝐶 : (𝐴 ⊗ 𝐵) ⊗ 𝐶 → 𝐴 ⊗ (𝐵 ⊗ 𝐶)
If the V-category A is symmetric monoidal, then its underlying category 𝑉 (A) is symmetricmonoidal. For any maps 𝑓 : 𝐴1 → 𝐵 1, 𝑔 : 𝐴2 → 𝐵 2 in A, we write the map 𝑓 ⊗𝑔 : 𝐴1 ⊗ 𝐴2 → 𝐵 1 ⊗ 𝐵 2
as a shorthand for the following composition.
𝑓 ⊗𝑔Tensor𝐼 −−−→ A(𝐴1, 𝐵 1 ) ⊗ A(𝐴2, 𝐵 2 ) −−−−−→ A(𝐴1 ⊗ 𝐴2, 𝐵 1 ⊗ 𝐵 2 )2.1

An Axiomatization of Enriched Categorical Models of Dynamic Lifting

In the following, we assume V to be a cartesian closed category with coproducts. For any 𝐴, 𝐵 ∈ V,
we write 𝐴 × 𝐵 for the cartesian product, 𝐴 ⇒ 𝐵 for the exponential object, and 1 ∈ V for theterminal object. Since V is cartesian closed, it is self-enriched, i.e., V is a V-category where thehom-objects are defined by V (𝐴, 𝐵) := 𝐴 ⇒ 𝐵.
We will now focus on defining a V-enriched category A that models dynamic lifting. We givea sequence of definitions that specify a sequence of properties (a)-(h), which will culminate in
Definition 2.8 of a model for Proto-Quipper with dynamic lifting.
Definition 2.3. A V-category A is a linear-non-linear programming language model if(a) A has coproducts and is symmetric monoidal closed, i.e., it is symmetric monoidal and there
is a V-adjunction − ⊗ 𝐴 ⊣ 𝐴 ⊸ − for each 𝐴 ∈ A.
(b) A is equipped with a V-adjunction
𝑝 :V→A⊣♭:A→V
such that 𝑝 is a strong monoidal V-functor.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

Proto-Quipper with Dynamic Lifting

11:9

Remarks.
• The requirement that A has coproducts and is symmetric monoidal closed implies
that it can model function types and sum types in a functional programming language.
Moreover, since − ⊗ 𝐴 is a left adjoint V-functor for any 𝐴 ∈ A, it preserves the coproducts,
so the tensor products distribute over coproducts in A.
• The adjunction in (b) is often called a linear-non-linear adjunction [Benton 1995]. Here, theassumption that 𝑝 is a strong monoidal V-functor means that there exist isomorphisms
𝑒 : 𝐼 → 𝑝1 and 𝑚 : 𝑝𝑋 ⊗ 𝑝𝑌 → 𝑝 (𝑋 × 𝑌 ) making some diagrams commute (see [Fu et al.
2022b, Appendix A]).
• Since 𝑝 is strong monoidal and V is cartesian, for any 𝑋 ∈ V, there are maps discard𝑋 :𝑝𝑋 → 𝐼 and dup𝑋 : 𝑝𝑋 → 𝑝𝑋 ⊗ 𝑝𝑋 in A. Moreover, for any map 𝑓 : 𝑋 → 𝑌 in V, we havethe following in A.
dup𝑌 ◦ 𝑝 𝑓 = (𝑝 𝑓 ⊗ 𝑝 𝑓 ) ◦ dup𝑋
We call objects of the form 𝑝𝑋 ∈ A parameter objects, since they can be duplicated anddiscarded. For example, Bool := 𝐼 + 𝐼  𝑝1 + 𝑝1  𝑝 (1 + 1) is a parameter object.
• For any 𝑋 ∈ V, 𝐵 ∈ A, we write 𝛿 for the isomorphism 𝛿 : A(𝑝𝑋, 𝐵)  V (𝑋, ♭𝐵), and force𝐵
for the counit force𝐵 : 𝑝♭𝐵 → 𝐵.

Definition 2.4. A convex space is a set 𝑋 equipped with a convex sum operation, which assigns
to any 𝑥, 𝑦 ∈ 𝑋 and 𝑝, 𝑞 ∈ [0, 1] such that 𝑝 + 𝑞 = 1 an element 𝑝𝑥 + 𝑞𝑦 ∈ 𝑋 , subject to certain
standard conditions, which are detailed in [Fu et al. 2022b, Appendix B]. A category is enrichedin convex spaces if each hom-set is equipped with the structure of a convex space, and moreover,composition is bilinear with respect to convex sum, i.e., (𝑝 𝑓 + 𝑞𝑔) ◦ ℎ = 𝑝 (𝑓 ◦ ℎ) + 𝑞(𝑔 ◦ ℎ) andℎ ◦ (𝑝 𝑓 + 𝑞𝑔) = 𝑝 (ℎ ◦ 𝑓 ) + 𝑞(ℎ ◦ 𝑔).
As mentioned in the introduction, Proto-Quipper-Dyn is parameterized by two (ordinary) small
categories M and Q of circuits and quantum operations, respectively. We now specify the properties
that these categories must satisfy.

Assumption 2.5. We assume that we are given two small symmetric monoidal categories M andQ, satisfying the following properties:(1) M and Q have the same objects, including a distinguished object called Bit. The category M
has distinguished morphisms zero, one : 𝐼 → Bit.
(2) Q has a coproduct Bit = 𝐼 + 𝐼 , and the tensor product in Q distributes over this coproduct.
(3) There exists a given strict symmetric monoidal functor 𝐽 : M → Q that is the identity on
objects and 𝐽 (zero) = inj1 : 𝐼 → 𝐼 + 𝐼, 𝐽 (one) = inj2 : 𝐼 → 𝐼 + 𝐼 . We call 𝐽 the interpretation
functor.
(4) The category Q is enriched in convex spaces.
(5) For any 𝐴 ∈ Q, and 𝑓 : 𝐼 → Bit ⊗ 𝐴 ∈ Q, we have 𝑓 = 𝑝 1 (inj1 ⊗ 𝑓1 ) + 𝑝 2 (inj2 ⊗ 𝑓2 ), where
inj1, inj2 : 𝐼 → 𝐼 + 𝐼 and 𝑝 1, 𝑝 2 ∈ [0, 1] are uniquely determined real numbers such that𝑝 1 + 𝑝 2 = 1. When 𝑝𝑖 ≠ 0, the map 𝑓𝑖 : 𝐼 → 𝐴 is also unique.

The categories M and Q are not only used in the categorical semantics, but also in the operationalsemantics of Proto-Quipper-Dyn (i.e., to run the program, we must know what a circuit is andwhat a quantum operation is). Therefore, these categories should be regarded as given as part ofthe language specification, rather than as a degree of freedom in the semantics. On the other hand,nothing in the operational or denotational semantics depends on particular properties of M and Q
other than properties (1)ś(5) above. Therefore, Proto-Quipper-Dyn can handle a wide variety ofpossible circuit models and physical execution models.
In practice, the category M will be a category of quantum circuits and the category Q will
be a category of quantum operations. These categories will typically have additional objects,
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

11:10Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger

such as Qubit and perhaps Qutrit, and additional morphisms, such as 𝐻 : Qubit → Qubit andMeas : Qubit → Bit. Assumption (5) means that any morphism with domain 𝐼 and a bit state in its
codomain is a convex sum of two morphisms. This property is used in the rule for dynamic liftingin the operational semantics.
Definition 2.6. Suppose the V-enriched category A is a linear-non-linear programming model.
We say it supports box-unbox operations if the following hold.
𝜓(c) There is a fully faithful embedding 𝜓 : M ↩→ 𝑉 (A) and 𝜓 is strong monoidal.
(d) Let S denote the set of objects in the image of 𝜓 . For any 𝑆, 𝑈 ∈ S, there is an isomorphism𝑒♭(𝑆 ⊸ 𝑈 )  A(𝑆, 𝑈 ).
Condition (c) implies that there is a circuit subcategory in A. Using condition (d), we define
box/unbox

box = 𝑝 (𝑒) and unbox = 𝑝 (𝑒 −1 ), and there is an isomorphism 𝑝♭(𝑆 ⊸ 𝑈 )
𝑝A(𝑆, 𝑈 ).
Elements of 𝑝A(𝑆, 𝑈 ) correspond to boxed circuits with input 𝑆 and output 𝑈 .
If a V-enriched category A satisfies (a)ś(d), then it is a model for Proto-Quipper without dynamic
lifting. For example, the Set-enriched category M in [Rios and Selinger 2018] is such a model. To
support dynamic lifting, we define the following monad to account for the category Q.

Definition 2.7. Let A be a symmetric monoidal V-category and let 𝑇 : A → A be a V-monad on
A. We say 𝑇 is a dynamic lifting monad if the following hold.
(e) 𝑇 is a commutative strong V-monad. For any 𝐴, 𝐵 ∈ A, we write 𝑡𝐴,𝐵 : 𝐴 ⊗ 𝑇 𝐵 → 𝑇 (𝐴 ⊗ 𝐵)
for the strength and 𝑠𝐴,𝐵 : 𝑇 𝐴 ⊗ 𝐵 → 𝑇 (𝐴 ⊗ 𝐵) for the costrength.
(f) Let 𝑉 (A) be the underlying category of A, let 𝑉𝑇 be the underlying monad of 𝑇 , and let
𝐾𝑙𝑉𝑇 (𝑉 (A)) be the Kleisli category of 𝑉𝑇 . The Kleisli category 𝐾𝑙𝑉𝑇 (𝑉 (A)) is enriched inconvex spaces.
(g) There are the following fully faithful embeddings:
𝜓M ↩→ 𝑉 (A),𝜙Q ↩→ 𝐾𝑙𝑉𝑇 (𝑉 (A)).
These embedding functors are strong monoidal, and 𝜙 preserves the convex sum. Moreover,the following diagram commutes for any 𝑆, 𝑈 ∈ M.
𝜓𝑆,𝑈

M(𝑆, 𝑈 )𝐽𝑆,𝑈

Q(𝑆, 𝑈 )𝑉 (A)(𝑆, 𝑈 )
𝐸𝑆,𝑈

𝜙𝑆,𝑈

𝐾𝑙𝑉𝑇 (𝑉 (A))(𝑆, 𝑈 )Here 𝐸 : 𝑉 (A) → 𝐾𝑙𝑉𝑇 (𝑉 (A)) is the the functor such that 𝐸 (𝐴) = 𝐴 and 𝐸 (𝑓 ) = 𝜂 ◦ 𝑓 .
(h) There are maps dynlift : Bit → 𝑇 Bool and init : Bool → Bit in A such that the following
diagram commutes.
Bit
init

Bool

𝜂

dynlift

𝑇 BoolRemarks.
• The objects of the Kleisli category 𝐾𝑙𝑉𝑇 (𝑉 (A)) are the same as the objects of A,
and the hom-set is given by 𝐾𝑙𝑉𝑇 (𝑉 (A))(𝐴, 𝐵) := 𝑉 (A)(𝐴, 𝑉𝑇 𝐵) = V (1, A(𝐴,𝑇 𝐵)) for any
𝐴, 𝐵 ∈ A. Moreover, V (1, A(𝐴,𝑇 𝐵)) = V (1, 𝐾𝑙𝑇 (A)(𝐴, 𝐵)) = 𝑉 (𝐾𝑙𝑇 (A))(𝐴, 𝐵).
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

Proto-Quipper with Dynamic Lifting

11:11• Note that in condition (f), we are not taking a V-enriched Kleisli category of the V-monad 𝑇 ,but just an ordinary Kleisli category of the ordinary monad 𝑉𝑇 . Thus, the Kleisli category is
not V-enriched. However, we do require it to be enriched in convex spaces, which amounts torequiring the existence of additional operations on its hom-sets, in the sense of Definition 2.4.
• Since 𝑇 is a commutative strong V-monad, 𝑉𝑇 is a commutative strong (ordinary) monad.
Therefore the Kleisli category 𝐾𝑙𝑉𝑇 (𝑉 (A)) is monoidal. For any 𝑓 : 𝐴1 → 𝑉𝑇 𝐵 1 and 𝑔 : 𝐴2 →𝑉𝑇 𝐵 2 in 𝐾𝑙𝑉𝑇 (𝑉 (A)), we define 𝑓 ⊗ 𝑔 ∈ 𝐾𝑙𝑉𝑇 (𝑉 (A))(𝐴1 ⊗ 𝐴2, 𝐵 1 ⊗ 𝐵 2 ) to be the following
𝑓 ⊗𝑔

𝑠

𝑇𝑡

𝜇

𝐴1 ⊗ 𝐴2 −−−→ 𝑉𝑇 𝐵 1 ⊗ 𝑉𝑇 𝐵 2 →− 𝑉𝑇 (𝐵 1 ⊗ 𝑉𝑇 𝐵 2 ) −−→ 𝑉𝑇𝑉𝑇 (𝐵 1 ⊗ 𝐵 2 ) →− 𝑉𝑇 (𝐵 1 ⊗ 𝐵 2 ).
• Condition (g) expresses the requirement that the enriched category A must combine bothcategories M and Q, i.e., they are subcategories of 𝑉 (A) and its Kleisli category, respectively.
Thus A has both quantum circuits and quantum operations. The commutative diagram implies
that a circuit in A can be used as a quantum operation.
• Since 𝜓 (𝑆) = 𝜙 (𝑆) for any 𝑆 ∈ M, Q, we define Bit = 𝜓 (Bit) = 𝜙 (Bit) ∈ A.
• Condition (h) gives a categorical characterization of dynamic lifting. The map dynlift is notin the image of 𝜙 or 𝜓 , and therefore it is neither a quantum circuit nor a quantum operation.
Definition 2.8. We say a V-enriched category A is a model for Proto-Quipper with dynamic lifting
if it satisfies (a)ś(h).
We have now axiomatized a general categorical model for Proto-Quipper with dynamic lifting.
In [Fu et al. 2022a], we give a construction of a concrete model based on biset-enrichment thatsatisfies (a)-(h). In the rest of this paper, we will be focusing on showing this abstract categoricalmodel A is sound with respect to the type system and the operational semantics.
3 A TYPE SYSTEM FOR DYNAMIC LIFTING
In this section, we present the syntax of Proto-Quipper-Dyn and a type system for dynamic lifting.
Our typing judgments have the form Γ ⊢𝛼 𝑀 : 𝐴, where 𝛼 ::= 0 | 1 is a modality used to keep
track of dynamic lifting. When 𝛼 = 1, the term 𝑀 is guaranteed not to perform any dynamic lifting
operations while it is being reduced to a value. Such computations can therefore be carried out atcircuit generation time. When 𝛼 = 0, 𝑀 may invoke dynamic lifting so the evaluation of 𝑀 needs
to be performed at circuit execution time.
Definition 3.1 (Syntax). The syntax of Proto-Quipper-Dyn is in Figure 1.
The modality 𝛼 appears in the linear function type 𝐴 ⊸𝛼 𝐵 and the linear exponential type!𝛼 𝐴. This is because the values of 𝐴 ⊸𝛼 𝐵 and !𝛼 𝐴 are thunks and we use the modality 𝛼 inthe types to keep track of the dynamic lifting within the thunks. Circ(𝑆, 𝑈 ) denotes a type ofcircuits with input 𝑆 and output 𝑈 . The values of this type are boxed quantum circuits. They canbe further manipulated by meta-operations such as circuit reversal, circuit iteration, or printing;these operations are treated as constants in the language, i.e., we do not fix a particular set ofsuch operations, but assume that they would be defined in a standard library that comes with any
particular instance of Proto-Quipper-Dyn.
The terms of our language are similar to the ones from [Rios and Selinger 2018], with the additionof a term construct for dynamic lifting dynlift 𝑀, which will be evaluated to a boolean value. The
term 𝑐 ranges over constants such as booleans, natural numbers, and built-in functions. A term ofparameter type can be duplicated or discarded. A value of simple type corresponds to a state. Ourlanguage and semantics can accommodate coproducts (sum types), but we elide the treatment here
for the sake of simplicity.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

11:12Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger

Modality
Types
Parameter Types
Simple Types
Terms
Simple Terms
Contexts
Parameter contexts
Label Contexts
ValuesCircuits

0|1
Unit | Qubit | Bit | Bool | !𝛼 𝐴 | 𝐴 ⊸𝛼 𝐵 | Circ(𝑆, 𝑈 ) | 𝐴 ⊗ 𝐵
Unit | Nat | !𝛼 𝐴 | Circ(𝑆, 𝑈 ) | 𝑃 ⊗ 𝑅
Unit | Qubit | Bit | 𝑆 ⊗ 𝑈
𝑐 | 𝑥 | 𝜆𝑥 .𝑀 | 𝑀 𝑁 | Unit | (𝑎, C, 𝑏) | apply(𝑀, 𝑁 ) | force𝑀| lift 𝑀 | box 𝑈 𝑀 | (𝑀, 𝑁 ) | let (𝑥, 𝑦) = 𝑁 in 𝑀 | dynlift 𝑀𝑎, 𝑏::= ℓ | Unit | (𝑎, 𝑏)Γ::= · | 𝑥 : 𝐴, Γ | ℓ : Qubit, Γ | ℓ : Bit, ΓΦ::= · | 𝑥 : 𝑃, Φ.
Σ::= · | ℓ : Qubit, Σ | ℓ : Bit, Σ𝑉::= 𝑥 | ℓ | 𝜆𝑥 .𝑀 | lift 𝑀 | (𝑎, C, 𝑏) | (𝑉 , 𝑉 ′ ) | Unit
C, D : Σ → Σ′
𝛼, 𝛽
𝐴, 𝐵
𝑃, 𝑅
𝑆, 𝑈
𝑀, 𝑁

::=
::=
::=
::=
::=

Fig. 1. The syntax for Proto-Quipper-Dyn

Φ, 𝑥 : 𝐴 ⊢1 𝑥 : 𝐴

varℓ : Qubit|Bit ⊢1 ℓ : Qubit|BitΓ2 ⊢𝛼 2 𝑁 : 𝐴

Γ1 ⊢𝛼 1 𝑀 : 𝐴 ⊸𝛽 𝐵

Γ1 + Γ2 ⊢𝛼 1 &𝛼 2 &𝛽 𝑀𝑁 : 𝐵Γ ⊢𝛼&𝛽 force 𝑀 : 𝐴Γ1 ⊢𝛼 𝑀 : Circ(𝑆, 𝑈 )Γ ⊢𝛼 𝑀 : !1 (𝑆 ⊸1 𝑈 )boxΓ ⊢𝛼 box 𝑆 𝑀 : Circ(𝑆, 𝑈 )force
Γ2 ⊢𝛽 𝑁 : 𝑆

Γ1 + Γ2 ⊢𝛼&𝛽 apply(𝑀, 𝑁 ) : 𝑈Σ 2 ⊢1 𝑏 : 𝑈Φ ⊢1 (𝑎, C, 𝑏) : Circ(𝑆, 𝑈 )Γ, 𝑥 : 𝐴 ⊢𝛼 𝑀 : 𝐵
lambdaΓ ⊢1 𝜆𝑥 .𝑀 : 𝐴 ⊸𝛼 𝐵Γ ⊢𝛽 𝑀 : !𝛼 𝐴Φ ⊢𝛼 𝑀 : 𝐴
liftΦ ⊢1 lift 𝑀 : !𝛼 𝐴

Σ1 ⊢1 𝑎 : 𝑆
C : Σ1 → Σ2

app

label

circ

Γ1 ⊢𝛼 1 𝑀 : 𝐴 Γ2 ⊢𝛼 2 𝑁 : 𝐵
pair
Γ1 + Γ2 ⊢𝛼 1 &𝛼 2 (𝑀, 𝑁 ) : 𝐴 ⊗ 𝐵

apply

Γ ⊢𝛼 𝑀 : Bit
dynliftΓ ⊢0 dynlift 𝑀 : Bool
Γ1, 𝑥 : 𝐴, 𝑦 : 𝐵 ⊢𝛼 1 𝑀 : 𝐶 Γ2 ⊢𝛼 2 𝑁 : 𝐴 ⊗ 𝐵
letΓ1 + Γ2 ⊢𝛼 1 &𝛼 2 let (𝑥, 𝑦) = 𝑁 in 𝑀 : 𝐶

Fig. 2. The typing rules for Proto-Quipper-Dyn

We make a distinction between variables and labels. A label ℓ corresponds to a wire in a circuit,or to an address of a bit or qubit state. Consequently, a label is a value that can only have typeBit or Qubit. Labels can only be renamed, not substituted. Every label context Σ has an obvious
interpretation JΣK in the category M as a tensor of the appropriate sequence of the objects Qubit
and Bit. We write D : Σ → Σ′ to denote a quantum circuit, i.e., a morphism D : JΣK → JΣ′ K.
Definition 3.2 (Typing). The typing rules are in Figure 2.
We write 𝛼 & 𝛽 for the boolean conjunction of 𝛼 and 𝛽 so that, e.g., 0 & 1 = 0. If Γ1 = Φ, Γ1′ andΓ2 = Φ, Γ2′ , we write Γ1 + Γ2 for Φ, Γ1′, Γ2′ .
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

Proto-Quipper with Dynamic Lifting

11:13

In the var rule, we require a parameter context Φ. In the lift and lambda rules, the modality 𝛼
is moved to the type and the current modality (i.e., modality in the conclusion) is set to 1. This isbecause the lift and lambda terms are values, and values do not perform dynamic lifting. In fact, allvalues have modality 1.
In elimination rules such as app and force, the modality in the type affects the current modalityof the typing judgment through boolean conjunction. This is related to how the evaluations are
performed for these terms. For example, when evaluating the term 𝑀𝑁 , we will first evaluate 𝑀,
then evaluate 𝑁 and finally perform a beta-reduction. Thus, the evaluation of 𝑀𝑁 could perform
dynamic lifting of 𝛼 1 = 0, 𝛼 2 = 0, or 𝛽 = 0. Consequently, the modality for the typing judgment of
𝑀𝑁 is the boolean conjunction of all these related modalities.
By the dynlift rule, an application of dynamic lifting sets the current modality to 0, signifyingthat a dynamic lifting is performed. In the box rule, a term 𝑀 can only be boxed into a circuit if it
has type !1 (𝑆 ⊸1 𝑈 ). This ensures that the value of 𝑀 (denoted by 𝑉 ) does not use dynamic lifting.
Thus, when evaluating the term (box 𝑆 𝑉 ), a dynamic lifting cannot occur. This prevents a class ofruntime errors in Quipper that are caused by boxing functions that use dynamic lifting.
In the apply rule, depending on the modality 𝛼 1 & 𝛼 2 , the term apply(𝑀, 𝑁 ) either appends thequantum circuit 𝑀 to 𝑁 , which is done at circuit generation time, or applies the quantum operation
𝑀 to 𝑁 , which is done at circuit execution time. The circ rule defines a well-typed quantum circuit.
In practice, we often assume that a set of well-typed quantum gates is provided as pre-definedconstants of the language, so that the programmer does not need to use the circ rule.
The following lemma shows that a value can only have modality 1 and, in particular, that thefree variables of a parameter must come from a parameter context.
Lemma 3.3. If Γ ⊢𝛼 𝑉 : 𝐵, then 𝛼 = 1. Moreover, if Γ ⊢𝛼 𝑉 : 𝑃, then 𝛼 = 1 and Γ = Φ.
The following lemma shows that the type system has the usual substitution property.
Lemma 3.4 (Substitution). If Γ1, 𝑥 : 𝐴, Γ1′ ⊢𝛼 𝑀 : 𝐵 and Γ2 ⊢1 𝑉 : 𝐴, then Γ1, Γ1′, Γ2 ⊢𝛼 [𝑉 /𝑥]𝑀 : 𝐵.
3.1

Interpretation of the Typing Rules

The modality is a syntactic device to track the dynamic lifting monad 𝑇 . We will interpret Γ ⊢1 𝑀 : 𝐴
as a map JΓK → J𝐴K in A, and Γ ⊢0 𝑀 : 𝐴 as a map JΓK → 𝑇 J𝐴K. The modalities in types such as
𝐴 ⊸𝛼 𝐵 and !𝛼 𝐴 also indicate occurrences of the dynamic lifting monad 𝑇 .
Definition 3.5. We interpret types as objects in A.
J𝐴 ⊸1 𝐵K
J𝐴 ⊸0 𝐵K
J𝐴 ⊗ 𝐵K
J!1𝐴K
J!0𝐴K
JCirc(𝑆, 𝑈 )K
JBoolK
JBitK
JQubitK

=
=
=
=
=
=
=
=
=

J𝐴K ⊸ J𝐵K
J𝐴K ⊸ 𝑇 J𝐵K
J𝐴K ⊗ J𝐵K𝑝♭J𝐴K𝑝♭𝑇 J𝐴K
𝑝A(J𝑆K, J𝑈 K)
𝑝 (1 + 1)
Bit
Qubit

For a parameter type 𝑃, there exists 𝑋 ∈ V such that J𝑃K = 𝑝𝑋 . For a simple type 𝑆, there exists
𝑌 ∈ M such that J𝑆K = 𝜓𝑌 . We call objects of the form 𝜓𝑌 simple objects. We write 𝛼J𝐴K to mean
𝑇 J𝐴K if 𝛼 = 0, otherwise it is J𝐴K. We interpret a context Γ as a tensor product of all objects inΓ (denoted by JΓK). The interpretation of parameter context JΦK is a parameter object and theProc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

11:14Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger

interpretation of a label context JΣK is a simple object. Without loss of generality, we assume that
if JΣK = JΣ′ K, then Σ = Σ′ (this condition can always be ensured by making additional isomorphic
copies of objects, if necessary).
The interpretation of typing judgements is defined as follows.
Definition 3.6 (Interpretation). To each valid typing judgement Γ ⊢𝛼 𝑀 : 𝐴, we associate a
map J𝑀K : JΓK → 𝛼J𝐴K in A, called its interpretation. Note that J𝑀K here is an abbreviation forJΓ ⊢𝛼 𝑀 : 𝐴K.
The interpretation is defined by induction on the derivation of Γ ⊢𝛼 𝑀 : 𝐴. Here we show a few
cases, the rest are in [Fu et al. 2022b, Appendix C].
• CaseΓ ⊢𝛼 𝑀 : BitΓ ⊢0 dynlift 𝑀 : Bool.

By induction hypothesis, we have J𝑀K : JΓK → 𝛼JBitK. If 𝛼 = 1, we define Jdynlift 𝑀K by
J𝑀 KdynliftJΓK −−−→ JBitK −−−−−→ 𝑇 JBoolK.
If 𝛼 = 0, we define Jdynlift 𝑀K by
J𝑀 K

𝑇 dynlift𝜇JΓK −−−→ 𝑇 JBitK −−−−−−→ 𝑇𝑇 JBoolK →− 𝑇 JBoolK.
• CaseΓ, 𝑥 : 𝐴 ⊢𝛼 𝑀 : 𝐵
Γ ⊢1 𝜆𝑥 .𝑀 : 𝐴 ⊸𝛼 𝐵.

By induction hypothesis, we have J𝑀K : JΓK ⊗ J𝐴K → 𝛼J𝐵K. Using monoidal closedness, wedefine J𝜆𝑥 .𝑀K := curry(J𝑀K) : JΓK → J𝐴K ⊸ 𝛼J𝐵K.
• CaseΦ, Γ1 ⊢𝛼 1 𝑀 : 𝐴 ⊸𝛽 𝐵 Φ, Γ2 ⊢𝛼 2 𝑁 : 𝐴
app
Φ, Γ1, Γ2 ⊢𝛼 1 &𝛼 2 &𝛽 𝑀𝑁 : 𝐵.

Here we only consider the case where 𝛼 1 = 𝛼 2 = 𝛽 = 0. The other cases are similar. By
induction hypothesis, we have morphisms J𝑀K : JΦK ⊗ JΓ1 K → 𝑇 (J𝐴K ⊸ 𝑇 J𝐵K)) andJ𝑁 K : JΦK ⊗ JΓ2 K → 𝑇 J𝐴K. Thus we define J𝑀𝑁 K to be the following.
dup⊗ JΓ1 K ⊗ JΓ2 K

J𝑀 K ⊗ J𝑁 KJΦK ⊗ JΓ1 K ⊗ JΓ2 K −−−−−−−−−−−→ JΦK ⊗ JΦK ⊗ JΓ1 K ⊗ JΓ2 K −−−−−−−→ 𝑇 (J𝐴K ⊸ 𝑇 J𝐵K)) ⊗ 𝑇 J𝐴K
𝑡

𝑇𝑠

𝜇

𝑇𝜖

→
− 𝑇 (𝑇 (J𝐴K ⊸ 𝑇 J𝐵K) ⊗ J𝐴K) −−→ 𝑇𝑇 ((J𝐴K ⊸ 𝑇 J𝐵K) ⊗ J𝐴K)𝜇→
− 𝑇 ((J𝐴K ⊸ 𝑇 J𝐵K) ⊗ J𝐴K) −−→ 𝑇𝑇 J𝐵K →− 𝑇 J𝐵K.
• CaseΦ ⊢𝛼 𝑀 : 𝐴Φ ⊢1 lift 𝑀 : !𝛼 𝐴.

By induction hypothesis, we have J𝑀K : JΦK = 𝑝𝑋 → 𝛼J𝐴K for some 𝑋 ∈ V. By the Vadjunction 𝑝 ⊢ ♭, we have 𝛿J𝑀K : 𝑋 → ♭𝛼J𝐴K. So we define Jlift 𝑀K := 𝑝𝛿J𝑀K : 𝑝𝑋 →𝑝♭𝛼J𝐴K.
• CaseΓ ⊢𝛽 𝑀 : !𝛼 𝐴Γ ⊢𝛼&𝛽 force 𝑀 : 𝐴.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

Proto-Quipper with Dynamic Lifting

11:15

We only consider the case where 𝛼 = 𝛽 = 0, the other cases are similar. By induction
hypothesis, we have a map J𝑀K : JΓK → 𝑇 𝑝♭𝑇 J𝐴K. Since there is a V-natural transformation
force : 𝑝♭𝑇 J𝐴K → 𝑇 J𝐴K, we define Jforce𝑀K by
J𝑀 K𝜇𝑇 forceJΓK −−−→ 𝑇 𝑝♭𝑇 J𝐴K −−−−→ 𝑇𝑇 J𝐴K →− 𝑇 J𝐴K.
• CaseΓ ⊢𝛼 𝑀 : !1 (𝑆 ⊸1 𝑈 )Γ ⊢𝛼 box 𝑆 𝑀 : Circ(𝑆, 𝑈 ).

Here we only consider the case 𝛼 = 1. By induction hypothesis, we have J𝑀K : JΓK →𝑝♭(J𝑆K ⊸ J𝑈 K). We define Jbox 𝑆𝑀K by
J𝑀 K

box

JΓK −−−→ 𝑝♭(J𝑆K ⊸ J𝑈 K) −−→ 𝑝A(J𝑆K, J𝑈 K).
• CaseΦ, Γ1 ⊢𝛼 𝑀 : Circ(𝑆, 𝑈 ) Φ, Γ2 ⊢𝛽 𝑁 : 𝑆
apply
Φ, Γ1, Γ2 ⊢𝛼&𝛽 apply(𝑀, 𝑁 ) : 𝑈

Here we only consider the case 𝛼 = 𝛽 = 0. By induction hypothesis, we have J𝑀K : JΓ1 K →𝑇 𝑝A(J𝑆K, J𝑈 K) and J𝑁 K : JΓ2 K → 𝑇 J𝑆K. Thus we define Japply(𝑀, 𝑁 )K by
dup⊗ JΓ1 K ⊗ JΓ2 K

JΦK ⊗ JΓ1 K ⊗ JΓ2 K −−−−−−−−−−−→ JΦK ⊗ JΦK ⊗ JΓ1 K ⊗ JΓ2 K
J𝑀 K ⊗ J𝑁 K−−−−−−−→ 𝑇 𝑝A(J𝑆K, J𝑈 K) ⊗ 𝑇 J𝑆K𝑡→− 𝑇 (𝑇 𝑝A(J𝑆K, J𝑈 K) ⊗ J𝑆K)
𝑇𝑠−−→ 𝑇𝑇 (𝑝A(J𝑆K, J𝑈 K) ⊗ J𝑆K)𝜇→
− 𝑇 (𝑝A(J𝑆K, J𝑈 K) ⊗ J𝑆K)
𝑇 ( (force ◦ unbox) ⊗ J𝑆 K )−−−−−−−−−−−−−−−−−−→ 𝑇 ((J𝑆K ⊸ J𝑈 K) ⊗ J𝑆K)
𝑇𝜖−−→ 𝑇 J𝑈 K.
Our interpretation of the typing rules satisfies the usual semantics substitution theorem. The
details of the proof are in [Fu et al. 2022b, Appendix D].
Theorem 3.7 (Substitution). If Φ, Γ1, 𝑥 : 𝐴, Γ2 ⊢𝛼 𝑀 : 𝐵 and Φ, Γ3 ⊢1 𝑉 : 𝐴, thenJ[𝑉 /𝑥]𝑀K = J𝑀K ◦ (JΦK ⊗ JΓ1 K ⊗ J𝑉 K ⊗ JΓ2 K) ◦ (dup ⊗ JΓ1 K ⊗ JΓ2 K ⊗ JΓ3 K) : JΦ, Γ1, Γ2, Γ3 K → 𝛼J𝐵K.
The next two theorems show that values of parameter type are in the image of functor 𝑝, andthat values of simple types are isomorphisms.
Theorem 3.8. If Φ ⊢1 𝑉 : 𝑃, then J𝑉 K = 𝑝 𝑓 : 𝑝𝑋 → 𝑝𝑌 for some 𝑓 : 𝑋 → 𝑌 ∈ V such thatJΦK = 𝑝𝑋, J𝑃K = 𝑝𝑌 .
Theorem 3.9. Suppose Σ ⊢1 𝑉 : 𝑆, then J𝑉 K : JΣK → J𝑆K is an isomorphism in A.
Since the embedding 𝜓 : M ↩→ 𝑉 (A) is fully faithful, J𝑉 K : JΣK → J𝑆K is also an isomorphism inM.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

11:16Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger

4 OPERATIONAL SEMANTICS AND SOUNDNESSIn this section, we will specify an operational semantics for Proto-Quipper-Dyn and show that it issound with respect to the V-enriched categorical model A for dynamic lifting.
We distinguish two kinds of evaluation in order to model Quipper’s two runtimes. The evaluation
rules for circuit generation time will work with morphisms in M, i.e., quantum circuits. On theother hand, the evaluation rules for circuit execution time will work with morphisms in Q, i.e.,quantum operations. Because of the embeddings 𝜓 : M ↩→ 𝑉 (A) and 𝜙 : Q ↩→ 𝐾𝑙𝑉𝑇 (𝑉 (A)), we areable to interpret the configurations for these two runtimes as maps in the V-enriched category A.
4.1 Operational Semantics for Circuit Generation TimeFirst of all, we specify the meaning of appending circuits in the category M.
Definition 4.1 (Circuit append). Suppose C : Σ → Σ1, Σ2 and D : Σ′1 → Σ3 are morphisms in M
and there are typing judgments Σ1 ⊢1 𝑉 : 𝑆 and Σ′1 ⊢1 𝑉 ′ : 𝑆. We define append(D, C, 𝑉 ′, 𝑉 ) to be
the following morphism in M.
((D ◦ J𝑉 ′ K−1 ◦ J𝑉 K) ⊗ JΣ2 K) ◦ C : Σ → Σ3, Σ2Thus append(D, C, 𝑉 ′, 𝑉 ) is the result of appending the circuit D to C by connecting theinterfaces 𝑉 ′ and 𝑉 . The following are evaluation rules for circuit generation time, where theunderlying states are given by morphisms in M.
Definition 4.2 (Circuit generation time evaluation).
(C1, 𝑀) ⇓ (C2, 𝜆𝑥 .𝑀 ′ )(C2, 𝑁 ) ⇓ (C3, 𝑉 )(C3, [𝑉 /𝑥]𝑀 ′ ) ⇓ (C4, 𝑉 ′ )(C1, 𝑀) ⇓ (C2, (𝑎, D, 𝑏))(C2, 𝑁 ) ⇓ (C3, 𝑉 )append(D, C3, 𝑎, 𝑉 ) = C ′(C1, 𝑀𝑁 ) ⇓ (C4, 𝑉 ′ )(C, 𝑀) ⇓ (C ′, lift 𝑀 ′ )gen(𝑆) = 𝑎(Id𝑆 , 𝑀 ′ 𝑎) ⇓ (D, 𝑏)(C, box 𝑆 𝑀) ⇓ (C ′, (𝑎, D, 𝑏))

apply(C, force 𝑀) ⇓ (C ′′, 𝑉 )(C, 𝑁 ) ⇓ (C ′, (𝑉1, 𝑉2 ))′(C , [𝑉1 /𝑥, 𝑉2 /𝑦]𝑀) ⇓ (C ′′, 𝑉 )(C, let (𝑥, 𝑦) = 𝑁 in 𝑀) ⇓ (C ′′, 𝑉 )(C, 𝑀) ⇓ (C ′, 𝑉1 )(C ′, 𝑁 ) ⇓ (C ′′, 𝑉2 )(C1, apply(𝑀, 𝑁 )) ⇓ (C ′, 𝑏)box(C, 𝑀) ⇓ (C ′, lift 𝑀 ′ )(C ′, 𝑀 ′ ) ⇓ (C ′′, 𝑉 )(C, (𝑀, 𝑁 )) ⇓ (C ′′, (𝑉1, 𝑉2 ))In the rule box, we use gen(𝑆) = 𝑎 to mean that the 𝑎 is a fresh simple term of type 𝑆. Note thatthe evaluation of (C, 𝑀) ⇓ (C ′, 𝑉 ) does not account for dynamic lifting, and the underlying states
are circuits. So it is the same set of evaluation rules as in [Rios and Selinger 2018]. The evaluation
comes with the following notion of configuration.
Definition 4.3 (Well-typed circuit configuration). We write Σ ⊢ (C, 𝑀) : 𝐴; Σ′ to mean there exists
Σ′′ such that C : Σ → Σ′, Σ′′ and Σ′′ ⊢1 𝑀 : 𝐴.
A well-typed circuit configuration requires a typed term with modality 1, i.e., ⊢1 𝑀 : 𝐴. It is aruntime error if a term with dynamic lifting is encountered when using the evaluation rules in
Definition 4.2. Our type system and the following type preservation theorem ensures that this can
not happen.
Theorem 4.4. If Σ ⊢ (C, 𝑀) : 𝐴; Σ′ and (C, 𝑀) ⇓ (C ′, 𝑉 ), then Σ ⊢ (C ′, 𝑉 ) : 𝐴; Σ′ .
In the following we define the interpretation JC, 𝑀K as a map in the V-category A.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

Proto-Quipper with Dynamic Lifting

11:17

Definition 4.5. Suppose Σ ⊢ (C, 𝑀) : 𝐴; Σ′ . We have maps 𝜓 C : JΣK → JΣ′ K ⊗ JΣ′′ K andJ𝑀K : JΣ′′ K → J𝐴K in A. We define JC, 𝑀K as follows:
𝜓C

JΣ′ K ⊗ J𝑀 K

JΣK −−→ JΣ′ K ⊗ JΣ′′ K −−−−−−−−→ JΣ′ K ⊗ J𝐴K.
The following theorem shows that the evaluation rules for circuit generation time are soundwith respect to the categorical model A. Since in this case dynamic lifting cannot occur, the proof
is similar to the one in [Rios and Selinger 2018].
Theorem 4.6. If Σ ⊢ (C, 𝑀) : 𝐴; Σ′ and (C, 𝑀) ⇓ (C ′, 𝑉 ), then JC, 𝑀K = JC ′, 𝑉 K.
4.2

Operational Semantics for Circuit Execution Time

Since dynamic lifting requires the ability to access the states in Q, we first define the concepts ofstate and addresses.
Definition 4.7 (State and addresses). For any object 𝑆 ∈ Q, a state is a morphism 𝑄 : 𝐼 → 𝑆 ∈ Q. We
write addr(𝑄) = Σ if 𝜙 (𝑆) = JΣK, we call Σ the addresses of 𝑄. (Recall that we have, for convenienceand without loss of generality, assumed that the interpretation function J−K is one-to-one on label
contexts).
We often write 𝑄 : 𝐼 → Σ ∈ Q for 𝑄 : 𝐼 → 𝑆, where 𝜙 (𝑆) = JΣK. The following read operation
will be used to define the operational semantics for dynamic lifting.
Definition 4.8 (Read operation). Suppose addr(𝑄) = Σ, ℓ : Bit and 𝑄 = 𝑝 1 (𝑄 1 ⊗inj1 ) +𝑝 2 (𝑄 2 ⊗inj2 ),where addr(𝑄 1 ) = addr(𝑄 2 ) = Σ and 𝑝 1, 𝑝 2 ∈ [0, 1] and 𝑝 1 + 𝑝 2 = 1. We define a formal sumread(𝑄, ℓ) = 𝑝 1 (𝑄 1, False) + 𝑝 2 (𝑄 2, True), where False, True : Bool.
Note that by the last condition in Assumption 2.5, we know that 𝑄 = 𝑝 1 (𝑄 1 ⊗ inj1 ) +𝑝 2 (𝑄 2 ⊗ inj2 ) :𝐼 → Σ ⊗ Bit for some essentially uniquely determined 𝑄 1, 𝑄 2 : 𝐼 → Σ, and 𝑝 1, 𝑝 2 ∈ [0, 1] such that𝑝 1 + 𝑝 2 = 1. The only time 𝑄𝑖 is not uniquely determined is when 𝑝𝑖 = 0, but in this case, it willturn out that the 𝑄𝑖 does not matter since it corresponds to a branch of computation taken withprobability zero. In this case, we can just make some fixed but arbitrary choice for 𝑄𝑖 . So the read
operation makes the information of the probabilities 𝑝 1, 𝑝 2 and the states 𝑄 1, 𝑄 2 available.
In the following, we define the circuit execution time counterpart of Definition 4.1. It specifies themeaning of updating a quantum state by applying a quantum circuit, where the identity-on-object
interpretation functor 𝐽 : M → Q is needed for the definition.
Definition 4.9. Suppose 𝑄 : 𝐼 → Σ1, Σ2 is a morphism in Q, and C : Σ′1 → Σ3 is a morphism in M,
and there are typing judgements Σ1 ⊢ 𝑉 : 𝑆 and Σ′1 ⊢ 𝑉 ′ : 𝑆. We define operate(C, 𝑄, 𝑉 ′, 𝑉 ) to be
the following map in Q.
(𝐽 (C ◦ J𝑉 ′ K−1 ◦ J𝑉 K) ⊗ JΣ2 K) ◦ 𝑄 : 𝐼 → Σ3, Σ2
We now we define the operational semantics for circuit execution time. The
Í underlying statesof the evaluation are the states in Q. The evaluation is of the form (𝑄, 𝑀) ⇓ 𝑖 ∈ [𝑛] 𝑝𝑖 (𝑄𝑖 , 𝑉𝑖 ). Its
intuitive meaning is that the configuration (𝑄, 𝑀) can be reduced to (𝑄𝑖 , 𝑉𝑖 ) with probability 𝑝𝑖 .
ÍThe notation 𝑖 ∈ [𝑛] 𝑝𝑖 (𝑄𝑖 , 𝑉𝑖 ) is a short hand for the formal sum 𝑝 1 (𝑄 1, 𝑉1 ) + ... + 𝑝𝑛 (𝑄𝑛 , 𝑉𝑛 ), andÍ
we assume 𝑖 ∈ [𝑛] 𝑝𝑖 = 1. We write [𝑛] = {1, ..., 𝑛}.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

11:18Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger

Definition 4.10 (Operational semantics for circuit execution time).
Í(𝑄, 𝑀) ⇓ 𝑖 ∈ [𝑛] 𝑝𝑖 (𝑄𝑖 , 𝜆𝑥 .𝑀𝑖′ )Í′ ,𝑉 )(𝑄𝑖 , 𝑁 ) ⇓ 𝑗 ∈ [𝑚] 𝑞𝑖,𝑗 (𝑄𝑖,𝑗
𝑖,𝑗
Í
′
′
′′ , 𝑉 ′ )(𝑄𝑖,𝑗 , [𝑉𝑖,𝑗 /𝑥]𝑀𝑖 ) ⇓ 𝑘 ∈ [𝑙 ] 𝑠𝑖,𝑗,𝑘 (𝑄𝑖,𝑗,𝑘
𝑖,𝑗,𝑘Í′′ , 𝑉 ′ )(𝑄, 𝑀𝑁 ) ⇓ (𝑖,𝑗,𝑘 ) ∈ [𝑛] × [𝑚] × [𝑙 ] 𝑝𝑖 𝑞𝑖,𝑗 𝑠𝑖,𝑗,𝑘 (𝑄𝑖,𝑗,𝑘𝑖,𝑗,𝑘Í(𝑄, 𝑀) ⇓ 𝑖 ∈ [𝑛] 𝑝𝑖 (𝑄𝑖 , lift 𝑀𝑖′ )Í′′ ,𝑉 )(𝑄𝑖 , 𝑀𝑖 ) ⇓ 𝑗 ∈ [𝑚] 𝑞𝑖,𝑗 (𝑄𝑖,𝑗𝑖,𝑗Í′ ,𝑉 )(𝑄, force𝑀) ⇓ (𝑖,𝑗 ) ∈ [𝑛] × [𝑚] 𝑝𝑖 𝑞𝑖,𝑗 (𝑄𝑖,𝑗𝑖,𝑗Í(𝑄, 𝑀) ⇓ 𝑖 ∈ [𝑛] 𝑝𝑖 (𝑄𝑖 , (𝑎𝑖 , D𝑖 , 𝑏𝑖 ))Í′ ,𝑉 )(𝑄𝑖 , 𝑁 ) ⇓ 𝑗 ∈ [𝑚] 𝑞𝑖,𝑗 (𝑄𝑖,𝑗𝑖,𝑗′′′operate(D𝑖 , 𝑄𝑖,𝑗 , 𝑎𝑖 , 𝑉𝑖,𝑗 ) = 𝑄𝑖,𝑗Í′′ , 𝑏 ) apply(𝑄, apply(𝑀, 𝑁 )) ⇓ (𝑖,𝑗 ) ∈ [𝑛] × [𝑚] 𝑝𝑖 𝑞𝑖,𝑗 (𝑄𝑖,𝑗𝑖′𝑖 ∈ [𝑛] 𝑝𝑖 (𝑄𝑖 , lift 𝑀𝑖 )gen(𝑆) = 𝑎(Id𝑆 , 𝑀𝑖′ 𝑎) ⇓ (D𝑖 , 𝑏𝑖 )Íbox
(𝑄, box 𝑆 𝑀) ⇓ 𝑖 ∈ [𝑛] 𝑝𝑖 (𝑄𝑖 , (𝑎, D𝑖 , 𝑏𝑖 ))(𝑄, 𝑀) ⇓ÍÍ(𝑄, 𝑀) ⇓ 𝑖 ∈ [𝑛] 𝑝𝑖 (𝑄𝑖 , ℓ𝑖 )′ , 𝑎 ) + 𝑞 (𝑄 ′ , 𝑎 )read(𝑄𝑖 , ℓ𝑖 ) = 𝑞𝑖,1 (𝑄𝑖,1𝑖,1𝑖,2𝑖,2 𝑖,2Í′ , 𝑎 ) dynlift(𝑄, dynlift 𝑀) ⇓ (𝑖,𝑗 ) ∈ [𝑛] × [2] 𝑝𝑖 𝑞𝑖,𝑗 (𝑄𝑖,𝑗𝑖,𝑗(𝑄, 𝑁 ) ⇓

Í′′ , 𝑉 ′′ )(𝑄𝑖′, [𝑉𝑖 /𝑥, 𝑉𝑖′ /𝑦]𝑀) ⇓ 𝑗 ∈𝑚 (𝑄𝑖,𝑗𝑖,𝑗Í′′ , 𝑉 ′′ )(𝑄, let (𝑥, 𝑦) = 𝑁 in 𝑀) ⇓ (𝑖,𝑗 ) ∈ [𝑛] × [𝑚] (𝑄𝑖,𝑗
𝑖,𝑗

Í

′
′
𝑖 ∈ [𝑛] 𝑝𝑖 (𝑄 𝑖 , (𝑉𝑖 , 𝑉𝑖 ))Í
(𝑄, 𝑀) ⇓ 𝑖 ∈ [𝑛] 𝑝𝑖 (𝑄𝑖 , 𝑉𝑖 )Í′ ,𝑉 ′ )(𝑄𝑖 , 𝑁 ) ⇓ 𝑗 ∈ [𝑚] 𝑞𝑖,𝑗 (𝑄𝑖,𝑗𝑖,𝑗Í′ , (𝑉 , 𝑉 ′ ))(𝑄, (𝑀, 𝑁 )) ⇓ 𝑖,𝑗 ∈ [𝑛] × [𝑚] (𝑄𝑖,𝑗𝑖 𝑖,𝑗In the apply rule, we use operate instead of append, which allows a quantum circuit to be applied
as a quantum operation. In the dynlift rule, for each (𝑄𝑖 , ℓ𝑖 ), we apply the operation read(𝑄𝑖 , ℓ𝑖 ),′ , 𝑎 ), (𝑄 ′ , 𝑎 ) with probabilities 𝑞 , 𝑞 , where
which gives rise to two possible outcomes (𝑄𝑖,1𝑖,1𝑖,1 𝑖,2𝑖,2 𝑖,2𝑎𝑖,1, 𝑎𝑖,2 : Bool and 𝑎𝑖,1 ≠ 𝑎𝑖,2 . This is the only rule that gives rise to probabilistic results in theevaluation. In the box rule, the evaluation of (Id𝑆 , 𝑀𝑖′𝑎) uses the rules defined in Definition 4.2, so
it is performed at circuit generation time.
We now define a well-typed configuration for evaluating a term under a quantum state.
Definition 4.11 (Well-typed configuration). We write ⊢𝛼 (𝑄, 𝑀) : 𝐴; Σ′ to mean there exists Σ′′
such that Σ′′ ⊢𝛼 𝑀 : 𝐴, and addr(𝑄) = Σ′′, Σ′ .

Since the evaluation rules in Definition 4.10 account for dynamic lifting, the above configuration
allows the term 𝑀 to have modality 0. The operational semantics defined in Definition 4.10 is
type-safe in the following sense.
Í
Theorem 4.12. If ⊢𝛼 (𝑄, 𝑀) : 𝐴; Σ′ and (𝑄, 𝑀) ⇓ 𝑖 ∈ [𝑛] 𝑝𝑖 (𝑄𝑖 , 𝑉𝑖 ), then ⊢1 (𝑄𝑖 , 𝑉𝑖 ) : 𝐴; Σ′ for all𝑖 ∈ [𝑛].
Í
Theorem 4.13. If ⊢1 (𝑄, 𝑀) : 𝐴; Σ′ and (𝑄, 𝑀) ⇓ 𝑖 ∈ [𝑛] 𝑝𝑖 (𝑄𝑖 , 𝑉𝑖 ), then 𝑛 = 1. In other words, we
actually have (𝑄, 𝑀) ⇓ (𝑄 ′, 𝑉 ).
In the following we interpret a well-typed configuration ⊢𝛼 (𝑄, 𝑀) : 𝐴; Σ′ as a map in the Kleisli
category 𝐾𝑙𝑇 (A).

Definition 4.14. Suppose ⊢𝛼 (𝑄, 𝑀) : 𝐴; Σ′ . We have 𝜙𝑄 : 𝐼 → 𝑇 (JΣ′1 K ⊗ JΣ′′ K ⊗ JΣ′2 K) andJ𝑀K : JΣ′′ K → 𝛼J𝐴K in A. We define J𝑄, 𝑀K by:• If 𝛼 = 1, then𝜙𝑄

𝑇 ( JΣ′1 K ⊗ J𝑀 K ⊗ JΣ′2 K )𝐼 −−→ 𝑇 (JΣ′1 K ⊗ JΣ′′ K ⊗ JΣ′2 K) −−−−−−−−−−−−−−−→ 𝑇 (JΣ′1 K ⊗ J𝐴K ⊗ JΣ′2 K).
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

Proto-Quipper with Dynamic Lifting

11:19• If 𝛼 = 0, then𝑇 ( JΣ′1 K ⊗ J𝑀 K ⊗ JΣ′2 K )𝜙𝑄

𝐼 −−→ 𝑇 (JΣ′1 K ⊗ JΣ′′ K ⊗ JΣ′2 K) −−−−−−−−−−−−−−−→ 𝑇 (JΣ′1 K ⊗ 𝑇 J𝐴K ⊗ JΣ′2 K)
𝑇 (𝑡 ⊗ JΣ′2 K )𝑇𝑠𝜇− 𝑇 (JΣ′1 K ⊗ J𝐴K ⊗ JΣ′2 K).
−−−−−−−−→ 𝑇 (𝑇 (JΣ′1 K ⊗ J𝐴K) ⊗ JΣ′2 K) −−→ 𝑇𝑇 (JΣ′1 K ⊗ J𝐴K ⊗ JΣ′2 K) →The following theorem shows that the operational semantics in Definition 4.10 is sound withrespect to the semantic model A.
ÍTheorem 4.15 (Soundness). If ⊢𝛼 (𝑄, 𝑀) : 𝐴; Σ′ , and (𝑄, 𝑀) ⇓ 𝑖 ∈ [𝑛] 𝑝𝑖 (𝑄𝑖 , 𝑉𝑖 ), then∑︁J𝑄, 𝑀K =𝑝𝑖 J𝑄𝑖 , 𝑉𝑖 K : 𝐼 → 𝑇 (J𝐴K ⊗ JΣ′ K).
𝑖 ∈ [𝑛]Proof sketch. The proof is by induction on the evaluation rules. Here we focus on the case fordynamic lifting. Please see [Fu et al. 2022b, Appendix E] for the proofs of the other cases.
Suppose addr(𝑄) = Σ′′, Σ′ , and Σ′′ ⊢0 𝑀 : 𝐴, andΣ′′ ⊢1 𝑀 : Bit
0 dynlift 𝑀 : Bool.

Σ′′ ⊢Consider the following.

(𝑄, 𝑀) ⇓ (𝑄 ′, ℓ)read(𝑄 ′, ℓ) = 𝑞 1 (𝑄 1′ , False) + 𝑞 2 (𝑄 2′ , True)(𝑄, dynlift 𝑀) ⇓ 𝑞 1 (𝑄 1′ , False) + 𝑞 2 (𝑄 2′ , True)
Since read(𝑄 ′, ℓ) = 𝑞 1 (𝑄 1′ , False) + 𝑞 2 (𝑄 2′ , True) implies that 𝑄 ′ = 𝑞 1 (𝑄 1′ ⊗ inj1 ) + 𝑞 2 (𝑄 2′ ⊗ inj2 )in Q, we have the following in A.

𝜙𝑄 ′ = 𝑞 1 (𝜇 ◦ 𝑇 𝑡 ◦ 𝑠 ◦ (𝜙𝑄 1′ ⊗ 𝜙 (inj1 ))) + 𝑞 2 (𝜇 ◦ 𝑇 𝑡 ◦ 𝑠 ◦ (𝜙𝑄 2′ ⊗ 𝜙 (inj2 ))),

where 𝜙𝑄 ′ : 𝐼 → 𝑇 (Bit ⊗ JΣ′ K), and 𝜙𝑄 1′ , 𝜙𝑄 2′ : 𝐼 → 𝑇 JΣ′ K, and 𝜙 (inj1 ), 𝜙 (inj2 ) : 𝐼 → 𝑇 Bit. Notethat by condition (g), we have 𝜙 (inj1 ) = 𝜂 ◦ init ◦ JFalseK and 𝜙 (inj2 ) = 𝜂 ◦ init ◦ JTrueK. We needto show that
J𝑄, dynlift 𝑀K = 𝑞 1 (𝑇 (JFalseK ⊗ JΣ′ K) ◦ 𝜙𝑄 1′ ) + 𝑞 2 (𝑇 (JTrueK ⊗ JΣ′ K) ◦ 𝜙𝑄 2′ ).

By induction hypothesis, we have J𝑄, 𝑀K = J𝑄 ′, ℓK, i.e., 𝑇 (J𝑀K ⊗ JΣ′ K) ◦ 𝜙𝑄 = 𝜙𝑄 ′ . Thus
J𝑄, dynlift 𝑀K = 𝜇 ◦ 𝑇 𝑠 ◦ 𝑇 ((dynlift ◦J𝑀K) ⊗ JΣ′ K) ◦ 𝜙𝑄
= 𝜇 ◦ 𝑇 𝑠 ◦ 𝑇 (dynlift ⊗JΣ′ K) ◦ 𝑇 (J𝑀K ⊗ JΣ′ K) ◦ 𝜙𝑄
= 𝜇 ◦ 𝑇 𝑠 ◦ 𝑇 (dynlift ⊗JΣ′ K) ◦ 𝜙𝑄 ′= 𝜇 ◦ 𝑇 𝑠 ◦ 𝑇 (dynlift ⊗JΣ′ K)◦(𝑞 1 (𝜇 ◦ 𝑇 𝑡 ◦ 𝑠 ◦ (𝜙𝑄 1′ ⊗ 𝜙 (inj1 ))) + 𝑞 2 (𝜇 ◦ 𝑇 𝑡 ◦ 𝑠 ◦ (𝜙𝑄 2′ ⊗ 𝜙 (inj2 ))))
= 𝑞 1 (𝜇 ◦ 𝑇 𝑠 ◦ 𝑇 (dynlift ⊗JΣ′ K) ◦ 𝜇 ◦ 𝑇 𝑡 ◦ 𝑠 ◦ (𝜙𝑄 1′ ⊗ 𝜙 (inj1 )))+𝑞 2 (𝜇 ◦ 𝑇 𝜎 ◦ 𝑇 (dynlift ⊗JΣ′ K) ◦ 𝜇 ◦ 𝑇 𝑡 ◦ 𝜎 ◦ (𝜙𝑄 2′ ⊗ 𝜙 (inj2 ))).

We just need to show

𝑇 (JFalseK ⊗ JΣ′ K) ◦ 𝜙𝑄 1′ = 𝜇 ◦ 𝑇 𝑠 ◦ 𝑇 (dynlift ⊗JΣ′ K) ◦ 𝜇 ◦ 𝑇 𝑡 ◦ 𝑠 ◦ (𝜙𝑄 1′ ⊗ 𝜙 (inj1 ))= 𝜇 ◦ 𝑇 𝑠 ◦ 𝑇 (dynlift ⊗JΣ′ K) ◦ 𝜇 ◦ 𝑇 𝑡 ◦ 𝑠 ◦ (𝜙𝑄 1′ ⊗ (𝜂 ◦ init ◦ JFalseK))

This is true because of the commutative diagram in Figure 3.

□

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

11:20Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger

𝐼
𝜙𝑄 1′

𝑇 JΣ′ K𝑇 𝜆 −1𝜆 −1𝑡

𝐼 ⊗ 𝑇 JΣ′ K

𝑇 (𝐼 ⊗ JΣ′ K)

JFalseK ⊗𝑇 JΣ′ K

𝑡Bool ⊗ 𝑇 JΣ′ K

𝑇 (Bool ⊗ JΣ′ K)

init⊗𝑇 JΣ′ K

Bit ⊗ 𝑇 JΣ′ K
𝜂⊗𝑇 JΣ′ K

Id

𝑇 ( JFalseK ⊗ JΣ′ K )𝑇 (init⊗ JΣ′ K )𝑡

𝑇 (𝜂⊗ JΣ′ K )𝑇 (Bit ⊗ JΣ′ K)

𝜂𝑇 (Bool ⊗ JΣ′ K)

𝑇 (𝜂⊗ JΣ′ K )𝑇 (𝑇 Bool ⊗ JΣ′ K)𝜇𝑇𝑠

𝑇 (dynlift ⊗ JΣ′ K )𝑇𝑇 (Bool ⊗ JΣ′ K)

𝑇 Bit ⊗ 𝑇 JΣ′ K𝑡Id𝜂𝑇 (𝑇 Bit ⊗ JΣ′ K)
𝑇𝑠

𝑇𝑇 (Bit ⊗ JΣ′ K)

𝜇𝑇 (Bit ⊗ JΣ′ K)

Fig. 3. A commutative diagram from the proof of Theorem 4.15

Remark. In practice, a closed term 𝑀 is always evaluated with the initial configuration (Id𝐼 , 𝑀),
where Id𝐼 : 𝐼 → 𝐼 is a state in Q. When 𝑀 has modality 0, we would need access to a quantum
computer/simulator in order to evaluate (Id𝐼 , 𝑀) and each run of (Id𝐼 , 𝑀) could give a different value.
When 𝑀 has modality 1, the evaluation of (Id𝐼 , 𝑀) is deterministic, i.e., the top-level quantum stateis updated in a deterministic fashion. In this case, instead of performing the quantum operations,
we could also just generate a list of gates, which can be done entirely in a classical computer.
5 DYNAMIC LIFTING IN PROTO-QUIPPER
While typing judgments and certain types (𝐴 ⊸𝛼 𝐵 and !𝛼 𝐴) are annotated with a modality,
information about this modality is meant to be hidden from the programmer unless an error
occurs. For example, if one attempt to box a function which uses dynamic lifting, the type checker
will raise a modality error. As a result, such programming errors are caught at compile time inProto-Quipper-Dyn, whereas they are only caught at runtime in Quipper.
The modality inference can readily be integrated into bi-directional type checking, which uses apair of recursively defined functions for type checking and type inference [Pierce and Turner 2000].
To work with modalities, the type checking function not only takes a term and a type as inputs,
but also the current modality of the typing judgment. For example, when checking a term 𝜆𝑥 .𝑀
against a type 𝐴 ⊸𝛼 𝐵 with current modality 𝛽, the type checking function first ensures that thecurrent modality 𝛽 is 1, then extends the current typing environment with 𝑥 : 𝐴 and recursively
checks the term 𝑀 against the type 𝐵, with the modality 𝛼. The type inference function takes aterm as input and outputs the inferred type as well as the inferred modality. For example, wheninferring the type for a term 𝑀𝑁 , the type inference function first infers a type 𝐴 ⊸𝛼 𝐵 and aProc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

Proto-Quipper with Dynamic Lifting

11:21

modality 𝛽 for 𝑀, and then it infers a type 𝐴 and a modality 𝛾 for the term 𝑁 , so the type inferencefunction will return the type 𝐵 and the inferred modality 𝛼 & 𝛽 & 𝛾.
We now discuss several Proto-Quipper-Dyn programs that make use of dynamic lifting. An
experimental implementation of Proto-Quipper-Dyn is available from https://gitlab.com/frankpeng-fu/dpq-remake, and the programs in Listings 1ś6 have been tested with that implementation.
Note that several of the following example programs make use of recursion. While we do notformally treat recursion in this paper, it is included in the prototype implementation.

5.1 Quantum Teleportation
The following circuit implements a one-qubit quantum teleportation protocol.

H
0

H

0

Meas

Meas
X

Z

This circuit is generated by the following Proto-Quipper-Dyn programs.
alice1 : !( Qubit -> Qubit -> Bit *Bit )alice1 a q =let (a , q) = CNot a q
q = H qin ( Meas a , Meas q)bob1 : !( Qubit -> Bit -> Bit -> Qubit)
bob1 q x y =let (q , x) = C_X q x(q , y) = C_Z q y_ = Discard x_ = Discard yin q

Listing 1. Alice and Bob circuits

bell00 : !( Unit -> Qubit * Qubit )bell00 u =let a = Init0 ()b = Init0 ()in CNot b (H a)tele1 : !( Qubit -> Qubit )tele1 q =let (b , a) = bell00 ()(x , y) = alice1 a q
z = bob1 b x y
in z
boxTele : Circ ( Qubit , Qubit )boxTele = box Qubit tele1

Listing 2. Teleportation circuit

As can be seen in Listings 1 and 2, the modality information is not visible to the programmer.
Because the programs in Listings 1 and 2 do not use dynamic lifting, the modalities in the fully
annotated types are all 1. For example, the fully annotated type of tele1 is !1 (Qubit ⊸1 Qubit).
We can therefore box tele1 into a quantum circuit. The evaluation of boxTele occurs on a classicalcomputer and generates the circuit diagram above.
For comparison, let us consider the following Proto-Quipper-Dyn programs that implement
quantum teleportation using dynamic lifting.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

11:22Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger

alice2 : !( Qubit -> Qubit -> Bool *Bool )
alice2 a q =let (a , q) = CNot a q
q = H qin ( dynlift ( Meas a) , dynlift ( Measq))bob2 : !( Qubit -> Bool -> Bool ->Qubit )
bob2 q x y =let q = if x then QNot q else q
q = if y then ZGate q else q
in q

Listing 3. Alice and Bob functions

tele2 : !( Qubit -> Qubit )tele2 q =let (b , a) = bell00 ()(x , y) = alice2 a q
z = bob2 b x yin z-- The following will raise an error
boxAttempt : Circ ( Qubit , Qubit )boxAttempt = box Qubit tele2
test : Bool
test =
dynlift ( Meas ( tele2 ( Init0 () )))Listing 4. Teleportation function

As before, the code in Listings 3 and 4 contains no modality annotations. In the alice2 function,
dynamic lifting is used right after the measurement gate Meas : Qubit → Bit. Accordingly, thefully annotated type of alice2 is !1 (Qubit ⊸1 Qubit ⊸0 Bool ∗ Bool). The bob2 function thenuses if-then-else expressions to decide whether to apply the gates QNot and ZGate, rather thanapplying the bit-controlled gates C_X and C_Z, as in the bob1 function in Listing 1.
The tele2 function calls the bob2 function with the booleans provided by the alice2 function.
Hence, the tele2 function implicitly uses dynamic lifting. Its fully annotated type is !1 (Qubit ⊸0
Qubit). Because of the modality inference, the type checker will issue a typing error for the
boxAttempt function. According to the typing rule for box, the box Qubit function requires anargument of type !1 (Qubit ⊸1 Qubit), which is distinct from the type of tele2. This error is sensible
because the tele2 function does not correspond to a circuit.
The test function applies tele2 to an input qubit in the |0⟩ state. The output value of test should
then be False with probability 1. Note that the evaluation of test requires access to a quantum
computer or a simulator.
5.2

Magic State Distillation

Magic states are quantum states that can be used, in conjunction with Clifford gates, to perform
universal quantum computing fault tolerantly [Bravyi and Kitaev 2005]. For example, there is a√𝜋𝑖standard method to implement a 𝑇 gate using the magic state (|0⟩ + 𝑒 4 |1⟩)/ 2, along with Cliffordgates and measurements. This enables the application of any operation from the Clifford+𝑇 gateset, a well-known universal set of quantum gates [Nielsen and Chuang 2002].
√
𝜋𝑖
The process of producing a magic state such as (|0⟩ + 𝑒 4 |1⟩)/ 2 from several imperfect states
is called magic state distillation [Bravyi and Kitaev 2005]. In order to distill a magic state |𝑀⟩, one
first prepares several qubits in a state that approximates |𝑀⟩ up to an error rate 𝜖. A carefully
designed quantum circuit is then applied to these qubits and some of them are measured. If allof the measurement results are 0, then the remaining qubits are guaranteed to be in a state thatapproximates |𝑀⟩ up to an improved error rate 𝜖 ′ < 𝜖. If any one of the measurement results is 1,
then all of the qubits are discarded and the entire process is restarted. In practice, several rounds of
distillation are required to obtain a state that approximates |𝑀⟩ up to an acceptable error rate.
A Proto-Quipper-Dyn implementation of Bravyi and Kitaev’s distillation algorithm is given in
Listing 5. In the distill function, we first apply a five-qubit error correction circuit fiveQubits tothe inputs, then measure the qubits and, through dynamic lifting, promote the resulting bits to
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

Proto-Quipper with Dynamic Lifting

11:23

distill : ! ( Qubit * Qubit * Qubit * Qubit * Qubit -> Maybe Qubit )distill input =let (a1 , a2 , a3 , a4 , a5 ) = fiveQubits input
a1 ' = dynlift ( Meas a1 )a2 ' = dynlift ( Meas a2 )a3 ' = dynlift ( Meas a3 )a4 ' = dynlift ( Meas a4 )in if a1 ' || a2 ' || a3 ' || a4 'then let a = dynlift ( Meas a5 ) in Nothingelse Just a5
distillation : ! ( Nat -> Qubit )distillation n =case n of
Z -> prepMixedState ()S n ' ->
let q1 = distillation n 'q2 = distillation n 'q3 = distillation n 'q4 = distillation n 'q5 = distillation n 'incase distill (q1 , q2 , q3 , q4 , q5 ) of
Nothing -> distillation n
Just q -> qListing 5. Bravyi and Kitaev’s algorithm

booleans. If all of the booleans are False, the distillation was successful and we return the remaining
qubit. Otherwise the distillation failed, so we discard the unmeasured qubit and return nothing.
Dynamic lifting is essential for defining the distill function because in this case the if-then-else
expression cannot be implemented as a circuit.
The distillation function performs 𝑛 rounds of magic state distillation. The function prepMixedState prepares an initial imperfect state. The distillation function is a recursive function thatassumes five successful distillations from the previous round and then applies the distill function
to the resulting qubits. If that function returns a qubit, the 𝑛-th round of distillation was successful,otherwise it will restart the whole process.
5.3

Repeat-Until-Success

The repeat-until-success paradigm provides a technique to apply a unitary that cannot be implemented exactly, at the cost of potentially running the same circuit multiple times. In order toapply a non-Clifford+T gate 𝑁 to a target qubit |𝜙⟩, one first initializes several ancillary qubits
before applying a well-chosen Clifford+T circuit 𝐶 to the target and the ancillas and measuring theancillas. If all of the measurement results are 0, the target qubit is guaranteed to be in the state
𝑁 |𝜙⟩. Otherwise, a correction is applied to the target to return it to its initial state and the process
is repeated.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

11:24Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger

Consider the following circuit used in [Paetznick and Svore 2014] to illustrate the implementation√of the gate 𝑉3 = 𝐼 +2𝑖𝑍
using the repeat-until-success method.
5
T
0

H

T*
0

T
H

H

Z

Meas
T

H

Meas

The top wire is the target qubit, while the wires below it are the ancillas. We apply a sequence ofgates (𝐻 , 𝐻 , 𝑇 ∗ , 𝐶𝑁𝑂𝑇 , 𝑇 , and 𝐻 ) to the ancillas before measuring the first ancilla. If, as we assume
here, the measurement result is 0, then we apply a sequence of gates (𝑇 , 𝑍 , 𝐶𝑁𝑂𝑇 , 𝑇 , and 𝐻 ) to
the target qubit and the second ancilla before measuring the second ancilla. Assuming, again, thatthe measurement result is 0, we then know that the target qubit is in the desired state. Note thatthe circuit above is not a representation of the entire repeat-until-success protocol. Instead, it is
the circuit constructed in the event that both measurement results are 0 (which can be shown tooccur with probability 5/8). If the measurements yield different results, the circuit constructed by
the repeat-until-success protocol is different. For example, if the result of the second measurement
is 1, a 𝑍 gate must be applied to the target qubit to return it to its initial state.
Listing 6 gives a precise description of the implementation of 𝑉3 in Proto-Quipper-Dyn.
v3 : !( Qubit -> Qubit )v3 q =
let a1 = tgate_inv (H ( Init0 () ))a2 = H ( Init0 () )(a1 , a2 ) = CNot a1 a2
a1 = H ( TGate a1 )in if dynlift ( Meas a1 )then
let _ = Discard ( Meas a2 )in v3 qelse let q = ZGate ( TGate q)(a2 , q) = CNot a2 q
a2 = H ( TGate a2 )in if dynlift ( Meas a2 )then v3 ( ZGate q)else qListing 6. A repeat-until-success example

Once again, dynamic lifting plays an essential role here. Note that the v3 function has type
!1 (Qubit ⊸0 Qubit); it is a quantum computation, rather than a quantum circuit.
6 CONCLUSION
We have given an axiomatization of an enriched categorical semantics for Proto-Quipper withdynamic lifting. We defined a type system with a modality to keep track of functions that use
dynamic lifting. The main benefit of our type system is that it statically ensures that the boxing
operation can only be applied to a function that does not use dynamic lifting. We also gave an
operational semantics for dynamic lifting. The operational semantics models both circuit generationand circuit execution. We also defined an abstract categorical semantics for this language andproved that the type system and the operational semantics are sound with respect to it. Lastly, wegave some examples of quantum algorithms that rely on dynamic lifting.
There are many things left to be done. One of them is how to combine dynamic lifting withdependent types and/or recursion. At this point, we have a model for dynamic lifting [Fu et al. 2022a],Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

Proto-Quipper with Dynamic Lifting

11:25

but it does not support dependent types or recursion. We also have a model for Proto-Quipper
with dependent types [Fu et al. 2020a], but it does not support dynamic lifting or recursion. Finally,
Lindenhovius et al. have a model for Proto-Quipper with recursion [Lindenhovius et al. 2018], but
it does not support dynamic lifting or dependent types. We do not think that adding recursion toProto-Quipper-Dyn would create fundamental difficulties at the level of the syntax, type system, or
operational semantics (although languages with recursion are usually better handled by small-step
operational semantics rather than the big-step semantics we considered here). On the other hand,finding a concrete denotational semantics gets more complicated the more features are includedin the programming language, and how to add dependent types or recursion to a semantics ofProto-Quipper-Dyn is an open problem.
ACKNOWLEDGEMENTS
We thank the referees for their thoughtful comments. This work was supported by the Natural
Sciences and Engineering Research Council of Canada (NSERC) and by the Air Force Office of
Scientific Research under Award No. FA9550-21-1-0041.
REFERENCES
Nick Benton. 1995. A mixed linear and non-linear logic: Proofs, terms and models (extended abstract). In Proceedings of
the 8th Workshop on Computer Science Logic, CSL’94, Selected Papers (Springer Lecture Notes in Computer Science 933).
121ś135.
Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin Vechev. 2020. Silq: A High-Level Quantum Language withSafe Uncomputation and Intuitive Semantics. In Proceedings of the 41st ACM SIGPLAN Conference on Programming
Language Design and Implementation (London, UK) (PLDI 2020). Association for Computing Machinery, New York, NY,
USA, 286ś300. https://doi.org/10.1145/3385412.3386007
Francis Borceux. 1994. Handbook of Categorical Algebra, Volume 2: Categories and Structures. Cambridge University Press.
Sergey Bravyi and Alexei Kitaev. 2005. Universal quantum computation with ideal Clifford gates and noisy ancillas. PhysicalReview A 71, 2 (2005), 022316.
Andrea Colledan and Ugo Dal Lago. 2022. On dynamic lifting and effect typing in circuit description languages (extended
version). (2022). Available from arXiv:2202.07636.
Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger. 2020b. A tutorial introduction to quantum circuit programmingin dependently typed Proto-Quipper. In Proceedings of the 12th International Conference on Reversible Computation, RC
2020, Oslo, Norway (Lecture Notes in Computer Science, Vol. 12227). Springer, 153ś168. https://doi.org/10.1007/978-3-03052482-1_9 Also available from arXiv:2005.08396.
Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger. 2022a. A biset-enriched categorical model for Proto-Quipper withdynamic lifting. (April 2022). To appear in QPL 2022. Available from arXiv:2204.13039.
Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger. 2022b. Proto-Quipper with dynamic lifting. (2022). Available fromarXiv:2204.13041.
Peng Fu, Kohei Kishida, and Peter Selinger. 2020a. Linear dependent type theory for quantum programming languages. In
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020, Saarbrücken, Germany.
440ś453. https://doi.org/10.1145/3373718.3394765 Also available from arXiv:2004.13472.
Alexander Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. 2013a. An introduction toquantum programming in Quipper. In Proceedings of the 5th International Conference on Reversible Computation, RC 2013,
Victoria, British Columbia (Lecture Notes in Computer Science, Vol. 7948). Springer, 110ś124. https://doi.org/10.1007/978-3642-38986-3_10 Also available from arXiv:1304.5485.
Alexander Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. 2013b. Quipper: a scalable quantum
programming language. In Proceedings of the 34th Annual ACM SIGPLAN Conference on Programming Language Design and
Implementation, PLDI 2013, Seattle (ACM SIGPLAN Notices, Vol. 48(6)). 333ś342. https://doi.org/10.1145/2499370.2462177
Also available from arXiv:1304.3390.
G. M. Kelly. 1982. Basic concepts of enriched category theory. Lecture Notes of the London Mathematical Society, Vol. 64.
Cambridge University Press.
Dongho Lee, Valentin Perrelle, Benoît Valiron, and Zhaowei Xu. 2021. Concrete categorical model of a quantum circuitdescription language with measurement. In 41st IARCS Annual Conference on Foundations of Software Technology andTheoretical Computer Science, FSTTCS 2021 (LIPIcs, Vol. 213), Mikolaj Bojanczyk and Chandra Chekuri (Eds.). Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 51:1ś51:20. https://doi.org/10.4230/LIPIcs.FSTTCS.2021.51
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.

11:26Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger

Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev. 2018. Enriching a linear/non-linear lambda calculus: A
programming language for string diagrams. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer
Science (Oxford, United Kingdom) (LICS ’18). Association for Computing Machinery, New York, NY, USA, 659ś668.
https://doi.org/10.1145/3209108.3209196
MetaOCaml 2020. MetaOCaml ś an OCaml dialect for multi-stage programming. https://okmij.org/ftp/ML/MetaOCaml.html.
Accessed: 2022-10-05.
Eugenio Moggi. 1991. Notions of computation and monads. Information and Computation 93, 1 (1991), 55ś92.
Michael A. Nielsen and Isaac L. Chuang. 2002. Quantum Computation and Quantum Information. Cambridge University
Press.
Bernhard Ömer. 1998. A Procedural Formalism for Quantum Computing. Master’s thesis. Department of Theoretical Physics,
Technical University of Vienna. http://tph.tuwien.ac.at/~oemer/qcl.html
Adam Paetznick and Krysta M. Svore. 2014. Repeat-until-success: Non-deterministic decomposition of single-qubit unitaries.
Quantum Information and Computation 14, 15ś16 (2014), 1277ś1301. https://doi.org/10.26421/QIC14.15-16-2 Also
available from arXiv:1311.1074.
Jennifer Paykin, Robert Rand, and Steve Zdancewic. 2017. QWIRE: a core language for quantum circuits. In Proceedingsof the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (ACM SIGPLAN Notices, Vol. 52). ACM,
846ś858.
Benjamin C. Pierce and David N. Turner. 2000. Local type inference. ACM Transactions on Programming Languages andSystems (TOPLAS) 22, 1 (2000), 1ś44.
Mathys Rennela and Sam Staton. 2020. Classical control, quantum circuits and linear logic in enriched category theory.
Logical Methods in Computer Science 16, 1 (2020), 30:1ś24. https://doi.org/10.23638/LMCS-16(1:30)2020
Francisco Rios and Peter Selinger. 2018. A categorical model for a quantum circuit description language. Extended
Abstract. In Proceedings of the 14th International Conference on Quantum Physics and Logic, QPL 2017, Nijmegen (Electronic
Proceedings in Theoretical Computer Science, Vol. 266). 164ś178. https://doi.org/10.4204/EPTCS.266.11 Also available
from arXiv:1706.02630.
Neil J. Ross. 2015. Algebraic and logical methods in quantum computation. Ph. D. Dissertation. Dalhousie University,
Department of Mathematics and Statistics. Available from arXiv:1510.02198.
Peter Selinger. 2004. Towards a quantum programming language. Mathematical Structures in Computer Science 14, 4 (2004),
527ś586.
Peter Selinger and Benoît Valiron. 2009. Quantum lambda calculus. In Semantic Techniques in Quantum Computation, SimonGay and Ian Mackie (Eds.). Cambridge University Press, Chapter 4, 135ś172.
Walid Taha and Tim Sheard. 2000. MetaML and multi-stage programming with explicit annotations. Theoretical Computer
Science 248, 1 (2000), 211ś242. https://doi.org/10.1016/S0304-3975(00)00053-0 PEPM’97.

Received 2022-07-07; accepted 2022-11-07

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 11. Publication date: January 2023.