This paper presents a type-safe model of quantum computing, building upon the model introduced by Sabry in Haskell. By applying type-level programming techniques, we extend the model to constrain invalid operations and states at compile time. Our implementation enforces the no-cloning theorem at the type level via memory access patterns, while maintaining expressiveness via monadic composition of quantum operations. The implementation serves both as an introduction to quantum computing fundamentals and as a case study in enforcing physical constraints through a functional programming type system.
This paper presents a type-safe model of quantum computing, building upon the model introduced by Sabry in Haskell. By applying type-level programming techniques, we extend the model to constrain invalid operations and states at compile time. Our implementation enforces the no-cloning theorem at the type level via memory access patterns, while maintaining expressiveness via monadic composition of quantum operations. The implementation serves both as an introduction to quantum computing fundamentals and as a case study in enforcing physical constraints through a functional programming type system.
This thesis looks at the development of a framework for a functional quantum programming language. The framework is first developed in Haskell, looking at how a monadic structure can be used to explicitly deal with the side-effects inherent in the measurement of quantum systems, and goes on to look at how a dependently-typed reimplementation in Agda gives us the basis for a formally\nverified quantum programming language. The two implementations are not in themselves fully developed quantum programming languages, as they are embedded in their respective parent languages, but are a major step towards the development of a full formally verified, functional quantum programming language. Dubbed the “Quantum IO Monad”, this framework is designed following a structural approach as given by a categorical model of quantum computation.
We discuss the design of a typed lambda calculus for quantum computation. After a brief discussion of the role of higher-order functions in quantum information theory, we define the quantum lambda calculus and its operational semantics. Safety invariants, such as the no-cloning property, are enforced by a static type system that is based on intuitionistic linear logic. We also describe a type inference algorithm and a categorical semantics. 4.1 Introduction The lambda calculus, developed in the 1930s by Church and Curry, is a formalism for expressing higher-order functions. In a nutshell, a higher-order function is a function that inputs or outputs a “black box,” which is itself a (possibly higher-order) function. Higher-order functions are a computationally powerful tool. Indeed, the pure untyped lambda calculus has the same computational power as Turing machines (Turing 1937). At the same time, higher-order functions are a useful abstraction for programmers. They form the basis of functional programming languages such as LISP (McCarthy 1960), Scheme (Sussman and Steele 1975), ML (Milner 1978), and Haskell (Hudak et al. 2007). In this chapter, we discuss how to combine higher-order functions with quantum computation. We believe that this is an interesting question for a number of reasons. First, the combination of higher-order functions with quantum phenomena raises the prospect of entangled functions . Certain well-known quantum phenomena can be naturally described in terms of entangled functions, and we give some examples of this in Section 4.2.
We show that the model of quantum computation based on density matrices and superoperators can be decomposed into a pure classical (functional) part and an effectful part modelling probabilities and measurement. The effectful part can be modelled using a generalisation of monads called arrows. We express the resulting executable model of quantum computing in the Haskell programming language using its special syntax for arrow computations. However, the embedding in Haskell is not perfect: a faithful model of quantum computing requires type capabilities that are not directly expressible in Haskell.
This paper applies established techniques for concurrent programming in Haskell to the case of Concurrent Quantum Programming. The foundation of the approach is an extension to Concurrent Quantum Programming of the technique of “virtual values ” proposed by Amr Sabry for quantum programming in Haskell. The basic idea is to encapsulate quantum values within MVars, the monadic variables that support thread synchronization and mutually exclusive accesses to shared references. In this way, quantum processes can be concurring to have access to quantum values and we will be applying the now established quantum programming paradigm of “control is classic, data is quantum ” to the concurrent and distributed quantum programming domain: the case in focus is that the control of concurrency is classical control, while shared data between quantum processes are quantum data. We illustrate the use of the proposed approach by programming sample algorithms for quantum teleportation and quantum cryptographic key distribution. 1.
Qubit allocation is a process to assign physical qubits to logical qubits in a quantum program. Since some quantum computers have connectivity constraints on applications of two-qubit operations, it is mainly concerned with finding an assignment and inserting instructions to satisfy the connectivity constraints. Many methods have been proposed for the qubit allocation problem for low-level quantum programs. This paper presents a type-based framework of qubit allocation for a quantum programming language with first-order functions. In our framework, the connectivity constraints are expressed by a simple graph of qubits called a coupling graph. We formalize (1) the source language, whose type system verifies that the number of qubits required for a given program to run does not exceed the number of nodes of the coupling graph, (2) the target language, whose qualified type system verifies that a well-typed program satisfies the connectivity constraints, and (3) an algorithm to translate a source program into a target program. We prove that both languages are type-safe and that the translation algorithm is type preserving.
Based on the similarity between the categorial derivation of classical programs from their specification and the category theory approach to quantum physics, this dissertation aims at extending the laws of classical program algebra to quantum programming. In this context, the principles of the algebra of classical programs are applied to quantum programming, in order to verify the feasibility of creating correct-by-construction quantum circuits that can run on quantum devices available in the IBM Q Experience. The reversibility restrictions of quantum circuits are ensured by minimal complements. Moreover, measurements are postponed to the end of recursive computations called “quantamorphisms” to avoid the collapse of quantum states. Quantamorphisms are classical catamorphisms extended to ensure quantum reversibility. The derived quantamorphisms implement quantum cycles (vulg. for-loops) and quantum folds on lists. By Kleisli correspondence, quantamorphisms can be written as monadic functional programs with quantum parameters. This enables the use of Haskell, a monadic functional programming language, to perform the experimental work. The examples of the calculated quantum programs are simulated in Haskell, Quipper and QISKit and run on the quantum computers of the IBM Q Experience. The main conclusions of this work are that, while all the simulations produced correspond to the predicted results, running these programs on real quantum devices results in a significant amount of errors. As quantum devices are constantly evolving, it is likely that in the near future these devices will increase their reliability, allowing programs to run more accurately. The extension of the quantamorphism concept to more general input structures, such as finite trees, remains a challenge that is left for future work. Also relevant will be the study of conditional quantum control without measurements, which will extend the scope of quantamorphisms as quantum circuit specifications.