Linear Dependent Type Theory for Quantum
Programming Languages
Extended Abstract
Peng Fu

Kohei KishidaPeter Selinger

Dalhousie University
CanadaUniversity of Illinois at
Urbana-Champaign
U.S.A.

Dalhousie University
CanadaAbstract

1

Introduction

Modern quantum programming languages integrate quantum resources and classical control. They must, on the one
hand, be linearly typed to reflect the no-cloning propertyof quantum resources. On the other hand, high-level andpractical languages should also support quantum circuits
as first-class citizens, as well as families of circuits that areindexed by some classical parameters. Quantum programming languages thus need linear dependent type theory. This
paper defines a general semantic structure for such a typetheory via certain fibrations of monoidal categories. The
categorical model of the quantum circuit description language Proto-Quipper-M in [28] constitutes an example ofsuch a fibration, which means that the language can readily
be integrated with dependent types. We then devise botha general linear dependent type system and a dependently
typed extension of Proto-Quipper-M, and provide them with
operational semantics as well as a prototype implementation.

1.1

Quantum programming and linear types

CCS Concepts: • Software and its engineering → Semantics.
Keywords: Quantum programming languages, linear dependent types, categorical model, fibration
ACM Reference Format:
Peng Fu, Kohei Kishida, and Peter Selinger. 2020. Linear Dependent
Type Theory for Quantum Programming Languages: Extended
Abstract. In Proceedings of the 35th Annual ACM/IEEE Symposiumon Logic in Computer Science (LICS ’20), July 8–11, 2020, Saarbrücken,
Germany. ACM, New York, NY, USA, 14 pages. https://doi.org/10.
1145/3373718.3394765
Permission to make digital or hard copies of all or part of this work forpersonal or classroom use is granted without fee provided that copies
are not made or distributed for profit or commercial advantage and that
copies bear this notice and the full citation on the first page. Copyrights
for components of this work owned by others than the author(s) must
be honored. Abstracting with credit is permitted. To copy otherwise, or
republish, to post on servers or to redistribute to lists, requires prior specificpermission and/or a fee. Request permissions from permissions@acm.org.
LICS ’20, July 8–11, 2020, Saarbrücken, Germany© 2020 Copyright held by the owner/author(s). Publication rights licensed
to ACM.
ACM ISBN 978-1-4503-7104-9/20/07. . . $15.00
https://doi.org/10.1145/3373718.3394765

Quipper [12, 13] is a functional programming language fordescribing and generating quantum circuits. In addition toproviding a low-level paradigm for generating circuits, wherecircuits are constructed by applying one gate at a time, italso provides a high-level paradigm, where circuits are firstclass citizens to which meta-operations can be applied. Thiswas found to provide an appropriate level of abstraction forformalizing many quantum algorithms in a way that is close
to how they are informally described in the literature [33].
Quipper is implemented as an embedded language within
Haskell and lacks formal foundations. This is why a familyof languages known as Proto-Quipper [28, 29] has been developed as a formalization of suitable fragments of Quipper,
susceptible to formal methods.
One aspect of the formal foundations missing in Quipper
is linear types. The “no-cloning” property of quantum mechanics means that quantum resources are linear in the sensethat one cannot duplicate a quantum state [22]. This is why
linear types [10, 34] have been adopted to provide a typetheory for quantum computing [31]. Since Haskell currently
lacks linear types, Quipper leaves the programmer with the
responsibility to keep track of the use of non-duplicablequantum resources. Proto-Quipper solves this problem bygiving a syntactically sound linear type system, so that any
duplication of a quantum state will be detected as a typing
error at compile time.
Since Quipper is a circuit description language, it sharescertain aspects of hardware description languages, such as a
distinction between circuit generation time and circuit runtime. Values that are known at circuit generation time arecalled parameters and values that are known at circuit runtime are called states. The parameter/state distinction ties inwith linearity, because although states can be linear (such as
qubits) or nonlinear (such as classical bits used in circuits),
parameters are always classical and therefore never linear.
One of Quipper’s design choices [33] is that parameters andstates share the same name space; in fact, they can occur
together in a single data structure, such as a pair of an integer
and a qubit, or a list of qubits (in which case the length of

LICS ’20, July 8–11, 2020, Saarbrücken, Germany

the list is a parameter and the actual qubits in the list arestates).
Among the languages of the Proto-Quipper family, ProtoQuipper-M [28] has several desirable features. Its linear typesystem accommodates nontrivial interactions of parametersand states. It supports higher-order functions and quantum
data types such as lists of qubits. And, most significantly
for our purposes, it has a denotational semantics in termsof a categorical model, called M, that takes advantage of alinear-nonlinear adjunction in the sense of Benton [4].
1.2

Quantum programming and dependent types

The existing versions of Proto-Quipper do not support dependent types [18].
Dependent types are good at expressing program invariants and constraints at the level of types [23]. In the context
of quantum circuit programming, dependent types give theprogrammer access to dependent quantum data types. For
example, when one considers a linear function such as thequantum Fourier transform, it is really a family of circuits,rather than a single circuit, indexed by the length of thevector of qubits that the function takes as input. Anotherimportant application of dependent types in quantum circuit
programming is the use of existential dependent quantum
data types to hide garbage qubits [7, 21], while guaranteeingthat they will be uncomputed. This facilitates the programming of large scale reversible circuits. It is therefore desirable
to equip Proto-Quipper with dependent types.
The problem of how to formally add dependent types to aquantum programming language is not restricted to ProtoQuipper. The quantum circuit description language QWire[24] also uses a linear type system and has a denotationalsemantics (based on density matrices). It was recently embedded in the proof assistant Coq [27], making it possible toformally verify some simple quantum programs. QWire does
not support quantum data types, much less dependent ones.
Paykin et al. [24, Section 6.2] briefly discuss dependent types
in the context of QWire but neither a semantic model nor adetailed analysis is given. The problem of defining a denotational semantics that can accommodate linear and dependent
types for quantum circuit programming has remained open
until now.
1.3

Linear dependent types

Designing a linear dependent type system is a challenge.
One of the major hurdles is to understand what it means
for a type to depend on a linear resource, and to provide asemantics for that kind of dependency. Indeed, suppose thata function 𝑓 has a linear dependent type (𝑥 : 𝐴) ⊸ 𝐵 [𝑥]and that we are given a linear resource 𝑎 : 𝐴. How should
we understand 𝑓 𝑎 : 𝐵 [𝑎] (note that this seems to use 𝑎 twice,once in a term and once in a type)?

Peng Fu, Kohei Kishida, and Peter Selinger

Several approaches to linear dependent types have been
proposed. Cervesato and Pfenning [6] extended the intuitionistic logical framework LF with linear types of the form𝐴 ⊸ 𝐵. Their system separates a context into a linear
part and an intuitionistic part: On the one hand, to form
ˆ .𝑀 : 𝐴 ⊸ 𝐵, the context 𝑥 :̂ 𝐴 musta lambda term 𝜆𝑥
be a linear one. On the other hand, to form a lambda term
𝜆𝑥 .𝑀 : (𝑥 : 𝐴) → 𝐵 [𝑥] of a dependent type, the context
𝑥 : 𝐴 must be an intuitionistic one. When applying the linear
ˆ .𝑀 to another term, one combines two linear
lambda term 𝜆𝑥contexts as usual. On the other hand, when applying the intuitionistic lambda term 𝜆𝑥 .𝑀 to another term 𝑁 , one has tomake sure that 𝑁 does not contain any linear variables. Notethat in this system, linear function types and dependent function types are completely separate; effectively this meansthat parameters and states live in different name spaces. A
similar approach is taken by Krishnaswami et al. [17], who
proposed a type system extending Benton’s logic LNL [4],Vakar [32], who extended Barber’s dual intuitionistic linear
logic [2] with dependent types, and Gaboardi et al. [9], who
combined lightweight indexed types with bounded linear
types [11].
From a unifying perspective, McBride [19] proposed theuse of indices 0, 1, 𝜔 to decorate the context. The indices0, 1, and 𝜔 mean that the variable they decorate is, respectively, never used, used exactly once, and used more thanonce. He then introduced linear dependent types of the form(𝑥 :𝑘 𝐴) ⊸ 𝐵 [𝑥], which correspond to the irrelevant quantification ∀(𝑥 : 𝐴).𝐵 [𝑥] à la Miquel [20] when 𝑘 = 0, to
Cervesato and Pfenning’s dependent type when 𝑘 = 𝜔, andto the linear dependent type when 𝑘 = 1. The typing judgments in McBride’s system are of the form Γ ⊢ 𝑀 :𝑘 𝐴, where
the index 𝑘 on the right of turnstile separates the set of typing
judgments into two kinds: Γ ⊢ 𝑀 :0 𝐴 for terms that occurin types and Γ ⊢ 𝑀 :1 𝐴 for terms that will be evaluatedat runtime. McBride’s understanding of 𝑓 𝑎 :1 𝐵 [𝑎] is thatthe term 𝑎 that occurs in the type 𝐵 [𝑎] has been “contemplated” (which happens at type checking time) but should
not be considered to have been “consumed” for the purposeof linearity (which can only happen at runtime).
In this paper, we propose to interpret the dependenceof 𝐵 on 𝑥 in (𝑥 : 𝐴) ⊸ 𝐵 [𝑥] as saying that 𝐵 depends
on the shape of 𝑥. Informally, if 𝑁 is a term of a quantum
data type 𝐴, for example a tree whose leaves are qubits,
then the shape of 𝑁 , denoted Sh(𝑁 ), is the same tree, but
without the leaves (or more precisely, where the data in theleaves has been replaced by data of unit type). We write
Sh(𝐴) for the type of shapes of 𝐴, so that Sh(𝑁 ) : Sh(𝐴).
With these conventions, the dependence of 𝐵 on 𝑥 in (𝑥 :𝐴) ⊸ 𝐵 [𝑥] is interpreted as 𝑥 : Sh(𝐴) ⊢ 𝐵 [𝑥] : ∗. It is
understood that, for any resource 𝑁 (linear or otherwise), its
shape Sh(𝑁 ) is duplicable. Accordingly, our typing rule forapplication has the following form (where Γ𝑖 has the formLinear Dependent Type Theory for Quantum Programming Languages

LICS ’20, July 8–11, 2020, Saarbrücken, Germany• In Section 4, we show how to extend the linear dependent type system of Section 3 to support programming
quantum circuits, giving rise to a dependently typed
version of Proto-Quipper. We discuss some practicalaspects of the implementation.

𝑥 1 :𝑘1 𝐴1, . . . , 𝑥𝑛 :𝑘𝑛 𝐴𝑛 , following McBride).
Γ1 ⊢ 𝑀 : (𝑥 : 𝐴) ⊸ 𝐵 [𝑥] Γ2 ⊢ 𝑁 : 𝐴
Γ1 + Γ2 ⊢ 𝑀𝑁 : 𝐵 [Sh(𝑁 )]So instead of separating typing contexts into linear andnonlinear parts like Cervesato and Pfenning, or of having
two kinds of typing judgments like McBride and like Atkey[1], we identify a subset of typing judgment of the form
Sh(Γ) ⊢ Sh(𝑁 ) : Sh(𝐴). This subfragment of typing accounts for the (duplicable) intuitionistic fragment that does
not change the quantum states. In this way, the notion ofshape does not only play a conceptual role in our understanding of the dependence of 𝐵 on 𝐴; it is indeed part of
the formalism of our treatment of linear dependent types.
Since the intuitionistic fragment Sh(Γ) ⊢ Sh(𝑁 ) : Sh(𝐴)is only used for typing and kinding purposes, in practiceprogrammers do not directly program with terms such as
Sh(𝑁 ).
A related concept under the name shapely types was considered by Jay and Cockett [14]. Their notion of shapely types
is defined as certain pullbacks of the list functor. Although
our notion of shape-unit functor is defined differently, it appears both notions of shapes coincide for data types such as
lists. However, our notion of shape-unit functor or the shapeoperation can also be used for mapping a state-modifying
program into a “pure” program that does not modify state.
This is beyond Jay and Cockett’s treatment of shapely types.
1.4

