Circuit Width Estimation via Effect Typing
and Linear Dependency (Long Version)

1,2]Andrea Colledan
1,2]Ugo Dal Lago
[1]University of Bologna, Italy
[2]INRIA Sophia Antipolis, France

Circuit description languages are a class of quantum programming languages in which programs are classical and produce a description of a quantum computation, in the form of a quantum circuit. Since these programs can leverage all the expressive power of high-level classical languages, circuit description languages have been successfully used to describe complex and practical quantum algorithms, whose circuits, however, may involve many more qubits and gate applications than current quantum architectures can actually muster. In this paper, we present , a circuit description language endowed with a linear dependent type-and-effect system capable of deriving parametric upper bounds on the width of the circuits produced by a program. We prove both the standard type safety results and that the resulting resource analysis is correct with respect to a big-step operational semantics. We also show that our approach is expressive enough to verify realistic quantum algorithms.

§ INTRODUCTION

With the promise of providing efficient algorithmic
solutions to many problems [28, 32, 12], some of which are traditionally believed to be intractable [54], quantum computing is the subject of intense investigation by various research communities within computer science, not least that of programming language theory [43, 25, 51]. Various proposals for idioms capable of tapping into this new computing paradigm have appeared in the literature since the late 1990s. Some of these approaches turn out to be fundamentally new [52, 1, 49], while many others are strongly inspired by classical languages and traditional programming paradigms [61, 53, 48, 44].

One of the major obstacles to the practical adoption of quantum algorithmic
solutions is the fact that despite huge efforts by scientists and
engineers alike, it seems that reliable quantum hardware, contrary to classical one, does not scale too easily: although quantum architectures with up to a couple hundred qubits have recently seen the light [10, 39, 11], it is not yet clear whether the so-called quantum advantage [45] is a concrete possibility, given the tremendous challenges posed by the quantum decoherence problem [50].

This entails that software which makes use of quantum hardware
must be designed with great care: whenever part of a computation has to be run on quantum hardware, the amount of resources it
needs, and in particular the amount of qubits it uses, should be kept to a
minimum. More generally, a fine control over the low-level aspects of the
computation, something that we willingly abstract from in most cases when dealing with classical computations, should be exposed to the programmer in the quantum case.
This, in turn, has led to the development and adoption of many domain-specific
programming languages and libraries in which the programmer explicitly manipulates qubits and quantum circuits, while still making use of all the features of a high-level classical programming language. This is the case of the  and  libraries [18], but also of the  language [26, 27].

At the fundamental level,  is a circuit description language embedded in . Because of this,  inherits all the expressiveness of the high level, higher-order functional programming language that is its host, but for the same reason it also lacks a formal semantics. Nonetheless, over the past few years, a number of calculi, collectively known as the  language family, have been developed to formalize interesting fragments and extensions of  and its type system [48, 46]. Extensions include, among others, dynamic lifting [36, 22, 9] and dependent types [23, 21], but resource analysis is still a rather unexplored research direction in the  community [56].

The goal of this work is to show that type systems indeed enable the
possibility of reasoning about the size of the circuits produced by a
program. Specifically, we show how linear dependent types in the
form given by Gaboardi and Dal Lago [13, 24, 15, 16] can be adapted to
, allowing to derive upper bounds on circuit widths that
are parametric on the size of the problem. This enables a form of static analysis of the resource consumption of circuit families and, consequently, of the quantum algorithms described in the language. Technically, a key ingredient of this analysis, besides linear dependency, is a novel form of effect typing in which the quantitative information coming from linear dependency informs the effect system and allows it to keep circuit widths under control.

The rest of the paper is organized as follows. Section <ref> informally explores the problem of estimating the width of circuits produced by , while also introducing the language.
Section <ref> provides a more formal definition of the  language. In particular, it gives an overview of the system of simple types due to Selinger and Rios [46], which however is not designed to reason about the size of circuits.
We then move on to the most important technical contribution of this work, namely the linear dependent and effectful type system, which is introduced in Section <ref> and proven to guarantee both type safety and a form of total correctness in Section <ref>.
Section <ref> is dedicated to an example of a practical application of our type and effect system, that is, a program that builds the Quantum Fourier Transform (QFT) circuit [12, 40] and which is verified to do so without any ancillary qubits.

§ AN OVERVIEW ON CIRCUIT WIDTH ESTIMATION

allows programmers to describe quantum circuits in a high-level and elegant way, using both gate-by-gate and circuit transformation approaches.  also supports  hierarchical and parametric circuits, thus promoting a view in which circuits become first-class citizens.  has been shown to be scalable, in the sense that it has been effectively used to describe complex quantum algorithms that easily translate to circuits involving trillions of gates applied to millions of qubits. The language allows the programmer to optimize the circuit, e.g. by using ancilla qubits for the sake of reducing the circuit depth, or recycling qubits that are no longer needed.

One feature that  lacks is a methodology for statically proving that important parameters — such as the the width — of the
underlying circuit are below certain limits, which of course can be parametric on the input size of the circuit. If this kind of analysis were available, then it would be possible to derive bounds on the number of qubits needed to solve any instance of a problem, and ultimately to know in advance how big of an instance can be possibly solved given a fixed amount of qubits.

In order to illustrate the kind of scenario we are reasoning about, this section offers some simple examples of  programs, showing in what sense we can think of capturing the quantitative information that we are interested in through types and effect systems and linear dependency. We proceed at a very high level for now, without any ambition of formality.

Let us start with the example of Figure <ref>. The  function on the left builds the quantum circuit on the right: an (admittedly  contrived) implementation of the quantum not operation. The  function implements negation using a controlled not gate and an ancillary qubit , which is initialized and discarded within the body of the function. This qubit does not appear in the interface of the circuit, but it clearly adds to its overall width, which is $2$.

[column sep=1.5em]
n    $\ket{1}$     1 q

$q$                   $q$

An implementation of the quantum not operation using an ancilla.

Consider now the higher-order function in Figure <ref>. This function takes as input a circuit building function , an integer  and describes the circuit obtained by applying 's circuit  times to the input qubit .
It is easy to see that the width of the circuit produced in
output by  is equal to $2$, even though, overall, the number of qubits initialized during the computation is equal to $n$. The point is that each ancilla is created only after the previous one has been discarded, thus enabling a form of qubit recycling.

\begin{quantikz}[column sep=0.8em]
\setwiretype{n}& \lstick{$\ket{1}$} & \ctrl{1} \setwiretype{q} & \ground{}  & \setwiretype{n} && \lstick{$\ket{1}$} & \ctrl{1} \setwiretype{q} & \ground{} & \setwiretype{n} \ \ldots \ &&&\lstick{$\ket{1}$} & \ctrl{1} \setwiretype{q} & \ground{} \\
\lstick{$q$} && \targ{} & &&& &\targ{}&& \ \ldots \ &&&& \targ{}&& \rstick{$q$}
\end{quantikz}
}_{n \text{ times}}$

A higher-order function which iterates a circuit-building function  on an input qubit  and the result of its application to the  function from Figure <ref>.

Is it possible to statically analyze the width of the circuit produced in output by  so as to conclude that it is constant and equal to $2$? What techniques can we use? Certainly, the presence of higher-order types complicates the problem, already in itself non-trivial. The approach we propose in this paper is based on two ingredients. The first is the so-called effect typing [41]. In this context, the effect produced by the program is nothing more than the circuit and therefore it is natural to think of an effect system in which the width of such circuit, and only that, is exposed. Therefore, the arrow type $\typeOne \to \typeTwo$ should be decorated with an expression indicating the width of the circuit produced by the corresponding function when applied to an argument of type $\typeOne$. Of course, the width of an individual circuit is a natural number, so it would make sense to annotate the arrow with a natural number. For technical reasons, however, it will also be necessary to keep track of another natural number, corresponding to the amount of wire resources that the function captures from the surrounding environment. This necessity stems from a need to keep close track of wires even in the presence of data hiding, and will be explained in further detail in Section <ref>.

Under these premises, the  function would receive type $\qubitt \to_{2,0} \qubitt$, meaning that it takes as input a qubit and produces a circuit of width $2$ which outputs a qubit.
Note that the second annotation is $0$, since we do not capture anything from the function's environment, let alone a wire. Consequently, because  iterates in sequence and because the ancillary qubit in  can be reused, the type of  would also be $\qubitt \to_{2,0} \qubitt$.

[column sep=2em, row sep=1em]
$q$     H     $q$

$\mathit{qs}_1$     H     $\mathit{qs}_1$

$\mathit{qs}_n$     H     $\mathit{qs}_n$

The  function implements a circuit family where circuits have width linear in their input size.

Let us now consider a slightly different situation, in which the width of the produced circuit is not constant, but rather increases proportionally to the circuit's input size. Figure <ref> shows a  function that returns a circuit on $n$ qubits in which the Hadamard gate is applied to each qubit. This simple circuit represents the preprocessing phase of many quantum algorithms, including Deutsch-Josza [8] and Grover's [28]. It is obvious that this function works on inputs of arbitrary size, and therefore we can interpret it as a circuit family, parametrized on the length of the input list of qubits. This quantity, although certainly a natural number, is unknown statically and corresponds precisely to the width of the produced circuit. A question therefore arises as to whether the kind of effect typing we briefly hinted at in the previous paragraph is capable of dealing with such a function. Certainly, the expressions used to annotate arrows cannot be, like in the previous case, mere constants, as they clearly depend on the size of the input list. Is there a way to reflect this dependency in types? Certainly, one could go towards a fully-fledged notion of dependent types, like the ones proposed in [23], but a simpler approach, in the style of Dal Lago and Gaboardi's linear dependent types [13, 24, 15, 16] turns out to be enough for this purpose. This is precisely the route that we follow in this paper. In this approach, terms can indeed appear in types, but that is only true for a very restricted class of terms, disjoint from the ordinary ones, called index terms. As an example, the type of the function  above could become $\listt{\ivarOne}{\qubitt} \to_{\ivarOne,0} \listt{\ivarOne}{\qubitt}$, where $\ivarOne$ is an index variable. The meaning of the type would thus be that  takes as input any list of qubits of length $\ivarOne$ and produces a circuit of width at most $\ivarOne$ which outputs $\ivarOne$ qubits. The language of indices is better explained in Section <ref>, but in general we can say that indices are arithmetical expressions over natural numbers and index variables, and can thus express non-trivial dependencies between input sizes and corresponding circuit widths.

§ THE

This section aims at introducing the  family of calculi to the non-specialist, without any form of resource analysis. At its core,  is a linear lambda calculus with bespoke constructs to build and manipulate circuits. Circuits are built as the side-effect of a computation, behind the scenes, but they can also appear and be manipulated as data in the language.

Types	    $\typeSet$	    $\typeOne,\typeTwo$     $
::= \unitt
\mid \wtypeOne
\mid \bang{\typeOne}
\mid \tensor{\typeOne}{\typeTwo}
\mid \typeOne \lineararrow \typeTwo
\mid \listt{}{\typeOne}
\mid \circt{}{\mtypeOne}{\mtypeTwo}$

Parameter types		    $\ptypeSet$	    $\ptypeOne,\ptypeTwo$     $
::= \unitt
\mid \bang{\typeOne}
\mid \tensor{\ptypeOne}{\ptypeTwo}
\mid \listt{}{\ptypeOne}
\mid \circt{}{\mtypeOne}{\mtypeTwo}$

Bundle types	    $\mtypeset$	    $\mtypeOne,\mtypeTwo$     $
::= \unitt
\mid \wtypeOne
\mid \tensor{\mtypeOne}{\mtypeTwo}$

