Linear dependent types for quantum circuit programming

Frank Fu
Dalhousie University
Joint work with: Kohei Kishida, Neil J. Ross, Peter Selinger

Feb 17, 2020, PL reading group, Maryland

QRAM modelCircuits

ClassicalQuantum

Measurement results

Quantum circuits

Quantum circuit programming languages

0000000000000000000000000• QISKit, Q#, Cirq, ProjectQ.
• Quipper.

0Linear types for quantum circuit programming• No-cloning: |φi 7→ |φi ⊗ |φi.
• Qwire.
• Proto-Quipper.

Linear types: A ( B, A ⊗ BDAf

EBhg
CP

Linear types: A ( B, A ⊗ BDAfEBhg

PC(1D ⊗ g ) ◦ (1D ⊗ 1E ⊗ h) ◦ (f ⊗ 1B )Linear types: A ( B, A ⊗ BDAf

EBhg

PC(1D ⊗ g ) ◦ (1D ⊗ 1E ⊗ h) ◦ (f ⊗ 1B )λ a b ->let (d, e) = f ac = h bp = g e cin (d, p)Parameters and states• Values that are known at circuit generation time (parameters).
• Values that are known at circuit execution time (states).
• For example, a family of circuits indexed by parameters.
• Qwire: parameters and states live in different name spaces.
• Proto-Quipper: parameters and states live in the same namespace.

Boxing and simple types• We use simple types to describe (quantum) states. E.g.,
Unit, Qubit, Qubit ⊗ Qubit.
• Box/unbox isomorphism.
box : (a ( b) → Circ(a, b)
unbox : Circ(a, b) → (a ( b)Note that a, b must be simple types.
• List of qubits is not a simple type because
List Qubit ∼= Unit + Qubit + Qubit ⊗ Qubit + ...

A problem with quantum data types• Can’t box qft : List Qubit ( List Qubit.
• Can’t reverse qft : List Qubit ( List Qubit.

A problem with quantum data types• Can’t box qft : List Qubit ( List Qubit.
• Can’t reverse qft : List Qubit ( List Qubit.
• Dependent types to the rescue.
qft : (n : Nat) ( (Vec Qubit n ( Vec Qubit n).
• Note that Vec Qubit n is a simple type.
⊗ QubitVec Qubit n ∼= Qubit|{z ⊗ ... ⊗ Qubit}nIncorporating linear and dependent types

Let f : (x : A) ( B[x] and a : A, what is the meaning off a : B[a]?
• Cervesato and Pfenning 1996. The term a is used twice,therefore it should be a parameter.
• McBride 2016. The term a in the type B[a] is not considered
used, it is only “comtemplated”.
• Our proposal (Fu, Kishida and Selinger 2020). The term a isused once, and the type B depends only on the shape of a.

Shape operation

Linear⊇ Parameters

Sh(Qubit)
Sh(List A)
Sh(A ⊗ B)
Sh((x : A) ( B[x])

====

Unit
List Sh(A)Sh A ⊗ Sh B
(x : Sh(A)) → Sh(B[x])Types depend on shapes• Kinding linear dependent types:
Φ, x : Sh(A) ` B[x] : ∗Φ ` (x : A) ( B[x] : ∗Types depend on shapes• Kinding linear dependent types:
Φ, x : Sh(A) ` B[x] : ∗Φ ` (x : A) ( B[x] : ∗• Typing rule for application:
Γ1 ` M : (x : A) ( B[x] Γ2 ` N : A
Γ1 + Γ2 ` MN : B[Sh(N)]For Γ2 ` N : A, we have:Sh(Γ2 ) ` Sh(N) : Sh(A)Proto-Quipper-D• A linear dependent type system for programming quantumcircuits.
• A categorical semantics based on state-parameter fibration.
• A prototype implementation of Proto-Quipper-D.
More details can be found in our recent drafts.
• “Linear dependent type theory for quantum programmingpanguages”, Fu, Kishida and Selinger, 2020.
• “An introduction to quantum circuit programming in
dependently typed Proto-Quipper”. Fu, Kishida, Ross andSelinger, 2020.

Demo. An implementation is available athttps://gitlab.com/frank-peng-fu/dpq-remake.

Thank you for your attention!