Contributions

In this paper, we provide a new framework of linear dependent type theory suitable for quantum circuit programming
languages. The framework comes with both operational anddenotational semantics. Indeed, the categorical structure forour denotational semantics subsumes Rios and Selinger’s
category M, showing that Proto-Quipper-M can be extended
with dependent types. Furthermore, our categorical structure,in terms of a fibration of a symmetric monoidal closed category over a locally cartesian closed category, can be viewed
as a generalization of Seely’s [30] semantics of nonlinear
dependent type theory.
• In Section 2, we define a notion of state-parameter
fibration. We then show how the state-parameter fibration naturally gives rise to concepts such as dependent
monoidal product, dependent function space, and ashape-unit functor that interprets the shapes of types
and terms.
• In Section 3, we provide typing rules and an operational semantics for a linear dependent type systemthat features the shape operation. We show that theshape operation corresponds to the shape-unit functor
on the state-parameter fibration. We interpret the typesystem using the state-parameter fibration and prove
the soundness of the interpretation.

2

Categorical structure

Since Seely [30], it has been well understood how (nonlinear)dependent type theory can be interpreted in locally cartesianclosed categories (LCCCs). To interpret a linear dependent
type theory, one might naively look for an analogous notion of “locally monoidal closed category.” However, no such
structure is readily available. Instead, to build our model, we
must take the notions of parameter and state seriously. We
believe that the correct way to do this is to consider a fibration of a symmetric monoidal closed category (representing
states) over an LCCC (representing parameters).
2.1

Pullbacks and fibrations

In modelling dependent types, pullbacks play the essential
role of interpreting substitution of terms into types and contexts. To carry this idea over to the linear setting, the perspective of fibrations proves useful.
Definition 2.1. Given a functor 𝐹 : E → B, a morphism
𝑓 : 𝐵 → 𝐴 of E is said to be cartesian if• For every 𝑔 : 𝐶 → 𝐴 in E and 𝑏 : 𝐹 (𝐶) → 𝐹 (𝐵) in B
such that 𝐹 (𝑔) = 𝐹 (𝑓 ) ◦ 𝑏, there is a unique 𝑢 : 𝐶 → 𝐵
such that 𝐹 (𝑢) = 𝑏 and 𝑓 ◦ 𝑢 = 𝑔.
𝐶
𝑔
𝑢
𝑓

𝐹 (𝐶)

𝐵

𝐴

𝑏

𝐹 (𝐵)

𝐹 (𝑓 )𝐹 (𝐴)Given an arrow 𝑎 : 𝑋 → 𝐹 (𝐴) of B, we say that 𝑓 : 𝐵 → 𝐴 is
a cartesian lifting of 𝑎 if 𝑎 = 𝐹 (𝑓 ) and 𝑓 is cartesian. We saythat 𝐹 is a Grothendieck fibration if every arrow 𝑎 : 𝑋 → 𝐹 (𝐴)has a cartesian lifting at 𝐴.
As the picture above suggests, cartesian arrows are akinto pullbacks. In fact, we have the following:
Fact 2.2. Suppose 𝐹 : E → B has a right adjoint 𝐺. Then anarrow 𝑓 of E is cartesian iff the following square is a pullback,where 𝜂 is the unit of the adjunction.
𝑓

𝐵

𝐴

𝜂𝐵

𝐺𝐹 (𝐵)𝜂𝐴
𝐺𝐹 (𝑓 )𝐺𝐹 (𝐴)

Indeed, the following subclass of fibrations can be characterized in terms of adjoints and pullbacks.

LICS ’20, July 8–11, 2020, Saarbrücken, Germany

Definition 2.3. Let us call a Grothendieck fibration ♯ : E →B a pullback fibration if(1) B has pullbacks, and(2) E has a terminal object 1 and ♯ preserves it.
Fact 2.4. Given any functor ♯ : E → B, it is a pullback
fibration iff(3) ♯ has a full and faithful right adjoint 𝑞, making B areflective subcategory of E, and moreover the counitof the adjunction is strictly the identity.
(4) B has a terminal object 1.
(5) Any arrows of E of the form 𝑞𝑓 : 𝑞𝑌 → 𝑞𝑋 andℎ : 𝐴 → 𝑞𝑋 have a pullback 𝐵, and ♯ preserves it to apullback of ♯𝑞𝑓 = 𝑓 and ♯ℎ.
𝜋2

𝐵

𝐴

𝜋1

ℎ
𝑞𝑓

𝑞𝑌

𝑞𝑋

In particular, if 𝑋 = ♯𝐴 and ℎ = 𝜂𝐴 for the unit ofadjunction 𝜂 : idE → 𝑞 ◦ ♯, then 𝑞𝑓 and ℎ have apullback 𝐵 as above with 𝑌 = ♯𝐵, 𝜋1 = 𝜂𝐵 , and 𝑓 = ♯𝜋2(hence 𝜋 2 is the cartesian lifting of 𝑓 ).
It is useful to note how a pullback fibration ♯ defines its
right adjoint 𝑞 in (3): since ♯1 is terminal in B, we set 𝑞♯1 = 1
and define 𝑞𝑋 and 𝑞𝑓 by cartesian liftings:
𝑞𝑓

𝑞𝑌

𝑞!𝑋

𝑞𝑋

𝑞♯1

Peng Fu, Kohei Kishida, and Peter Selinger(7) If arrows 𝑓 and 𝑔 of E are cartesian, so is 𝑓 ⊗ 𝑔.
Our setup also gives rise to several useful structures. One
is a “sublocal” monoidal structure:
Definition 2.6. Let ♯ : E → B be a monoidal closed pullback
fibration, and B be an LCCC, so that therefore each slice
category B/𝑋 is cartesian closed, with ×𝑋 and ⇒𝑋 . Let 𝐴, 𝐵
be objects in E/𝑞𝑋 . We then define the fibered monoidal
product 𝐴 ⊗𝑞𝑋 𝐵 and the fibered function space 𝐴 ⊸𝑞𝑋 𝐵 as
the following cartesian liftings.
𝐴 ⊗𝑞𝑋 𝐵𝐴⊗𝐵

𝐴 ⊸𝑞𝑋 𝐵𝐴⊸𝐵

𝐴 ×𝑋 𝐵

𝐴×𝐵

𝐴 ⇒𝑋 𝐵𝐴⇒𝐵

𝐴 ⊗𝑞𝑋 𝐵 and 𝐴 ⊸𝑞𝑋 𝐵 are also objects of E/𝑞𝑋 . We willassume that(8) − ⊗𝑞𝑋 𝐴 ⊣ 𝐴 ⊸𝑞𝑋 − for every object 𝑋 of B,
so that each E/𝑞𝑋 is monoidal closed. We call E “sublocally” monoidal closed: while E/𝐴 is not monoidal closed forevery object 𝐴, it is if 𝐴 is in the subcategory B.
Another structure is a functor that gives parameter-indexed families of monoidal units:
Definition 2.7. Given a monoidal closed pullback fibration♯ : E → B, we define a functor 𝑝 : B → E by setting 𝑝1 = 𝐼
and taking cartesian liftings of the entire B, or equivalently,
pulling back !𝑝1 = 𝜂𝐼 : 𝐼 → 𝐼 .
𝑝𝑓

𝑝𝑌
𝑋

𝑝𝑌

𝑝!𝑋

𝑝𝑋

𝑝1
!𝑝1 =𝜂𝐼

♯1.
!𝑋

𝑓

Notation 2.5. By abuse of notation, we may write 𝑋 for 𝑞𝑋(since 𝑞 is a full embedding), and 𝐴 for both ♯𝐴 and 𝑞♯𝐴.
We use the total category E of such a fibration ♯ as a category of quantum structures. It may not have all pullbacks, but
the ones given by ♯ are enough for interpreting dependent
types.
2.2

𝑝1

!𝑋

𝑓

𝑌

𝑝𝑓

𝑝!𝑋

𝑝𝑋

State-parameter fibration

Our semantics takes a pullback fibration ♯ of a symmetricmonoidal closed category E of quantum (and other) state
spaces over a locally cartesian closed subcategory B of parameter spaces. A state space 𝐴 of E then sits over a parameter space ♯𝐴 via 𝜂𝐴 : 𝐴 → 𝑞♯𝐴. With this we express aparameter-indexed family of quantum states—formally by
assuming:(6) ♯ is a monoidal closed functor.
This means that ♯ preserves the monoidal closed structure,i.e., it maps ⊗, ⊸, 𝐼 in E to ×, ⇒, 1 in B.
In this setup, cartesian arrows are understood as simply
reindexing parameters, without any effect on quantum states.
This understanding implies that

𝑌

𝑋

𝑞𝑓

1

𝑞𝑌

𝑞!𝑋

𝑞𝑋

𝑞1

It follows that ♯ ◦ 𝑝 = idB . We see 𝑝𝑋 as a family of themonoidal unit 𝐼 indexed by parameters in 𝑋 ; it is indeed themonoidal unit of E/𝑞𝑋 . (One may also note that 𝑝𝑋 = 𝐼 ×𝑞𝑋 .)We may therefore refer to each 𝑝𝑋 as an “𝑋 -parameterized
unit.” We will assume that(9) 𝑝 has a right adjoint ♭,which is enough to make 𝑝 ⊣ ♭ a linear-nonlinear adjunction as defined by Benton [4]. We then write ! for thecomonad 𝑝 ◦ ♭ and force : ! → idE for the counit.
Putting everything together, we arrive at the following
definition.
Definition 2.8. We say that a pullback fibration ♯ : E →B over an LCCC B (see (1)–(5)) is a linear-state-nonlinearparameter fibration, or state-parameter fibration for short,
if (6)–(9) hold. We call the associated 𝑞, 𝑝 : B → E theparameterized-terminal and parameterized-unit functors, respectively, of ♯.
Fact 2.9. Given any state-parameter fibration ♯, its parameterized-unit functor 𝑝 is strong monoidal, i.e., 𝑝 (𝑋 × 𝑌 ) Linear Dependent Type Theory for Quantum Programming Languages

LICS ’20, July 8–11, 2020, Saarbrücken, Germany𝑝𝑋 ⊗ 𝑝𝑌 and 𝑝1  𝐼 , and 𝑝 ⊣ ♭ is a linear-nonlinear adjunction.