The types of  are given in Figure <ref>. Speaking at a high level, we can say that  types are generally linear. In particular, $\wtypeOne\in\{\bitt,\qubitt\}$ is a wire type and is linear, while $\lineararrow$ is the linear arrow constructor. A subset of types, called parameter types, represent the values of the language that are not linear and that can therefore be copied. Any term of type $\typeOne$ can be lifted into a duplicable parameter of type $\bang{\typeOne}$ if its type derivation does not require the use of linear resources.

Terms	    $\termSet$	    $\termOne,\termTwo$     $ ::= \app{\valOne}{\valTwo}
\mid \dest{\varOne}{\varTwo}{\valOne}{\termOne}
\mid \force{\valOne}
\mid \boxt{\mtypeOne}{\valOne}$
\mid \apply{\valOne}{\valTwo}
\mid \return{\valOne}
\mid \letin{\varOne}{\termOne}{\termTwo}$

Values	    $\valSet$	    $\valOne,\valTwo$     $
::= \unitv
\mid \varOne
\mid \labOne
\mid \abs{\varOne}{\typeOne}{\termOne}
\mid \lift{\termOne}
\mid \boxedCirc{\struct\labOne}{\circuitOne}{\struct{\labTwo}}
\mid \tuple{\valOne}{\valTwo}$
\mid \nil
\mid \cons{\valOne}{\valTwo}
\mid \fold{}{\valOne}{\valTwo}$

Wire bundles	    $\mvalset$	    $\struct\labOne,\struct\labTwo$     $
::= \unitv
\mid \labOne
\mid \tuple{\struct\labOne}{\struct\labTwo}$

Now, let us informally dissect the language as presented in Figure <ref>, starting with the language of values. The main constructs of interest are  labels and boxed circuits.
A label $\labOne$ represents a reference to a free wire of the underlying circuit being built and is attributed a wire type $\wtypeOne\in\{\bitt,\qubitt\}$. Labels have to be treated linearly due to the no-cloning property of quantum states [40]. Arbitrary structures of labels form a subset of values which we call wire bundles and which are given bundle types.
On the other hand, a boxed circuit $\boxedCirc{\struct\labOne}{\circuitOne}{\struct\labTwo}$ represents a circuit object $\circuitOne$ as a datum within the language, together with its input and output interfaces, given as wire bundles $\struct\labOne$ and $\struct\labTwo$. Such a value is given type $\circt{}{\mtypeOne}{\mtypeTwo}$, where bundle types $\mtypeOne$ and $\mtypeTwo$ are the input and output types of the circuit, respectively. Boxed circuits can be copied, manipulated by primitive functions and, more importantly, applied to the underlying circuit.
This last operation, which lies at the core of 's circuit-building capabilities, is possible thanks to the $\applyoperator$ operator. This operator takes as first argument a boxed circuit $\boxedCirc{\struct\labOne}{\circuitOne}{\struct\labTwo}$ and appends $\circuitOne$ to the underlying circuit $\circuitTwo$. How does $\applyoperator$ know where exactly in $\circuitTwo$ to apply $\circuitOne$? Thanks to a second argument: a bundle of wires $\struct\labThree$ coming from the free output wires of $\circuitTwo$, which identifies the exact location where $\circuitOne$ is supposed to be appended.

The language is expected to be endowed with constant boxed circuits corresponding to fundamental gates (e.g. Hadamard, controlled not, etc.), but the programmer can also introduce their own boxed circuits via the $\boxoperator$ operator. Intuitively, $\boxoperator$ takes as input a circuit-building function and evaluates it in a sandboxed environment, on dummy arguments, in a way that leaves the underlying circuit unchanged. This evaluation produces a standalone circuit $\circuitOne$, which is then returned by the $\boxoperator$ operator as a boxed circuit $\boxedCirc{\struct\labOne}{\circuitOne}{\struct\labTwo}$.

Figure <ref> shows the  term corresponding to the  program in Figure <ref>, as an example of the use of the language. Note that $\letin{\tuple{\varOne}{\varTwo}}{\termOne}{\termTwo}$ is syntactic sugar for $\letin{\varThree}{\termOne}{\dest{\varOne}{\varTwo}{\varThree}{\termTwo}}$.  The $\mathit{dumbNot}$ function is given type $\qubitt \lineararrow \qubitt$ and builds the circuit shown in Figure <ref> when applied to an argument.

\begin{align*}
\mathit{dumbNot} \triangleq \abs{q}{\qubitt}{\,&
\letin{a}{\apply{\mathsf{INIT_1}}{\unitv}}{\\&
\letin{\tuple{q}{a}}{\apply{\mathsf{CNOT}}{\tuple{q}{a}}}{\\&
\letin{\_}{\apply{\mathsf{DISCARD}}{a}}{\\&
\return{q}}}}}
\end{align*}

An example  program. $\mathsf{INIT_1,CNOT}$ and $\mathsf{DISCARD}$ are primitive boxed circuits implementing the corresponding elementary operations.

On the classical side of things, it is worth mentioning that  as presented in this section does not support general recursion. A limited form of recursion on lists is instead provided via a primitive $\foldoperator$ constructor, which takes as argument a (copiable) step function of type $\bang{((\tensor{\typeTwo}{\typeOne}) \lineararrow \typeTwo)}$, an initial value of type $\typeTwo$, and constructs a function of type $\listt{}{\typeOne} \multimap \typeTwo$ implementing the fold of the step function over the input list. Although this workaround is not enough to recover the full power of general recursion, it appears that it is enough to describe many quantum algorithms. Figure <ref> shows an example of the use of $\foldoperator$ to reverse a list. Note that $\abs{\tuple{\varOne}{\varTwo}}{\tensor{\typeOne}{\typeTwo}}{\termOne}$ is syntactic sugar for $\abs{\varThree}{\tensor{\typeOne}{\typeTwo}}{\dest{\varOne}{\varTwo}{\varThree}{\termOne}}$.

\begin{align*}
\mathit{rev} \triangleq
\fold{}{\lift{(\abs{\tuple{\mathit{revList}}{q}}{\tensor{\listt{}{\qubitt}}{\qubitt}}{\return{(\cons{q}{\mathit{revList}})}})}}{\nil}
\end{align*}

Function rev reverses a list of qubits.

To conclude this section, we just remark how all of the  programs shown in Section <ref> can be encoded in . However, 's system of simple types in unable to tell us anything about the resource consumption of these programs. Of course, one could run  on a concrete input and examine the size of the circuit produced at run-time, but this amounts to testing, not verifying the program, and lacks the qualities of staticity and parametricity that we seek.

§ INCEPTING LINEAR DEPENDENCY AND EFFECT TYPING

We are now ready to expand on the informal definition of the  language given in Section <ref>, to reach a formal definition of : a linearly and dependently typed language whose type system supports the derivation of upper bounds on the width of the circuits produced by programs.

§.§ Types and Syntax of

Types	    $\typeSet$	    $\typeOne,\typeTwo$     $
::= \unitt
\mid \wtypeOne
\mid \bang{\typeOne}
\mid \tensor{\typeOne}{\typeTwo}
\mid \arrowt{\typeOne}{\typeTwo}{\indexOne}{\indexTwo}
\mid \listt{\indexOne}{\typeOne}
\mid \circt{\indexOne}{\mtypeOne}{\mtypeTwo}$

Param. types		    $\ptypeSet$	    $\ptypeOne,\ptypeTwo$     $
::= \unitt
\mid \bang{\typeOne}
\mid \tensor{\ptypeOne}{\ptypeTwo}
\mid \listt{\indexOne}{\ptypeOne}
\mid \circt{\indexOne}{\mtypeOne}{\mtypeTwo}$

Bundle types	    $\mtypeset$	    $\mtypeOne,\mtypeTwo$     $
::= \unitt
\mid \wtypeOne
\mid \tensor{\mtypeOne}{\mtypeTwo}
\mid \listt{\indexOne}{\mtypeOne},$

Terms	    $\termSet$	    $\termOne,\termTwo$     $ ::= \app{\valOne}{\valTwo}
\mid \dest{\varOne}{\varTwo}{\valOne}{\termOne}
\mid \force{\valOne}
\mid \boxt{\mtypeOne}{\valOne}$
\mid \apply{\valOne}{\valTwo}
\mid \return{\valOne}
\mid \letin{\varOne}{\termOne}{\termTwo}$

Values	    $\valSet$	    $\valOne,\valTwo$     $
::= \unitv
\mid \varOne
\mid \labOne
\mid \abs{\varOne}{\typeOne}{\termOne}
\mid \lift{\termOne}
\mid \boxedCirc{\struct\labOne}{\circuitOne}{\struct{\labTwo}}
\mid \tuple{\valOne}{\valTwo}$
\mid \nil
\mid \cons{\valOne}{\valTwo}
\mid \fold{\ivarOne}{\valOne}{\valTwo}$

Wire bundles	    $\mvalset$	    $\struct\labOne,\struct\labTwo$     $
::= \unitv
\mid \labOne
\mid \tuple{\struct\labOne}{\struct\labTwo}
\mid \nil
\mid \cons{\struct\labOne}{\struct\labTwo}$

Indices     $\indexSet$     $\indexOne,\indexTwo$     $
::= \ivarOne
\mid \natOne
\mid \iplus{\indexOne}{\indexTwo}
\mid \iminus{\indexOne}{\indexTwo}
\mid \imult{\indexOne}{\indexTwo}
\mid \imax{\indexOne}{\indexTwo}
\mid \imaximum{\ivarOne}{\indexOne}{\indexTwo}$

syntax and types.

The types and syntax of  are given in Figure <ref>.
As we mentioned, one of the key ingredients of our type system are the index terms which we annotate standard  types with. These indices provide quantitative information about the elements of the resulting types, in a manner reminiscent of refinement types [19, 47]. In our case, we are primarily concerned with circuit width, which means that the natural starting point of our extension of  is precisely the circuit type $\circt{}{\mtypeOne}{\mtypeTwo}$: $\circt{\indexOne}{\mtypeOne}{\mtypeTwo}$ has elements the boxed circuits of input type $\mtypeOne$, output type $\mtypeTwo$, and width bounded by $\indexOne$. Term $\indexOne$ is precisely what we call an index, that is, an arithmetical expression denoting a natural number. Looking at the grammar for indices, their interpretation is fairly straightforward: $\natOne$ is a natural number, $\ivarOne$ is an index variable, $\iplus{\indexOne}{\indexTwo},\imult{\indexOne}{\indexTwo}$ and $\imax{\indexOne}{\indexTwo}$ have their intuitive meaning, $\iminus{\indexOne}{\indexTwo}$ denotes natural subtraction, and $\imaximum{\ivarOne}{\indexOne}{\indexTwo}$ is the maximum for $\ivarOne$ going from $0$ (included) to $\indexOne$ (excluded) of $\indexTwo$, where $\ivarOne$ can occur free in $\indexTwo$.

