# On Dynamic Lifting and Effect Typing in Circuit Description Languages

Andrea Colledan, Ugo Dal Lago

<figure><img src="image_1.png" /></figure>

## To cite this version:

Andrea Colledan, Ugo Dal Lago. On Dynamic Lifting and Effect Typing in Circuit Description Languages. TYPES 2022 - 28th International Conference on Types for Proofs and Programs, Jun 2022, Nantes, France. 10.4230/LIPIcs.TYPES.2022.3 . hal-04350852

HAL Id: hal-04350852

https://inria.hal.science/hal-04350852v1

Submitted on 18 Dec 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# On Dynamic Lifting and Effect Typing in Circuit Description Languages

Andrea Colledan

University of Bologna, Italy
INRIA Sophia Antipolis, France

Ugo Dal Lago

University of Bologna, Italy
INRIA Sophia Antipolis, France

## Abstract

In the realm of quantum computing, circuit description languages represent a valid alternative to traditional QRAM-style languages. They indeed allow for finer control over the output circuit, without sacrificing flexibility nor modularity. We introduce a generalization of the paradigmatic lambda-calculus Proto-Quipper-M, which models the core features of the quantum circuit description language Quipper. The extension, called Proto-Quipper-K, is meant to capture a very general form of dynamic lifting. This is made possible by the introduction of a rich type and effect system in which not only computations, but also the very types are effectful. The main results we give for the introduced language are the classic type soundness results, namely subject reduction and progress.

**2012 ACM Subject Classification** Theory of computation → Operational semantics; Theory of computation → Type theory; Hardware → Quantum computation

**Keywords and phrases** Circuit-Description Languages, λ-calculus, Dynamic lifting, Type and effect systems

Digital Object Identifier 10.4230/LIPIcs.TYPES.2022.3

Related Version Extended Version: https://arxiv.org/abs/2202.07636 [2]

**Funding** The research leading to these results has received funding from the European Union - NextGenerationEU through the Italian Ministry of University and Research under PNRR - M4C2 - I1.4 Project CN00000013 "National Centre for HPC, Big Data and Quantum Computing".

## 1 Introduction

Despite the undeniable fact that large-scale, error-free quantum hardware has yet to be built [19], research into programming languages specifically designed to be compiled towards architectures including quantum hardware has taken hold in recent years [17]. Most of the proposals in this sense (see [9, 22, 24] for some surveys) concern languages that either express or can be compiled into some form of *quantum circuit* [15], which can then be executed by quantum hardware. This reflects the need to have tighter control over the kind and amount of quantum resources that programs employ. In this scenario, the idea of considering high-level languages that are specifically designed to *describe* circuits and in which the latter are treated as first-class citizens is particularly appealing.

A typical example of this class of languages is **Quipper** [10, 11], whose underlying design principle is precisely that of enriching a very expressive and powerful functional language like **Haskell** with the possibility of manipulating quantum circuits. In other words, programs do not just build circuits, but also treat them like data, as can be seen in the example from Figure 1. **Quipper**'s meta-theory has been studied in recent years through the introduction of a family of research languages that correspond to suitable **Quipper** fragments and extensions,

<figure><img src="image_3.png" /></figure>

© Andrea Colledan and Ugo Dal Lago;
licensed under Creative Commons License CC-BY 4.0

28th International Conference on Types for Proofs and Programs (TYPES 2022).

Editors: Delia Kesner and Pierre-Marie Pédrot; Article No. 3; pp. 3:1–3:21

<figure><img src="image_4.png" /></figure>

LIPICS

Leibniz International Proceedings in Informatics

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
## 3:2 On Dynamic Lifting and Effect Typing in Circuit Description Languages

```
alice :: Qubit -> Qubit -> Circ (Bit,Bit)
alice q a = do
    a <- qnot a 'controlled' q
    q <- hadamard q
    (x,y) <- measure (q,a)
    return (x,y)
```

<figure><img src="image_5.png" /></figure>

Figure 1 Alice's part of the quantum teleportation circuit. The Quipper program on the left builds the circuit on the right, but while doing so it also manipulates the smaller circuit qnot a, enriching it with control.

```
teleport :: Qubit -> Qubit -> Qubit -> Circ Qubit
teleport b q a = do
    a <- qnot a 'controlled' q
    q <- hadamard q
    (x,y) <- measure (q,a)
    (u,s) <- dynamic_lift (x,y)
    b <- if s then gate_X b else return b
    b <- if u then gate_Z b else return b
    return b
```

<figure><img src="image_6.png" /></figure>

Figure 2 Quantum teleportation circuit with dynamic lifting. The gray box is not a gate, but rather represents the dynamic lifting of bit wires x and y into variables u and s and the extension of the circuit with one of four possible continuations for the remaining wire b, depending on the outcome of the intermediate measurements.

which usually take the form of linear λ-calculi. We are talking about a family of languages whose members include Proto-Quipper-S [21], Proto-Quipper-M [20], Proto-Quipper-D [5, 7], Proto-Quipper-L [13] and Proto-Quipper-Dyn [6].

An aspect that until very recently has only marginally been considered by the research community is the study of the meta-theory of so-called *dynamic lifting*, i.e. the possibility of allowing the (classical) value flowing in one of the wires of the underlying circuit, naturally unknown at circuit building time, to be *visible* in the host program for control flow. As an example, one could append a unitary to some of the wires *only if* a previously performed measurement has yielded a certain outcome. This is commonly achieved in many quantum algorithms via classical control, but Quipper also offers a higher-level solution precisely in the form of dynamic lifting, as can be seen in the example program in Figure 2. Notably, such a program cannot be captured by any of the calculi in the Proto-Quipper family, with the exception of Proto-Quipper-L [13] and Proto-Quipper-Dyn [6], arguably the most recent additions to the family.

Looking at the Quipper program in Figure 2, one immediately realizes that the two branches of both occurrences of the `if` operator change the underlying circuit in a uniform way, i.e. the number and type of the wires are the same in either branch. What if, for instance, we wanted to condition the execution of a measurement on a lifted value, like in Figure 3? Unfortunately, Quipper does *not* allow the program in Figure 3 to be typed, on account of the two branches of the `if` operators having different types. A program such as this could come from the so-called *measurement calculus* [4], where it would be referred to as a *pattern*, i.e. a sequence of simple operations that act on qubits in a way not so different from what happens in quantum circuits, but with the crucial difference that the basis of a
oneWay :: Qubit -> Qubit -> Bit

oneWay q a = do

q <- hadamard q

x <- measure q

u <- dynamic_lift x

a <- if u then meas_alpha a else return a

a <- if not u then meas beta a else return a

return a

<figure><img src="image_7.png" /><figcaption>Figure 3 An example of conditional measurement, where meas_α and meas_β measure a qubit in two distinct bases. This program is ill-typed in Quipper.</figcaption></figure>

<figure><img src="image_8.png" /><figcaption>Figure 4 The circuit produced by the program in Figure 3 without the last conditional.</figcaption></figure>

measurement can depend on the outcome of previous measurements. Globally, the program builds a uniformly typed circuit (which always outputs a bit), but locally there are some intermediate steps where the output type is heterogeneous. Of course, in this case, the two `if` operators could be collapsed into one, avoiding local heterogeneity, but there are cases in which keeping two conditionals would be preferable. For example, we might be interested in doing away with the second `if` and reusing the resulting heterogeneous sub-circuit (shown in Figure 4) multiple times when building a more complex circuit, changing only the basis of the second measurement from time to time.

Giving a proper status to the programs that build this kind of heterogeneous circuits would thus endow the programming language with greater flexibility and modularity, so it is natural to wonder whether that of Quipper is an intrinsic limitation or if a richer type system can deal with a more general form of circuits.

In this paper, we introduce a generalization of Proto-Quipper-M, called Proto-Quipper-K, in which dynamic lifting is available in a very general form, even more so than in the original Quipper language. This newly introduced language is capable of producing not only circuits like the one in Figure 2, but rather a more general class of circuits whose structure and type essentially depend on the values flowing through the lifted channels, like the one in Figure 4. We show throughout the paper that this asks for a non-trivial generalization of Proto-Quipper-M's type system, in which types reflect the different behaviors a circuit can have. This is achieved through a type and effect system [16] which assigns any Proto-Quipper-K computation (possibly) distinct types depending on the state of the lifted variables. The main results, beside the introduction of the language itself, its type system, and its operational semantics, are the type soundness results of subject reduction and progress, which together let us conclude that well-typed Proto-Quipper-K programs do not go wrong. An extended version of this paper with more detailed definitions and proofs is available [2].

## 2 Circuits and Dynamic Lifting: a Bird's-Eye View

This section is meant to provide an informal introduction to the peculiarities of the Proto-Quipper family of paradigmatic programming languages, for the non-specialists. The host language, namely Haskell, is modeled as a linearly typed λ-calculus. Terms, in addition
3:4 On Dynamic Lifting and Effect Typing in Circuit Description Languages

$$
\begin{align*}
\lambda q_{\text{Qubit}} \cdot \lambda a_{\text{Qubit}} . \text{let } (q, a) &= \text{apply}(\text{CNOT}, (q, a)) \text{ in} \\
&\quad \text{let } q = \text{apply}(H, q) \text{ in } \text{apply}(\text{Meas}_2, (q, a))
\end{align*}
$$

■ **Figure 5** A Proto-Quipper-M program describing the circuit shown in Figure 1. We assume that we have a constant boxed circuit *CNOT*, *H*, *Meas2*, etc. for every available primitive operation.

to manipulating ordinary data structures and computing (possibly) higher-order functions,
are allowed to act on an underlying circuit, which we usually refer to as *C*. During program
evaluation, *C* can be modified with the addition of wires, gates or entire sub-circuits. This
is made possible through a dedicated operator called **apply**. But how can the programmer
specify *where* in *C* these modifications have to be carried out? This is possible thanks to
the presence of *labels*, that is, names that identify distinct output wires of *C*. These labels
are ordinary terms which can be passed around, but have to be treated linearly. Among
other things, they can be passed to **apply**, together with the specification of which gate or
sub-circuit is to be appended to the underlying circuit *C*.