Fact 2.11. The functor ♯ : M → Set is a state-parameter
fibration.

Proof. 𝑝1  𝐼 by definition. To show 𝑝 (𝑋 × 𝑌 )  𝑝𝑋 ⊗ 𝑝𝑌 ,note that 𝑝!𝑋 : 𝑝𝑋 → 𝑝1  𝐼 and 𝑝!𝑌 are cartesian; hence
𝑝!𝑋 ⊗ 𝑝!𝑌 : 𝑝𝑋 ⊗ 𝑝𝑌 → 𝑝1 ⊗ 𝑝1  𝑝1 is also cartesianby (7), while 𝑝𝑋 ⊗ 𝑝𝑌  𝑋 × 𝑌 . Thus 𝑝𝑋 ⊗ 𝑝𝑌 = 𝑝 (𝑋 ×
𝑌 ) by Definition 2.7. Then, by [16, Theorem 1.5], strong
monoidal 𝑝 makes ♭ monoidal and 𝑝 ⊣ ♭ a linear-nonlinear
adjunction.
□

The remainder of this section and Section 3 explore how
state-parameter fibrations can model linear dependent types.
Fact 2.11 then means that Proto-Quipper-M can be extended
with dependent types, as we will see in Section 4.

2.3

Example: M over Set

Rios and Selinger’s [28] categorical model of Proto-QuipperM naturally gives rise to a state-parameter fibration. This
concrete example may help the reader see how our idea ofstates and parameters works conceptually.
The definition of the model first fixes a symmetric monoidal category M of “generalized circuits” (which could be, forexample, a category of quantum circuits), and fully embeds
it into some symmetric monoidal closed category M withproducts, e.g., by taking the Yoneda embedding. Then
Definition 2.10. Let M be the free coproduct completionof M. More concretely, it is given as follows:• An object 𝐴 is a pair (𝐴, (𝐴𝑥 )𝑥 ∈𝐴 ) of a set 𝐴 and anindexed family of objects 𝐴𝑥 of the category M.
• An arrow 𝑓 : 𝐴 → 𝐵 is a pair (𝑓 , (𝑓𝑥 )𝑥 ∈𝐴 ) of a function
𝑓 : 𝐴 → 𝐵 and an indexed family of arrows 𝑓𝑥 : 𝐴𝑥 →𝐵 𝑓 (𝑥) of M.
Objects and arrows of M are families of objects and morphisms of M, indexed by parameters in sets. The obvious
functor ♯ : M → Set :: 𝐴 ↦→ 𝐴 is a Grothendieck fibration:
the cartesian lifting of a function 𝑓 : 𝑋 → 𝐴 at 𝐴 has domain (𝑋, (𝐴 𝑓 (𝑥) )𝑥 ∈𝑋 ) and consists of 𝑓 paired with a family(id𝐴 𝑓 (𝑥 ) )𝑥 ∈𝑋 of identity arrows—thus, cartesian arrows simply reindex parameters and have no effect on states. Since♯ preserves the terminal (1, 1) of M to 1 (and since Set isan LCCC), it is a pullback fibration. While ♯ has a full andfaithful right adjoint 𝑞 : Set → M :: 𝑋 ↦→ (𝑋, (1)𝑥 ∈𝑋 ),there is also 𝑝 : Set → M :: 𝑋 ↦→ (𝑋, (𝐼 )𝑥 ∈𝑋 ), which canbe obtained as in Definition 2.7. Since 𝑝 has a right adjointÍ♭ : M → Set :: 𝐴 ↦→ 𝑥 ∈𝐴 M(𝐼, 𝐴𝑥 ), property (9) holds.
The category M is symmetric monoidal closed, with 𝐼 ,⊗, ⊸ defined by indexed families of 𝐼 , ⊗, ⊸ of M withparameter sets that make ♯ monoidal closed: 𝐼 = (1, 𝐼 ),𝐴 ⊗ 𝐵 = (𝐴 × 𝐵, (𝐴𝑥 ⊗ 𝐵 𝑦 )𝑥 ∈𝐴,𝑦 ∈𝐵 ), and 𝐴 ⊸ 𝐵 = (𝐴 ⇒
Î𝐵, ( 𝑥 ∈𝐴 (𝐴𝑥 ⊸ 𝐵 𝑓 (𝑥) )) 𝑓 :𝐴→𝐵 ). This definition and the characterization of cartesian arrows above imply (7). Moreover,𝐴 ⊗𝑞𝑋 𝐵 and 𝐴 ⊸𝑞𝑋 𝐵 are defined to be subfamilies of𝐴 ⊗ 𝐵 and 𝐴 ⊸ 𝐵 (with smaller parameter sets 𝐴 ×𝑋 𝐵 and𝐴 ⇒𝑋 𝐵), which implies (8), that M/𝑞𝑋 is monoidal closed.
To sum up,

2.4

Structures for dependent types

The sublocally monoidal closed structure of a state-parameter fibration ♯ : E → B enables us to interpret dependent
types with several constructions.
First let us note that any arrow 𝜋 : 𝐴 → 𝑞𝑋 , i.e., any objectof E/𝑞𝑋 , factors as 𝜋 ◦ 𝜂𝐴 . We take this to signify that 𝐴,
intuitively an 𝐴-indexed family of state spaces, is dependent,
via 𝜋, on parameters in 𝑋 . In the same vein, any arrow of
E/𝑞𝑋 is parameterized by 𝑋 . Based on this idea, we use E/𝑞𝑋
as the category of (objects and arrows interpreting) types
and terms dependent on parameters in 𝑋 . So, schematically, acontext Γ ⊢, a dependent type Γ ⊢ 𝐴 : ∗, and a term Γ ⊢ 𝑀 : 𝐴
are interpreted respectively by Γ, 𝜋, and 𝑀 in
Γ
𝜂Γ

𝑀
𝐴
𝜋
Γ

In the LCCC interpretation of nonlinear dependent typetheory, one would use an identity arrow idΓ : Γ → Γ on
the left of the triangle. In our semantics, it is crucial to use𝜂 Γ : Γ → Γ instead—because, while 𝑀 is dependent onparameters, it may use resources contained in its domain.
That is, to generalize the LCCC interpretation to the linear
dependent case, we need to split the context object into two:a parameterized terminal Γ as the base of the slice E/Γ toexpress dependency, and a (generally) linear object Γ as thedomain of a term to embody linear resources.
One may still note that, when we apply the functor ♯ tothe above triangle, 𝜂 Γ = idΓ becomes the usual triangle fromthe nonlinear case. In other words, our semantics uses a
fibration ♯ of the linear type theory of E over the nonlinear
dependent type theory of parameters of the LCCC B.
Now, keeping in mind that 𝜋 : 𝐵 → 𝐴 means the dependency of 𝐵 on (parameters of) 𝐴, we define:
Definition 2.12. Given 𝜋 : 𝐵 → 𝐴, i.e., when 𝐵 is in E/𝐴,
we call 𝐴 ⊗𝐴 𝐵 a dependent monoidal product, and write 𝐴 ⊗ 𝐵
for it.
Dependent monoidal products will be used to interpretlinear Σ-types (𝑥 : 𝐴) ⊗ 𝐵, but they will also prove necessary
in interpreting contexts. If Γ, 𝑥 : 𝐴 ⊢ is a well-formed context,
we must have Γ ⊢ 𝐴 : ∗, and therefore an arrow 𝜋 : 𝐴 → Γ;then Γ ⊗ 𝐴 is the interpretation of Γ, 𝑥 : 𝐴 ⊢. In the nonlinear
case, an object 𝑋 would interpret the context Γ, 𝑥 : 𝑋 ⊢, but
in the linear case, we must not drop Γ from Γ ⊗ 𝐴, since theLICS ’20, July 8–11, 2020, Saarbrücken, Germany

Peng Fu, Kohei Kishida, and Peter Selinger

linear resource contained in Γ is crucial. Observe howeverthat 𝐴 ⊗ 𝐵 = 𝐴 ×𝐴 𝐵  𝐵. Thus, as far as parameters areconcerned, the context Γ, 𝑥 : 𝐴 ⊢ has a parameter space 𝐴,
agreeing with the nonlinear dependent type theory of B. One
may in addition observe that ⊗ is associative.
For linear Π-types, we introduce the following definition:
Definition 2.13. Let 𝐴 be an object in E/𝑞𝑋 and 𝐵 an object
in E/𝐴 (and hence in E/𝑞𝑋 ). We define the dependent function
space Π𝑞𝑋 ,𝐴 𝐵 in E as the following cartesian lifting, whereΠ𝑋 ,𝐴 𝐵 is the dependent function space in B/𝑋 .
Π𝑞𝑋 ,𝐴 𝐵

𝐴 ⊸𝑞𝑋 𝐵

Π𝑋 ,𝐴 𝐵𝐴 ⇒𝑋 𝐵

This can interpret linear Π-types (𝑥 : 𝐴) ⊸ 𝐵 due to thefollowing theorem, which provides a semantics for linear
dependent function abstraction and application.
Theorem 2.14. There is an adjunction− ⊗𝑞𝑋 𝐴
M/𝐴

2.5⊥
Π𝑞𝑋 ,𝐴

M/𝑞𝑋

Parameters and shapes

The linear type theory of E is fibered over the nonlinear
dependent type theory of parameters in B, so that dependent
types are dependent on parameters. This role of parameters
will be reflected in the syntax of the type theory we will propose in Section 3, which specifies special subclasses of types
and terms, namely, parameter types and parameter terms.
They refer primarily to objects and arrows in B. Nonetheless,given our objective of treating parameter types and othertypes uniformly, we need to formally interpret parametertypes and terms in E. We do this by embedding B into E in
two ways, namely, by the functors 𝑞 and 𝑝: while the imageof 𝑞 provides slices E/𝑞𝑋 and sublocally monoidal closed
structure, parameterized monoidal units 𝑝𝑋 and reindexing maps 𝑝 𝑓 interact with other objects and arrows within
the monoidal structure of E or E/𝑞𝑋 , in the way that was
explained in Section 2.4.
For this reason, we interpret the shape operation on types
and terms by ♯ but also by the two endofunctors 𝑞 ◦ ♯ and𝑝 ◦ ♯ on E, which we dub the shape-terminal functor andshape-unit functor, respectively. While 𝑞 ◦ ♯ is a monad (of♯ ⊣ 𝑞), 𝑝 ◦ ♯ is not, but one may note that 𝑝 ◦ ♯ ⊣ 𝑞 ◦ ♭.
The following equalities regarding 𝑝 ◦ ♯ will be useful ininterpreting shapes in Section 3.
Fact 2.15. The shape-unit functor 𝑝◦♯ satisfies the following
for any 𝑋 in B and any 𝐴, 𝐵 in E:• 𝑝 (𝑝𝑋 ) = 𝑝𝑋 .
• 𝑝𝑆 = 𝐼 for any 𝑆 in E such that 𝑆 = 1.