\begin{align*}
\interpret{\wfjudgment{\icontextOne}{\indexOne}} :&\ \mathbb{N}^{|\icontextOne|} \to \mathbb{N} \\
\interpret{\wfjudgment{\icontextOne}{n}} \left(n_1,\dots,n_{|\icontextOne|}\right) =&\ n \\
\interpret{\wfjudgment{\icontextOne,\ivarOne}{\ivarOne}} \left(n_1,\dots,n_{|\icontextOne|},n_i\right) =&\ n_\ivarOne \\
\interpret{\wfjudgment{\icontextOne}{\iplus{\indexOne}{\indexTwo}}} \left(n_1,\dots,n_{|\icontextOne|}\right) =&\ \interpret{\wfjudgment{\icontextOne}{\indexOne}}\left(n_1,\dots,n_{|\icontextOne|}\right) + \interpret{\wfjudgment{\icontextOne}{\indexTwo}}\left(n_1,\dots,n_{|\icontextOne|}\right) \\
\interpret{\wfjudgment{\icontextOne}{\imult{\indexOne}{\indexTwo}}}  \left(n_1,\dots,n_{|\icontextOne|}\right) =&\ \interpret{\wfjudgment{\icontextOne}{\indexOne}}\left(n_1,\dots,n_{|\icontextOne|}\right)\interpret{\wfjudgment{\icontextOne}{\indexTwo}}\left(n_1,\dots,n_{|\icontextOne|}\right) \\
\interpret{\wfjudgment{\icontextOne}{\iminus{\indexOne}{\indexTwo}}}  \left(n_1,\dots,n_{|\icontextOne|}\right) =&\ \max\left(0,\interpret{\wfjudgment{\icontextOne}{\indexOne}}\left(n_1,\dots,n_{|\icontextOne|}\right) - \interpret{\wfjudgment{\icontextOne}{\indexTwo}}\left(n_1,\dots,n_{|\icontextOne|}\right)\right) \\
\interpret{\wfjudgment{\icontextOne}{\imax{\indexOne}{\indexTwo}}}  \left(n_1,\dots,n_{|\icontextOne|}\right) =&\ \max\left(\interpret{\wfjudgment{\icontextOne}{\indexOne}}\left(n_1,\dots,n_{|\icontextOne|}\right), \interpret{\wfjudgment{\icontextOne}{\indexTwo}}\left(n_1,\dots,n_{|\icontextOne|}\right)\right) \\
\interpret{\wfjudgment{\icontextOne}{\imaximum{\ivarOne}{\indexOne}{\indexTwo}}} \left(n_1,\dots,n_{|\icontextOne|}\right) =&\ \max_{n\in\{0,\dots,\interpret{\wfjudgment{\icontextOne}{\indexOne}}\left(n_1,\dots,n_{|\icontextOne|}\right)-1\}} \interpret{\wfjudgment{\icontextOne,\ivarOne}{\indexTwo}}\left(n_1,\dots,n_{|\icontextOne|},n\right)
\end{align*}

Interpretation of well-formed indices.

Let $\icontextOne$ be a set of index variable names, which we call an index context. An index $\indexOne$ is well-formed under context $\icontextOne$, and we write $\wfjudgment{\icontextOne}{\indexOne}$, when all its free index variables are in $\icontextOne$. Figure <ref> provides a more formal interpretation of well-formed indices.

While the index in a circuit type denotes an upper bound, the index in a type of the form $\listt{\indexOne}{\typeOne}$ denotes the exact length of the lists of that type. While this refinement is quite restrictive in a generic scenario, it allows us to include lists of labels among wire bundles, since they are effectively isomorphic to finite tensors of labels and therefore represent wire bundles of known size.
Lastly, as we anticipated in Section <ref>, an arrow type $\arrowt{\typeOne}{\typeTwo}{\indexOne}{\indexTwo}$ is annotated with two indices: $\indexOne$ is an upper bound to the width of the circuit built by the function once it is applied to an argument of type $\typeOne$, while $\indexTwo$ describes the exact number of wire resources captured in the function's closure. The utility of this last annotation will be clearer in Section <ref>.

The languages for terms and values are almost the same as in , with the minor difference that the $\foldoperator$ operator now binds the index variable name $\ivarOne$ within the scope of its first argument. This variable appears locally in the type of the step function, in such a way as to allow each iteration of the fold to contribute to the overall circuit width in a different way.

§.§ A Formal Language for Circuits

The type system of  is designed to reason about the width of circuits. Therefore, before we formally introduce the type system in Section <ref>, we ought to introduce circuits themselves in a formal way. So far, we have only spoken of circuits at a very high and intuitive level, and we have represented them only graphically. Looking at the circuits in Section <ref>, what do they have in common? At the fundamental level, they are made up of elementary operations applied to specific wires. Of course, the order of these operations matters, as does the order of wires that they are applied to (e.g. a controlled not operation does not have the same semantics if we switch the target and control qubits).

In the existing literature on , circuits are usually interpreted as morphisms in a symmetric monoidal category [46], but this approach makes it particularly hard to reason about their intensional properties, such as width. For this reason, we opt for a concrete model of wires and circuits, rather than an abstract one.

Luckily, we already have a datatype modeling ordered structures of wires, that is, the wire bundles that we introduced in the previous sections. We use them as the foundation upon which we build circuits.

Wire bundles	    $\mvalset$	    $\struct\labOne,\struct\labTwo$     $
::= \unitv
\mid \labOne
\mid \tuple{\struct\labOne}{\struct\labTwo}
\mid \nil
\mid \cons{\struct\labOne}{\struct\labTwo},$

Bundle types		    $\mtypeset$	    $\mtypeOne,\mtypeTwo$     $
::= \unitt \mid
\wtypeOne
\mid \tensor{\mtypeOne}{\mtypeTwo}
\mid \listt{\indexOne}{\mtypeOne},$

Circuits	    $\circset$	    $\circuitOne,\circuitTwo$     $ ::= \cidentity{\lcOne}
\mid \circuitOne;\gateapp{\gateOne}{\struct\labOne}{\struct\labTwo}.$

syntax and types.

That being said, Figure <ref> introduces the  () which we use as the target for circuit building in . Wire bundles are exactly as in Figure <ref> and represent arbitrary structures of wires, while circuits themselves are defined very simply as a sequence of elementary operations applied to said structures. We call $\lcOne$ a label context and define it as a partial mapping from label names to wire types. We use label contexts as a mean to keep track of the set of labels available at any point during a computation, alongside their respective types. Circuit $\cidentity{\lcOne}$ represents the identity circuit taking as input the labels in $\lcOne$ and returning them unchanged, while $\circuitOne;\gateapp{\gateOne}{\struct\labOne}{\struct\labTwo}$ represents the application of the elementary operation $\gateOne$ to the wires identified by $\struct\labOne$ among the outputs of $\circuitOne$. Operation $\gateOne$ outputs the wire bundle $\struct\labTwo$, whose labels become part of the outputs of the circuit as a whole. Note that an “elementary operation” is usually the application of a gate, but it could also be a measurement, or the initialization or discarding of a wire. Although semantically very different, from the perspective of circuit building these operations are just elementary building blocks in the construction of a more complex structure, and it makes no sense to distinguish between them syntactically.
Circuits are amenable to a form of concatenation, defined as follows.

We define the concatenation of  circuits $\circuitOne$ and $\circuitTwo$, written $\concat{\circuitOne}{\circuitTwo}$, as follows

\begin{align}
\concat{\circuitOne}{\cidentity{\lcOne}} &= \circuitOne \\
\concat{\circuitOne}{(\circuitTwo;\gateapp{\gateOne}{\struct{\labOne}}{\struct{\labTwo}})} &= (\concat{\circuitOne}{\circuitTwo});\gateapp{\gateOne}{\struct{\labOne}}{\struct{\labTwo}}
\end{align}

§.§.§ Circuit Typing

Naturally, not all circuits built from the  grammar make sense. For example $\cidentity{(\labOne:\qubitt)};\gateapp{H}{\labTwo}{\labTwo}$ and $\cidentity{(\labOne:\qubitt)};\gateapp{\mathit{CNOT}}{\tuple{\labOne}{\labOne}}{\tuple{\labTwo}{\labThree}}$ are both syntactically correct, but the first applies a gate to a non-existing wire, while the second violates the no-cloning theorem by duplicating $\labOne$. To rule out such ill-formed circuits, we employ a rudimentary type system for circuits which allows us to derive judgments of the form $\circjudgment{\circuitOne}{\lcOne}{\lcTwo}$, which informally read “circuit $\circuitOne$ is well-typed with input label context $\lcOne$ and output label context $\lcTwo$”.

type system.

The typing rules for  are given in Figure <ref>. We call $\mjudgment{\lcOne}{\struct\labOne}{\mtypeOne}$ a wire judgment, and we use it to give a structured type $\mtypeOne$ to an otherwise unordered label context $\lcOne$, by means of a wire bundle $\struct{\labOne}$. Most rules are straightforward, except those for lists, which rely on a judgment of the form $\eqjudgment{}{\indexOne}{\indexTwo}$. This is to be intended as a semantic judgment asserting that $\indexOne$ and $\indexTwo$ are closed and equal when interpreted as natural numbers. Within the typing rules for lists, this judgment reflects the idea that there are many ways to syntactically represent the length of a list. For example, $\nil$ can be given type $\listt{0}{\mtypeOne}$, but also $\listt{\iminus{1}{1}}{\mtypeOne}$ or $\listt{\imult{0}{5}}{\mtypeOne}$. This kind of flexibility might seem unwarranted for such a simple language, but it is useful to effectively interface  and the more complex . Speaking of the actual circuit judgments, the seq rule tells us that the the application of an elementary operation $\gateOne$ is well-typed whenever $\gateOne$ only acts on labels occurring in the outputs of $\circuitOne$ (those in $\struct\labOne$, or equivalently in $\lcThree$), produces in output labels that do not clash with the remaining outputs of $\circuitOne$ (since $\lcTwo,\lcFour$ denotes the union of two label contexts with disjoint domains) and has the right signature. This last requirement is expressed as $\gateOne\in\gateset(\mtypeOne,\mtypeTwo)$, where $\gateset(\mtypeOne,\mtypeTwo)$ is the subset of elementary operations that can be applied to an input of type $\mtypeOne$ to obtain an output of type $\mtypeTwo$. For example, the Hadamard gate, which acts on a single qubit, is in $\gateset(\qubitt,\qubitt)$, the controlled not gate is in $\gateset(\tensor{\qubitt}{\qubitt},\tensor{\qubitt}{\qubitt})$ and the single-qubit measurement is in $\gateset(\qubitt,\bitt)$.

§.§.§ Circuit Width

Among the many properties of circuits, we are interested in width, so we conclude this section by giving a formal status to this quantity. As we saw in Section <ref>, when we initialize a new wire, we can reuse previously discarded wires in such a way that the width of a circuit is not always equal to the number of wires that are initialized. We formalize this intuition in the following definition.

We define the width of a  circuit $\circuitOne$, written $\width{\circuitOne}$, as follows

\begin{align}
\width{\cidentity{\lcOne}} &= |\lcOne|\\
\width{\circuitOne;\gateapp{\gateOne}{\struct\labOne}{\struct\labTwo}} &= \width{\circuitOne} + \max(0, \inits{\gateOne} - \discarded{\circuitOne})
\end{align}

where $\discarded{\circuitOne} = \width{\circuitOne} - \operatorname{outputs}(\circuitOne)$ and

\begin{align}
\operatorname{outputs}(\cidentity{\lcOne}) &= |\lcOne|\\
\operatorname{outputs}(\circuitOne;\gateapp{\gateOne}{\struct{\labOne}}{\struct{\labTwo}}) &= \operatorname{outputs}(\circuitOne) + \inits{\gateOne}
\end{align}

In the definition above, $|\lcOne|$ is the number of labels in $\lcOne$ and $\inits{\gateOne}$ represents the net number of new wires initialized by $\gateOne$. If $\gateOne$ outputs less wires than it consumes, then $\inits{\gateOne}$ is negative. The idea is that whenever we require a new wire in our computation, first we try to reuse a previously discarded wire, in which case the initialization does not add to the total width of the circuit ($\inits{\gateOne} \leq \discarded{\circuitOne}$), and only if we cannot do so we actually create a new wire, increasing the overall width of the circuit ($\inits{\gateOne} > \discarded{\circuitOne}$).

