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.
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/ or https://github.com/quantumlib/Stim/
Hey, when everyone else is falling back to "oh we just simulate the hard cases to verify them", making simulation faster is making verification better.
I do agree that, for actual serious work on a hypothetical real large quantum computer, this ability may not be a high priority.
square : constant integer -> constant integer
(Amusingly, gcc can do this. asm’s "i" has precisely this restriction. Use with caution.)
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