• 𝑝 (𝐴 ⊗ 𝐵) = 𝑝𝐴 ⊗ 𝑝𝐵.
• 𝑝 (𝐴 ⊗𝑞𝑋 𝐵) = 𝑝𝐴 ⊗𝑞𝑋 𝑝𝐵.
• 𝑝 (!𝐴) = !𝐴.
• 𝑝 (𝐴 ⊸ 𝐵) = 𝑝 (𝐴 ⇒ 𝐵).
• 𝑝 (Π𝑞𝑋 ,𝐴 𝐵) = 𝑝 (Π𝑋 ,𝐴 𝐵).
Note that 𝑝 (𝐴 ⊸ 𝐵) ≠ 𝑝𝐴 ⊸ 𝑝𝐵, since 𝑝 does not map ⇒to ⊸. Although 𝑝 (𝐴 ⊸ 𝐵) = 𝑝 (𝐴 ⇒ 𝐵) is not an exponential in E, it is (trivially) an exponential in 𝑝B, the (non-full)subcategory of images of 𝑝. Parameterized units and cartesian arrows in 𝑝B correspond to a state-free fragment of E, inwhich (nonlinear) function abstraction and application areinterpreted by the exponential structure of B (or its image
under 𝑝).

3

A linear dependent type system

We now consider a type system for the state-parameter fibration ♯ : E → B.
3.1

Syntax and typing rules

As was mentioned in Section 2.5, the syntax of our typetheory specifies subclasses of types and terms, namely, parameter types and parameter terms, in parallel to the LCCC
B being the subcategory of E with no linear resources orstate. Furthermore, our syntax allows only parameter terms
to appear in types. This restriction has the consequence thatthe evaluation of types during type checking will not change
quantum states.
Definition 3.1 (Syntax).
Types 𝐴, 𝐵 ::= 𝐶 | Unit | !𝐴 | (𝑥 : 𝐴) ⊸ 𝐵 [𝑥]| (𝑥 : 𝐴) ⊗ 𝐵 [𝑥] | (𝑥 : 𝑃1 ) → 𝑃2 [𝑥]Parameter types 𝑃 ::= Unit | !𝐴 | (𝑥 : 𝑃1 ) ⊗ 𝑃2 [𝑥]| (𝑥 : 𝑃1 ) → 𝑃 2 [𝑥]Terms 𝑀, 𝑁 , 𝐿 ::= 𝑥 | 𝜆𝑥 .𝑀 | 𝑀𝑁 | force 𝑀 | force′ 𝑅| lift 𝑀 | (𝑀, 𝑁 ) | let (𝑥, 𝑦) = 𝑁 in 𝑀 | 𝜆 ′𝑥 .𝑅 | 𝑅1 @𝑅2
Parameter terms 𝑅 ::= 𝑥 | 𝜆 ′𝑥 .𝑅 | 𝑅1 @𝑅2 | force′ 𝑅 | lift 𝑀| (𝑅1, 𝑅2 ) | let (𝑥, 𝑦) = 𝑅1 in 𝑅2
Values 𝑉 ::= 𝑥 | 𝜆𝑥 .𝑀 | 𝜆 ′𝑥 .𝑅 | lift 𝑀
Indices 𝑘 ::= 0 | 1 | 𝜔Contexts Γ ::= · | 𝑥 :𝑘 𝐴, Γ
Parameter contexts Φ ::= · | 𝑥 :𝑘 𝐴, Φ, where 𝑘 = 1 only if
𝐴 is a parameter type.
Here, 𝐶 denotes a basic type of states, e.g., qubits or bits.
We have the usual linear exponential type !𝐴, which is aparameter type and is duplicable. The term lift 𝑀 introduces
the type !𝐴, and the term force 𝑀 eliminates !𝐴 to 𝐴. In thelinear Π- and Σ-types (𝑥 : 𝐴) ⊸ 𝐵 [𝑥] and (𝑥 : 𝐴) ⊗ 𝐵 [𝑥], weallow 𝐴 to be any type. We write 𝐴 ⊸ 𝐵 and 𝐴 ⊗ 𝐵 for themin the special case in which 𝐵 does not depend on 𝑥 : 𝐴.
The linear Σ-type (𝑥 : 𝐴) ⊗ 𝐵 [𝑥] is a parameter type when
𝐴 and 𝐵 [𝑥] are. The same is not the case for the Π-type: weintroduce a separate, intuitionistic Π-type (𝑥 : 𝑃1 ) → 𝑃2 [𝑥].

Linear Dependent Type Theory for Quantum Programming Languages

This is introduced and eliminated by parameter terms 𝜆 ′𝑥 .𝑅
and 𝑅1 @𝑅2 , respectively.
The term force′ 𝑅 eliminates !𝐴 to the shape of 𝐴, i.e.,
Sh(𝐴). We interpret force′ as the shape of the counit force :! → idE of the adjunction 𝑝 ⊣ ♭.
The operations 𝜆 ′, @, and force′, as well as the corresponding type former →, are not part of the “surface language”,
i.e., they are not intended to be used directly by the user ofthe programming language. Rather, they are generated by
the type checker and only play a role in type checking andduring evaluation.
We use the indices 0, 1, 𝜔 to keep track of the use of variables in a typing context. In a well-formed context, a linear
type can only have the index 0 or 1, and not 𝜔. On the other
hand, a parameter type can have any index. Addition andmultiplication of the indices are defined to be commutative
so that 0 and 1 are the additive and multiplicative units, with𝑘 + ℓ = 𝜔 for 𝑘, ℓ ≠ 0 and with 0 · 𝑘 = 0 and 𝜔 · 𝜔 = 𝜔. It
is straightforward to extend these operations pointwise tocontexts: given two contexts Γ1 = (𝑥 1 :𝑘1 𝐴1, . . . , 𝑥𝑛 :𝑘𝑛 𝐴𝑛 )and Γ2 = (𝑥 1 :ℓ1 𝐴1, . . . , 𝑥𝑛 :ℓ𝑛 𝐴𝑛 ) with the same sequenceof types, we write Γ1 + Γ2 = (𝑥 1 :𝑘1 +ℓ1 𝐴1, . . . , 𝑥𝑛 :𝑘𝑛 +ℓ𝑛 𝐴𝑛 ),while 𝑘Γ1 = (𝑥 1 :𝑘 ·𝑘1 𝐴1, . . . , 𝑥𝑛 :𝑘 ·𝑘𝑛 𝐴𝑛 ).
Parameter contexts Φ are typing contexts in which all
linear types have the index 0. Note that parameter contexts
are just a special kind of contexts, rather than being formallydistinct from other contexts Γ.
One of the most significant pieces of machinery in ourtype system is the shape operation, which maps a term to aparameter term and a type to a parameter type. It is interpreted by the shape-unit functor 𝑝 ◦ ♯, and the type-part ofthe operation corresponds to equalities in Fact 2.15.
Definition 3.2 (Shape operation).
Sh(𝐶) = Unit
Sh(!𝐴) = !𝐴
Sh((𝑥 : 𝐴) ⊸ 𝐵 [𝑥]) = (𝑥 : Sh(𝐴)) → Sh(𝐵 [𝑥])Sh((𝑥 : 𝐴) ⊗ 𝐵 [𝑥]) = (𝑥 : Sh(𝐴)) ⊗ Sh(𝐵 [𝑥])Sh(𝑃) = 𝑃Sh(𝑥) = 𝑥Sh(𝜆𝑥 .𝑁 ) = 𝜆 ′𝑥 . Sh(𝑁 )Sh(𝑀𝑁 ) = Sh(𝑀)@ Sh(𝑁 )Sh(force 𝑀) = force′ Sh(𝑀)
Sh(lift 𝑀) = lift 𝑀
Sh(𝑀, 𝑁 ) = (Sh(𝑀), Sh(𝑁 ))Sh(let (𝑥, 𝑦) = 𝑁 in 𝑀) = let (𝑥, 𝑦) = Sh(𝑁 ) in Sh(𝑀)
Sh(𝑅) = 𝑅
Observe that the shape operation is idempotent, just likethe shape-unit functor 𝑝 ◦ ♯. Also note that the shape operation is a meta-operation on terms, like substitution, and nota term constructor. The shape operation is intended to be
applied to well-typed terms. Although we define Sh(𝑥) = 𝑥,

LICS ’20, July 8–11, 2020, Saarbrücken, Germany

the type of the variable 𝑥 is changed according to the shapeoperation (see Theorem 3.6).
Let us write Sh(Γ) to mean applying the shape operation
to all the types in Γ. So Sh(Γ) is a parameter context. We
often ignore the index information of a variable if it is of aparameter type 𝑃.
The well-formedness of the context depends on kinding.
The main purpose of a well-formed context is to make sure alinear type cannot have index 𝜔. The next three definitions
are mutually recursive, as is common in dependent typetheory.
Definition 3.3 (Well-formed context). Γ ⊢·⊢Γ ⊢ Sh(Γ) ⊢ 𝐴 : ∗ where 𝑘 = 𝜔 only if 𝐴 is aparameter typeΓ, 𝑥 :𝑘 𝐴 ⊢In the above definition, we use the shape of the context
Sh(Γ) to kind check a type.
Definition 3.4 (Selected kinding rules). Φ ⊢ 𝐴 : ∗Φ, 𝑥 : Sh(𝐴) ⊢ 𝐵 [𝑥] : ∗Φ ⊢ (𝑥 : 𝐴) ⊸ 𝐵 [𝑥] : ∗Φ, 𝑥 : Sh(𝐴) ⊢ 𝐵 [𝑥] : ∗Φ ⊢ (𝑥 : 𝐴) ⊗ 𝐵 [𝑥] : ∗Φ⊢𝐴:∗Φ ⊢ !𝐴 : ∗Φ, 𝑥 : 𝑃1 ⊢ 𝑃2 [𝑥] : ∗Φ ⊢ (𝑥 : 𝑃1 ) → 𝑃2 [𝑥] : ∗We only use parameter contexts for kinding, since only
parameter terms can appear in types. The kinding rules for(𝑥 : 𝐴) ⊗ 𝐵 [𝑥] and (𝑥 : 𝐴) ⊸ 𝐵 [𝑥] suggest that the type𝐵 only depends on the shape of 𝐴, i.e., Sh(𝐴), which is aparameter type.
Definition 3.5 (Selected typing rules). Γ ⊢ 𝑀 : 𝐴
Γ1 ⊢ 𝑀 : (𝑥 : 𝐴) ⊸ 𝐵 [𝑥] Γ2 ⊢ 𝑁 : 𝐴
Γ1 + Γ2 ⊢ 𝑀𝑁 : 𝐵 [Sh(𝑁 )]0Γ, 𝑥 :1 𝐴, 0Γ ′ ⊢0Γ, 𝑥 :1 𝐴, 0Γ ′ ⊢ 𝑥 : 𝐴

Γ, 𝑥 :𝑘 𝐴 ⊢ 𝑀 : 𝐵 [𝑥] 𝑘 ≠ 1 ⇒ 𝐴 = 𝑃Γ ⊢ 𝜆𝑥 .𝑀 : (𝑥 : 𝐴) ⊸ 𝐵 [𝑥]Φ⊢𝑀 :𝐴Φ ⊢ lift 𝑀 : !𝐴Γ1 ⊢ 𝑀 : 𝐴 Γ2 ⊢ 𝑁 : 𝐵 [Sh(𝑀)]Γ1 + Γ2 ⊢ (𝑀, 𝑁 ) : (𝑥 : 𝐴) ⊗ 𝐵 [𝑥]Γ ⊢ 𝑀 : !𝐴Γ ⊢ force 𝑀 : 𝐴

