3 ms·

It's very concerning that the type system can't understand quantum teleportation without adding manual assertions verified by a state vector simulator (exponent

It's very concerning that the type system can't understand quantum teleportation without adding manual assertions verified by a state vector simulator (exponentially costly in number of qubits) [1]. Similarly, teleportation takes 13 lines to specify, instead of 13 characters [1]. For context, teleportation is like the swiss army knife of quantum computing. You're gonna be using variations of it everywhere so it'd better be easy to write and fast to check. As an analogy... imagine if declaring a local variable required you to manually request a runtime check that its address wasn't the same as the address of another local variable. It's ridiculous overhead for something that should be transparently correct. More fundamentally, as someone who has done some compiling of quantum algorithms down into gates, I don't see how it would have been useful to me to solve the problem that this language's type system solves (are two quantum states separable or entangled). In basically any algorithm I can picture, the qubits are all immediately entangled, and they stay entangled until they are measured. Almost any situation where a state goes from entangled to separable (without a measurement) is an opportunity to optimize that state out of the algorithm. The main exception I'm aware of is catalysis, where the catalyst state should be restored by the end. To me this language looks like I pay a huge boilerplate tax to receive a benefit I can't really use. I think they need to iterate more on how the type system can be helpful and on reducing boilerplate before I'd download it. [1] Fig 4 of https://dl.acm.org/doi/pdf/10.1145/3498691 https://dl.acm.org/doi/pdf/10.1145/3498691

krastanov 5y ago
From my superficial understanding, your goals (e.g. compilation into realistic gates) are very different from the goals of these language designers (study of abstract structure of quantum algorithms). Also, I tend to strongly disagree with your first paragraph: if teleportation was "built-in" for the language, then the language would be useless for anything but "numerics" - it would be a Fortran instead of being a Lisp. When you study abstract algorithmic structures, you want to be able to access such low-level implementations. And once they have defined their `teleport` function (in something like a standard library), they can reuse it wherever they want (hence addressing your worry).
- Strilanc 5y ago
  > your goals (e.g. compilation into realistic gates) are very different from the goals of these language designers (study of abstract structure of quantum algorithms) But the abstract structure of quantum algorithms is all about the carefully orchestrated structure within entanglement, not whether entanglement is present. Also, even just considering whether entanglement is present, the rules that they use in the language are far too weak. They basically amount to "if you do a two qubit operation it might be entangled". How is something like that ever going to help verify, for example, that already-allocated-but-currently-unused qubits being used as dirty ancillae (as in [1]) are being correctly restored (e.g. disentangled from the context where they were temporarily used)? It's just going to say "I dunno, they touched, they might be entangled". But I know they touched and might be entangled. I'm looking for a more gradual transition from "I applied no operations therefore everything is fine" to "I need to spin up a Turing complete simulator and do runtime analysis". > if teleportation was "built-in" for the language, then the language would be useless for anything but "numerics" I didn't mean to suggest hard-coding teleportation. What I was picturing is that the language would understand the stabilizer formalism [2], which is powerful enough to encode many quantum protocols but restricted enough to guarantee efficient classical analysis. Teleportation is a special case of things efficiently handled by the stabilizer formalism. 1: https://arxiv.org/abs/1611.07995 https://arxiv.org/abs/1611.07995 2: https://arxiv.org/abs/quant-ph/9705052 https://arxiv.org/abs/quant-ph/9705052
  - krastanov 5y ago
    Yup, I concur, it is a bit too weak currently, but my answer would be that I am really excited even for such baby steps, because it is so much more interesting of an approach than the (I would say) boring high-performance simulation libraries from google/ibm/other quantum startups/etc.
    - Strilanc 5y ago
      Hahaha, this is quite funny to me since I write some of those boring high performance simulation libraries. In my defense I'll note that e.g. Stim [1] isn't just fast; it has correctness tools. For example, stim circuits can include DETECTOR annotations that state which measurement sets should be deterministic. It's not a type system, but oh boy does verifying that information help a lot when debugging error correction circuits. I have other examples, but I digress. I would love if someone could make a type system that gave me similar benefits and scaled to complete algorithms. But a verbose system for keeping track of who-touched-who just isn't it. 1: https://quantum-journal.org/papers/q-2021-07-06-497/ https://quantum-journal.org/papers/q-2021-07-06-497/ or https://github.com/quantumlib/Stim/ https://github.com/quantumlib/Stim/
amluto 5y ago
I would argue that a language that can prove that the result of teleporting a pure state is pure is fairly neat. It’s not quite as nice as proving that it’s equal to the initial state, but it’s still nifty. I do agree that, for actual serious work on a hypothetical real large quantum computer, this ability may not be a high priority.
- Strilanc 5y ago
  But the language can't prove that. In the paper they show that it thinks the output is mixed until you add a manual assertion telling it to simulate the thing to check.
  - amluto 5y ago
    It’s also an odd feature of a programming language. Imagine the classical equivalent: square : constant integer -> constant integer square(2) is 4. square(4) is 8. square(readint()) doesn’t compile because readint() may return a mixture (if, say the user rolled a die and entered the result on the keyboard), so the input isn’t pure and you can’t square it. This is, of course, almost useless. (Amusingly, gcc can do this. asm’s "i" has precisely this restriction. Use with caution.)

krastanov 5y ago

From my superficial understanding, your goals (e.g. compilation into realistic gates) are very different from the goals of these language designers (study of abstract structure of quantum algorithms). Also, I tend to strongly disagree with your first paragraph: if teleportation was "built-in" for the language, then the language would be useless for anything but "numerics" - it would be a Fortran instead of being a Lisp. When you study abstract algorithmic structures, you want to be able to access such low-level implementations. And once they have defined their `teleport` function (in something like a standard library), they can reuse it wherever they want (hence addressing your worry).

Strilanc 5y ago
> your goals (e.g. compilation into realistic gates) are very different from the goals of these language designers (study of abstract structure of quantum algorithms) But the abstract structure of quantum algorithms is all about the carefully orchestrated structure within entanglement, not whether entanglement is present. Also, even just considering whether entanglement is present, the rules that they use in the language are far too weak. They basically amount to "if you do a two qubit operation it might be entangled". How is something like that ever going to help verify, for example, that already-allocated-but-currently-unused qubits being used as dirty ancillae (as in [1]) are being correctly restored (e.g. disentangled from the context where they were temporarily used)? It's just going to say "I dunno, they touched, they might be entangled". But I know they touched and might be entangled. I'm looking for a more gradual transition from "I applied no operations therefore everything is fine" to "I need to spin up a Turing complete simulator and do runtime analysis". > if teleportation was "built-in" for the language, then the language would be useless for anything but "numerics" I didn't mean to suggest hard-coding teleportation. What I was picturing is that the language would understand the stabilizer formalism [2], which is powerful enough to encode many quantum protocols but restricted enough to guarantee efficient classical analysis. Teleportation is a special case of things efficiently handled by the stabilizer formalism. 1: https://arxiv.org/abs/1611.07995 https://arxiv.org/abs/1611.07995 2: https://arxiv.org/abs/quant-ph/9705052 https://arxiv.org/abs/quant-ph/9705052
- krastanov 5y ago
  Yup, I concur, it is a bit too weak currently, but my answer would be that I am really excited even for such baby steps, because it is so much more interesting of an approach than the (I would say) boring high-performance simulation libraries from google/ibm/other quantum startups/etc.
  - Strilanc 5y ago
    Hahaha, this is quite funny to me since I write some of those boring high performance simulation libraries. In my defense I'll note that e.g. Stim [1] isn't just fast; it has correctness tools. For example, stim circuits can include DETECTOR annotations that state which measurement sets should be deterministic. It's not a type system, but oh boy does verifying that information help a lot when debugging error correction circuits. I have other examples, but I digress. I would love if someone could make a type system that gave me similar benefits and scaled to complete algorithms. But a verbose system for keeping track of who-touched-who just isn't it. 1: https://quantum-journal.org/papers/q-2021-07-06-497/ https://quantum-journal.org/papers/q-2021-07-06-497/ or https://github.com/quantumlib/Stim/ https://github.com/quantumlib/Stim/

amluto 5y ago

I would argue that a language that can prove that the result of teleporting a pure state is pure is fairly neat. It’s not quite as nice as proving that it’s equal to the initial state, but it’s still nifty. I do agree that, for actual serious work on a hypothetical real large quantum computer, this ability may not be a high priority.

Strilanc 5y ago
But the language can't prove that. In the paper they show that it thinks the output is mixed until you add a manual assertion telling it to simulate the thing to check.
- amluto 5y ago
  It’s also an odd feature of a programming language. Imagine the classical equivalent: square : constant integer -> constant integer square(2) is 4. square(4) is 8. square(readint()) doesn’t compile because readint() may return a mixture (if, say the user rolled a die and entered the result on the keyboard), so the input isn’t pure and you can’t square it. This is, of course, almost useless. (Amusingly, gcc can do this. asm’s "i" has precisely this restriction. Use with caution.)