[HN Gopher] Twist: MIT's Quantum Programming Language
       ___________________________________________________________________
        
       Twist: MIT's Quantum Programming Language
        
       Author : georgehill
       Score  : 62 points
       Date   : 2022-02-19 09:28 UTC (2 days ago)
        
 (HTM) web link (spectrum.ieee.org)
 (TXT) w3m dump (spectrum.ieee.org)
        
       | Strilanc wrote:
       | 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
        
         | krastanov wrote:
         | 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 wrote:
           | > _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
        
             | krastanov wrote:
             | 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 wrote:
               | 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/
        
               | krastanov wrote:
               | 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).
        
               | Strilanc wrote:
               | 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.
        
               | krastanov wrote:
               | 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.
        
       | adamnemecek wrote:
       | Here's the GitHub repo https://github.com/psg-mit/twist-popl22
        
       | prophesi wrote:
       | 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.
        
         | Redimo wrote:
         | 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.
        
           | throw1234651234 wrote:
           | 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.
        
             | Redimo wrote:
             | 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
        
       | krastanov wrote:
       | 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.
        
       ___________________________________________________________________
       (page generated 2022-02-21 23:01 UTC)