Φ, 𝑥 : 𝑃1 ⊢ 𝑅 : 𝑃 2 [𝑥]Φ ⊢ 𝜆 ′𝑥 .𝑅 : (𝑥 : 𝑃1 ) → 𝑃2 [𝑥]Φ ⊢ 𝑅 : !𝐴Φ ⊢ force ′ 𝑅 : Sh(𝐴)Φ ⊢ 𝑅1 : (𝑥 : 𝑃1 ) → 𝑃 2 [𝑥] Φ ⊢ 𝑅2 : 𝑃1
Φ ⊢ 𝑅1 @𝑅2 : 𝐵 [𝑅2 ]Remark. (i) In the typing rule for 𝑀𝑁 , the parameter term
Sh(𝑁 ) is substituted into the type, therefore the term 𝑁 only
occurs once in the term 𝑀𝑁 and its shape Sh(𝑁 ) can occur
many times in the type 𝐵 [Sh(𝑁 )].
(ii) In the typing rule for 𝜆𝑥 .𝑀, we do not allow abstracting
over a variable of linear type with index 0, because this

LICS ’20, July 8–11, 2020, Saarbrücken, Germany

violates linearity. This differs from the formulation used by
McBride and by Atkey, where abstracting over zero uses ofa resource is allowed.
(iii) In the typing rule for lift 𝑀, we require the context tobe a parameter context Φ. Although the term 𝑀 may not be
a parameter term, the term lift 𝑀 is considered a parameter
term because it has an interpretation in 𝑝B.
(iv) In the typing rule for (𝑀, 𝑁 ), the term 𝑀 also appears
as a parameter term Sh(𝑀) in the type 𝐵. All linear variablesof 𝑀 will have index 0 in the context Γ2 and index 1 in Γ1 , so
𝑀 is considered used exactly once in the term (𝑀, 𝑁 ).
(v) We identify a subset of typing rules Φ ⊢ 𝑅 : 𝑃 for typing
parameter terms. We do not formally separate the typing
rules into two fragments. In the semantics, the interpretationof Φ ⊢ 𝑅 : 𝑃 is an arrow in 𝑝B.
(vi) The typing rules for the parameter terms 𝑅1 @𝑅2 and𝜆 ′𝑥 .𝑅 are the usual ones from intuitionistic dependent types,
where the contexts are required to be parameter contexts.
The parameter term force′ 𝑅 has a type of the form Sh(𝐴).
(vii) We implicitly assume all contexts appearing in typing
rules to be well-formed (i.e., if it is not well-formed, the rule
does not apply). In particular, this applies to contexts of theform Γ1 + Γ2 , which carry the side condition that a type withindex 𝜔 must be a parameter type.
We have the following standard syntactic results: a wellformed typing judgment implies that the type and the context
are well-formed, and the shape operation preserves typing.
Theorem 3.6.
• If Γ ⊢ 𝑀 : 𝐴, then Sh(Γ) ⊢ 𝐴 : ∗ and Γ ⊢.
• If Γ ⊢ 𝑀 : 𝐴, then Sh(Γ) ⊢ Sh(𝑀) : Sh(𝐴).
Since parameter terms have no side effects (i.e., do notaffect states), we can freely substitute them into a term ora type. We cannot freely substitute a general term becauseside effects may get duplicated after the substitution. Sincea value can be of a linear type, when substituting it into atype, we must apply the shape operation to the value. Tosummarize, we have:
Theorem 3.7 (Substitution).
• If Φ, 𝑥 : 𝑃 ⊢ 𝐵 [𝑥] : ∗ and Φ ⊢ 𝑅 : 𝑃, then Φ ⊢ 𝐵 [𝑅] : ∗.
• If Φ, 𝑥 : 𝑃, Γ ⊢ 𝑀 : 𝐵 [𝑥] and Φ ⊢ 𝑅 : 𝑃, then Φ, [𝑅/𝑥]Γ ⊢[𝑅/𝑥]𝑀 : 𝐵 [𝑅].
• If Γ1, 𝑥 :𝑘 𝐴, Γ ′ ⊢ 𝑀 : 𝐵 [𝑥] and Γ2 ⊢ 𝑉 : 𝐴, then
Γ1 + 𝑘Γ2, [Sh(𝑉 )/𝑥]Γ ′ ⊢ [𝑉 /𝑥]𝑀 : 𝐵 [Sh(𝑉 )].
3.2

Operational semantics

We adopt a big-step call-by-value operational semantics forour type system. A term in our language may in principle
modify the state. However, since we have not yet introduced
any primitive operations that can actually update the state,
the state has been omitted from the statement of the following evaluation rules. We will return to the state change

Peng Fu, Kohei Kishida, and Peter Selinger

in Section 4.2, when we discuss a concrete language withspecific primitive operations.
Definition 3.8 (Selected evaluation rules). 𝑀 ⇓ 𝑁
𝑀 ⇓ 𝜆𝑥 .𝑀 ′𝑁 ⇓ 𝑉 [𝑉 /𝑥]𝑀 ′ ⇓ 𝑁 ′𝑀𝑁 ⇓ 𝑁 ′𝑅1 ⇓ 𝜆 ′𝑥 .𝑅1′

𝑅2 ⇓ 𝑉𝑅1 @𝑅2[𝑉 /𝑥]𝑅1′ ⇓ 𝑅 ′⇓ 𝑅′

𝑀 ⇓ lift 𝑀 ′ 𝑀 ′ ⇓ 𝑁force 𝑀 ⇓ 𝑁
𝑅 ⇓ lift 𝑀 Sh(𝑀) ⇓ 𝑅 ′force ′ 𝑅 ⇓ 𝑅 ′Note that a term of the form lift 𝑀 is a parameter term,even when 𝑀 is not. So to ensure that the resulting parameter
term force′ (lift 𝑀) does not modify state, we must evaluate
it to Sh(𝑀), which is again a parameter term. This motivatesthe evaluation rule force′ 𝑅.
Since the evaluation rules are also used during type checking, the evaluation is defined on open terms. Thus it may
not always evaluate a term to a value. We treat variables asvalues to facilitate type-level evaluation.
We have the following type conversion rule for equalityof types.
Definition 3.9 (Type conversion).
Γ ⊢ 𝑀 : 𝐴[𝑅] 𝑅 ⇓ 𝑅 ′Γ ⊢ 𝑀 : 𝐴[𝑅 ′]The type preservation for the big-step evaluation can beproved by induction on the evaluation rules. The main insight that is needed to prove type preservation is that only
values and parameter terms can be substituted into anotherterm.
Theorem 3.10 (Type preservation). If Γ ⊢ 𝑀 : 𝐴 and 𝑀 ⇓𝑀 ′, then we have Γ ⊢ 𝑀 ′ : 𝐴.
3.3

Denotational semantics

We interpret our type system with a state-parameter fibration, by providing contexts Γ ⊢, dependent types Γ ⊢ 𝐴 : ∗,and terms Γ ⊢ 𝑀 : 𝐴 with interpretations J−K in the manner
described in Section 2.4, and by interpreting the shape operation by the shape-unit functor 𝑝 ◦ ♯ as in Section 2.5. In
addition, the substitution of a term into a type corresponds
to a pullback in the standard fashion. This semantics is encapsulated in the following theorem (and its proof). Recall
that 𝐴 is a notation for ♯𝐴. We often write JΓK instead ofJΓ ⊢K.
Theorem 3.11. An interpretation J−K can be defined in sucha way that(10) JΓK is an object of E.
(11) JΦ ⊢ 𝐴 : ∗K is an object of E/JΦK. We may write 𝜋 :J𝐴K → JΦK for it.
(12) JΓ ⊢ 𝑀 : 𝐴K is an arrow of E/JΓK from 𝜂 JΓK to JΓ ⊢ 𝐴 : ∗K.

Linear Dependent Type Theory for Quantum Programming Languages(13) JSh(Γ)K = 𝑝JΓK, an object of 𝑝B.
(14) JΦ ⊢ Sh(𝐴) : ∗K = 𝑝JΦ ⊢ 𝐴 : ∗K, an object of 𝑝B/JΦK.
(15) JSh(Γ) ⊢ Sh(𝑀) : Sh(𝐴)K = 𝑝JΓ ⊢ 𝑀 : 𝐴K, an arrow of
𝑝B/JΓK.
(16) Suppose 𝜋 = JΦ, 𝑥 : 𝑃 ⊢ 𝐵 : ∗K : J𝐵K → JΦ, 𝑥 : 𝑃K and
J𝑅K = JΦ ⊢ 𝑅 : 𝑃K : JΦK → J𝑃K in 𝑝B/JΦK. Then 𝜋 ′ =JΦ ⊢ [𝑅/𝑥]𝐵 : ∗K : J[𝑅/𝑥]𝐵K → JΦK is the pullback of
𝜋 along J𝑅K as in
J[𝑅/𝑥]𝐵K

J𝐵K𝜋′LICS ’20, July 8–11, 2020, Saarbrücken, GermanyJΓ, 𝑥 : 𝐴, Γ ′K.
𝑝JΓK ⊗ J𝐴K ⊗ 𝑝JΓ ′K
𝑓
𝑢

𝜂

JΦK

𝜋

JΓ, 𝑥 : 𝐴, Γ ′K = JΓ ′K

JΓK(iv) The fourth case isΓ, 𝑥 :𝑘 𝐴 ⊢ 𝑀 : 𝐵 [𝑥] 𝑘 = 0 ⇒ 𝐴 = 𝑃Γ ⊢ 𝜆𝑥 .𝑀 : (𝑥 : 𝐴) ⊸ 𝐵 [𝑥]JΦ, 𝑥 : 𝑃K = J𝑃K

The proof of this theorem goes by simultaneous induction
on the derivation, with each case of the inductive step showing how exactly the semantics works. Here we show someexamples of the cases (for the other cases please see [8]).
(i) The first is

J𝐴K

𝜋′

𝜋
J𝑅 K

JΓ ′K ×JΓK J𝐴K

By the assumptions, we have a morphism J𝑀K : JΓK ⊗JΓK

J𝐴K𝑘 → J𝐵K over JΓ, 𝑥 : 𝐴K. By the adjunction in Theoremg : JΓK → Î
2.14, we define J𝜆𝑥 .𝑀K = J𝑀K
𝑘 J𝐵K as aJΓ K,J𝐴K

morphism over JΓK.
(v) The last case we review here isΓ ⊢ Sh(Γ) ⊢ 𝐴 : ∗𝑘 = 𝜔 only if 𝐴 is a parameter typeΓ, 𝑥 :𝑘 𝐴 ⊢Γ1 ⊢ 𝑀 : (𝑥 : 𝐴) ⊸ 𝐵 [𝑥] Γ2 ⊢ 𝑁 : 𝐴
Γ1 + Γ2 ⊢ 𝑀𝑁 : 𝐵 [Sh(𝑁 )]By the assumptions, we have objects JΓK of E and 𝜋 : J𝐴K →JSh(Γ)K = JΓK of E/JΓK. We therefore define