But is **apply** the only way of manipulating circuits? The answer is negative. Circuits,
once built by means of a term, can be “boxed”, potentially copied, and passed to other parts
of the program, where they can be used, usually by appending them to multiple parts of the
underlying circuit. From a linguistic point of view, this is possible thanks to an additional
operator, called **box**, which is responsible for turning a circuit-building term *M* of type
!(*T* → *U*) – the type of duplicable functions from label tuples to label tuples – into a term
of type *Circ*(*T*, *U*) – the type of circuits. The term **box* *M* does not touch the underlying
circuit, but rather evaluates *M* “behind the scenes”, in a sandboxed environment, to obtain
a standalone circuit which is then returned as a *boxed circuit*.

Measure as a Label-Lifting Operation

The above considerations are agnostic to the kind of circuits being built. In fact, any
type of circuit-like structure can be produced in output by programs of the **Proto-Quipper**
family of languages, provided that it can be interpreted as a morphism in an underlying
symmetric monoidal category [20]. If we imagine that the produced structure is an *actual*
quantum circuit, however, it is only natural to wonder whether all the examples of circuits
that we talked about informally in the introduction can be captured by some instance of
**Proto-Quipper**. Unsurprisingly, the program in Figure 1 is not at all problematic, and can be
handled easily by all languages in the **Proto-Quipper** family (see Figure 5).

The program in Figure 2, on the other hand, can only be handled by **Proto-Quipper-L** (see Figure 6) and **Proto-Quipper-Dyn**. In **Proto-Quipper-L**, a measurement can return the *Boolean value* corresponding to the outcome of the measurement. When this happens, the ongoing computation is split into two branches: one in which the Boolean output is true and one in which it is false. This way, further circuit-altering operations down the line can depend on the classical information produced by the intermediate measurement. In **Proto-Quipper-Dyn** on the other hand, a bespoke operator *dynlift* allows to turn a term of type *Bit* into a term of type *Bool*, whose result can be used to a similar effect.

How about the program in Figure 3? Unfortunately, this case exceeds the expressiveness
of both **Proto-Quipper-L** and **Proto-Quipper-Dyn**, in that it requires the distinct execution
branches to yield values of different *types*, although only temporarily. The two languages,
on the other hand, require all branches of a computation to share the same type, like in
**Quipper**. This is where our contribution starts.
$$
\begin{align*}
\lambda b_{\text{Qubit}} \cdot \lambda q_{\text{Qubit}} \cdot \lambda a_{\text{Qubit}} \cdot \text{let } (q, a) &= (\text{unbox } \text{CNOT}) (q, a) \text{ in} \\
\text{let } q &= (\text{unbox } H) q \text{ in} \\
\text{let } (u, s) &= (\text{unbox } \text{MeasLift2}) (q, a) \text{ in} \\
\text{let } b &= \text{if } s \text{ then } (\text{unbox } X) b \text{ else } b \text{ in} \\
\text{let } b &= \text{if } u \text{ then } (\text{unbox } Z) b \text{ else } b \text{ in } b
\end{align*}
$$

Figure 6 A Proto-Quipper-L program describing the circuit shown in Figure 2. Informally, terms of the form (unbox H)q correspond to terms of the form apply(H, q) in Proto-Quipper-M.

$$
u \begin{array}{c} \xrightarrow{1} \\ \downarrow \\ 0 \end{array} \epsilon
s \begin{array}{c} \xrightarrow{1} \\ \downarrow \\ 0 \end{array} \epsilon
$$

Figure 7 An example of a lifting tree. The empty tree is denoted by $\epsilon$.

The Basic Ideas Underlying Proto-Quipper-K

The approach to dynamic lifting that we follow in this paper is radical. The evaluation
of a term *M* involving the *apply* operator can give rise to the lifting of a bit value into
a variable *u* and consequently produce in output not a single result in the set *VAL* of
values, but possibly one distinct result for each possible value of *u*. Therefore, it is natural
to think of *M* as a computation that results in an object in the set *K*<sub>{u}</sub>(*VAL*), where
*K*<sub>{u}</sub> = *X* ↦→ (*{u}* → {0, 1}) → *X* is a functor such that, for each possible assignment of a
Boolean value to *u*, *K*<sub>{u}</sub>(*X*) returns an element of *X*.

What if *more than one* variable is lifted? For example, a program could lift *s* after having
lifted *u*, but *only if* the latter has value 0. This shows that one cannot just take *K*<sub>{u,s}</sub> =
*X* ↦→ (*{u,s}* → {0, 1}) → *X*, simply because not all assignments in *{u,s}* → {0, 1} are
relevant. Instead, one should just focus on the three assignments (*u* = 0, *s* = 0), (*u* = 0, *s* = 1)
and (*u* = 1), namely those assignments which are consistent with the tree in Figure 7, which
we call a *lifting tree*. This is a key concept in this work, which we will discuss in detail in
Section 3. Our type system captures the lifting pattern of an underlying well-typed program
through a lifting tree *t* and the result of the corresponding computation is an element of
*K*<sub>*t*</sub>(*VAL*) where *K*<sub>*t*</sub> = *X* ↦→ (*P*<sub>*t*</sub> → *X*) and *P*<sub>*t*</sub> is the set of all assignments of variables
which describe a root-to-leaf path in *t*. Since by design we want to handle situations in which
a circuit, and by necessity the term building it, can produce results which have distinct
*types* – and not only distinct *values* – depending on the values of the lifted variables, we also
employ (in the spirit of the type and effects paradigm [16]) an effectful notion of *type*, in
which computations are typed according to an element of *K*<sub>*t*</sub>(*TYPE*), where *TYPE* is the
set of Proto-Quipper-K types.

3 Generalized Quantum Circuits

A quantum circuit describes a quantum computation by means of the application of *quantum gates*, which represent basic unitary operations, to a number of typed *input wires*, to obtain a number of typed *output wires*. In this section, we introduce a general form of circuits in which the application of *any gate* to one or more wires can be carried out *conditionally* on the classical value flowing in a lifted channel. This is possible even when the gate inputs are *not* the same number and type of the gate outputs. This implies that the number and type of the outputs of a circuit can depend on the values flowing in its wires.
3:6 On Dynamic Lifting and Effect Typing in Circuit Description Languages

