[TYPES] Quantun functional programming

[Andre van Tonder]

Hello Thorsten and Jonathan,

Indeed, aspects of your calculus reminded me a lot of the low-level 
implementation of a very simple simulator I wrote for mine in Scheme, 
which you can find at

   http://www.het.brown.edu/people/andre/qlambda/index.html

If I have time, I may try to adapt the simulator to execute a 
(type-erased) version of your calculus also.  It should be relatively 
easy.  You are of course welcome to play with it too if you feel so 
inclined.

Especially the section near the bottom "Simulator primitives" may look 
familiar to you.  I introduce a quantum nondeterministic operator "quamb", 
which corresponds to your { | }.

Then, for example, I can write the Hadamard gate as

   (define (H a)
     (case a
       [(0) (quamb (1/sqrt2 0) (1/sqrt2  1))]
       [(1) (quamb (1/sqrt2 0) (-1/sqrt2 1))]))

which looks similar to your version.  Executing at the prompt

   (qeval (H (H (H (H 0)))))

then gives

   (superposition (1.0 0))

It was the problem of maintaining unitarity and coherence when using 
"quamb" that led me to the eventual formulation of my calculus using 
linear logic.  I eventually did not use "quamb" due to the undecidability 
of ensuring orthogonality in the presence of recursion, unless perhaps 
the subterms in the "quamb" or { | } are restricted in a way that is 
probably equivalent to the eventual solution that I adopted, which was to 
take gates, such as "H", as primitives.  Linearity is then still required 
to prevent decoherence.

My version does not include weakening (corresponding to intermediate 
measurement).  This is presumably not a problem from a foundational point 
of view, since my calculus is universal (equivalent to the quantum Turing 
machine), and measurements can always be deferred until the end of the 
computation (see the teleportation example in my paper).  Still, 
being able to describe measurement explicitly is useful and I like the way 
that you have included it.

On the other hand, it seems that the absence of weakening makes 
higher-order types more natural (I construct a suitable monoidal 
closed category for them in my second paper) and recursion 
easier (as in the "untyped" version of my first paper).  It would be very 
interesting to see how your proposal for modeling higher order types in 
your framework works out...

Best regards
Andre van Tonder