The assumptions give arrows J𝑀K : JΓ1 K → Π JΓK,J𝐴K J𝐵K
and J𝑁 K : JΓ2 K → J𝐴K of E/JΓK for JΓK = JΓ1 K = JΓ2 K, as
well as 𝜋 : J𝐵K → JSh(Γ), 𝑥 :𝑘 Sh(𝐴)K = J𝐴K. Note that
JSh(𝑁 )K = J𝑁 K, since (15) implies JSh(𝑁 )K = 𝑝J𝑁 K. Hence(16) gives the pullback square in the following. We therefore
define J𝑀𝑁 K as the unique arrow 𝑢 that makes the diagram
commute.

JΓ, 𝑥 :𝑘 𝐴K = JΓK ⊗ J𝐴K𝑘
using a dependent monoidal product, where J𝐴K𝑘 = 𝑝J𝐴K if

𝑘 = 0 and J𝐴K𝑘 = J𝐴K otherwise.
(ii) The second case isJΓ1 + Γ2 K

Φ, 𝑥 :𝑘 Sh(𝐴) ⊢ 𝐵 [𝑥] : ∗Φ ⊢ (𝑥 : 𝐴) ⊸ 𝐵 [𝑥] : ∗J𝑀K ⊗JΓK J𝑁 K

(Π JΓK,J𝐴K J𝐵K) ⊗JΓK J𝐴K𝑢𝜖J𝐵 [Sh(𝑁 )]K

J𝐵K

𝜂
𝜋

The assumption implies Φ ⊢ 𝐴 : ∗. Hence we have arrows 𝜋 :J𝐵K → JΦ, 𝑥 :𝑘 Sh(𝐴)K = J𝐴K and J𝐴K → JΦK. We therefore
defineJΦ ⊢ (𝑥 : 𝐴) ⊸ 𝐵 [𝑥] : ∗K = Π JΦK,J𝐴K J𝐵K,
using a dependent function space that gives an object in
E/JΦK.
(iii) The third case is0Γ, 𝑥 :1 𝐴, 0Γ ′ ⊢0Γ, 𝑥 :1 𝐴, 0Γ ′ ⊢ 𝑥 : 𝐴
Since Sh(Γ) ⊢ 𝐴 : ∗, by (11) we have 𝜋 : J𝐴K → JΓK.
Note that there is a canonical morphism 𝑓 : 𝑝JΓK ⊗ J𝐴K ⊗𝑝JΓ ′K → J𝐴K over JΓK. We define J𝑥K as the following 𝑢 over

JΓK

J𝑁 K

J𝐴K

It is crucial to observe that JΓ1 + Γ2 K = JΓ1 K ⊗ JΓ2 K. This thenenables us to use 𝜖 : (Π JΓK,J𝐴K J𝐵K) ⊗JΓK J𝐴K → J𝐵K, the counitof the adjunction of Theorem 2.14.
For this semantics, we have the following soundness theorem. The main step in proving this theorem is proving thesemantic version of the substitution theorem (Theorem 3.7).
Theorem 3.12 (Soundness). If Γ ⊢ 𝑀 : 𝐴 and 𝑀 ⇓ 𝑀 ′, thenwe have J𝑀K = J𝑀 ′K.

4

Dependently typed Proto-Quipper

The type system we defined in Section 3 is abstract. For example, there is no mention of quantum data types, concrete

LICS ’20, July 8–11, 2020, Saarbrücken, Germany

representation of quantum circuits, circuit boxing and unboxing. This is because the language is derived directly fromthe general semantics of Section 2.
In this section we show how to support programming
quantum circuits. On the semantic side, this means that wewill work with a concrete state-parameter fibration, i.e., ♯ :M → Set. On the syntactic side, this means that we will
extend the type system of Section 3 with several constructs
to work with quantum circuits. We call the resulting typesystem “dependently typed Proto-Quipper”, or sometimes
Proto-Quipper-D.1
4.1

Simple types and quantum circuits

Recall from Section 2.3 that the model M of [28] contains
a (full) monoidal subcategory M of (generalized) circuits.
Objects 𝑆 of M (or (1, 𝑆) of M) are called simple. It follows
that 𝑆 is simple iff ♯𝑆 = 1. Such objects represent states
without parameters (i.e., a single state space, rather thanan indexed family of them). We call a type simple if it isinterpreted by a simple object. For any simple objects 𝑆 1 and𝑆 2 , we have the isomorphism!(𝑆 1 ⊸ 𝑆 2 )box/unbox

𝑝M(𝑆 1, 𝑆 2 ).

This isomorphism means that the function type !(𝑆 1 ⊸ 𝑆 2 )literally represents a hom-set of the category M, which we
can think of as a set of circuits with input 𝑆 1 and output 𝑆 2 .
We equip the programming language with a type Circ(𝑆 1, 𝑆 2 )representing such circuits as first-class citizens. These linear
functions of simple types correspond to quantum circuits.
The type Qubit is defined as (1, Q), where Q is a designated object in M representing the qubit type. As a resultof being a free coproduct completion, M has coproducts.
Thus Proto-Quipper-M admits quantum data types. For example, the type List Qubit can be interpreted as an object
Σ𝑛 ∈N (1, Q ⊗𝑛 ) = (N, (Q ⊗𝑛 )𝑛 ∈N ).
A problem of quantum data types. The box/unbox isomorphism only holds for simple types. However, List Qubit
is not a simple type since ♯JList QubitK = ♯(N, (Q ⊗𝑛 )𝑛 ∈N ) =N. Thus, there is no such type as Circ(List Qubit, List Qubit)
in Proto-Quipper-M, and a function of type !(List Qubit ⊸List Qubit) cannot be converted into a circuit. This makes
sense, because such a function actually represents a familyof circuits, indexed by the length of the input list. In practice,
however, we want programmers to be able to work withquantum data types and linear functions between them. The
above limitation makes boxing circuits in Proto-Quipper-M
awkward.
Solution via dependent quantum data types. We solve
this problem by working with dependent quantum data types,
such as Vec Qubit 𝑛. For a value 𝑛 of type Nat, we define
JVec Qubit 𝑛K as 𝑉𝑛 = (1, Q ⊗𝑛 ) as in the following pullback

1 A full specification of dependently typed Proto-Quipper is available in [8].

Peng Fu, Kohei Kishida, and Peter Selinger

square. Note that the existence of the pullback is guaranteedby the state-parameter fibration ♯ : M → Set.
JList QubitK = Σ𝑛 ∈N (1, Q ⊗𝑛 )JVec Qubit 𝑛K = 𝑉𝑛
𝑞𝑛

𝑞1

𝑞N

Thus ♯JVec Qubit 𝑛K = ♯𝑉𝑛 = 1 and Vec Qubit 𝑛 is a simple
type. Now a linear function of the type !(Vec Qubit 𝑛 ⊸Vec Qubit 𝑛) can be boxed into a circuit, which has the type
Circ(Vec Qubit 𝑛, Vec Qubit 𝑛). Together with the dependentfunction type, the programmer can now define a function of
the type!((𝑛 : Nat) ⊸ Circ(Vec Qubit 𝑛, Vec Qubit 𝑛)).
Such a function represents a family of circuits indexed by 𝑛.
We extend the syntax of Definition 3.1 with simple types,
circuit types, dependent data types, and the boxing and unboxing operations for circuits.
Definition 4.1 (Extended syntax).
Types 𝐴, 𝐵 ::= ... | Nat | List 𝐴 | Vec 𝐴 𝑅 | Circ(𝑆 1, 𝑆 2 )Simple Types 𝑆 ::= Qubit | Unit | 𝑆 1 ⊗ 𝑆 2 | Vec 𝑆 𝑅
Parameter types 𝑃 ::= ... | Nat | List 𝑃 | Vec 𝑃 𝑅 | Circ(𝑆 1, 𝑆 2 )Terms 𝑀 ::= ... | ℓ | (𝑎, C, 𝑏) | box𝑆 𝑀 | unbox 𝑀

Note that the vector data type Vec 𝐴 𝑅 requires the length
index to be a parameter term 𝑅, as only parameter terms canappear in types. The type Circ(𝑆 1, 𝑆 2 ) is considered a parameter type because JCirc(𝑆 1, 𝑆 2 )K = 𝑝M(J𝑆 1 K, J𝑆 2 K), which isa parameter object.
Following Proto-Quipper-M, we extend terms with labelsℓ, which are distinct from variables. Labels are used to represent wires of a quantum circuit (or more generally, components of a tensor product). Unlike variables, labels cannot be
substituted. We also extend contexts with label contexts ofthe form Σ = ℓ1 :𝑘1 Qubit, ..., ℓ𝑛 :𝑘𝑛 Qubit, where 𝑘𝑖 ∈ {0, 1}.
The semantics of Σ is a tensor product of qubits, and we
identify each Σ with the corresponding object in M.
The canonical inhabitants of Circ(𝑆 1, 𝑆 2 ) are boxed circuitsof the form (𝑎, C, 𝑏), where C is a morphism of M and 𝑎, 𝑏
are interfaces connecting the inputs and outputs of C to thetypes 𝑆 1 and 𝑆 2 , respectively (see [28] for more details).
The typing rules for Circ(𝑆 1, 𝑆 2 ) are the same as in ProtoQuipper-M:Σ1 ⊢ 𝑎 : 𝑆 1 Σ2 ⊢ 𝑏 : 𝑆 2 C : Σ1 → Σ2
Φ ⊢ (𝑎, C, 𝑏) : Circ(𝑆 1, 𝑆 2 )Γ ⊢ 𝑀 : !(𝑆 1 ⊸ 𝑆 2 )Γ ⊢ 𝑀 : Circ(𝑆 1, 𝑆 2 )Γ ⊢ box𝑆1 𝑀 : Circ(𝑆 1, 𝑆 2 ) Γ ⊢ unbox 𝑀 : !(𝑆 1 ⊸ 𝑆 2 )Boxed circuits are not part of the surface language; rather
they are built and consumed by the box and unbox operations. Certain built-in boxed circuits, called gates, may bebound to constant symbols of the language (or provided bya standard library). An implementation may also provideLinear Dependent Type Theory for Quantum Programming Languages

