Twist: MIT’s Quantum Programming Language | Hacker News Reader

Twist: MIT’s Quantum Programming Language

spectrum.ieee.org

88 pointsgeorgehill18 comments

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

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).

> 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

2: https://arxiv.org/abs/quant-ph/9705052

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.

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/ or https://github.com/quantumlib/Stim/

Yup, I am a big fan of Stim, and work on similar tools in Julia. It is awesome to be able to run 1Gqubit Pauli multiplication in a few milliseconds, however I feel it is reasonable to call this "boring" high-performance libraries given how "fortran-ie" they still feel. Even if the application of these libraries is not boring at all (I have seen what Stim can do).

Ah, you're that krastanov. https://github.com/Krastanov/QuantumClifford.jl/commit/aafd5...

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.

You are right. And, practically, I probably will be using Stim much more in the next few years than this particular toy language. Same as you, I hope this toy language leads to more research in useful type theory for quantum algos.

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.

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.

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.)

Here’s the GitHub repo https://github.com/psg-mit/twist-popl22

I think this made the top of HN a few days ago: https://ionq.com/posts/june-24-2021-hello-many-worlds

I was disappointed that all of them were Python libraries (besides Microsoft's Q#, but I don't find a C#-like language attractive either), so I'm definitely interested in what it looks like coding in Twist.

I feel you. I write mostly Java code, but I've worked heavily with python + qiskit for quantum ML the past 3 months, and it's excellent. Qiskit is "low" level enough to give me the freedom I want, and with Jupyter Notebooks it's just so much easier to quickly construct something and evaluate, as well as extract it in a way I can put it in a paper.

C# and Java feels exactly the same to me now that Java has lambda/stream collection methods to match LINQ. Not sure how you feel there is any difference between the two. The only difficulty I have is when I have to work with Java Frameworks, even though I "never" use Java until I have to jump into a specific feature for other teams.

I never said there is a difference? I'm talking about Java <-> Python/qiskit/jupyter. Its a very different way of doing things, but just as enjoyable, and I'd say it's the currently best solution for any r&d and prototyping

This seems like the first "quantum programming language" that actually contributes something interesting, besides being yet another way to write low-level commands to your quantum simulator (or experiment). I am very excited to see a language where the type system and the rest of the construct actually contributes something useful, as opposed to yet another useless SDK.

Still prefer silq [0].

[0] https://silq.ethz.ch/

Reply on news.ycombinator.com