Dear Andre, the answer, unfortunately, is no. At least we don't think so. We developed this programming language for IARPA, an agency of the U.S. government, and effectively nobody knows whether they have a quantum computer or not. In any case, the language is designed so that it *could* run on a quantum computer, if there was one. So now we are just standing by until somebody builds the hardware :) There is actually one kind of quantum computer that is already on the market: the DWave quantum computer. Unfortunately, our language is not compatible with it; the DWave machine uses a technology called "adiabatic quantum computing", and people are still figuring out how to program it. Our language would be compatible with quantum computers based on the quantum circuit model. Maybe the underlying point of your question is: why would anybody care about a quantum programming language, when there is no quantum computer? One possible answer is: to help figure out how much it would actually cost to build one. It is one thing for a quantum algorithm to appear in a research paper. You will find a lot of statements like "it is well-known that such-and-such can be done in O(n^2) operations", "by applying such-and-such trick this problem can be reduced to another problem with polynomial overhead", and so on. It is quite a different thing to actually program the algorithm, and to worry about how to do so efficiently. The difference between using 10^10 operations or 10^50 operations matters a lot in practice, but not in theory. Moreover, one can then account for additional overhead that people don't usually think about much, like the cost of adding many layers of error correction, physical fail-safe mechanisms, and so on. By coding up some algorithms for "realistic" problem sizes, we get a much better idea of what kind of computing resources this would actually require. ("Realistic" can be defined as the problem size where a hypothetical quantum computer would actually outperform a classical computer running the best known classical algorithm for the problem). Finally, there is some interesting theory that we can discover by considering programming languages for quantum computing. To our surprise, we even found a minor, yet satisfying, application of identity types from type theory. Best wishes, -- Peter Joyal, Andr?? wrote:

Dear Peter,

I would like to ask you a naive question:

Is it runned on an actual quantum computer?

Best, Andr??

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Dear Peter, I thank you for your answer. Is it possible to "simulate" quantum computing on ordinary computers? Operator algebra is matrix algebra. Surely, there will be a loss of efficiency. But it might help understanding the nature of quantum computations. Best wishes, -André -----Original Message----- From: Peter Selinger [mailto:selinger@mathstat.dal.ca] Sent: Thu 6/20/2013 3:36 PM To: Joyal, André Cc: Categories List Subject: Re: categories: Quipper: a quantum programming language Dear Andre, the answer, unfortunately, is no. At least we don't think so. We developed this programming language for IARPA, an agency of the U.S. government, and effectively nobody knows whether they have a quantum computer or not. In any case, the language is designed so that it *could* run on a quantum computer, if there was one. So now we are just standing by until somebody builds the hardware :) There is actually one kind of quantum computer that is already on the market: the DWave quantum computer. Unfortunately, our language is not compatible with it; the DWave machine uses a technology called "adiabatic quantum computing", and people are still figuring out how to program it. Our language would be compatible with quantum computers based on the quantum circuit model. Maybe the underlying point of your question is: why would anybody care about a quantum programming language, when there is no quantum computer? One possible answer is: to help figure out how much it would actually cost to build one. It is one thing for a quantum algorithm to appear in a research paper. You will find a lot of statements like "it is well-known that such-and-such can be done in O(n^2) operations", "by applying such-and-such trick this problem can be reduced to another problem with polynomial overhead", and so on. It is quite a different thing to actually program the algorithm, and to worry about how to do so efficiently. The difference between using 10^10 operations or 10^50 operations matters a lot in practice, but not in theory. Moreover, one can then account for additional overhead that people don't usually think about much, like the cost of adding many layers of error correction, physical fail-safe mechanisms, and so on. By coding up some algorithms for "realistic" problem sizes, we get a much better idea of what kind of computing resources this would actually require. ("Realistic" can be defined as the problem size where a hypothetical quantum computer would actually outperform a classical computer running the best known classical algorithm for the problem). Finally, there is some interesting theory that we can discover by considering programming languages for quantum computing. To our surprise, we even found a minor, yet satisfying, application of identity types from type theory. Best wishes, -- Peter Joyal, André wrote:

Dear Peter,

I would like to ask you a naive question:

Is it runned on an actual quantum computer?

Best, André

-----Original Message----- From: Peter Selinger [mailto:selinger@mathstat.dal.ca] Sent: Wed 6/19/2013 3:40 PM To: Categories List Subject: categories: Quipper: a quantum programming language

Dear Category Theorists,

we are proud to announce the first public release of Quipper, an embedded, scalable functional programming language for quantum computing. The Quipper distribution is available here:

http://www.mathstat.dal.ca/~selinger/quipper/

and includes extensive documentation, as well as seven worked examples of non-trivial quantum algorithms from the literature. Here are some highlights:

* High-level circuit description language, including both gate-by-gate descriptions and powerful higher-order operators for assembling and manipulating circuits.

* A monadic semantics, allowing for a mixture of procedural and declarative programming styles.

* Built-in facilities for automatic synthesis of reversible quantum circuits, including from classical Haskell code.

* Support for hierarchical circuits.

* Extensible quantum data types.

* Programmable circuit transformers (that are essentially monoidal functors).

* Support for a dynamic lifting operation to allow circuit generation to depend on parameters generated at circuit execution time.

* Extensive libraries of quantum functions, including: libraries for quantum integer and fixed-point arithmetic; the Quantum Fourier transform; an efficient quantum random access memory implementation; libraries for simulation of pseudo-classical circuits, Stabilizer circuits, and arbitrary circuits; libraries for exact and approximate decomposition of circuits into specific gate sets.

Comments are welcome!

Alexander S. Green Peter LeFanu Lumsdaine Neil Julien Ross Peter Selinger Benoit Valiron

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

P.S.: I think I might be required to include this disclaimer: Disclaimer: The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of IARPA, DoI/NBC, or the U.S. Government.

Dear Anthony, you asked a detail question, so I'll give a detailed answer. This may not be of interest to all the readers of this list, so I hope people will feel free to skip this message. As I mentioned, the application is a bit minor (but nevertheless fun). Suppose in Haskell (or another functional programming language), you need to define a data type F(X) that is parametric (often functorial) on another type X. One basic example is that of lists: data List x = Nil | Cons x (List x) For those not familiar with Haskell syntax, this simply corresponds to the categorical equation List(X) ~= 1 + X x List(X), which can be solved by taking an initial algebra of the functor F(A) = 1 + X x A. There are two constructors "Nil" and "Cons". Now suppose that, for some reason, we need a third constructor "Third", but we want that constructor to be available *only* when X is equal to some particular type X_0. In other words, we want: data List x = Nil | Cons x (List x) { when x is not x0 } data List x = Nil | Cons x (List x) | Third x { when x is x0 } It is of course not possible in Haskell to define a polymorphic type by case distinction like this. We could get around it by defining data List x = Nil | Cons x (List x) | Third x for all x, and making it a *convention* that the third constructor is only going to be used when x = x0. However, this does not work well, because many reasonable programs will not type-check. The problem arises when one needs to define a function from List x to some other type by case distinction. When it comes to the third case, the type checker cannot prove that x = x0, and in general, it may not be possible to define the desired function so that it works for arbitrary x. The solution is to define an identity type data Identity a b = Identity (a->b, b->a) and four functions reflexivity :: Identity a a symmetry :: Identity a b -> Identity b a transitivity :: Identity a b -> Identity b c -> Identity a c identity :: Identity a b -> a -> b. (And we make sure that no additional primitive functions of this type can be defined, for example by making it an abstract type). Then we can define data List x = Nil | Cons x (List x) | Third (Identity x x0) x And this does exactly the right thing. When it comes to doing a case distinction on the type List x, in the third case, we can actually *prove* that x is equal to x0, because the identity type contains a witness of this fact. The specific thing we needed this for in Quipper is in our library for arithmetic with fixed-but-arbitrary length quantum integers. We needed a type Int(X) representing integers in fixed-length binary notation, but using elements of the type X instead of the usual {0,1} as the digits. This gives us, for example, a type Int(Bool) of classical integers, and a type Int(Qubit) of quantum integers. Working with fixed-length integers is sometimes a bit tedious, because when you write an arithmetic expression such as 0 + a, you need to first specify what the length of 0 is, and then it needs to match the length of a. In order to infer this kind of information automatically, we added an alternative to the type Int(Bool), where one could store an ordinary integer (not yet specialized to a particular number of digits). However, this was only going to work for Int(Bool) and not, e.g., for Int(Qubit). So we used the above trick to do it. (Before starting a long discussion, I should add that we are of course aware that there are other ways of dealing with fixed-but-arbitrary length integers in Haskell, for example, by using type-level integers to parameterize a type Int(n) of n-bit integers. The above is just one particular example of something we did; I'm not saying that it is the only or even the best way to do it). -- Peter Anthony Bordg wrote:

Hi,

can you describe the application of identity types from type theory that you found ?

Best wishes

Anthony

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]