additional primitive operations on boxed circuits, such as
reverse : Circ(𝑆 1, 𝑆 2 ) → Circ(𝑆 2, 𝑆 1 ). Indeed, although thetypes !(𝑆 1 ⊸ 𝑆 2 ) and Circ(𝑆 1, 𝑆 2 ) are semantically isomorphic, they are operationally distinct, because Circ(𝑆 1, 𝑆 2 ) has
canonical inhabitants whereas !(𝑆 1 ⊸ 𝑆 2 ) does not.
The shape operation can be extended naturally.
Definition 4.2 (Extended shape operation).
Sh(Nat) = Nat
Sh(List 𝐴) = List Sh(𝐴)
Sh(Vec 𝐴 𝑅) = Vec Sh(𝐴) 𝑅
Sh(Circ(𝑆 1, 𝑆 2 )) = Circ(𝑆 1, 𝑆 2 )Sh(ℓ) = unit
Sh(𝑎, C, 𝑏) = (𝑎, C, 𝑏)
Sh(box𝑆 𝑀) = box𝑆 Sh(𝑀)
Sh(unbox 𝑀) = unbox Sh(𝑀)This definition is semantically sound for List and Vec
because the shape-unit functor 𝑝♯ preserves tensor products
and coproducts in M. We also observe that Sh(List Qubit) =List Unit  Nat and Sh(Vec Qubit 𝑅) = Vec Unit 𝑅  Unit.
Safe list-to-vector conversion. Allowing types to dependon the shape of any other types allows us to define a function
to safely convert a list of qubits into a vector of qubits.2
conv : !((𝑥 : List Qubit) ⊸ Vec Qubit (toNat 𝑥))
conv =
lift (𝜆𝑥 . case 𝑥 of
Nil → VNilCons 𝑦 𝑦𝑠 → VCons 𝑦 (force conv 𝑦𝑠))
Let us consider the type(𝑥 : List Qubit) ⊸ Vec Qubit (toNat 𝑥).
Here toNat : List Unit → Nat is the isomorphism that converts a list of units to a natural number. Using the kinding
rules of Definition 3.4 to kind check this type, we only needto kind check the following
𝑥 : Sh(List Qubit) = List Unit ⊢ Vec Qubit (toNat 𝑥) : ∗,which is a valid kinding judgment. So a function of the type(𝑥 : List Qubit) ⊸ Vec Qubit (toNat 𝑥) takes a list of qubits
as input and outputs a vector of qubits, where the length ofthe vector is the length of the input list.
The above conversion would not be possible if we required
dependent types to be only of the form (𝑥 : 𝑃) → 𝐵 [𝑥],where 𝑃 is a parameter type. McBride’s conversion function
has a different flavor. In [19, Section 5], he defines conv :𝜔
(𝑥 :1 List 𝑋 ) ⊸ Vec 𝑋 (length 𝑥), where length :0 (𝑥 :0
List 𝑋 ) ⊸ Nat. We cannot define a length function of type
List Qubit ⊸ Nat because it violates linearity.
2 A dependently typed Proto-Quipper program for conv can be found in [8].

LICS ’20, July 8–11, 2020, Saarbrücken, Germany

4.2

Operational semantics

In Proto-Quipper-M [28], the call-by-value big-step evaluation is defined on a configuration of the form (C, 𝑀), where
C denotes a morphism of M, and 𝑀 is a term that can append
quantum gates to C when evaluated.
Definition 4.3. We define a well-typed configuration
Γ; Σ ⊢ (C, 𝑀) : 𝐴; Σ ′to mean there exists Σ ′′ such that C : Σ → Σ ′′ ⊗ Σ ′ andΓ, Σ ′′ ⊢ 𝑀 : 𝐴.
Our definition of well-typed configurations allows 𝑀 to
be an open term, with free variables from the context Γ. The
reason for this is that the evaluation rules can be used during
type checking, where there can be free variables in types.
We can visualize the configuration (C, 𝑀) in the above
definition as the following diagram, where the term 𝑀 in
(C, 𝑀) is using the output wires from Σ ′′.

Σ

Σ′

C

Σ ′′
𝐴

𝑀
Γ

Dependently typed Proto-Quipper has the same evaluation rules as Proto-Quipper-M, plus rules for reducing parameter terms.3
Definition 4.4 (Selected evaluation rules).
(C1, 𝑀) ⇓ (C2, force(unbox (𝑎, D, 𝑏)))(C2, 𝑁 ) ⇓ (C3, 𝑎 ′)C4 = append(C3, 𝑎 ′, (𝑎, D, 𝑏)), FV(𝑀𝑁 ) = ∅(C1, 𝑀𝑁 ) ⇓ (C4, 𝑏)(C, 𝑀) ⇓ (C ′, lift 𝑀 ′)(id𝑎 , 𝑀 ′ 𝑎) ⇓ (D, 𝑏)
𝑎 = gen(𝑆 [𝑉 ])(id𝐼 , 𝑅) ⇓ (_, 𝑉 )FV(box𝑆 [𝑅 ] 𝑀) = ∅(C, box𝑆 [𝑅 ] 𝑀) ⇓ (C ′, (𝑎, D, 𝑏))(C, 𝑀) ⇓ (C ′, 𝜆𝑥 .𝑀 ′)(C ′′, [𝑉 /𝑥]𝑀 ′) ⇓ (C ′′′, 𝑁 ′)(C ′, 𝑁 ) ⇓ (C ′′, 𝑉 )(C, 𝑀𝑁 ) ⇓ (C ′′′, 𝑁 ′)(C, 𝑀) ⇓ (C ′, lift 𝑀 ′) (C ′, 𝑀 ′) ⇓ (C ′′, 𝑁 )(C, force 𝑀) ⇓ (C ′′, 𝑁 )(C, 𝑀) ⇓ (C ′, unbox 𝑀 ′)(C, box𝑆 𝑀) ⇓ (C ′, 𝑀 ′)3 A detailed definition of the evaluation rules is in [8].

LICS ’20, July 8–11, 2020, Saarbrücken, Germany(C1, 𝑅1 ) ⇓ (C2, 𝜆 ′𝑥 .𝑅1′ )(C3, [𝑉 /𝑥]𝑅1′ ) ⇓ (C4, 𝑅 ′)Peng Fu, Kohei Kishida, and Peter Selinger(C2, 𝑅2 ) ⇓ (C3, 𝑉 )(C1, 𝑅1 @𝑅2 ) ⇓ (C4, 𝑅 ′)(C1, 𝑅) ⇓ (C2, lift 𝑀) (C1, Sh(𝑀)) ⇓ (C3, 𝑅 ′)(C1, force′ 𝑅) ⇓ (C3, 𝑅 ′)In the first evaluation rule, the term 𝑀𝑁 appends a circuit
D to the circuit C3 , resulting in an updated circuit C4 . The
term 𝑁 evaluates to a label tuple 𝑎 ′, pointing to some of theoutputs of the then-current circuit C3 . This tuple 𝑎 ′ mustmatch the input interface 𝑎 of the boxed circuit (𝑎, D, 𝑏).
Finally, the operation append(C3, 𝑎 ′, (𝑎, D, 𝑏)) constructs a
new circuit C4 by connecting the outputs 𝑎 ′ of C3 to the
inputs 𝑎 of (𝑎, D, 𝑏). As a result, C4 will expose 𝑏 as part ofits output interface.
The second evaluation rule is for boxing a circuit. The
notation 𝑆 [𝑅] denotes a simple type 𝑆 that may contain aparameter term 𝑅. The type annotation 𝑆 [𝑅] on the keyword box is used to generate a data structure 𝑎 = gen(𝑆 [𝑉 ])holding fresh wire labels. The evaluator then evaluates 𝑀 ′ 𝑎under the identity circuit id𝑎 , which produces a circuit D
and a circuit output 𝑏.
The third to fifth evaluation rules are the same as ProtoQuipper-M. The last two rules are for evaluating parameter
terms. Since parameter terms do not change states, the evaluation of these terms does not append any quantum gates.
We have the following theorem.
Theorem 4.5. If (C, 𝑅) ⇓ (C ′, 𝑅 ′), then we have C = C ′.
The semantics of well-typed configurations is given below. It corresponds to the above diagram for (C, 𝑀), wherevertical composition is interpreted as the fibered monoidal
product ⊗JΓK .
Definition 4.6. Let Γ; Σ ⊢ (C, 𝑀) : 𝐴; Σ ′ be a well-typed
configuration. We define′J(C, 𝑀)K : JΓK ⊗ JΣK → J𝐴K ⊗ JΣ K
= (J𝑀K ⊗ JΣ ′K) ◦ (JΓK ⊗ C),a morphism over JΓK in M/JΓK.

Dependently typed Proto-Quipper satisfies type preservation and soundness.
Theorem 4.7 (Type preservation and soundness). If Γ; Σ ⊢(C, 𝑀) : 𝐴; Σ ′ and (C, 𝑀) ⇓ (C ′, 𝑀 ′), then we have Γ; Σ ⊢(C ′, 𝑀 ′) : 𝐴; Σ ′ and J(C, 𝑀)K = J(C ′, 𝑀 ′)K.
4.3

Prototype implementation

We have implemented a prototype for dependently typed
Proto-Quipper, called Proto-Quipper-D. We will now discuss
some essential features that enable the type system in thispaper to scale to a usable programming language. For more

information about programming in Proto-Quipper-D, pleasesee [8] and the tutorial introduction [7].
Type inference and elaboration. It is a well-known issue that programming with linear types can be quite invasive:the programmer must supply linearity annotations, which
is burdensome for large programs. Recent research tries toaddress this problem. For example, Paykin and Zdancewic[25] propose embedding a linear-nonlinear type system in
Haskell. Bernardy et al. [5] propose extending Haskell withlinear types.
In our implementation, every top-level declaration must
be of parameter type (since top-level functions are reusable).
Programs can be written without using annotations such as
lift and force. We implemented a type elaborator that extends
the well-known bi-directional type inference algorithm [26]with the ability to insert linearity annotations. The basic
idea is that when checking a program 𝑀 with type !𝐴, theelaborator produces a new term lift 𝑀 ′, where 𝑀 ′ is the resultof checking 𝑀 against the type 𝐴. When inferring a type forthe application 𝑀𝑁 , where 𝑀 has the type !(𝐴 ⊸ 𝐵), theelaborator will produce a new term (force 𝑀) 𝑁 ′ and a type𝐵, where 𝑁 ′ is the result of checking 𝑁 against 𝐴. We also
implemented a secondary checker to recheck the annotatedterms produced by the elaborator. We have found that thistwo-step elaboration-and-checking works well in practiceand linear annotations are manageable with the help of thetype elaborator.
Simple data types and parameter data types. We implement Haskell 98 style [15] data types (which begin withthe keyword data). For example, list data type can be declared as data List a = Nil | Cons a (List a). We also
implemented a special kind of dependent data types that wecall simple data type declarations (which begin with the keyword simple). For example, the following is a declaration ofa vector data type.
simple Vec a : Nat -> Type where
Vec a Z = VNil
Vec a (S n) = VCons a (Vec a n)
As we mentioned in Section 4.1, only linear functions ofsimple types can be boxed into circuits and simple types
can be characterized semantically by ♯𝑆 = 1. Simple types
can also be described syntactically as types that uniquelydetermine the size of their inhabitants. For example, List is
not a simple type because List Qubit may have inhabitantsof different sizes, while inhabitants of Vec Qubit 3 must havesize 3, so it is a simple type. In Proto-Quipper-D, the simple
data type declaration is checked by the compiler using a
syntactic characterization of simple types. Note that such asimplicity check is undecidable in general, as it is equivalent
to checking termination of a recursive function (e.g., the vector data type declaration above can be viewed as a primitive
recursive function which recurs on a second input of typeLinear Dependent Type Theory for Quantum Programming Languages

Nat). We implemented a simplicity checker that only accepts
certain declarations that correspond to primitive recursivefunctions.
Since we allow user-defined types, the notion of parametertypes and simple types must account for such extensions. We
implement parameter types and simple types as type classes[35], and their instances are automatically generated by thecompiler upon defining a data type.
For example, the list data type declaration will generate an
instance (Parameter a) => Parameter (List a), whichmeans that List a is a parameter type if the type a is aparameter type. Similarly, the vector data type declaration
will generate an instance (Simple a) => Simple (Vec an), which means Vec a n is a simple type if the type a issimple.
With simple type constraints, we can give the circuit boxing operator box the following type (Simple a, Simpleb) => !(a -> b) -> Circ(a, b). This way the typechecker will be able check at compile time whether the linear functions we are boxing are indeed linear functions ofsimple types. With parameter type constraints, we can safely
discard reusable variables without violating linearity. For
example, we can define a function fst to retrieve the left
element of a pair, which will have type !((Parameter b)=> a * b -> a). Here a * b means 𝑎 ⊗ 𝑏. Since type b is aparameter type, it is safe to discard the right element.
Irrelevant quantification. Besides the linear dependent
types described in this paper, we also implemented a versionof Miquel’s irrelevant quantification [3, 20]. Although theusual dependent quantification is enough in theory, it isbeneficial to implement irrelevant quantification. Because
irrelevant arguments are erased during evaluation, lengthindexed data types such as Vec will not store their length atruntime, hence making the evaluator more efficient.
In Proto-Quipper-D, a dependent quantification takes theform (n : Nat) -> T, and an irrelevant quantification
takes the form forall (n : Nat) -> T. We implement thefollowing typing rules for irrelevant quantification.
Φ, 𝑥 : 𝑃, Γ ⊢ 𝑀 : 𝐵 [𝑥]Φ, Γ ⊢ 𝜆{𝑥 }.𝑀 : ∀(𝑥 : 𝑃).𝐵 [𝑥]Φ, Γ ⊢ 𝑀 : ∀(𝑥 : 𝑃).𝐵 [𝑥] Φ ⊢ 𝑅 : 𝐴
Φ, Γ ⊢ 𝑀 {𝑅} : 𝐵 [𝑅]Both irrelevant abstraction 𝜆{𝑥 }.𝑀 and application 𝑀 {𝑅} areerased to |𝑀 | during evaluation. So we must be able to discard
the irrelevant argument 𝑅. Hence we require the irrelevant
quantification to be of the form ∀(𝑥 : 𝑃).𝐵 [𝑥] (where 𝑃 must
be a parameter type), and the irrelevant arguments to beparameter terms. The shape operation can be extended for

