Book contents
- Frontmatter
- Contents
- Contributors
- Preface
- 1 No-Cloning in Categorical Quantum Mechanics
- 2 Classical and Quantum Structuralism
- 3 Generalized Proof-Nets for Compact Categories with Biproducts
- 4 Quantum Lambda Calculus
- 5 The Quantum IO Monad
- 6 Abstract Interpretation Techniques for Quantum Computation
- 7 Extended Measurement Calculus
- 8 Predicate Transformer Semantics of Quantum Programs
- 9 The Structure of Partial Isometries
- 10 Temporal Logics for Reasoning about Quantum Systems
- 11 Specification and Verification of Quantum Protocols
- Index
- References
5 - The Quantum IO Monad
Published online by Cambridge University Press: 05 July 2014
- Frontmatter
- Contents
- Contributors
- Preface
- 1 No-Cloning in Categorical Quantum Mechanics
- 2 Classical and Quantum Structuralism
- 3 Generalized Proof-Nets for Compact Categories with Biproducts
- 4 Quantum Lambda Calculus
- 5 The Quantum IO Monad
- 6 Abstract Interpretation Techniques for Quantum Computation
- 7 Extended Measurement Calculus
- 8 Predicate Transformer Semantics of Quantum Programs
- 9 The Structure of Partial Isometries
- 10 Temporal Logics for Reasoning about Quantum Systems
- 11 Specification and Verification of Quantum Protocols
- Index
- References
Summary
Abstract
The quantum IO monad is a purely functional interface to quantum programming implemented as a Haskell library. At the same time it provides a constructive semantics of quantum programming. The QIO monad separates reversible (i.e., unitary) and irreversible (i.e., probabilistic) computations and provides a reversible let operation (ulet), allowing us to use ancillas (auxiliary qubits) in a modular fashion. QIO programs can be simulated either by calculating a probability distribution or by embedding it into the IO monad using the random number generator. As an example we present a complete implementation of Shor's algorithm.
5.1 Introduction
We present an interface from a pure functional programming language, Haskell, to quantum programming: the quantum IO monad, and use it to implement Shor's factorization algorithm. The implementation of the QIO monad provides a constructive semantics for quantum programming, i.e., a functional program that can also be understood as a mathematical model of quantum computing. Actually, the Haskell QIO library is only a first approximation of such a semantics; we would like to move to a more expressive language that is also logically sound. Here we are thinking of a language such as Agda (Norell 2007), which is based on Martin Löf's type theory. We have already investigated this approach of functional specifications of effects in a classical context (Swierstra and Altenkirch 2007, 2008; Swierstra 2008). At the same time the QIO monad provides a high-level interface to a hypothetical quantum computer.
- Type
- Chapter
- Information
- Semantic Techniques in Quantum Computation , pp. 173 - 205Publisher: Cambridge University PressPrint publication year: 2009
References
- 16
- Cited by