Dear Peter, thanks for your detailed answer and this interesting point. 2013/6/21 Peter Selinger <selinger@mathstat.dal.ca>

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

2013/6/20 Joyal, André <joyal.andre@uqam.ca>

...

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

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