LICS ’20, July 8–11, 2020, Saarbrücken, Germany

irrelevant quantification.
Sh(∀(𝑥 : 𝑃).𝐵 [𝑥]) = ∀(𝑥 : 𝑃). Sh(𝐵 [𝑥])Sh(𝜆{𝑥 }.𝑀) = 𝜆{𝑥 }. Sh(𝑀)
Sh(𝑀 {𝑅}) = Sh(𝑀){𝑅}
Other than annotating types using the keyword forall,
programmers do not need to work with irrelevant abstraction and application explicitly. Our type elaborator automatically generates the irrelevance annotations, just like linearity
annotations. For example, in Proto-Quipper-D, the vector
append function has type !(forall a (n m : Nat) -> Vec
a n -> Vec a m -> Vec a (add n m)), but its definitionis the same as that of the list append function.

5

Conclusion

We defined state-parameter fibrations, and showed that theymodel a general notion of linear dependent types. We derived a linear dependent type system based on the categoricalstructures obtained from the state-parameter fibration. We
showed that Rios and Selinger’s M admits a state-parameter
fibration ♯ : M → Set. We further extended the linear dependent type system to obtain a programming language forquantum circuits, called dependently typed Proto-Quipper.
We showed how the fibration ♯ : M → Set can be used
to interpret dependently typed Proto-Quipper. We proved
the type preservation and the soundness for the big-stepevaluation. We implemented a prototype for dependently
typed Proto-Quipper and discussed practical aspects of theimplementation.

Acknowledgments
We thank Neil J. Ross for helpful discussions of a draft of thispaper, and Marco Gaboardi and Aaron Stump for pointing
out related works. This work was supported by the Air Force
Office of Scientific Research under award number FA955015-1-0331. Any opinions, findings and conclusions or recommendations expressed in this material are those of theauthors and do not necessarily reflect the views of the U.S.
Department of Defense.

References[1] Robert Atkey. 2018. Syntax and semantics of quantitative type theory.
In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in
Computer Science. ACM, 56–65.
[2] Andrew Barber. 1996. Dual intuitionistic linear logic. Technical Report
ECS-LFCS-96-347. University of Edinburgh, Department of Computer
Science.
[3] Bruno Barras and Bruno Bernardo. 2008. The implicit calculus of
constructions as a programming language with dependent types. In
International Conference on Foundations of Software Science and Computational Structures. Springer, 365–379.
[4] P. Nick Benton. 1994. A mixed linear and non-linear logic: Proofs,
terms and models. In International Workshop on Computer Science Logic.
Springer, 121–135.

LICS ’20, July 8–11, 2020, Saarbrücken, Germany[5] Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R Newton, Simon
Peyton Jones, and Arnaud Spiwack. 2018. Linear Haskell: practicallinearity in a higher-order polymorphic language. In Proceedings ofthe 45th ACM SIGPLAN Symposium on Principles of Programming Languages. ACM, 1–29.
[6] Iliano Cervesato and Frank Pfenning. 1996. A linear logical framework.
In Proceedings 11th Annual IEEE Symposium on Logic in Computer
Science. IEEE, 264–275.
[7] Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger. 2020. A tutorial
introduction to quantum circuit programming in dependently typed
Proto-Quipper. In Proceedings of the 12th International Conference on
Reversible Computation. Springer. To appear.
[8] Peng Fu, Kohei Kishida, and Peter Selinger. 2020. Linear dependent
type theory for quantum programming languages. (2020). Available
from arXiv:2004.13472.
[9] Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, andBenjamin C Pierce. 2013. Linear dependent types for differential privacy. In Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages (ACM SIGPLAN Notices), Vol. 48.
ACM, 357–370.
[10] Jean-Yves Girard. 1987. Linear logic. Theoretical Computer Science 50,
1 (1987), 1–101.
[11] Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. 1992. Boundedlinear logic: a modular approach to polynomial-time computability.
Theoretical Computer Science 97, 1 (1992), 1–66.
[12] Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter
Selinger, and Benoît Valiron. 2013. An introduction to quantum programming in Quipper. In Proceedings of the 5th International Conference
on Reversible Computation. Springer, 110–124.
[13] Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter
Selinger, and Benoît Valiron. 2013. Quipper: a scalable quantum
programming language. In Proceedings of the 34th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation (ACM SIGPLAN Notices), Vol. 48. ACM, 333–342.
[14] C. Barry Jay and J. Robin B. Cockett. 1994. Shapely types and shapepolymorphism. In European Symposium on Programming. Springer,
302–316.
[15] Simon Peyton Jones. 2003. Haskell 98 language and libraries: the revised
report. Cambridge University Press.
[16] G. Max Kelly. 1974. Doctrinal adjunction. In Category Seminar.
Springer, 257–280.
[17] Neelakantan R Krishnaswami, Pierre Pradic, and Nick Benton. 2015.
Integrating linear and dependent types. In Proceedings of the 42nd ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages(ACM SIGPLAN Notices), Vol. 50. ACM, 17–30.
[18] Per Martin-Löf and Giovanni Sambin. 1984. Intuitionistic type theory.
Bibliopolis Naples.
[19] Conor McBride. 2016. I got plenty o’ nuttin’. In A List of Successes
That Can Change the World. Springer, 207–233. Available from https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.pdf.
[20] Alexandre Miquel. 2001. The implicit calculus of constructions extending pure type systems with an intersection type binder and subtyping.
In International Conference on Typed Lambda Calculi and Applications.
Springer, 344–359.
[21] Michele Mosca, Martin Roetteler, and Peter Selinger. 2018. Quantum
Programming Languages (Dagstuhl Seminar 18381). Dagstuhl Reports
8, 9 (2018), 112–132. https://doi.org/10.4230/DagRep.8.9.112[22] Michael A. Nielsen and Isaac L. Chuang. 2002. Quantum Computation
and Quantum Information. Cambridge University Press.
[23] Bengt Nordström, Kent Petersson, and Jan M. Smith. 1990. Programming in Martin-Löf’s type theory. Oxford University Press Oxford.
[24] Jennifer Paykin, Robert Rand, and Steve Zdancewic. 2017. QWIRE: acore language for quantum circuits. In Proceedings of the 44th ACM
SIGPLAN Symposium on Principles of Programming Languages (ACM

Peng Fu, Kohei Kishida, and Peter Selinger
SIGPLAN Notices), Vol. 52. ACM, 846–858.
[25] Jennifer Paykin and Steve Zdancewic. 2017. The linearity monad. In
Proceedings of the 10th ACM SIGPLAN International Symposium on
Haskell (ACM SIGPLAN Notices), Vol. 52. ACM, 117–132.
[26] Benjamin C. Pierce and David N. Turner. 2000. Local type inference.
ACM Transactions on Programming Languages and Systems (TOPLAS)
22, 1 (2000), 1–44.
[27] Robert Rand, Jennifer Paykin, and Steve Zdancewic. 2018. QWIRE practice: Formal verification of quantum circuits in Coq. (2018). Available
from arXiv:1803.00699.
[28] Francisco Rios and Peter Selinger. 2017. A categorical model for aquantum circuit description language. In Proceedings of the 14th International Conference on Quantum Physics and Logic, QPL 2017, Nijmegen,
The Netherlands, 3-7 July 2017. 164–178.
[29] Neil J. Ross. 2015. Algebraic and logical methods in quantum computation. Ph.D. Dissertation. Dalhousie University, Department ofMathematics and Statistics. Available from arXiv:1510.02198.
[30] Robert A. G. Seely. 1984. Locally cartesian closed categories and typetheory. In Mathematical Proceedings of the Cambridge PhilosophicalSociety, Vol. 95. Cambridge University Press, 33–48.
[31] Peter Selinger and Benoît Valiron. 2006. A Lambda Calculus for Quantum Computation with Classical Control. Mathematical Structures in
Computer Science 16, 3 (2006), 527–552.
[32] Matthijs Vákár. 2015. A categorical semantics for linear logical frameworks. In Foundations of Software Science and Computation Structures 18th International Conference, FoSSaCS 2015. London, UK, April 11-18,
2015. Proceedings. 102–116.
[33] Benoît Valiron, Neil J. Ross, Peter Selinger, D. Scott Alexander, andJonathan M. Smith. 2015. Programming the quantum future. Commun.
ACM 58, 8 (2015), 52–61. https://doi.org/10.1145/2699415[34] Philip Wadler. 1990. Linear types can change the world!. In Programming Concepts and Methods, Vol. 3. Citeseer, 5.
[35] Philip Wadler and Stephen Blott. 1989. How to make ad-hoc polymorphism less ad hoc. In Proceedings of the 16th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages. ACM, 60–76.