<table><caption>Figure 8 Syntax and rule system for M-types and M-values.</caption>
  <tbody>
    <tr>
      <td>M-types</td>
      <td>MTYPE</td>
      <td>T, U</td>
      <td>::= 1 | w | T &otimes; U.</td>
    </tr>
    <tr>
      <td>M-values</td>
      <td>MVAL</td>
      <td>&#x20D7;, &#x20D8;</td>
      <td>::= * | &ell; | (&#x20D7;, &#x20D8;).</td>
    </tr>
    <tr>
      <td>unit</td>
      <td>&emptyset; &vdash;<sub>m</sub> * : 1</td>
      <td>label</td>
      <td>&ell; : w &vdash;<sub>m</sub> &ell; : w</td>
    </tr>
    <tr>
      <td></td>
      <td></td>
      <td>tuple</td>
      <td>
        Q &vdash;<sub>m</sub> &#x20D7; : T<br>
        L &vdash;<sub>m</sub> &#x20D8; : U<br>
        Q, L &vdash;<sub>m</sub> (&#x20D7;, &#x20D8;) : T &otimes; U
      </td>
    </tr>
  </tbody>
</table>

A Syntax for Circuits

We represent the inputs and outputs of a circuit as *label contexts*, that is, partial mappings from the set *L* of *label names* to the set *W* = {*Bit*, *Qubit*} of wire types. The set *L* contains precisely the kind of labels that we mentioned in Section 2, therefore a label context is a way to attach type information to labeled wires. We write the set of all label contexts as *Q*.

Whereas the order of wires in a circuit as a whole is irrelevant, the order of wires in a *gate application* is crucial. For this reason, we perform gate applications not on label contexts, but rather on *label tuples*, which imbue label contexts with a specific ordering via a simple form of typing judgment. The grammar and typing rules for label tuples, which we call *M-values* and whose types we call *M-types*, following [20], are given in Figure 8. Note that *l* ∈ *L*, *w* ∈ *W*, and *Q* and *L* are label contexts whose disjoint union is denoted by *Q*, *L*.

► **Definition 1 (Gate Set).** Let $\mathcal{G}$ be a set of gates, equipped with two functions in Type : $\mathcal{G} \rightarrow$ MTYPE and outType : $\mathcal{G} \rightarrow$ MTYPE. We denote by $\mathcal{G}(T, U)$ the set of gates with input type T and output type U.

As an example, $\mathcal{G}$ (Qubit, Qubit) includes the so-called Hadamard gate, which is used to put a single qubit into a perfect superposition. Besides the set of labels $\mathcal{L}$, there is also another set of names, called $\mathcal{V}$, which is disjoint from it and contains the lifted variables. An assignment of lifted variables is then simply a finite sequence of equalities ($u_1 = p_1, \dots, u_n = p_n$) which assign the values $p_1, \dots, p_n \in \{0, 1\}$ to the distinct variables $u_1, \dots, u_n \in \mathcal{V}$, respectively. We usually indicate assignments with metavariables such as $a, b$ and $c$.

We now introduce a low-level language to describe quantum circuits at the gate level, which will serve as a target for circuit building in Proto-Quipper-K. We call it *circuit representation language* (CRL) and define it via the following grammar:

$$
C, D ::= \text{input}(Q) \mid C; a?g(\vec{l}) \rightarrow \vec{k} \mid C; a?\text{lift}(l) \Rightarrow u. \tag{1}
$$

The base case input(Q) corresponds to the trivial identity circuit that takes as input the wires represented by Q and does nothing to them. The notation a?g(\vec{l}) \to \vec{k} denotes the application of a gate g to the wires identified by \vec{l} to obtain the wires in \vec{k}, provided that the condition expressed by a is met. We simply write g(\vec{l}) \to \vec{k} when a gate is applied unconditionally (i.e. when a = \emptyset). Figure 9a shows a simple example of a CRL circuit consisting exclusively of gate applications.

On the other hand, $a?\text{lift}(\ell) \Rightarrow u$ represents the dynamic lifting of the bit wire $\ell$ if the condition expressed by $a$ is met. When we perform dynamic lifting on a bit, we promote its contents to a Boolean value that is bound to the lifted variable $u$. This variable can then be mentioned in subsequent assignments to control whether further operations in the circuit are executed or not. The introduction of $u$ thus naturally leads to two distinct execution branches: one in which $u=0$ and one in which $u=1$. As we do for gate applications, we write $\text{lift}(\ell) \Rightarrow u$ when a lifting operation is unconditional. A CRL circuit that performs dynamic lifting is shown in Figure 9b.
input(b₀ : Qubit, q₀ : Qubit, a₀ : Qubit);
CNOT(q₀, a₀) → (q₁, a₁);
H(q₁) → q₂;
Meas2(q₂, a₁) → (x, y);
lift(x) ⇒ u;
lift(y) ⇒ s;
(s = 1) ? X(b₀) → b₁;
(u = 1; s = 0) ? Z(b₀) → b₂;
(u = 1; s = 1) ? Z(b₁) → b₃;

(a) Circuit from Figure 1.

(b) Circuit from Figure 2.

<caption>**Figure 9** Two examples of CRL descriptions of a quantum circuit.</caption>

## Lifting Trees

Naturally, not all CRL expressions denote reasonable circuits. For example, conditioning the application of a gate on the value of a lifted variable which has not yet been introduced should be avoided, for obvious reasons. Capturing this idea at the type level is nontrivial, since the presence of a variable can itself depend on previous liftings. This is where the concept of lifting tree, which we introduced informally in Section 2, really comes into play.

**► Definition 2 (Lifting Tree).** We define the set $\mathcal{T}$ of lifting trees, along with their variable set on assignment $a$, seen as a function $\text{var}_a : \mathcal{T} \to \mathcal{P}(\mathcal{Y})$, as the smallest set of expressions and functions such that

■ $\epsilon \in \mathcal{T}$ with $\text{var}_a(\epsilon) = \emptyset$.

■ If $t_0 \in \mathcal{T}$ and $t_1 \in \mathcal{T}$, then for every $u$ that is neither in $\text{var}_0(t_0)$ nor in $\text{var}_0(t_1)$ we have $u \{t_0\} \{t_1\} \in \mathcal{T}$ and

$$ \text{var}_a(u \{t_0\} \{t_1\}) = \{u\} \cup \begin{cases} \text{var}_a(t_0) & \text{if } a(u) = 0, \\ \text{var}_a(t_1) & \text{if } a(u) = 1, \\ \text{var}_a(t_0) \cup \text{var}_a(t_1) & \text{if } a(u) \text{ is undefined.} \end{cases} \quad (2) $$

We often write $\text{var}(t)$ as shorthand for $\text{var}_0(t)$ to denote all the variables mentioned in $t$. By way of lifting trees, we can keep track of whether an assignment, representing a condition, is consistent with the current state of the lifted variables. Given a lifting tree $t$, we call $\mathcal{A}_t$ the set of such assignments (which is easily defined by induction on $t$, see [2]). Among these consistent assignments, there are some which are maximal, i.e. that cannot be further extended: they describe root-to-leaf paths in $t$ and correspond exactly to the elements of the set $\mathcal{P}_t$ which we introduced in Section 2. Unsurprisingly, for all $t$ we have $\mathcal{P}_t \subseteq \mathcal{A}_t$. As an example, let $t$ be the tree from Figure 7. We have $\text{var}(t) = \{u, s\}$, $\mathcal{A}_t = \{\emptyset, (u = 0), (u = 1), (s = 0), (s = 1), (u = 0, s = 0), (u = 0, s = 1)\}$ and $\mathcal{P}_t = \{(u = 1), (u = 0, s = 0), (u = 0, s = 1)\}$.

Finally, we can formally define one of the key notions of this paper, not only for circuits, but also for programs: given a generic set $X$, $\mathcal{K}_t(X)$ indicates the set $\mathcal{P}_t \to X$, which we call the *lifting* of $X$, and whose elements we refer to as *lifted objects*. Despite the fact that
3:8 On Dynamic Lifting and Effect Typing in Circuit Description Languages

<figure><img src="image_9.png" /><figcaption>Figure 10 An example of composition with overwriting.</figcaption></figure>

lifted objects are formally mappings, seeing them as decorated lifting trees whose leaves
are labeled with objects from X is perhaps more intuitive. Following this interpretation,
given $x \in X$, we indicate by $\{x\}$ the trivial lifted object in $\mathcal{K}_\epsilon(X)$ defined as the mapping
$\emptyset \mapsto x$, and by $u\{\xi_0\}\{\xi_1\}$ the object in $\mathcal{K}_{u\{t_0\}\{t_1\}}(X)$ defined as $a \mapsto \xi_{a(u)}(a')$, where
$\xi_0 \in \mathcal{K}_{t_0}(X)$, $\xi_1 \in \mathcal{K}_{t_1}(X)$ and $a' \in \mathcal{P}_{t_{a(u)}}$ is obtained from $a$ by excluding $u$ from its domain.
A graphical representation of this intuition can be found in the form of the trees shown in
figures 10 and 11.

► **Example 3.** Consider Figure 9. The CRL circuit on the left does not perform lifting and therefore has a trivial output $\{x : \text{Bit}, y : \text{Bit}\}$, while the CRL circuit on the right does and has output $u\{s\{b_0 : \text{Qubit}\}\{b_1 : \text{Qubit}\}\}\{s\{b_2 : \text{Qubit}\}\{b_3 : \text{Qubit}\}\}$.

The same intuition informs the various operations that we define homogeneously on lifting
trees and lifted objects. The first is a very natural one: if $t$ is a lifting tree and $\{x_a\}_{a \in I}$ is
a family of elements in $X$ indexed on a subset $I \subseteq \mathcal{P}_t$ of the root-to-leaf paths of $t$, then
the expression $t[x_a]_a^I$ stands for the lifted object obtained by sticking each $x_a$ to the leaf
of $t$ identified by $a \in I$. Note that this operation, which we call *composition*, is generally
loosely typed and can give rise to heterogeneous lifted objects. However, in the case $I = \mathcal{P}_t$,
the resulting lifted object belongs to $\mathcal{K}_t(X)$. In this case we also write $t[x_a]_a$ as shorthand
for $t[x_a]_{a}^{\mathcal{P}_t}$, whereas when $I$ is a singleton $\{b\}$ we usually omit the subscript $a$ and write
$t[x]^{\{b\}}$ for $t[x_a]^{\{b\}}$. We also allow already specified lifted objects to appear on the left of a
composition, in which case we overwrite the interested leaves. For instance, if $\Delta$ is a lifted
label context, we often write the expression $\Delta[Q]^{\{a\}}$ to denote the lifted label context that
associates $Q$ to $a$ and is otherwise equal to $\Delta$ on all the other branches.

► **Definition 4 (Composition).** Given $\xi \in \mathcal{K}_t(X)$, an index set $I \subseteq \mathcal{P}_t$ and a family $\{x_a\}_{a \in I}$ of elements in $X$, we define the composition of $\xi$ and $\{x_a\}_{a \in I}$, written $\xi[x_a]_a^I$, as

$$
\begin{align*}
\{y\}[x_a]_a^\emptyset &= \{y\}, \\
\{y\}[x_a]_a^{\{0\}} &= \{x_a\}, \\
u\{\xi_0\}\{\xi_1\}[x_a]_a^I &= u\{\xi_0[x_a]_{a_0}^{I_0}\}\{\xi_1[x_a]_{a_1}^{I_1}\},
\end{align*}
\tag{3}
$$

where $I_b = \{a|_{\text{var}(t)\setminus\{u\}} | a \in I \wedge a(u) = b\}$ and $a|_{\text{var}(t)\setminus\{u\}}$ denotes the exclusion of $u$ from the domain of $a$.

**Example 5.** Let $t = u \{s \{\epsilon\} \{\epsilon\} \} \{\epsilon\}$ and let $\Delta = u \{s \{q_0 : \text{Qubit}\} \{c_1 : \text{Bit}\} \} \{c_2 : \text{Bit}\} \in \mathcal{K}_t(\mathcal{Q})$ be a lifted label context, which graphically corresponds to the tree shown in Figure 10a. We have $\Delta[c_0 : \text{Bit}]^{\{u=0,s=0\}} = u \{s \{c_0 : \text{Bit}\} \{c_1 : \text{Bit}\} \} \{c_2 : \text{Bit}\} \in \mathcal{K}_t(\mathcal{Q})$, which corresponds to the tree shown in Figure 10b.

The second operation is a *flattening* operation, which we indicate with $\lfloor \cdot \rfloor$. Intuitively, if we have a lifted object whose leaves are themselves trees, the flattening operation “unwraps” the trees in the leaves so that they become sub-trees of said lifted object. Given a family of
<figure><img src="image_10.png" /><figcaption>Figure 11 An example of flattening.</figcaption></figure>

trees {$\mathbf{r}_a$}$_{a \in \mathcal{P}_t}$ the difference between $t[\mathbf{r}_a]_a$ and $\lfloor t[\mathbf{r}_a]_a \rfloor$ is therefore that the former is an element of $\mathcal{K}_t(\mathcal{T})$, whereas the latter is a proper element of $\mathcal{T}$. This operation is well-defined when $\mathrm{var}_a(t) \cap \mathrm{var}(\mathbf{r}_a) = \emptyset$ for every $a \in \mathcal{P}_t$. We can also flatten when we have have lifted objects on the right side of a composition: if we have $t[\xi_a]_a$, where $\xi_a \in \mathcal{K}_{\mathbf{r}_a}(X)$ for every $a \in \mathcal{P}_t$, then $\lfloor t[\xi_a]_a \rfloor \in \mathcal{K}_{\lfloor t[\mathbf{r}_a]_a \rfloor}(X)$.

A formal definition of flattening requires us to consider a slightly more general operation $\lfloor \cdot \rfloor^{\mathcal{V}}$, where $\mathcal{V}$ is a finite set of lifted variables which are accumulated as a lifted object is traversed. At the leaf level, $\lfloor \{x\} \rfloor^{\mathcal{V}} = x$ only if $x$ is a lifted object in which none of the lifted variables in $\mathcal{V}$ occur (a condition expressed in the first line of Equation 4). In case of name clashes, the whole operation is undefined and a renaming of lifted variables is required prior to composition and flattening.

**Definition 6 (Flattening).** Given $\xi \in \mathcal{K}_t(X)$, we define the flattening of $\xi$ under $\mathcal{V}$, written $\lfloor \xi \rfloor^{\mathcal{V}}$, as

$$ \lfloor \{y\} \rfloor^{\mathcal{V}} = \begin{cases} y & \text{if } \exists \mathbf{r}, Y \text{ s.t. } y \in \mathcal{K}_{\mathbf{r}}(Y) \text{ and } \mathcal{V} \cap \mathrm{var}(\mathbf{r}) = \emptyset, \\ \{y\} & \text{if } \nexists \mathbf{r}, Y \text{ s.t. } y \in \mathcal{K}_{\mathbf{r}}(Y), \end{cases} \quad (4) \\ \lfloor u \{\xi_0\} \{\xi_1\} \rfloor^{\mathcal{V}} = u \{\lfloor \xi_0 \rfloor^{\mathcal{V} \cup \{u\}}\} \{\lfloor \xi_1 \rfloor^{\mathcal{V} \cup \{u\}}\}. $$

The actual flattening operation that we employ in the rest of the paper can then be defined as $\lfloor \cdot \rfloor = \lfloor \cdot \rfloor^{\emptyset}$.

**Example 7.** Reconsider $t$ and $u \{s \{c_0 : \mathrm{Bit}\} \{c_1 : \mathrm{Bit}\} \} \{c_2 : \mathrm{Bit}\} = \Delta'$ from Example 5. Let $\xi = \Delta'[s \{c_2 : \mathrm{Bit}\} \{c_3 : \mathrm{Bit}\}] \{u=1\} = u \{s \{c_0 : \mathrm{Bit}\} \{c_1 : \mathrm{Bit}\} \} \{\{s \{c_2 : \mathrm{Bit}\} \{c_3 : \mathrm{Bit}\}\} \in \mathcal{K}_t(\mathcal{Q} \cup \mathcal{K}_{s \{\epsilon\} \{\epsilon\}}(\mathcal{Q}))\}$. Note that this object, corresponding to Figure 11a, is not properly a lifted label context, as one of its leaves is itself a lifted label context. Because $s$ does not occur in $\mathrm{var}_{u=1}(t) = \{u\}$, we can write $\lfloor \xi \rfloor = u \{s \{c_0 : \mathrm{Bit}\} \{c_1 : \mathrm{Bit}\} \} \{s \{c_2 : \mathrm{Bit}\} \{c_3 : \mathrm{Bit}\} \} \in \mathcal{K}_{\mathcal{V}}(\mathcal{Q})$, for $t' = u \{s \{\epsilon\} \{\epsilon\}\} \{s \{\epsilon\} \{\epsilon\}\}$. This is an actual lifted label context, which corresponds to Figure 11b.

In conjunction, these two operations greatly simplify our treatment of dynamic lifting, as they allow us to describe in detail the desired shape of a lifted object. For example, in later sections we often write $\Delta = \lfloor \Delta'[\Delta'', \Lambda]^{\{a\}} \rfloor$ to say that the lifted label context $\Delta$ is such that if we start from its root and follow the path described by $a$, we find a sub-tree $\Delta''$, $\Lambda$ (the disjoint union is lifted in a natural way, as the disjoint union of the corresponding leaves of $\Delta''$ and $\Lambda$ when these have the same underlying lifted tree), and that we are interested in only some elements of the corresponding lifted label context, for instance those that occur in $\Lambda$.
3:10 On Dynamic Lifting and Effect Typing in Circuit Description Languages

$$
\begin{array}{c}
\begin{array}{c}
\text{id} \\
\text{input}(Q) \vdash^\epsilon Q \triangleright \{Q\}
\end{array}
\\[2em]
\begin{array}{c}
\text{lift} \\
\frac{C \vdash^t Q \triangleright \Delta^a; \ell : \text{Bit} \quad a \in \mathcal{A}_t \quad u \notin \text{var}_a(t)}{C; a ? \text{lift}(\ell) \Rightarrow u \vdash^{t \lhd^a u \{\epsilon\}\{\epsilon\}} Q \triangleright \Delta^{<a} u \{\epsilon\}\{\epsilon\}}
\end{array}
\\[2em]
\begin{array}{c}
\text{gate} \\
\frac{C \vdash^t Q \triangleright \Delta^a; Q' \quad a \in \mathcal{A}_t \quad g \in \mathcal{G}(T, U) \quad Q' \vdash_m \vec{l} : T \quad L \vdash_m \vec{k} : U \quad \text{fresh}(\vec{k}, C)}{C; a ? g(\vec{l}) \rightarrow \vec{k} \vdash^t Q \triangleright \Delta^a; L}
\end{array}
\end{array}
$$

<caption>Figure 12 The rules for CRL circuit signatures.</caption>

A Formal System for Circuit Signatures

Now that we have introduced lifting trees and lifted objects as a means to reason about
dynamic lifting, we are ready to introduce the notion of signature of a circuit.

► **Definition 8 (Circuit Signature).** *Given a circuit C, a lifting tree t, a label context Q and a
lifted label context Δ, a circuit signature is an expression of the form C ⊢<t> Q ▷ Δ.*

Informally, $C \vdash^t Q \triangleright \Delta$ means that $C$ takes as input the labels in $Q$, performs lifting according to tree $t$ and outputs any of the leaves in $\Delta$, which is a lifted label context backed by $t$. More formally, a valid circuit signature is derived by the rules in Figure 12. Note that $\Delta^a; Q'$ represents the extension of $\Delta$ with $Q'$ on all leaves reachable by an assignment consistent with $a$. Formally, $\Delta^a; Q'$ is shorthand for $\Delta'[Q', Q_b]_{b}^{\mathcal{P}_t^a}$ if $\Delta = \Delta'[Q_b]_{b}^{\mathcal{P}_t^a}$, where $\mathcal{P}_t^a$ contains the paths in $\mathcal{P}_t$ which extend $a \in \mathcal{A}_t$. On the other hand, for any $\xi \in \mathcal{K}_t(X)$ and $r \in \mathcal{T}$ such that $\mathrm{var}_a(t) \cap \mathrm{var}(r) = \emptyset$, we write $\xi \prec^a r$ to denote $\xi$ in which every leaf $x$ reachable by an assignment consistent with $a$ is expanded to a sub-tree $r$ whose leaves are all $x$. More formally, $\xi \prec^a r$ is shorthand for $[\xi'[r[x_b]_b]_{b}^{\mathcal{P}_t^a}]$, if $\xi = \xi'[x_b]_{b}^{\mathcal{P}_t^a}$.

4 Proto-Quipper-K

We are finally ready to introduce Proto-Quipper-K, a programming language designed exactly to manipulate the kind of circuits that we presented in the previous section and guarantee the degree of flexibility that we mentioned in Section 2.

**4.1 Types and Terms**

The types and syntax of Proto-Quipper-K are given in Figure 13, where $x$ and $y$ range over
the set of variable names, $u_1, \dots, u_n$ over the set $\mathcal{V}$ of lifted variable names, $t$ over the
set $\mathcal{T}$ of lifting trees and Greek letters generally indicate lifted objects. More precisely,
$\alpha, \beta \in \mathcal{K}_t(\text{TYPE})$, $v \in \mathcal{K}_t(\text{MTYPE})$, $\mu \in \mathcal{K}_t(\text{TERM})$ and $\lambda \in \mathcal{K}_t(\text{MVAL})$, each for some $t$.
Note that parameter types are the types given to non-linear resources, i.e. duplicable values.
Note also that the M-values and M-types that we introduced in Section 3 are now a proper
subset of Proto-Quipper-K's values and types, respectively.

A value of the form `(el, C, λ)`<sub>t</sub> is what we called a *boxed circuit* in Section 2, that is, a datum representation of a circuit *C* that takes as input the labels in the tuple `(el, ...)`<sub>t</sub>, performs lifting according to *t* and outputs one of the possible label tuples of *λ* depending on the lifted variables in *t*. Correspondingly, parameter types of the form `Circ<sub>t</sub>(T, v)` are called *circuit types* and represent boxed circuits. Both boxed circuits and circuit types abstract over the lifted variables in `var(t)` and thus enjoy a notion of *α*-equivalence. The *box* and *apply* constructs are those described in Section 2 and they respectively introduce and consume boxed circuits. Specifically, the programmer is never expected to write values of the form `(el, C, λ)`<sub>t</sub> by hand.
<table><caption>Figure 13 Types and terms of Proto-Quipper-K.</caption><tr><td>Types</td><td>TYPE</td><td>A, B</td><td>::= 1 | w | A →<sub>t</sub> β | !α | Circ<sub>t</sub>(T, v) | A ⊗ B.</td></tr><tr><td>Parameter Types</td><td>PTYPE</td><td>P, R</td><td>::= 1 | !α | Circ<sub>t</sub>(T, v) | P ⊗ R.</td></tr><tr><td>M-types</td><td>MTYPE</td><td>T, U</td><td>::= 1 | w | T ⊗ U.</td></tr><tr><td>Terms</td><td>TERM</td><td>M, N</td><td>::= VW | let x = M in μ | let (x, y) = V in M<br>| force V | box<sub>T</sub> V | apply<sub>u<sub>1</sub>...,u<sub>n</sub></sub>(V, W) | return V.</td></tr><tr><td>Values</td><td>VAL</td><td>V, W</td><td>::= * | x | ℓ | λx<sub>A</sub>.M | lift M | (ℓ̃, C, λ)<sub>t</sub> | (V, W).</td></tr><tr><td>M-values</td><td>MVAL</td><td>ℓ̃, k</td><td>::= * | ℓ | (ℓ̃, k).</td></tr></table>

Rather, they are expected to introduce the desired circuit by supplying an appropriate circuit-building term *M* to the box operator, obtaining a term of the form `box<sub>T</sub>(lift *M*). The use of lift guarantees that *M* does not make use of any linear resources from the current environment, i.e. that it can be safely evaluated in an isolated environment to produce *C*. After a boxed circuit `((ℓ̃, C, λ)<sub>t</sub>)` is introduced, the programmer can potentially copy it and apply it to the underlying circuit *D* via a term of the form `apply<sub>u<sub>1</sub>...,u<sub>n</sub></sub>((ℓ̃, C, λ)<sub>t</sub>, k)`. Such a term “unboxes” *C*, finds the wires identified by `k̄` among the outputs of *D* and appends *C* to them. In this process, any lifted variables in `var(t)`, which were abstracted in `((ℓ̃, C, λ)<sub>t</sub>)`, have to be instantiated with concrete names. To this end, the programmer supplies the `n = |var(t)|` lifted variables `u<sub>1</sub>, ..., u<sub>n</sub>`, which are expected to be fresh.

Notice that there exists a strong distinction between values and terms, the latter representing effectful computations that can introduce new lifted variables as a consequence of dynamic lifting. This choice does not detract from the expressiveness of the language, since first and foremost a value *V* can always be turned into an effectless computation `return *V*`. Furthermore, we have that terms such as *MN* can still be recovered in Proto-Quipper-K as `let x = M in {let y = N in {xy}}`. The `let` construct is in fact a central construct in Proto-Quipper-K: on top of serving as a sequencing operator it also doubles as a conditional statement. When we evaluate the term `let x = M in μ`, we first carry out the computation described by *M*, which performs dynamic lifting according to some lifting tree *t* and consequently results in a lifted value `φ ∈ K<sub>t</sub>(VAL)`. At this point, we are not limited to passing each and every possible value of *φ* to the same continuation. Rather, we can define a different continuation for every possible outcome of the liftings in *t*. To this effect, the programmer supplies a lifted term `μ ∈ K<sub>t</sub>(TERM)`, which matches *φ*'s lifting tree and thus effectively provides such a roster of continuations. The following example is meant to help convey the role of `let` as a control flow operator.

**► Example 9.** Imagine we wanted to measure qubit $\ell$, dynamically lift its value into a variable $u$ and then apply the Hadamard gate to a second qubit $k$ only if $u = 1$. Suppose we had CRL definitions $ML = \text{input}(\ell: \text{Qubit}); \text{Meas}(\ell) \to \ell'; \text{lift}(\ell') \Rightarrow u$ and $H = \text{input}(\ell: \text{Qubit}); H(\ell) \to \ell'$, corresponding to the circuit that measures and then lifts a qubit and the circuit that just applies the Hadamard gate to its input, respectively. We would write the following Proto-Quipper-K program:

$$ \text{let } \_ = \text{apply}_u((\ell, ML, u \{*\}\{*\})_{u\{\epsilon\}\{\epsilon\}}, \ell) \text{ in} \\ u\{\text{return } k\}\{\text{apply}((\ell, H, \{\ell'\})_\epsilon, k)\}, \qquad (5) $$

which may appear more familiar under the following Haskell-like syntactic sugar:

$$ \begin{array}{l} \text{apply}_u((\ell, ML, u \{*\}\{*\})_{u\{\epsilon\}\{\epsilon\}}, \ell) \\ \text{when } (u = 1) \text{ apply}((\ell, H, \{\ell'\})_\epsilon, k). \end{array} \qquad (6) $$

<figure><img src="image_11.png" /></figure>
3:12 On Dynamic Lifting and Effect Typing in Circuit Description Languages

$\lambda q_{\text{Qubit}}$. return $\lambda a_{\text{Qubit}}$.let $q = \text{apply}((\ell, H, \{\ell'\}), q)$ in { 
let $\_ = \text{apply}_u((\ell, ML, u \{*\}\{*\})_{u\{\epsilon\}\{\epsilon\}}, q)$ in 
u \{\text{return }a\}\{\text{apply}((\ell, Meas}_\alpha, \{\ell'\}), a)\}}

<caption>Figure 14 A Proto-Quipper-K program describing the circuit shown in Figure 4.</caption>

In light of this example, we can see how the circuit shown in Figure 4 can be described in
Proto-Quipper-K through a program such as the one in Figure 14. To conclude this section,
recall that we mentioned earlier that whenever we apply a boxed circuit we need to instantiate
its lifted variables with concrete names. This process is formalized through the lifted variable
analog of substitution, which we call renaming.

**Definition 10 (Renaming of Lifted Variables).** *Given a lifted variable-bearing object x and a permutation π of V, we call π a renaming of lifted variables and we define x⟨π⟩ as x in which every occurrence of a lifted variable u is replaced by π(u). We denote by s₁/u₁, ..., sₙ/uₙ a permutation that exchanges s₁ for u₁, ..., sₙ for uₙ.*

4.2 Proto-Quipper-K's Typing Rules

At its core, Proto-Quipper-K's type system is a linear type system which distinguishes between
*computations* (i.e. terms), which can be effectful, and *values*. We therefore introduce two
kinds of typing judgments. One for terms, which are given lifted types, and one for values,
which have regular types.

**Definition 11 (Typing Judgments).** *Given a typing context Γ, a label context Q, a term M and a lifted type α, a computational typing judgment is an expression of the form*

$$
\Gamma; Q \vdash_c^t M : \alpha. \tag{7}
$$

Given $\Gamma, Q$, a value $V$ and a type $A$, a value typing judgment is an expression of the form

$$
\Gamma; Q \vdash_v V : A. \tag{8}
$$

When a typing context contains *exclusively* variables with parameter types, we write it as
Φ, but in general a typing context Γ can contain both linear and parameter variables. Typing
judgments are derived via the rules in Figure 15, where s₁, ..., sₙ range over V. Note that
we assume that V is totally ordered, so that when we write var(t) = {u₁, ..., uₙ}, e.g. in
the apply rule, we have u₁ ≤ u₂ ≤ ... ≤ uₙ. The relational symbols ⊩_c and ⊩_v denote the
lifting of the computation and value typing judgments to some tree t.

**Definition 12 (Lifted Typing Judgments).** *Given a lifting tree t, if for all a ∈ P_t we have*
Γ_a: Q_a ⊢_c^a M_a : α_a, then we write

$$
t[\Gamma_a]_a; t[Q_a]_a \Vdash_c^t t[M_a]_a : t[\alpha_a]_a. \qquad (9)
$$

If for all $a \in \mathcal{P}_t$ we have $\Gamma_a; Q_a \vdash_v V_a : A_a$, then we write

$$
t[\Gamma_a]_a; t[Q_a]_a \Vdash_v^t t[V_a]_a : t[A_a]_a. \tag{10}
$$

For convenience, within such judgments, every lifted object (e.g. $\Delta$ in $\emptyset$; $\Delta \Vdash_v^t \lambda : v$ in the *circ* rule) is assumed to be backed by $t$, whereas every component which is *not* a lifted object (e.g. $\Phi$ or $x$ in $\Phi$, $\Gamma_2$, $x : \alpha$; $Q_2 \Vdash_c^t t[\Gamma_a]_a$ $\mu : \theta$ in the *let* rule) is assumed to be constant across the branches of $t$.
<figure><img src="image_12.png" /><figcaption>Figure 15 The typing rules of Proto-Quipper-K.</figcaption></figure>

The *let* rule is unsurprisingly the most interesting rule of the system: if *M* is a term of lifted type *α* ∈ K<sub>t</sub>(*TYPE*), *μ* is a lifted term with the same underlying tree structure *t* and for every root-to-leaf path *a* in *t* we have Φ, Γ₂, *x*: *α*; *Q*₂ ⊢<sub>*t*<sup>*α*</sup></sub> *μ*(*a*) : *θ*(*a*) (note that this last condition is captured by the lifted typing judgment), then the lifted type of *let* *x* = *M* in *μ* is obtained by simply flattening the generic lifted object *θ* to ⌊*θ*⌋ ∈ K<sub>⌊*t*[*τ*<sub>*a*</sub>]*⌋(*TYPE*). The *apply* rule also plays a pivotal role, as it actually introduces lifting into the type of a term. If *V* is a value of type Circ<sub>*t*</sub>(*T*, *v*), and thus corresponds to a boxed circuit which performs lifting according to *t*, then applying *V* to some appropriate wires *W* of the underlying circuit introduces the same lifting pattern into the computation, which has type *v*⟨*π*⟩ ∈ K<sub>*t*⟨*π*⟩</sub>(*MTYPE*). The renaming of lifted variables *π* is required to avoid name clashes.

An example of a type derivation that leverages the full expressiveness of Proto-Quipper-K's
type system is the one for the program shown in Figure 14 (describing the circuit in Figure 4),
which can be found in Appendix A. To conclude this section, notice how just like M-values
and M-types are a subset of the values and types of Proto-Quipper-K, the type system for
M-values is in a one-to-one correspondence with a subset of Proto-Quipper-K's type system.

4.3 A Big-Step Operational Semantics

The big-step operational semantics of the language is based on an evaluation relation
(*C*, *a*, *M*) ⇝ (*D*, *φ*), where *φ* is a lifted value. This means that the term *M* evaluates to one
of the possible values in *φ*, depending on the outcome of intermediate measurements, and
updates the underlying circuit *C* upon branch *a* as a side effect, obtaining an updated circuit
*D*. We call (*C*, *a*, *M*) a *left configuration* and (*D*, *φ*) a *right configuration*. Before we give the
actual rules of the semantics, we must first give some definitions.
3:14 On Dynamic Lifting and Effect Typing in Circuit Description Languages

First and foremost, note that we are not as interested in the actual names of labels within a boxed circuit as much as we are in the structure that they convey. In fact, when we apply circuits to one another, it might be necessary to rename some of the labels occurring in the applicand in order to avoid naming conflicts, all the while preserving its structure. For this reason, whenever two circuits share the same structure and only differ by their respective labels, we consider them to be equivalent.

**► Definition 13 (Equivalent Boxed Circuits).** We say that two boxed circuits $(\vec{l}, C, \lambda)_t$ and $(\vec{l}', C', \lambda')_t$ are equivalent, and we write $(\vec{l}, C, \lambda)_t \cong (\vec{l}', C', \lambda')_t$, when they only differ by a renaming of labels.

Next, we define the two operations that actually implement the semantics of apply. The circuit insertion function $::_a$ is just a simple concatenation function defined on CRL circuits and all the heavy lifting is actually performed by the append function. This function is responsible for the actual unboxing of a boxed circuit, the renaming of its labels (to match the outputs of the underlying circuit and avoid labeling conflicts), the instantiation of the abstracted lifted variable names within it and its insertion in the underlying circuit.

**► Definition 14 (Insertion of Circuits).** Suppose C and D are two circuits. We define the insertion of D in C on branch a, written $C ::=_a D$ as:

$$ 
\begin{align*}
C ::=_a \text{input}(Q) &= C, \\
C ::=_a (D'; b? g(\vec{l}) \rightarrow \vec{k}) &= (C ::=_a D'); a \cup b? g(\vec{l}) \rightarrow \vec{k}, \tag{11} \\
C ::=_a (D'; b? \text{lift}(\ell) \Rightarrow u) &= (C ::=_a D'); a \cup b? \text{lift}(\ell) \Rightarrow u,
\end{align*}
$$

where $a \cup b$ denotes the union of two assignments with disjoint domains.

**► Definition 15 (append).** Suppose $C \vdash_t Q \triangleright \Delta$ is a circuit and $(\vec{l}, D, \lambda)_r$ is a boxed circuit with $\text{var}(r) = \{u_1, \dots, u_n\}$. Suppose $a \in \mathcal{P}_t$ and let $\vec{k}$ be a label tuple whose labels all occur in $\Delta(a)$. Finally, let $s_1, \dots, s_n$ be a sequence of distinct lifted variable names which do not occur in $\text{var}_a(t)$. We define $\text{append}(C, a, \vec{k}, (\vec{l}, D, \lambda)_r, s_1, \dots, s_n)$ as the function that

1. Finds $(\vec{k}, D', \lambda')_t \cong (\vec{l}, D, \lambda)_t$ such that all the labels occurring in $D'$, but not in $\vec{k}$, are fresh in C,

2. $\text{Computes } D'' = D' \langle s_1/u_1, \dots, s_n/u_n \rangle$ and $\lambda'' = \lambda' \langle s_1/u_1, \dots, s_n/u_n \rangle$,

3. Returns $(C ::=_a D'', \lambda'')$.

The rules of the operational semantics can be found in Figure 16, where freshlabels($T$) produces a pair $(Q, \vec{l})$ such that $Q \vdash_m \vec{l} : T$. Note that, for each $t$, we assume to have a total order over the elements of $\mathcal{P}_t$, so that when we write $\mathcal{P}_t = \{a_1, \dots, a_n\}$ we have $a_1 \le a_2 \le \dots \le a_n$ and the semantics is deterministic. In order to prove progress in Section 5, we also consider a notion of divergence for configurations. Intuitively, a configuration $(C, a, M)$ diverges, and we write $(C, a, M) \uparrow$, when its evaluation does not terminate. More formally, divergence is defined coinductively by means of the rules in Figure 17.

5 Type Soundness

In general, the well-typedness of a Proto-Quipper-K configuration strongly depends on the underlying circuit. Specifically, a term $M$ is well-typed when all the free labels occurring in it can be found with the appropriate type in the outputs of the underlying circuit, on the branch that $M$ is manipulating. For this reason, we give the following notions of well-typedness.
$$ \text{app} \frac{(C, a, M[V/x]) \Downarrow (D, \phi)}{(C, a, (\lambda x_A.M)V) \Downarrow (D, \phi)} $$

$$ \text{dest} \frac{(C, a, M[V/x, W/y]) \Downarrow (D, \phi)}{(C, a, \text{let } (x, y) = (V, W) \text{ in } M) \Downarrow (D, \phi)} $$

$$ \text{let} \frac{(C, a, M) \Downarrow (C_1, \phi) \quad \phi \in \mathcal{K}_t(\text{VAL}) \quad \mu \in \mathcal{K}_t(\text{TERM})}{\mathcal{P}_t = \{a_1, \dots, a_n\} \quad (C_i, a \cup a_i, \mu(a_i)[\phi(a_i)/x]) \Downarrow (C_{i+1}, \psi_{a_i}) \text{ for } i = 1, \dots, n} \quad (C, a, \text{let } x = M \text{ in } \mu) \Downarrow (C_{n+1}, \lfloor t[\psi_a]_a \rfloor) $$

$$ \text{force} \frac{(C, a, M) \Downarrow (D, \phi)}{(C, a, \text{force}(\text{lift } M)) \Downarrow (D, \phi)} $$

$$ \text{apply} \frac{(C', \lambda') = \text{append}(C, a, \vec{k}, (\vec{l}, D, \lambda)_t, s_1, \dots, s_n)}{(C, a, \text{apply}_{s_1, \dots, s_n}((\vec{l}, D, \lambda)_t, \vec{k})) \Downarrow (C', \lambda')} $$

$$ \text{box} \frac{(Q, \vec{l}) = \text{freshlabels}(T) \quad (\text{input}(Q), \emptyset, \text{let } x = M \text{ in } \{x\vec{l}\}) \Downarrow (D, \lambda) \quad \lambda \in \mathcal{K}_t(\text{MVAL})}{(C, a, \text{box}_T(\text{lift } M)) \Downarrow (C, \{(\vec{l}, D, \lambda)_t\})} $$
$$ \text{return} \frac{(C, a, \text{return } V) \Downarrow (C, \{V\})}{(C, a, \text{return } V) \Downarrow (C, \{V\})} $$

<caption>Figure 16 The big-step operational semantics of Proto-Quipper-K.</caption>

$$ \text{app} \frac{(C, a, M[V/x]) \Uparrow}{(C, a, (\lambda x_A.M)V) \Uparrow} $$

$$ \text{dest} \frac{(C, a, M[V/x, W/y]) \Uparrow}{(C, a, \text{let } (x, y) = (V, W) \text{ in } M) \Uparrow} $$

$$ \text{force} \frac{(C, a, M) \Uparrow}{(C, a, \text{force}(\text{lift } M)) \Uparrow} $$

$$ \text{let-now} \frac{(C, a, M) \Uparrow}{(C, a, \text{let } x = M \text{ in } \mu) \Uparrow} $$

$$ \mathcal{P}_t = \{a_1, \dots, a_n\} \quad (C_i, a \cup a_i, \mu(a_i)[\phi(a_i)/x]) \Downarrow (C_{i+1}, \psi_{a_i}) \text{ for } i = 1, \dots, j-1 \\ (C_j, a \cup a_j, \mu(a_j)[\phi(a_j)/x]) \Uparrow $$

$$ \text{let-then} \frac{(C, a, \text{let } x = M \text{ in } \mu) \Uparrow}{(C, a, \text{let } x = M \text{ in } \mu) \Uparrow} $$

$$ \text{box} \frac{(Q, \vec{l}) = \text{freshlabels}(T) \quad (\text{input}(Q), \emptyset, \text{let } x = M \text{ in } \{x\vec{l}\}) \Uparrow}{(C, a, \text{box}_T(\text{lift } M)) \Uparrow} $$

<caption>Figure 17 The big-step divergence rules of Proto-Quipper-K.</caption>

► **Definition 16 (Well-Typed Configuration).** We say that

- a left configuration $(C, a, M)$ is well-typed with input $Q$, past lifting tree $t$, future lifting tree $\mathfrak{r}$, lifted type $\alpha$ and outputs $\Delta$, and we write $Q \vdash_t^\alpha (C, a, M) : \alpha; \Delta$, when $a \in \mathcal{P}_t$, $\text{var}_a(t) \cap \text{var}(\mathfrak{r}) = \emptyset$, $C \vdash^t Q \vdash \Delta^a; Q'$ and $\emptyset; Q' \vdash_c^\alpha M : \alpha$,

- a right configuration $(C, \phi)$ is well-typed in the $a$ branch with input $Q$, overall lifting tree $t$, lifted type $\alpha$ and outputs $\Delta$, and we write $Q \vdash_t^a (C, \phi) : \alpha; \Delta$, when $t = [t'[\mathfrak{r}]^{\{a\}}]$, $\Delta = [\Delta'[\Delta'']^{\{a\}}]$, $C \vdash^t Q \vdash [\Delta'[\Delta'', \Lambda]^{\{a\}}]$ and $\emptyset; \Lambda \vdash_c^\alpha \phi : \alpha$.

That being said, we are mainly interested in closed computations, in which the evaluation of a term builds the underlying circuit entirely from scratch. That is, we are interested in computations that start from configurations of the form $(\text{input}(\emptyset), \emptyset, M)$, for some $M$. Whenever $(\text{input}(\emptyset), \emptyset, M) \Downarrow (C, \phi)$ for some $C, \phi$, we simply write $M \Downarrow (C, \phi)$ and whenever $(\text{input}(\emptyset), \emptyset, M) \Uparrow$ we write $M \Uparrow$. In the same guise, we say that $M$ is a well-typed term with lifted type $\alpha$ depending on $t$, and we write $\vdash^t M : \alpha$, whenever $\emptyset \vdash_c^t (\text{input}(\emptyset), \emptyset, M) : \alpha; \{\emptyset\}$, while we say that $(C, \phi)$ is a well-typed closed configuration with lifted type $\alpha$ depending on $t$, and we write $\vdash^t (C, \phi) : \alpha$, whenever $\emptyset \vdash_t^\emptyset (C, \phi) : \alpha; t[\emptyset]_b$. We are now ready to give the relevant type safety results for Proto-Quipper-K.
► **Theorem 17 (Subject Reduction).** If $\vdash^t M : \alpha$ and $\exists C, \phi$ s.t. $M \Downarrow (C, \phi)$, then $\vdash^t (C, \phi) : \alpha$.

**Proof sketch.** We prove the more general claim that whenever $Q \vdash_{\mathfrak{r}}^t (D, a, M) : \alpha; \Delta$ and $\exists C, \phi$ s.t. $(D, a, M) \Downarrow (C, \phi)$, then $Q \vdash_{[\mathfrak{r}[t]\{a\}]}^a (C, \phi) : \alpha; \Delta \prec^a t$, from which we obtain the subject reduction claim by choosing $D = \text{input}(\emptyset), a = \emptyset, Q = \emptyset, \mathfrak{r} = \epsilon$ and $\Delta = \{\emptyset\}$. We proceed by induction on $(D, a, M) \Downarrow (C, \phi)$ and case analysis on the last rule used in its derivation. A number of cases require additional lemmata, more specifically:

1. A substitution lemma is naturally required for the *app*, *dest*, *let* cases. In our scenario, this amounts to proving that whenever $\Phi, \Gamma'; Q' \vdash_v V : A$ and $\Pi$ is a type derivation, then

a. If the conclusion of $\Pi$ is $\Phi, \Gamma, x : A; Q \vdash_c^t M : \alpha$, then $\Phi, \Gamma, \Gamma'; Q, Q' \vdash_c^t M[V/x] : \alpha$,

b. If the conclusion of $\Pi$ is $\Phi, \Gamma, x : A; Q \vdash_v W : B$, then $\Phi, \Gamma, \Gamma'; Q, Q' \vdash_v W[V/x] : B$, We prove the claim separately for the cases in which $V$ has parameter type and linear type. In both cases, we proceed by induction on the size of $\Pi$ and case analysis on its last rule.

2. The *apply* case is particularly delicate and requires us to prove that all the operations performed by the *append* function on the applicand and the underlying circuit alter their respective circuit signatures in a predictable way. More specifically:

a. For the first step of *append*, we show that equivalent circuits have the same type, that is, that whenever $\emptyset; \emptyset \vdash_v (\vec{l}, C, \lambda)_t : \text{Circ}_t(T, v)$ and $(\vec{l}, C, \lambda)_t \cong (\vec{l}', C', \lambda')_t$, then $\emptyset; \emptyset \vdash_v (\vec{l}', C', \lambda')_t : \text{Circ}_t(T, v)$. This reflects the idea that the type of a circuit depends on its structure, and not on the specific labels used to convey said structure.

b. Similarly, for the second step, we show that lifted variable renaming preserves circuit signatures and lifted typing judgments, that is, that for every renaming of lifted variables $\pi$, $C \vdash^t Q \triangleright \Delta$ implies $C\langle\pi\rangle \vdash^{t(\pi)} Q \triangleright \Delta\langle\pi\rangle$ and $\gamma; \Delta \Vdash_v^t \phi : \alpha$ implies $\gamma\langle\pi\rangle; \Delta\langle\pi\rangle \Vdash_v^t \phi\langle\pi\rangle : \alpha\langle\pi\rangle$, where $\gamma$ is a lifted context in $\mathcal{K}_t(CONTEXT)$. Similarly to the previous point, this reflects the idea that the structure of a lifted object is more important than the specific lifted variable names used to convey said structure.

c. For the third step, we show that whenever we have an underlying circuit $C$ and an applicand $D$ whose labels and lifted variables have already been renamed appropriately, the concatenated circuit $C ::_a D$ is such that its output on branch $a$ contains both the outputs of $D$ and the outputs of $C$ that $D$ was *not* applied on. That is, we prove that whenever $C \vdash^t Q \triangleright \Delta [Q', Q'']^{\{a\}}$ for some $a \in \mathcal{P}_t$ and $D \vdash^r Q' \triangleright \Lambda$ for some $D$ such that the labels that occur in $D$, but not in $Q'$, are fresh in $C$ and $\text{var}_a(t) \cap \text{var}(\mathfrak{r}) = \emptyset$, then $C ::_a D \vdash^{[t[\mathfrak{r}]^{\{a\}}]} Q \triangleright [\Delta[\Lambda, Q'']^{\{a\}}]$. We prove this by induction on $D \vdash^r Q' \triangleright \Lambda$. This result clearly allows us to conclude the subject reduction claim for the *apply* case.

3. The *let* case is also particularly delicate, although more technical than the *apply* case: it requires us to apply the inductive hypothesis once for the evaluation of the left side of the let and $n$ times for the evaluation of each of the possible branches on the right side, which happens in sequence. This means that the conclusion of each application of the inductive hypothesis must become the premise of the following application. More specifically, for every well-typed right configuration $(C_{i+1}, \psi_{a_i})$ we must be able to prove that $(C_{i+1}, a \cup a_{i+1}, \mu(a_{i+1})[\phi(a_{i+1})/x])$ is a well-typed left configuration. A key lemma in this process tells us that for any two generic lifted objects $\xi \in \mathcal{K}_t(X)$ and $\theta \in \mathcal{K}_t(X)$ and any two assignments $a \in \mathcal{P}_t$ and $b \in \mathcal{A}_t$, we have $[\xi[\theta[x_c]]^{\mathcal{P}_t^b}_{c}]^{\{a\}} = [\xi[\theta]^{\{a\}}] [x_c]^{\mathcal{A}_t}_{c}$.

◄

► **Theorem 18 (Progress).** If $\vdash^t M : \alpha$, then either $\exists C, \phi$ s.t. $M \Downarrow (C, \phi)$ or $M \Uparrow$.
**Proof sketch.** We consider the equivalent claim that if $\vdash^t M : \alpha$ and $\nvdash C, \phi.M \Downarrow (C, \phi)$, then $M \Uparrow$. We then prove the more general result that if $Q \vdash_t^t (D, a, M) : \alpha; \Delta$ and $\nvdash C, \phi.(D, a, M) \Downarrow (C, \phi)$, then $(D, a, M) \Uparrow$, from which we obtain the progress claim by choosing $D = \text{input}(\emptyset), a = \emptyset, Q = \emptyset, t = \epsilon$ and $\Delta = \{\emptyset\}$. We proceed by coinduction and case analysis on $M$. The proof is fairly straightforward and makes extensive use of the general subject reduction theorem and of some of its lemmata. The one interesting case is *apply*, which is proven vacuously by showing that *append* is always defined under the hypothesis:

1. The first step of append must find a circuit $(\vec{k}, D', \lambda')_t \cong (\vec{\ell}, D, \lambda)_t$ such that the labels in $\vec{k}$ are given and correspond to the target labels in the underlying circuit $C$ and all the other labels in $D'$ are fresh in $C$. A key lemma tells us that since $\vec{\ell}$ and $\vec{k}$ have the same M-type $T$, then it is possible to rename the former to the latter. It is then straightforward to extend this renaming to all the labels occurring in $D$ in a way that fulfills the aforementioned requirements.

2. The second step must compute $D'\langle\pi\rangle$ and $\lambda'\langle\pi\rangle$. This is always possible since $\pi$ is a valid renaming of lifted variables and thus a permutation.

3. The last step must compute $C ::=_a D'\langle\pi\rangle$. We show that for every assignment $b$ occurring in $D'\langle\pi\rangle$ it holds that $\text{dom}(a) \cap \text{dom}(b) = \emptyset$. Therefore, the concatenation operation is defined and append returns $(C ::=_a D'\langle\pi\rangle, \lambda'\langle\pi\rangle)$. $\quad$

Detailed proofs of subject reduction (Theorem 17) and progress (Theorem 18) can be found in the extended version of the paper [2].

# 6 Conclusion

## Our Contributions

This paper introduces a new paradigmatic language for dynamic lifting belonging to the Proto-Quipper family of languages. The language, called Proto-Quipper-K, can be seen as an extension of Proto-Quipper-M which allows for the Boolean information flowing within bit wires to be lifted from the circuit level to the program level. In order to make the circuit construction process as flexible and as general as possible, a powerful type and effect system based on lifting trees has been introduced. This allows for the typing of programs which produce highly non-uniform circuits, making Proto-Quipper-K strictly more expressive than Quipper and potentially useful in scenarios such as one-way quantum computing [4]. Although the use of the syntax introduced in this paper is not essential to implement the measurement patterns encountered in one-way quantum computing (which, after all, can be simulated by regular quantum circuits), the non-uniform approach to dynamic lifting that we adopt in our work would allow for a higher degree of flexibility in building and manipulating patterns. In other words, even when the circuit produced at the end of the computation is a uniform circuit, we can build it incrementally, going through non-uniform circuits. The main technical results we obtained for Proto-Quipper-K are type soundness, in the sense of subject reduction and progress theorems.

## Future Work

In this paper we focused on the operational aspects, leaving an investigation about a possible denotational account of Proto-Quipper-K as future work. A related problem is that of understanding the precise nature of the lifting operation that we use pervasively in the paper. In particular, while it would be tempting to interpret $\mathcal{K}_t$ as a graded monad [8, 12] with unit $\eta : X \to \mathcal{K}_\epsilon(X)$ defined as $\eta x = \{x\}$ and multiplication $\cdot : \mathcal{K}_t(\mathcal{K}_\epsilon(X)) \to \mathcal{K}_{t[\epsilon]}(X)$,
3:18 On Dynamic Lifting and Effect Typing in Circuit Description Languages

we generally work with objects that do not belong to $\mathcal{K}_t(\mathcal{K}_r(X))$ for some fixed $t, r$, so we
find that this interpretation is not entirely appropriate, at least if we assume grades to be
elements of *one fixed monoid*.

Another aspect that we left open is the consolidation of homogeneous branches in a computation. In many contexts, it is extremely natural to ask that the type of a term be uniform with respect to a certain lifted variable *u*, i.e. that it be of the form *u{α}{α*}. If a term *M* were typed this way, it would be natural to construct a new term *νu*.M in which *u* is no longer lifted and which could thus be given the type *α*. We claim that such a local name binder can be added to the language without substantially altering its metatheory.

The last problem that we deliberately leave open concerns the notion of generalized circuits
used in this paper. On the one hand, it can certainly be said that it can model quantum
circuits in their full generality, including those measurement patterns found in measurement-
based quantum computing [4]. On the other hand, while it is clear that such circuits make
computational sense (after all, any such computation can be simulated by a classically
controlled quantum Turing machine [18]), it is not clear what kind of correspondence exists
between them and quantum circuits in their usual form [15], which is the one most often
considered in the literature.

Related Work

As already mentioned in the introduction, various paradigmatic λ-calculi modeling the
**Quipper** programming language have been introduced in the literature [6, 7, 13, 20, 21]. In
this work, we took inspiration from **Proto-Quipper-M** [20], which however cannot handle
dynamic lifting. The only members of the **Proto-Quipper** family that can handle dynamic
lifting, in a uniform and more restricted form than ours, are **Proto-Quipper-L** [13] and **Proto-Quipper-Dyn** [6], which have been introduced very recently and independently of this work.
Interestingly, the class of circuits targeted by **Proto-Quipper-L**— which the authors have named
**quantum channels** — indeed includes non-uniform circuits like the one in Figure 4, which
leads us to believe that they actually match our generalized quantum circuits in terms of
expressiveness. However, **Proto-Quipper-L**'s type system rejects the programs that build
such circuits. On the other hand, **Proto-Quipper-Dyn** follows a different approach, with two
interleaved operational semantics: one for circuit building, which only happens inside a boxing
operator and does *not* support dynamic lifting, and one for circuit execution, where dynamic
lifting is allowed. Therefore, as a circuit description language, **Proto-Quipper-Dyn** targets
traditional circuits. At the type level, this distinction is reflected in a modal type system
which keeps track of whether dynamic lifting is used, and therefore whether a circuit-building
function can be boxed or not. That being said, most of the aforementioned contributions
differ from ours in that they focus mainly on the denotational semantics of the language
rather than its operational semantics.

The type and effect system paradigm is well known from the literature [3, 12, 14, 16] and
has been used in various contexts as a way to reflect information on the effects produced by
a program in its type. In our case, the relevant effect is a choice effect, which is mirrored
both in the operational semantics and in the type system. As already stated, the problem of
giving a proper monadic status to the considered choice effect remains open, although this
work shows that *operationally speaking* everything works smoothly.

Finally, it is worth mentioning that the circuit description paradigm is not the only
approach to designing quantum programming languages and calculi. For instance, QCL [25],
QML [1] and Selinger and Valiron's quantum λ-calculus [23] are some examples of quantum
programming languages whose instructions are designed to be executed immediately on
quantum hardware, without any direct reference to quantum circuits.
References

1 Thorsten Altenkirch and Jonathan Grattage. A functional quantum programming language. In Proc. of LICS, 2005. doi:10.1109/lics.2005.1.

2 Andrea Colledan and Ugo Dal Lago. On dynamic lifting and effect typing in circuit description languages (extended version), 2022. arXiv:2202.07636.

3 Ugo Dal Lago and Charles Grellois. Probabilistic termination by monadic affine sized typing. ACM Trans. Program. Lang. Syst., 41(2), March 2019. doi:10.1145/3293605.

4 Vincent Danos, Elham Kashefi, and Prakash Panangaden. The measurement calculus. J. ACM, 54(2), April 2007. doi:10.1145/1219092.1219096.

5 Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger. A tutorial introduction to quantum circuit programming in dependently typed proto-quipper. In Proc. of RC, Berlin, Heidelberg, 2020. Springer-Verlag. doi:10.1007/978-3-030-52482-1_9.

6 Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger. Proto-quipper with dynamic lifting. Proc. ACM Program. Lang., 7(POPL), January 2023. doi:10.1145/3571204.

7 Peng Fu, Kohei Kishida, and Peter Selinger. Linear dependent type theory for quantum programming languages: Extended abstract. In Proc. of LICS, 2020. doi:10.1145/3373718.3394765.

8 Soichiro Fujii, Shin-ya Katsumata, and Paul-André Melliès. Towards a formal theory of graded monads. In Proc. of FoSSaCS, Berlin, Heidelberg, 2016. doi:10.1007/978-3-662-49630-5_30.

9 Simon J. Gay. Quantum programming languages: Survey and bibliography. Math. Struct. Comput. Sci., 16(4):581–600, August 2006. doi:10.1017/S0960129506005378.

10 Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. An introduction to quantum programming in quipper. In Proc. of RC, pages 110–124, 2013. doi:10.1007/978-3-642-38986-3_10.

11 Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. Quipper. In Proc. of PLDI, pages 333–342, June 2013. doi:10.1145/2499370.2462177.

12 Shin-ya Katsumata. Parametric effect monads and semantics of effect systems. In Proc. of POPL, pages 633–645, January 2014. doi:10.1145/2578855.2535846.

13 Dongho Lee, Valentin Perrelle, Benoît Valiron, and Zhaowei Xu. Concrete Categorical Model of a Quantum Circuit Description Language with Measurement. In Proc. of FSTTCS, volume 213 of LIPIcs, pages 51:1–51:20, 2021. doi:10.4230/LIPIcs.FSTTCS.2021.51.

14 Alan Mycroft, Dominic Orchard, and Tomas Petricek. Effect systems revisited—control-flow algebra and semantics. In Christian W. Probst, Chris Hankin, and René Rydhof Hansen, editors, Semantics, Logics, and Calculi: Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays, pages 1–32. Springer International Publishing, Cham, 2016. doi:10.1007/978-3-319-27810-0_1.

15 Michael A. Nielsen and Isaac L. Chuang. Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press, 2010. doi:10.1017/CBO9780511976667.

16 Flemming Nielson and Hanne Riis Nielson. Type and effect systems. In Ernst-Rüdiger Olderog and Bernhard Steffen, editors, Correct System Design: Recent Insights and Advances, pages 114–136. Springer Berlin Heidelberg, 1999. doi:10.1007/3-540-48092-7_6.

17 Jens Palsberg. Toward a universal quantum programming language. XRDS: Crossroads, 26(1):14–17, September 2019. doi:10.1145/3355759.

18 Simon Perdrix and Philippe Jorrand. Classically controlled quantum computation. Math. Struct. Comput. Sci., 16(04):601, July 2006. doi:10.1017/s096012950600538x.

19 John Preskill. Quantum Computing in the NISQ era and beyond. Quantum, 2:79, August 2018. doi:10.22331/q-2018-08-06-79.

20 Francisco Rios and Peter Selinger. A categorical model for a quantum circuit description language. In Proc. of QPL, volume 266, June 2017. doi:10.4204/EPTCS.266.11.

21 Neil Ross. Algebraic and Logical Methods in Quantum Computation. PhD thesis, Dalhousie University, 2015.
3:20 On Dynamic Lifting and Effect Typing in Circuit Description Languages

22 Peter Selinger. A brief survey of quantum programming languages. In Proc. of FLOPS, pages 1–6, 2004. doi:10.1007/978-3-540-24754-8_1.

23 Peter Selinger and Benoît Valiron. A lambda calculus for quantum computation with classical control. In Proc. of TLCA, pages 354–368, 2005. doi:10.1007/11417170_26.

24 Mingsheng Ying. Foundations of Quantum Programming. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1st edition, 2016. doi:10.1016/C2014-0-02660-3.

25 Bernhard Ömer. Classical concepts in quantum programming. Int. J. Theor. Phys., 44(7):943–955, July 2005. doi:10.1007/s10773-005-7071-x.

A Type Derivations

$$
\begin{array}{r@{\quad}l}
\text{return} & \overline{\begin{array}{@{}c@{}} \text{var} \\ \text{\_} \end{array}} : \mathsf{1}, a : \text{Qubit}; \emptyset \vdash_v a : \text{Qubit} \\
& \overline{\begin{array}{@{}c@{}} \text{\_} \\ \text{\_} \end{array}} : \mathsf{1}, a : \text{Qubit}; \emptyset \vdash_c^\epsilon \text{ return } a : \{\text{Qubit}\}
\end{array}
$$

■ **Figure 18** Sub-derivation $\Pi'$, corresponding to the $u = 0$ branch of the lifted computational judgment $\_ : u \{\mathsf{1}\} \{\mathsf{1}\}, a : \text{Qubit}; \emptyset \vdash_c^u \{\{\epsilon\}\} \{\{\epsilon\}\} u \{\text{return } a\} \{\text{apply}(\text{Meas}_\alpha, a)\} : u \{\{\text{Qubit}\}\} \{\{\text{Bit}\}\}$ required by sub-derivation $\Pi$ of Figure 20.

$$
\begin{array}{r@{\quad}l}
\text{apply} & \overline{\begin{array}{@{}c@{}} \text{\_} : \mathsf{1}; \emptyset \vdash_v \text{Meas}_\alpha : \text{Circ}_\epsilon(\text{Qubit}, \{\text{Bit}\}) \\ \text{\_} : \mathsf{1}, a : \text{Qubit}; \emptyset \vdash_v a : \text{Qubit} \end{array}} \quad \overline{\begin{array}{@{}c@{}} \text{var} \\ \text{\_} \end{array}} : \mathsf{1}, a : \text{Qubit}; \emptyset \vdash_v a : \text{Qubit} \\
& \overline{\begin{array}{@{}c@{}} \text{\_} : \mathsf{1}, a : \text{Qubit}; \emptyset \vdash_c^\epsilon \text{ apply}(\text{Meas}_\alpha, a) : \{\text{Bit}\} \end{array}}
\end{array}
$$

■ **Figure 19** Sub-derivation $\Pi''$, corresponding to the $u = 1$ branch of the lifted computational judgment $\_ : u \{\mathsf{1}\} \{\mathsf{1}\}, a : \text{Qubit}; \emptyset \vdash_c^u \{\{\epsilon\}\} \{\{\epsilon\}\} u \{\text{return } a\} \{\text{apply}(\text{Meas}_\alpha, a)\} : u \{\{\text{Qubit}\}\} \{\{\text{Bit}\}\}$ required by sub-derivation $\Pi$ of Figure 20.

$$
\begin{array}{r@{\quad}l}
\text{apply} & \overline{\begin{array}{@{}c@{}} \emptyset; \emptyset \vdash_v ML : \text{Circ}_u \{\epsilon\} \{\epsilon\} (\text{Qubit}, u \{\mathsf{1}\} \{\mathsf{1}\}) \\ \text{\_} \end{array}} \quad \overline{\begin{array}{@{}c@{}} \text{var} \\ \text{\_} \end{array}} : \text{Qubit}; \emptyset \vdash_v q : \text{Qubit} \\
& \overline{\begin{array}{@{}c@{}} q : \text{Qubit}; \emptyset \vdash_c^u \{\epsilon\} \{\epsilon\} \text{ apply}_u (ML, q) : u \{\mathsf{1}\} \{\mathsf{1}\} \\ u \{\text{return } a\} \{\text{apply}(\text{Meas}_\alpha, a)\} \in \mathcal{K}_u \{\epsilon\} \{\epsilon\} (\text{TERM}) \end{array}} \qquad \Pi' \quad \Pi'' \\
\text{let} & \overline{\begin{array}{@{}c@{}} q : \text{Qubit}, a : \text{Qubit}; \emptyset \vdash_c^u \{\epsilon\} \{\epsilon\} \text{ let } \_ = \text{apply}_u (ML, q) \text{ in} \\ u \{\text{return } a\} \{\text{apply}(\text{Meas}_\alpha, a)\} : u \{\text{Qubit}\} \{\text{Bit}\} \end{array}}
\end{array}
$$

■ **Figure 20** Sub-derivation $\Pi$, where the conclusion is the expansion of the (trivial) lifted computational judgment required by the *let* rule in Figure 21.
<figure><img src="image_13.png" /><figcaption>■ **Figure 21** Type derivation for the Proto-Quipper-K program in Figure 14. For brevity, $H$, $Meas_\alpha$ and $ML$ stand for the corresponding boxed circuits employed in Figure 14 and arrow annotations are omitted. Sub-derivation II is given in Figure 20.</figcaption></figure>