Now that we have a formal definition of circuit types and width, we can state a fundamental property of the concatenation of well-typed circuits, which is illustrated in Figure <ref> and proven in Theorem <ref>. We use this result pervasively in proving the correctness of  in section <ref>.

Given $\circjudgment{\circuitOne}{\lcOne}{\lcTwo,\lcThree}$ and $\circjudgment{\circuitTwo}{\lcThree}{\lcFour}$ such that the labels shared by $\circuitOne$ and $\circuitTwo$ are all and only those in $\lcThree$, we have

* $\circjudgment{\concat{\circuitOne}{\circuitTwo}}{\lcOne}{\lcTwo,\lcFour},$

* $\width{\concat{\circuitOne}{\circuitTwo}} \leq \maxf{\width{\circuitOne}}{\width{\circuitTwo} + |\lcTwo|}.$

By induction of the derivation of $\circjudgment{\circuitTwo}{\lcThree}{\lcFour}$.

.98[row sep=1em]
$\lcOne$     ||     [2]             ||             $\lcTwo$

n             q         ||          ||    $\lcFour$

The concatenation of well-typed circuits $\circuitOne$ and $\circuitTwo$.

§.§ Typing Programs

Going back to , we have already seen how the standard  types are refined with quantitative information. However, decorating types is not enough for the purposes of width estimation. Recall that, in general, a  program produces a circuit as a side effect of its evaluation. If we want to reason about the width of said circuit, it is not enough to rely on a regular linear type system, although dependent. Rather, we have to introduce the second ingredient of our analysis and turn to a type-and-effect system [41], revolving around a type judgment of the form

\begin{equation}
\cjudgment{\icontextOne}{\contextOne}{\lcOne}{\termOne}{\typeOne}{\indexOne},
\end{equation}

which intuitively reads “for all values of the index variables in $\icontextOne$, under typing context $\contextOne$ and label context $\lcOne$, term $\termOne$ has type $\typeOne$ and produces a circuit of width at most $\indexOne$”. Therefore, the index variables in $\icontextOne$ are universally quantified in the rest of the judgment. Context $\contextOne$ is a typing context for parameter and linear variables alike. When a typing context contains exclusively parameter variables, we write it as $\pcontextOne$. In this judgment, index $\indexOne$ plays the role of an effect annotation, describing a relevant aspect of the side effect produced by the evaluation of $\termOne$ (i.e. the width of the produced circuit). The attentive reader might wonder why this annotation consists only of one index, whereas when we discussed arrow types in previous sections we needed two. The reason is that the second index, which we use to keep track of the number of wires captured by a function, is redundant in a typing judgment where the same quantity can be inferred directly from the environments $\contextOne$ and $\lcOne$. A similar typing judgment is introduced for values, which are effect-less:

\begin{equation}
\vjudgment{\icontextOne}{\contextOne}{\lcOne}{\valOne}{\typeOne}.
\end{equation}

= ;(1)

type system.

well-formedness rules.

The rules for deriving typing judgments are those in Figure <ref>, where $\contextOne_1,\contextOne_2$ and $\lcOne_1,\lcOne_2$ denote the union of two contexts with disjoint domains. The well-formedness judgment $\wfjudgment{\icontextOne}{\indexOne}$ is extended to types as shown in Figure <ref> and then lifted to typing contexts in the natural way. Among interesting typing rules, we can see how the circ rule bridges between  and . A boxed circuit $\boxedCirc{\struct\labOne}{\circuitOne}{\struct\labTwo}$ is well typed with type $\circt{\indexOne}{\mtypeOne}{\mtypeTwo}$ when $\circuitOne$ is no wider than the quantity denoted by $\indexOne$, $\circjudgment{\circuitOne}{\lcOne}{\lcTwo}$ and $\struct\labOne,\struct\labTwo$ contain all and only the labels in $\lcOne$ and $\lcTwo$, respectively, acting as a language-level interface to $\circuitOne$.

The two main constructs that interact with circuits are $\applyoperator$ and $\boxoperator$. The apply rule is the foremost place where effects enter the type derivation:

\begin{equation*}
\inference[\textit{apply}]
\vjudgment{\icontextOne}{\pcontextOne,\contextOne_2}{\lcOne_2}{\valTwo}{\mtypeOne}}
\end{equation*}

Since $\valOne$ represents some boxed circuit of width at most $\indexOne$, its application to an appropriate wire bundle $\valTwo$ produces exactly a circuit of width at most $\indexOne$.
The box rule, on the other hand, works more or less in the opposite direction:

\begin{equation*}
\inference[\textit{box}]
\end{equation*}

If $\valOne$ is a circuit building function that, once applied to an input of type $\mtypeOne$, would build a circuit of output type $\mtypeTwo$ and width at most $\indexOne$, then boxing it means turning it into a boxed circuit with the same characteristics. Note that the box rule requires that the typing context be devoid of linear variables. This reflects the idea that $\valOne$ is meant to be executed in complete isolation, to build a standalone, replicable circuit, and therefore it should not capture any linear resource (e.g. a label) from the surrounding environment.

§.§.§ Wire Count

Notice that many rules rely on an operator written $\rcount{\cdot}$, which we call the wire count operator. Intuitively, this operator returns the number of wire resources (in our case, bits or qubits) represented by a type or context. To understand how this is important, consider the return rule:

\begin{equation*}
\inference[\textit{return}]
\end{equation*}

The $\returnoperator$ operator turns a value $\valOne$ into a trivial computation that evaluates immediately to $\valOne$, and therefore it would be tempting to give it an effect annotation of $0$. However, $\valOne$ is not necessarily a closed value. In fact, it might very well contain many bits and qubits, coming both from the typing context $\contextOne$ and the label context $\lcOne$. Although nothing happens to these bits and qubits, they still corresponds to wires in the underlying circuit, and these wires have a width which must be accounted for in the judgment for the otherwise trivial computation. The return rule therefore produces an effect annotation of the form $\rcount{\contextOne;\lcOne}$, which corresponds exactly to this quantity. A formal description of the wire count operator on types is given in the following Definition <ref>.

We define the wire count of a type $\typeOne$, written $\rcount{\typeOne}$, as a function $\rcount{\cdot}:\typeSet\to\indexSet$ such that

=  =  =0
= 1
=  =

This definition is lifted to typing and label contexts in the natural way. Note that, for any label context $\lcOne$, we have $\rcount{\lcOne}=|\lcOne|$. Annotation $\rcount{\contextOne;\lcOne}$ is then shorthand for $\iplus{\rcount{\contextOne}}{|\lcOne|}$. This definition is fairly straightforward, except for the arrow case. By itself, an arrow type does not give us any information about the amount of qubits or bits captured in the corresponding closure. This is precisely where the second index $\indexTwo$, which keeps track exactly of this quantity, comes into play. This annotation is introduced by the abs rule and allows our analysis to circumvent data hiding.

The let rule is another rule in which wire counts are essential:

\begin{equation*}
\inference[\textit{let}]
\cjudgment{\icontextOne}{\pcontextOne,\contextOne_2,\varOne:\typeOne}{\lcOne_2}{\termTwo}{\typeTwo}{\indexTwo}}
\end{equation*}

The two terms $\termOne$ and $\termTwo$ build the circuits $\circuitOne_\termOne$ and $\circuitOne_\termTwo$, whose widths are bounded by $\indexOne$ and $\indexTwo$, respectively. Once again, it might be tempting to conclude that the overall circuit built by the let construct has width bounded by $\imax{\indexOne}{\indexTwo}$, but this fails to take into account the fact that while $\termOne$ is building $\circuitOne_\termOne$ starting from the wires contained in $\contextOne_1$ and $\lcOne_1$, we must keep aside the wires contained in $\contextOne_2$ and $\lcOne_2$, which will be used by $\termTwo$ to build $\circuitOne_\termTwo$. These wires must flow alongside $\circuitOne_\termOne$ and their width, i.e. $\rcount{\contextOne_2;\lcOne_2}$, adds up to the total width of the left-hand side of the $\letoperator$ construct, leading to an overall width upper bound of $\imax{\indexOne+\rcount{\contextOne_2;\lcOne_2}}{\indexTwo}$. This situation is better illustrated in Figure <ref>.

.98[row sep=1.5em, column sep=3em]
$\contextOne_1$    _1     [2]_     n

$\lcOne_1$    _1        x:           [3]_

$\contextOne_2$    _2

$\lcOne_2$    _2

The shape of a circuit built by a $\letoperator$ construct.

The last rule that makes substantial use of wire counts is fold, arguably the most complex rule in the system:

\begin{equation*}
\inference[\textit{fold}]
\vjudgment{\icontextOne,\ivarOne}{\pcontextOne}{\emptycontext}{\valOne}{\bang{(\arrowt{(\tensor{\typeTwo}{\typeOne})}{\typeTwo\isub{\iplus{\ivarOne}{1}}{\ivarOne}}{\indexTwo}{\indexTwo'})}}
\\
\wfjudgment{\icontextOne}{\indexOne}
\wfjudgment{\icontextOne}{\typeOne}
\indexThree = \imax{\rcount{\contextOne;\lcOne}}{\imaximum{\ivarOne}{\indexOne}{\iplus{\indexTwo}{\imult{(\iminus{\iminus{\indexOne}{1}}{\ivarOne})}{\rcount{\typeOne}}}}}}
\end{equation*}

The main ingredient of the fold rule is the bound index variable $\ivarOne$, which occurs in the accumulator type $\typeTwo$ and is used to keep track of the number of steps performed by the fold. Let $(\cdot)\isub{\indexOne}{\ivarOne}$ denote the capture-avoiding substitution of the index term $\indexOne$ for the index variable $\ivarOne$ inside an index, type, context, value or term, not unlike $(\cdot)\sub{\valOne}{\varOne}$ denotes the capture-avoiding substitution of the value $\valOne$ for the variable $\varOne$. Intuitively, if the accumulator has initially type $\typeTwo\isub{0}{\ivarOne}$ and each application of the step function increases $\ivarOne$ by one, then when we fold over a list of length $\indexOne$ we get an output of type $\typeTwo\isub{\indexOne}{\ivarOne}$. Index $\indexThree$ is the upper bound to the width of the overall circuit built by the fold: if the input list is empty, then the width of the circuit is just the number of wires contained in the initial accumulator, that is, $\rcount{\contextOne;\lcOne}$. If the input list is non-empty, on the other hand, things get slightly more complicated. At each step $\ivarOne$, the step function builds a circuit $\circuitOne_\ivarOne$ of width bounded by $\indexTwo$, where $\indexTwo$ might depend on $\ivarOne$. This circuit takes as input all the wires in the accumulator, as well as the wires contained in the first element of the input list, which are $\rcount{\typeOne}$. The wires contained in remaining $\indexOne - 1 - \ivarOne$ elements have to flow alongside $\circuitOne_\ivarOne$, giving a width upper bound of $\indexTwo + (\indexOne - 1 - \ivarOne) \times \rcount{\typeOne}$ at each step $\ivarOne$. The overall width upper bound is then the maximum for $\ivarOne$ going from $0$ to $\indexOne-1$ of this quantity, i.e. precisely $\imaximum{\ivarOne}{\indexOne}{\indexTwo + (\indexOne - 1 - \ivarOne) \times \rcount{\typeOne}}$. Once again, a graphical representation of this scenario is given in Figure <ref>.

.98[column sep=2em, row sep=1em]
$\contextOne$          [3]_0

1         [2]_1

2      …    n

n                     …    q-1           [2]_-1

The shape of a circuit built by a fold applied to an input list of type $\listt{\indexOne}{\typeOne}$.

§.§.§ Subtyping

Notice that 's type system includes two rules for subtyping, which are effectively the same rule for terms and values, respectively: csub and vsub.
We mentioned that our type system resembles a refinement type system, and all such systems induce a subtyping relation between types, where $\typeOne$ is a subtype of $\typeTwo$ whenever the former is “at least as refined” as the latter. In our case, a subtyping judgment such as $\subtypejudgment{\icontextOne}{\typeOne}{\typeTwo}$ means that for all natural values of the index variables in $\icontextOne$, $\typeOne$ is a subtype of $\typeTwo$.

subtyping rules.

We derive this kind of judgments by the rules in Figure <ref>. Note that $\sametypejudgment{\icontextOne}{\typeOne}{\typeTwo}$ is shorthand for “$\subtypejudgment{\icontextOne}{\typeOne}{\typeTwo}$ and $\subtypejudgment{\icontextOne}{\typeTwo}{\typeOne}$”. Subtyping relies in turn on a judgment of the form $\leqjudgment{\icontextOne}{\indexOne}{\indexTwo}$, which is a generalization of the semantic judgment that we used in the  type system in Section <ref>. Such a judgment asserts that for all values of the index variables in $\icontextOne$, $\indexOne$ is lesser or equal than $\indexTwo$. More formally, the meaning of $\leqjudgment{\icontextOne}{\indexOne}{\indexTwo}$ is that $\wfjudgment{\icontextOne}{\indexOne},\wfjudgment{\icontextOne}{\indexTwo}$ and for all $n_1,\dots,n_{|\icontextOne|}$: $\interpret{\wfjudgment{\icontextOne}{\indexOne}}(n_1,\dots,n_{|\icontextOne|}) \leq \interpret{\wfjudgment{\icontextOne}{\indexTwo}}(n_1,\dots,n_{|\icontextOne|})$.
Consequently, $\eqjudgment{}{\indexOne}{\indexTwo}$ is just shorthand for $\eqjudgment{\emptycontext}{\indexOne}{\indexTwo}$, which in turn is shorthand for “$\leqjudgment{\icontextOne}{\indexOne}{\indexTwo}$ and $\leqjudgment{\icontextOne}{\indexTwo}{\indexOne}$”. We purposefully leave the decision procedure of this kind of judgments unspecified, with the prospect that, in a practical scenario, they could be delegated to an SMT solver [7].

§.§ Operational Semantics

Operationally speaking, it does not make sense, in the  languages, to speak of the semantics of a term in isolation: a term is always evaluated in the context of an underlying circuit that supplies all of the term's free labels. We therefore define the operational semantics of  as a big-step evaluation relation $\eval$ on configurations, i.e. circuits paired with either terms or values. Intuitively, $\config{\circuitOne}{\termOne}\eval\config{\circuitTwo}{\valOne}$ means that $\termOne$ evaluates to $\valOne$ and updates $\circuitOne$ to $\circuitTwo$ as a side effect.

big-step operational semantics.

The rules for evaluating configurations are given in Figure <ref>, where $\circuitOne,\circuitTwo$ and $\circuitThree$ are circuits, $\termOne$ and $\termTwo$ are terms, while $\valOne,\valTwo,\valThree,\valFour$ and $\valFive$ are values. Most evaluation rules are straightforward, with the exception perhaps of apply, box and fold-step.
Being the fundamental block of circuit-building, the semantics of $\applyoperator$ lies almost entirely in the way it updates the underlying circuit:

\begin{equation*}
\inference[\textit{apply}]
{\config{\circuitThree}{\struct{\labFour}} = \append{\circuitOne}{\struct{\labThree}}{\boxedCirc{\struct\labOne}{\circuitTwo}{\struct{\labTwo}}}}
{\config{\circuitOne}{\apply{\boxedCirc{\struct\labOne}{\circuitTwo}{\struct{\labTwo}}}{\struct{\labThree}}} \eval \config{\circuitThree}{\struct{\labFour}}}
\end{equation*}

The concatenation of the underlying circuit $\circuitOne$ and the applicand $\circuitTwo$ is delegated entirely to the $\appendfunction$ function, which is defined as follows.

We define the append of $\boxedCirc{\struct\labOne}{\circuitTwo}{\struct{\labTwo}}$ to $\circuitOne$ on $\struct\labThree$, written $\append{\circuitOne}{\struct\labThree}{\boxedCirc{\struct\labOne}{\circuitTwo}{\struct{\labTwo}}}$, as the function that performs the following steps:

* Finds $\boxedCirc{\struct\labThree}{\circuitTwo'}{\struct{\labFour}}$ equivalent to $\boxedCirc{\struct\labOne}{\circuitTwo}{\struct{\labTwo}}$ such that the labels shared by $\circuitOne$ and $\circuitTwo'$ are all and only those in $\struct\labThree$,

* Computes $\circuitThree = \concat{\circuitOne}{\circuitTwo'}$,

* Returns $\config{\circuitThree}{\struct{\labFour}}$.

Note that two circuits are equivalent when they only differ by a renaming of labels, that is, when they have the same fundamental structure. What the renaming does, in this case, is instantiate the generic input interface $\struct\labOne$ of circuit $\circuitTwo$ with the actual labels that it is going to be appended to, namely $\struct\labThree$, and ensure that there are no name clashes between the labels occurring in the resulting $\circuitTwo'$ and those occurring in $\circuitOne$.

On the other hand, the semantics of a term of the form $\boxt{\mtypeOne}{(\lift{\termOne})}$ relies on the $\freshlabelsfunction$ function:

\begin{equation*}
\inference[\textit{box}]
\config{\cidentity{\lcOne}}{\termOne} \eval \config{\cidentity{\lcOne}}{\valOne}
\config{\cidentity{\lcOne}}{\app{\valOne}{\struct{\labOne}}} \eval \config{\circuitTwo}{\struct{\labTwo}}}
{\config{\circuitOne}{\boxt{\mtypeOne}{(\lift{\termOne})}} \eval \config{\circuitOne}{\boxedCirc{\struct{\labOne}}{\circuitTwo}{\struct{\labTwo}}}}
\end{equation*}

What $\freshlabelsfunction$ does is take as input a bundle type $\mtypeOne$ and instantiate fresh $\lcOne,\struct\labOne$ such that $\mjudgment{\lcOne}{\struct\labOne}{\mtypeOne}$. The wire bundle $\struct\labOne$ is then used as a dummy argument to $\valOne$, the circuit-building function resulting from the evaluation of $\termOne$. This function application is evaluated in the context of the identity circuit $\cidentity{\lcOne}$ and eventually produces a circuit $\circuitTwo$, together with its output labels $\struct{\labTwo}$. Finally, $\struct{\labOne}$ and $\struct{\labTwo}$ become respectively the input and output interfaces of the resulting boxed circuit $\boxedCirc{\struct{\labOne}}{\circuitTwo}{\struct{\labTwo}}$.
Note, at this point, that $\mtypeOne$ controls how many labels are initialized by the $\freshlabelsfunction$ function. Because $\mtypeOne$ can contain indices (e.g. it could be that $\mtypeOne \equiv \listt{3}{\qubitt}$), it follows that in  indices are not only relevant to typing, but they also have operational value. For this reason, the semantics of  is well-defined only on terms closed both in the sense of regular variables and index variables, since a circuit-building function of input type, e.g., $\listt{\ivarOne}{\qubitt}$ does not correspond to any individual circuit, and therefore it makes no sense to try and box it.

The operational significance of indices is also apparent in the fold-step rule:

\begin{equation*}
\inference[\textit{fold-step}]
{\config{\circuitOne}{\termOne\isub{0}{\ivarOne}} \eval \config{\circuitOne}{\valFour}
\config{\circuitOne}{\app{\valFour}{\tuple{\valOne}{\valTwo}}} \eval \config{\circuitThree}{\valFive}
\\
\config{\circuitThree}{\app{(\fold{\ivarOne}{(\lift{\termOne\isub{\iplus{\ivarOne}{1}}{\ivarOne}})}{\valFive})}{\valTwo'}} \eval \config{\circuitTwo}{\valThree}}
{\config{\circuitOne}{\app{(\fold{\ivarOne}{(\lift{\termOne})}{\valOne})}{(\cons{\valTwo}{\valTwo'})}} \eval \config{\circuitTwo}{\valThree}}
\end{equation*}

Here, the index variable $\ivarOne$ occurring free in $\termOne$ is instantiated to $0$ before evaluating $\termOne$ to obtain the step function $\valFour$. Next, the new accumulator $\valFive$ is computed. Then, before evaluating the next iteration, $\ivarOne$ is replaced with $\iplus{\ivarOne}{1}$ in $\termOne$. This way, each time $\termOne$ is evaluated, $\ivarOne$ is equal to the number of the current iteration, and the evaluation can result in a function $\valFour$ which is operationally distinct for each iteration.

§ TYPE SAFETY AND CORRECTNESS

Because the operational semantics of  is based on configurations, we ought to adopt a notion of well-typedness which is also based on configurations. The following definition of well-typed configuration is thus central to our type-safety analysis.

We say that configuration $\config{\circuitOne}{\termOne}$ is well-typed with input $\lcOne$, type $\typeOne$, width $\indexOne$ and output $\lcTwo$, and we write $\cconfigjudgment{\lcOne}{\config{\circuitOne}{\termOne}}{\typeOne}{\indexOne}{\lcTwo}$, whenever $\circjudgment{\circuitOne}{\lcOne}{\lcTwo,\lcThree}$ for some $\lcThree$ such that $\cjudgment{\emptycontext}{\emptycontext}{\lcThree}{\termOne}{\typeOne}{\indexOne}$.
We write $\vconfigjudgment{\lcOne}{\config{\circuitOne}{\valOne}}{\typeOne}{\lcTwo}$ whenever $\circjudgment{\circuitOne}{\lcOne}{\lcTwo,\lcThree}$ for some $\lcThree$ such that $\vjudgment{\emptycontext}{\emptycontext}{\lcThree}{\valOne}{\typeOne}$.

The three results that we want to show in this section are that any well-typed term configuration $\cconfigjudgment{\lcOne}{\config{\circuitOne}{\termOne}}{\typeOne}{\indexOne}{\lcTwo}$ evaluates to some configuration $\config{\circuitTwo}{\valOne}$, that $\vconfigjudgment{\lcOne}{\config{\circuitTwo}{\valOne}}{\typeOne}{\lcTwo}$ and that $\circuitTwo$ is obtained from $\circuitOne$ by extending it with a sub-circuit of width at most $\indexOne$. These claims correspond to the subject reduction and total correctness properties that we will prove at the end of this section. However, both these results rely on a central lemma and on the mutual notions of realization and reducibility, which we first give formally.

We define $\realizes{\valOne}{\lcOne}{\typeOne}$, which reads $\valOne$ realizes $\typeOne$ under $\lcOne$, as the smallest relation such that

\begin{align*}
\realizes{\unitv&}{\emptylc}{\unitt}\\
\realizes{\labOne&}{\labOne:\wtypeOne}{\wtypeOne}\\
\realizes{\valOne&}{\lcOne}{\arrowt{\typeOne}{\typeTwo}{\indexOne}{\indexTwo}} \text{ iff } \eqjudgment{}{\indexTwo}{|\lcOne|}\text{ and }\forall \valTwo: \realizes{\valTwo}{\lcTwo}{\typeOne} \implies \reducible{\app{\valOne}{\valTwo}}{\lcOne,\lcTwo}{\indexOne}{\typeTwo}\\
\realizes{\lift{\termOne}&}{\emptylc}{\bang{\typeOne}}\text{ iff }\reducible{\termOne}{\emptylc}{0}{\typeOne}\\
\realizes{\tuple{\valOne}{\valTwo}&}{\lcOne,\lcTwo}{\tensor{\typeOne}{\typeTwo}}\text{ iff }\realizes{\valOne}{\lcOne}{\typeOne}\text{ and }\realizes{\valTwo}{\lcTwo}{\typeTwo}\\
\realizes{\nil&}{\emptycontext}{\listt{\indexOne}{\typeOne}}\text{ iff }\eqjudgment{}{\indexOne}{0}\\
\realizes{\cons{\valOne}{\valTwo}&}{\lcOne,\lcTwo}{\listt{\indexOne}{\typeOne}}\text{ iff }\eqjudgment{}{\indexOne}{\iplus{\indexTwo}{1}}\text{ and }\realizes{\valOne}{\lcOne}{\typeOne}\text{ and } \realizes{\valTwo}{\lcTwo}{\listt{\indexTwo}{\typeOne}}\\
\realizes{\boxedCirc{\struct\labOne}{\circuitOne}{\struct{\labTwo}}&}{\emptylc}{\circt{\indexOne}{\mtypeOne}{\mtypeTwo}}\text{ iff }\circjudgment{\circuitOne}{\lcOne}{\lcTwo}\text{ and } \mjudgment{\lcOne}{\struct\labOne}{\mtypeOne}\text{ and } \mjudgment{\lcTwo}{\struct{\labTwo}}{\mtypeTwo}\text{ and }\leqjudgment{}{\width{\circuitOne}}{\indexOne}
\end{align*}

We say that $\termOne$ is reducible under $\lcOne$ with type $\typeOne$ and width $\indexOne$, and we write $\reducible{\termOne}{\lcOne}{\indexOne}{\typeOne}$, if, for all $\circuitOne$ such that $\circjudgment{\circuitOne}{\lcTwo}{\lcOne,\lcThree}$, there exist $\circuitTwo,\valOne$ such that

* $\config{\circuitOne}{\termOne} \eval \config{\concat{\circuitOne}{\circuitTwo}}{\valOne},$

* $\leqjudgment{}{\width{\circuitTwo}}{\indexOne}$

* $\circjudgment{\circuitTwo}{\lcOne}{\lcFour}$ for some $\lcFour$ such that $\realizes{\valOne}{\lcFour}{\typeOne}$.

Both relations, and in particular reducibility, are given in the form of unary logical relations [55]. The intuition is pretty straightforward: a term is reducible with width $\indexOne$ if it evaluates correctly when paired with any circuit $\circuitOne$ which provides its free labels and if it extends $\circuitOne$ with a sub-circuit $\circuitTwo$ whose width is bounded by $\indexOne$. Realization, on the other hand, is less immediate. For most cases, realizing type $\typeOne$ loosely corresponds to being closed and well-typed with type $\typeOne$, but a value realizes an arrow type $\arrowt{\typeOne}{\typeTwo}{\indexOne}{\indexTwo}$ when its application to a value realizing $\typeOne$ is reducible with type $\typeTwo$ and width $\indexOne$.

By themselves, realization and reducibility are defined only on terms and values closed in the sense both of regular and index variables. To extend these notions to open terms and values, we adopt the standard approach of reasoning explicitly about the substitutions that could render them closed.

We define the set $\vsubSet$ of closing value substitutions as the smallest subset of $\valSet\cup\termSet \to \valSet\cup\termSet$ such that

* $\emptysub\in\vsubSet$ with $\emptysub(\termOne) = \termOne$.

* If $\vsubOne\in\vsubSet$, $\varOne$ is a variable name and $\valOne\in\valSet$ is closed, then $\vsubOne[\varOne\mapsto\valOne]\in\vsubSet$ with $\vsubOne[\varOne\mapsto\valOne](\termOne) = \vsubOne(\termOne\sub{\valOne}{\varOne})$.

We define the set $\isubSet$ of closing index substitutions as the smallest subset of $\indexSet\cup\typeSet\cup\valSet\cup\termSet \to \indexSet\cup\typeSet\cup\valSet\cup\termSet$ such that

* $\emptysub\in\isubSet$ with $\emptysub(\termOne) = \termOne$.

* If $\isubOne\in\isubSet$, $\ivarOne$ is an index variable name and $\indexOne\in\indexSet$ is closed, then $\isubOne[\ivarOne\mapsto\indexOne]\in\isubSet$ with $\isubOne[\ivarOne\mapsto\indexOne](\termOne) = \isubOne(\termOne\isub{\indexOne}{\ivarOne})$.

We say that $\vsubOne$ implements a typing context $\contextOne$ using label context $\lcOne$, and we write $\vimplements{\vsubOne}{\lcOne}{\contextOne}$, when it replaces every variable $\varOne_i$ in the domain of $\contextOne$ with a value $\valOne_i$ such that $\realizes{\valOne_i}{\lcOne_i}{\contextOne(\varOne_i)}$ and $ \lcOne=\biguplus_{\varOne_i\in\operatorname{dom}(\contextOne)} \lcOne_i$. Similarly, we say that $\isubOne$ implements an index context $\icontextOne$, and we write $\iimplements{\isubOne}{\icontextOne}$, when it replaces every index variable in $\icontextOne$ with a closed index term.
This allows us to give the following fundamental lemma, which will be used while proving all other claims.

Let $\Pi$ be a type derivation. For all $\iimplements{\isubOne}{\icontextOne}$ and $\vimplements{\vsubOne}{\lcOne}{\isubOne(\contextOne)}$, we have that

\begin{align*}
\Pi \proves \cjudgment{\icontextOne}{\contextOne}{\lcTwo}{\termOne}{\typeOne}{\indexOne} &\implies \reducible{\vsubOne(\isubOne(\termOne))}{\lcOne,\lcTwo}{\isubOne(\indexOne)}{\isubOne(\typeOne)}\\
\Pi \proves \vjudgment{\icontextOne}{\contextOne}{\lcTwo}{\valOne}{\typeOne} &\implies \realizes{\vsubOne(\isubOne(\valOne))}{\lcOne,\lcTwo}{\isubOne(\typeOne)}
\end{align*}

By induction on the size of $\Pi$, making use of Theorem <ref>.

Lemma <ref> tells us that any well-typed term (resp. value) is reducible (resp. realizes its type) when we instantiate its free variables according to its contexts.
Now that we have Lemma <ref>, we can proceed to proving the aforementioned results of subject reduction and total correctness. We start with the former, which unsurprisingly requires the following substitution lemmata.

Let $\Pi$ be a type derivation and let $\indexOne$ be an index such that $\wfjudgment{\icontextOne}{\indexOne}$. We have that

\begin{align*}
\Pi \proves \cjudgment{\icontextOne,\ivarOne}{\contextOne}{\lcOne}{\termOne}{\typeOne}{\indexTwo} &\implies \cjudgment{\icontextOne}{\contextOne\isub{\indexOne}{\ivarOne}}{\lcOne}{\termOne\isub{\indexOne}{\ivarOne}}{\typeOne\isub{\indexOne}{\ivarOne}}{\indexTwo\isub{\indexOne}{\ivarOne}},\\
\Pi \proves \vjudgment{\icontextOne,\ivarOne}{\contextOne}{\lcOne}{\valOne}{\typeOne} &\implies \vjudgment{\icontextOne}{\contextOne\isub{\indexOne}{\ivarOne}}{\lcOne}{\valOne\isub{\indexOne}{\ivarOne}}{\typeOne\isub{\indexOne}{\ivarOne}}.
\end{align*}

By induction on the size of $\Pi$.

Let $\Pi$ be a type derivation and let $\valOne$ be a value such that $\vjudgment{\icontextOne}{\pcontextOne,\contextOne_1}{\lcOne_1}{\valOne}{\typeOne}$. We have that

\begin{align*}
\Pi \proves \cjudgment{\icontextOne}{\pcontextOne,\contextOne_2,\varOne:\typeOne}{\lcOne_2}{\termOne}{\typeTwo}{\indexOne} &\implies \cjudgment{\icontextOne}{\pcontextOne,\contextOne_1,\contextOne_2}{\lcOne_1,\lcOne_2}{\termOne\sub{\valOne}{\varOne}}{\typeTwo}{\indexOne},\\
\Pi \proves \vjudgment{\icontextOne}{\pcontextOne,\contextOne_2,\varOne:\typeOne}{\lcOne_2}{\valTwo}{\typeTwo} &\implies \vjudgment{\icontextOne}{\pcontextOne,\contextOne_1,\contextOne_2}{\lcOne_1,\lcOne_2}{\valTwo\sub{\valOne}{\varOne}}{\typeTwo}.
\end{align*}

By induction on the size of $\Pi$.

The main result is then stated in the following theorem.

If $\cconfigjudgment{\lcOne}{\config{\circuitOne}{\termOne}}{\typeOne}{\indexOne}{\lcTwo}$ and $\config{\circuitOne}{\termOne} \eval \config{\circuitTwo}{\valOne}$, then $\vconfigjudgment{\lcOne}{\config{\circuitTwo}{\valOne}}{\typeOne}{\lcTwo}$.

By induction on the derivation of $\config{\circuitOne}{\termOne} \eval \config{\circuitTwo}{\valOne}$ and case analysis on the last rule used in its derivation. Lemma <ref> is essential to the app,dest and let cases, while Lemma <ref> is used in the fold-step case. Lemma <ref> is essential to the box case, as it is the only case in which the side effect of the evaluation (the circuit built by the function being boxed), whose preservation is the a matter of correctness, becomes a value (the resulting boxed circuit).

Of course, type soundness is not enough: we also want the resource analysis carried out by our type system to be correct, as stated in the following theorem.

If $\cconfigjudgment{\lcOne}{\config{\circuitOne}{\termOne}}{\typeOne}{\indexOne}{\lcTwo}$, then there exist $\circuitTwo,\valOne$ such that $\config{\circuitOne}{\termOne} \eval \config{\concat{\circuitOne}{\circuitTwo}}{\valOne}$ and $\leqjudgment{}{\width{\circuitTwo}}{\indexOne}$.

By definition, $\cconfigjudgment{\lcOne}{\config{\circuitOne}{\termOne}}{\typeOne}{\indexOne}{\lcTwo}$ entails that $\circjudgment{\circuitOne}{\lcOne}{\lcTwo,\lcThree}$ and $\cjudgment{\emptycontext}{\emptycontext}{\lcThree}{\termOne}{\typeOne}{\indexOne}$. Since an empty context is trivially implemented by an empty closing substitution, by Lemma <ref> we get $\reducible{\termOne}{\lcThree}{\indexOne}{\typeOne}$, which by definition entails that there exist $\circuitTwo,\valOne$ such that $\config{\circuitOne}{\termOne}\eval\config{\concat{\circuitOne}{\circuitTwo}}{\valOne}$ and $\leqjudgment{}{\width{\circuitTwo}}{\indexOne}$.

§ A PRACTICAL EXAMPLE

This section provides an example of how  can be used to verify the resource usage of realistic quantum algorithms. In particular, we use our language to implement the QFT algorithm [12, 40] and verify that the circuits it produces have width no greater than the size of their input, i.e. that the QFT algorithm does not overall use additional ancillary qubits.

\begin{align*}
\mathit{qft} &\triangleq \fold{\ivarTwo}{\mathit{qftStep}}{\nil}\\
\mathit{qftStep} &\triangleq \lift{(\return{\abs{\tuple{\mathit{qs}}{q}}{\tensor{\listt{\ivarTwo}{\qubitt}}{\qubitt}}{\\&
\letin{\tuple{n}{\mathit{qs}}}{\app{\mathit{qlen}}{\mathit{qs}}}{\\&
\letin{\mathit{revQs}}{\app{\mathit{rev}}{\mathit{qs}}}{\\&
\letin{\tuple{q}{\mathit{qs}}}{\app{(\fold{\ivarThree}{(\lift{(\app{\mathit{rotate}}{n})})}{\tuple{q}{\nil}})}{\mathit{revQs}}}{\\&
\letin{q}{\apply{\mathsf{H}}{q}}{\\&
\return{(\cons{q}{\mathit{qs}})}}}}}}}})
\\\\
\mathit{rotate} &\triangleq \abs{n}{\natt}{\return{\abs{\tuple{\tuple{q}{\mathit{cs}}}{c}}{\tensor{(\tensor{\qubitt}{\listt{\ivarThree}{\qubitt}})}{\qubitt}}{\\&
\letin{\tuple{m}{\mathit{cs}}}{\app{\mathit{qlen}}{\mathit{cs}}}{\\&
\letin{\mathit{rgate}}{\app{\mathsf{makeRGate}}{(n+1-m)}}{\\&
\letin{\tuple{q}{c}}{\apply{\mathit{rgate}}{\tuple{q}{c}}}{\\&
\return{\tuple{q}{\cons{c}{\mathit{cs}}}}}}}}}}
\end{align*}

A  implementation of the Quantum Fourier Transform circuit family. The usual syntactic sugar is employed.

The  implementation of the QFT algorithm is given in Figure <ref>. As we walk through the various parts of the program, be aware that we will focus on the resource aspects of the algorithm, ignoring much of its actual meaning. Starting bottom-up, we assume that we have an encoding of naturals in the language and that we can perform arithmetic on them. We also assume some primitive gates and gate families: $\mathsf{H}$ is the boxed circuit corresponding to the Hadamard gate and has type $\circt{1}{\qubitt}{\qubitt}$, whereas the $\mathsf{makeRGate}$ function has type $\arrowt{\natt}{\circt{2}{\tensor{\qubitt}{\qubitt}}{\tensor{\qubitt}{\qubitt}}}{0}{0}$ and produces instances of the parametric controlled $R_n$ gate.

\begin{align*}
\mathit{qlen} &\triangleq \abs{\mathit{ql}}{\listt{\ivarOne}{\qubitt}}{\\&
\letin{\varOne}{\app{(\fold{\ivarTwo}{\mathit{qlenStep}}{\tuple{0}{\nil}})}{\mathit{ql}}}{\\&
\dest{n}{\mathit{revQl}}{\varOne}{\\&
\letin{\mathit{preQl}}{\app{\mathit{rev}}{\mathit{revQl}}}{\\&
\return{\tuple{n}{\mathit{preQl}}}}}}}
\\
\mathit{qlenStep} &\triangleq \lift{(\return{\abs{\varOne}{\tensor{(\tensor{\natt}{\listt{\ivarOne}{\qubitt}})}{\qubitt}}{\\&
\dest{\mathit{acc}}{q}{\varOne}{\\&
\dest{n}{\mathit{revQl}}{\mathit{acc}}{\\&
\return{\tuple{n+1}{\cons{q}{\mathit{revQl}}}}}}}})}
\\\\
\mathit{rev} &\triangleq \fold{\ivarOne}{\mathit{revStep}}{\nil}
\\
\mathit{revStep} &\triangleq \lift{(\return{\abs{\varOne}{\tensor{\listt{\ivarOne}{\qubitt}}{\qubitt}}{\\&
\dest{\mathit{revQl}}{q}{\varOne}{\return({\cons{q}{\mathit{revQl}})}}}})}
\end{align*}

The implementation of the auxiliary functions qlen and rev.

On the other hand, $\mathit{qlen}$ and $\mathit{rev}$ stand for regular language terms which implement respectively the linear list length and reverse functions. Their implementation is given in Figure <ref> and they have types $\mathit{qlen}::\arrowt{\listt{\ivarOne}{\qubitt}}{(\tensor{\natt}{\listt{\ivarOne}{\qubitt}})}{\ivarOne}{0}$ and $\mathit{rev}::\arrowt{\listt{\ivarOne}{\qubitt}}{\listt{\ivarOne}{\qubitt}}{\ivarOne}{0}$ in our type system.
We now turn our attention to the actual QFT algorithm. Function $\mathit{qftStep}$ builds a single step of the QFT circuit. The width of the circuit produced at step $\ivarTwo$ is dominated by the folding of the $\app{\mathit{rotate}}{n}$ function, which applies controlled rotations between appropriate pairs of qubits and has type

\begin{equation}
\end{equation}

meaning that $\app{\mathit{rotate}}{n}$ rearranges the structure of its inputs, but overall does not introduce any new wire. We fold this function starting from an accumulator $\tuple{q}{\nil}$, meaning that we can give $\fold{\ivarTwo}{(\lift{(\app{\mathit{rotate}}{n}}))}{\tuple{q}{\nil}}$ type as follows:

\begin{equation}
\inference[\textit{fold}]
\\
\vjudgment{\ivarOne,\ivarTwo}{q:\qubitts}{\emptycontext}{\tuple{q}{\nil}}{\tensor{\qubitts}{\listt{0}{\qubitts}}}
\wfjudgment{\ivarOne,\ivarTwo}{\ivarTwo}
\wfjudgment{\ivarOne,\ivarTwo}{\qubitts}
\end{equation}

where $\qubitts$ is shorthand for $\qubitt$ and where we implicitly use the fact that $\eqjudgment{\ivarOne,\ivarTwo}{\imax{1}{\imaximum{\ivarThree}{\ivarTwo}{\iplus{\iplus{\ivarThree}{2}}{\imult{(\iminus{\iminus{\ivarTwo}{1}}{\ivarThree})}{1}}}}}{\iplus{\ivarTwo}{1}}$ to simplify the arrow's width annotation using vsub and the arrow subtyping rule. Next, we fold over $\mathit{revQs}$, which has the same elements as $\mathit{qs}$ and thus has length $\ivarTwo$, and we obtain that the fold produces a circuit whose width is bounded by $\iplus{\ivarTwo}{1}$. Therefore, $\mathit{qftStep}$ has type

\begin{equation}
\bang{(\arrowt{\tensor{(\listt{\ivarTwo}{\qubitt}}{\qubitt})}{\listt{\iplus{\ivarTwo}{1}}{\qubitt}}{\iplus{\ivarTwo}{1}}{0})},
\end{equation}

which entails that when we pass it as an argument to the topmost $\foldoperator$ together with $\nil$ we can conclude that the type of the $\mathit{qft}$ function is

\begin{equation}
\inference[\textit{fold}]
\vjudgment{\ivarOne,\ivarTwo}{\emptycontext}{\emptycontext}{\mathit{qftStep}}{\bang{(\arrowt{\tensor{(\listt{\ivarTwo}{\qubitt}}{\qubitt})}{\listt{\iplus{\ivarTwo}{1}}{\qubitt}}{\iplus{\ivarTwo}{1}}{0})}}
\\
\vjudgment{\ivarOne}{\emptycontext}{\emptycontext}{\nil}{\listt{0}{\qubitt}}
\wfjudgment{\ivarOne}{\ivarOne}
\wfjudgment{\ivarOne}{\qubitt}
\end{equation}

where we once again implicitly simplify the arrow type using the fact that $\eqjudgment{\ivarOne}{\imax{0}{\imaximum{\ivarTwo}{\ivarOne}{\iplus{\iplus{\ivarTwo}{1}}{\imult{(\iminus{\iminus{\ivarOne}{1}}{\ivarTwo})}{1}}}}}{\ivarOne}$. This concludes our analysis and the resulting type tells us that $\mathit{qft}$ produces a circuit of width at most $\ivarOne$ on inputs of size $\ivarOne$, without overall using any additional wires. If we instantiate $\ivarOne$ to $3$, for example, we can apply $\mathit{qft}$ to a list of $3$ qubits to obtain the circuit shown in Figure <ref>, whose width is exactly $3$.

.98[column sep=1em, row sep=1em]

$q_3$              R_3     R_2     H     $q_3$

$q_2$        R_2     H        -1        $q_2$

$q_1$     H     -1        -2           $q_1$

The circuit of input size $3$ produced by $\app{\mathit{qft}}{(\cons{q_1}{\cons{q_2}{\cons{q_3}{\nil}}})}$.

To conclude this section, note that for ease of exposition $\mathit{qft}$ actually produces the reversed QFT circuit. This is not a problem, since the two circuits are equivalent resource-wise and the actual QFT circuit can be recovered by boxing the result of $\mathit{qft}$ and reversing it via a primitive operator. Besides, note that 's internal implementation of the QFT is also reversed [17].

§ RELATED WORK

The metatheory of quantum circuit description languages, and in
particular of -style languages, has been the subject of quite some
work in recent years, starting with Ross's thesis on  [48] and going forward with Selinger and Rios's  [46]. In the last five years, some proposals have also appeared for more expressive type systems or for language extensions that can handle non-standard language features, such as the so-called dynamic lifting [36, 22, 9], available in the  language, or dependent types [23]. Although some embryonic contributions in the direction of analyzing the size of circuits produced using  have been given [56], no contribution tackles the problem of deriving resource bounds parametric on the size of the input. In this, the ability to have types which depend on the input, certainly a feature of  [23], is not useful for the analysis of intensional attributes of the underlying circuit, simply because such attributes are not visible in types.

If we broaden the horizon to quantum programming languages other than ,
we come across, for example, the recent works of Avanzini et al. [5] and Liu et al. [37] on adapting the classic weakest precondition technique to the cost analysis of quantum programs, which however focus on programs in an imperative language. The work of Dal Lago et al. [14] on a quantum language which characterizes complexity classes for quantum polynomial time should certainly be remembered: even though the language allows the use of higher-order functions, the manipulation of quantum data occurs directly and not through circuits. Similar considerations hold for the recent work of Hainry et al. [30] and Yamakami's algebra of functions [59] in the style of Bellantoni and Cook [6], both characterizing quantum polynomial time.

If we broaden our scope further and become interested in the analysis of the
cost of classical or probabilistic programs, we face a
vast literature, with contributions employing a variety of techniques on heterogeneous languages and calculi: from functional programs [2, 34, 33] and term
rewriting systems [3, 4, 42] to probabilistic [35] and object-oriented programs [29, 20].
In this context, the resource under analysis is often assumed to be computation
time, which is relatively easy to analyze given its strictly monotonic nature. Circuit width, although monotonically non-decreasing, evolves in a way that depends on a non-monotonic quantity, i.e. the number of wires discarded by a circuit. As a result, width has the flavor of space and its analysis is less straightforward.

It is also worth mentioning that linear dependent types can be seen as a specialized version of refinement types [19], which have been used extensively in the literature to automatically verify interesting properties of programs [60, 38]. In particular, the work of Vazou et al. on  [58, 57] has been of particular inspiration, on account of  being embedded precisely in . The liquid type system [47] of  relies on SMT solvers to discharge proof obligations and has been used fruitfully to reason about both the correctness and the resource consumption (mainly time complexity) of concrete, practical programs [31].

§ GENERALIZATION TO OTHER RESOURCE TYPES

This work focuses on estimating the width of the circuits produced by  programs. This choice is dictated by the fact that the width of a circuit corresponds to the maximum number of distinct wires, and therefore individual qubits, required to execute it. Nowadays, this is considered as one of the most precious resources in quantum computing, and as such must be kept under control. However, this does not mean that our system could not be adapted to the estimation of other parameters. This section outlines how this may be possible.

First, estimating strictly monotonic resources, such as the
total number of gates in a circuit, is possible and in fact simpler
than estimating width. A single index
term $\indexOne$ that measures the number of gates in the circuit built by a computation would be enough to carry out this analysis. This index would be appropriately increased any time an $\applyoperator$ instruction is executed, while sequencing two terms via $\letoperator$ would simply add together the respective indices.

If the parameter of interest were instead the depth of the circuit, then the approach would have to be slightly different. Although in principle it would be possible to still rely on a single index $\indexOne$, this would give rise to a very coarse approximation, effectively collapsing the analysis of depth to a gate count analysis. A more precise approximation could instead be obtained by keeping track of depth locally rather than globally. More specifically, it would be sufficient to decorate each occurrence of a wire type $\wtypeOne$ with an index term $\indexOne$ so that if a label $\labOne$ were typed with $\wtypeOne^\indexOne$, it would mean that the sub-circuit rooted in $\labOne$ has a depth at most equal to $\indexOne$.

Finally, it should be mentioned that the resources considered, i.e. the depth, width, and gate count of a circuit, can be further refined so as to
take into account only some kinds of wires and gates. For instance, one could want to keep track of the maximum number of qubits needed, ignoring the number of classical bits, or at least distinguishing the two parameters, which of course have distinct levels of criticality in current quantum hardware.

§ CONCLUSION AND FUTURE WORK

In this paper we introduced a linear dependent type system based on index refinements and effect typing for the paradigmatic calculus , with the purpose of using it to derive upper bounds on the width of the circuits produced by programs. We proved not only the classic type safety properties, but also that the upper bounds derived via the system are correct. We also showed how our system can verify a realistic quantum algorithm and elaborated on some ideas on how our technique could be adapted to other crucial resources types, like gate count and circuit depth.
Ours is the first type system designed specifically for the purpose of resource analysis to target circuit description languages such as . Technically, the main novelties are the smooth combination of effect typing and index refinements, but also the proof of correctness, in which reducibility and effects are shown to play well together.

Among topics for further work, we can identify three main research directions. First and foremost, it would be valuable to investigate the ideas presented in this paper from a more practical perspective, that is, to provide a prototype implementation of the language and, more importantly, of the type-checking procedure. This would require understanding the role that SMT solvers may play in discharging the semantic judgments which we use pervasively in our approach.

Staying instead on the theoretical side of things, on the one hand we have the prospect of denotational semantics: most incarnations of  are endowed with categorical semantics that model both circuits and the terms of the language that build them [46, 36, 23, 22]. We already mentioned how the intensional nature of the quantity under analysis renders the formulation of an abstract categorical semantics for  and its circuits a nontrivial task, but we believe that one such semantics would help  fit better in the  landscape.

On the other hand, in Section <ref> we briefly discussed how our system could be modified to handle the analysis of different resource types. It would be interesting to test this path and to investigate the possibility of actually generalizing our resource analysis, that is, of making it parametric on the kind of resource being analyzed. This would allow for the same program in the same language to be amenable to different forms of verification, in a very flexible fashion.

[1]
Thorsten Altenkirch and Jonathan Grattage.
A functional quantum programming language.
In Proc. of LICS '05, 2005.

[2]
Martin Avanzini, Ugo Dal Lago, and Georg Moser.
Analysing the complexity of functional programs: Higher-order meets
In Proc. of ICFP 2015, 2015.

[3]
Martin Avanzini and Georg Moser.
Complexity analysis by rewriting.
In Proc. of FLOPS 2008, 2008.

[4]
Martin Avanzini and Georg Moser.
Tyrolean Complexity Tool: Features and Usage.
In Proc. of RTA 2013, volume 21, 2013.

[5]
Martin Avanzini, Georg Moser, Romain Pechoux, Simon Perdrix, and Vladimir
Quantum expectation transformers for cost analysis.
In Proc. of LICS '22, 2022.

[6]
Stephen Bellantoni and Stephen Cook.
A new recursion-theoretic characterization of the polytime functions
(extended abstract).
In STOC '92, 1992.

[7]
Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh.
Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications.
IOS Press, 2021.

[8]
R. Cleve, A. Ekert, C. Macchiavello, and M. Mosca.
Quantum algorithms revisited.
Proc. Math. Phys. Eng. Sci. P ROY SOC A-MATH PHY, 454(1969),

[9]
Andrea Colledan and Ugo Dal Lago.
On Dynamic Lifting and Effect Typing in Circuit Description
In TYPES 2022, volume 269, 2023.

[10]
Hugh Collins and Chris Nay.
Ibm unveils 400 qubit-plus quantum processor and next-generation ibm
quantum system two, 2022.
retrieved on Oct. 15, 2023.

[11]
Emily Conover.
Light-based quantum computer jiuzhang achieves quantum supremacy,
retrieved on Oct. 15, 2023.

[12]
D. Coppersmith.
An approximate fourier transform useful in quantum factoring, ibm
research report rc19642, 2002.

[13]
Ugo Dal Lago and Marco Gaboardi.
Linear dependent types and relative completeness.
In Proc. of LICS '11, 2011.

[14]
Ugo Dal Lago, Andrea Masini, and Margherita Zorzi.
Quantum implicit computational complexity.
TCS, 411(2), 2010.

[15]
Ugo Dal lago and Barbara Petit.
Linear dependent types in a call-by-value scenario.
In Proc. of PPDP '12, 2012.

[16]
Ugo Dal lago and Barbara Petit.
The geometry of types.
In Proc. of POPL '13, 2013.

[17]
Richard Eisenberg, Alexander Green, Peter Lumsdaine, Keith Kim, Siun-Chuon Mau,
Baranidharan Mohan, Won Ng, Joel Ravelomanantsoa-Ratsimihah, Neil Ross, Artur
Scherer, Peter Selinger, Benoît Valiron, Alexandr Virodov, and Stephan
Retrieved on Oct. 15, 2023.

[18]
Mark Fingerhuth, Tomáš Babej, and Peter Wittek.
Open source software in quantum computing.
PLOS ONE, 13(12), 2018.

[19]
Tim Freeman and Frank Pfenning.
Refinement types for ml.
In Proc. of PLDI '91, 1991.

[20]
Florian Frohn and Jürgen Giesl.
Complexity analysis for java with aprove.
In Proc. of IFM 2017, 2017.

[21]
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, 2020.

[22]
Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger.
Proto-quipper with dynamic lifting.
In Proc. of POPL '23, 2023.

[23]
Peng Fu, Kohei Kishida, and Peter Selinger.
Linear dependent type theory for quantum programming languages:
Extended abstract.
In Proc. of LICS '20, 2020.

[24]
Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C.
Linear dependent types for differential privacy.
In Proc. of POPL '13, 2013.

[25]
Simon J. Gay.
Quantum programming languages: Survey and bibliography.
Math. Struct. Comput. Sci., 16(4), 2006.

[26]
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, 2013.

[27]
Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and
Benoît Valiron.
In Proc. of PLDI, 2013.

[28]
L. K. Grover.
A fast quantum mechanical algorithm for database search.
In Proc. of STOC, 1996.

[29]
Emmanuel Hainry and Romain Péchoux.
Type-based heap and stack space analysis in Java, 2013.
Technical report.

[30]
Emmanuel Hainry, Romain Péchoux, and Mário Silva.
A programming language characterizing quantum polynomial time.
In Proc. of FoSSaCS 2023, 2023.

[31]
Martin Handley, Niki Vazou, and Graham Hutton.
Liquidate your assets: reasoning about resource usage in liquid
PACMPL, 4, 2019.

[32]
Aram W. Harrow, Avinatan Hassidim, and Seth Lloyd.
Quantum algorithm for linear systems of equations.
Phys. Rev. Lett., 103, 2009.

[33]
Jan Hoffmann, Klaus Aehlig, and Martin Hofmann.
Resource aware ml.
In Computer Aided Verification, 2012.

[34]
Jan Hoffmann and Martin Hofmann.
Amortized resource analysis with polynomial potential.
In Programming Languages and Systems, 2010.

[35]
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico
Weakest precondition reasoning for expected run–times of
probabilistic programs.
In Programming Languages and Systems, Berlin, Heidelberg, 2016.

[36]
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, 2021.

[37]
Junyi Liu, Li Zhou, Gilles Barthe, and Mingsheng Ying.
Quantum weakest preconditions for reasoning about expected runtimes
of quantum programs.
In Proc. of LICS '22, 2022.

[38]
Yitzhak Mandelbaum, David Walker, and Robert Harper.
An effective theory of type refinements.
In Proc. of ICFP '03, 2003.

[39]
John Martinis.
Quantum supremacy using a programmable superconducting processor,
Retrieved on Oct. 15, 2023.

[40]
Michael A. Nielsen and Isaac L. Chuang.
Quantum Computation and Quantum Information: 10th Anniversary
Cambridge University Press, 2010.

[41]
Flemming Nielson and Hanne Riis Nielson.
Type and effect systems.
In Correct System Design: Recent Insights and Advances. 1999.

[42]
Lars Noschinski, Fabian Emmes, and Jürgen Giesl.
Analyzing innermost runtime complexity of term rewriting by
dependency pairs.
Journal of Automated Reasoning, 51(1), 2013.

[43]
Jens Palsberg.
Toward a universal quantum programming language.
XRDS: Crossroads, 26(1), 2019.

[44]
Jennifer Paykin, Robert Rand, and Steve Zdancewic.
Qwire: A core language for quantum circuits.
In Proc. of POPL '17, 2017.

[45]
John Preskill.
Quantum computing and the entanglement frontier, 2012.

[46]
Francisco Rios and Peter Selinger.
A categorical model for a quantum circuit description language.
In Proc. of QPL '17, 2017.

[47]
Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala.
Liquid types.
In Proc. of PLDI '08, 2008.

[48]
Neil Ross.
Algebraic and Logical Methods in Quantum Computation.
PhD thesis, 2015.

[49]
J. W. Sanders and P. Zuliani.
Quantum programming.
In Proc. of MPC 2000, 2000.

[50]
Maximilian Schlosshauer.
Decoherence and the Quantum-To-Classical Transition.
Springer Berlin Heidelberg, 2007.

[51]
Peter Selinger.
A brief survey of quantum programming languages.
In Proc. of FLOPS 2004, 2004.

[52]
Peter Selinger.
Towards a quantum programming language.
Math. Struct. Comput. Sci., 14(4), 2004.

[53]
Peter Selinger and Benoît Valiron.
A lambda calculus for quantum computation with classical control.
In Proc. of TLCA, 2005.

[54]
P.W. Shor.
Algorithms for quantum computation: discrete logarithms and
In Proc. of FOCS '94, 1994.

[55]
Lau Skorstengaard.
An introduction to logical relations, 2019.

[56]
Benoit Valiron.
Automated, parametric gate count of quantum programs, 2016.
Retrieved on Oct. 15 2023.

[57]
Niki Vazou, Eric L. Seidel, and Ranjit Jhala.
Liquidhaskell: Experience with refinement types in the real world.
In Proc. of Haskell '14, 2014.

[58]
Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon
Refinement types for Haskell.
In Proc. of ICFP '14, 2014.

[59]
Tomoyuki Yamakami.
A schematic definition of quantum polynomial time computability.
The Journal of Symbolic Logic, 85(4), 2020.

[60]
Ezgi Çiçek, Deepak Garg, and Umut Acar.
Refinement Types for Incremental Computational Complexity.
In Programming Languages and Systems, volume 9032. 2015.

[61]
Bernhard Ömer.
Classical concepts in quantum programming.
Int. J. Theor. Phys., 44(7), 2005.