No more quantum and quantum_functional

[lmondada]

It is no secret, I have never liked having two functions for every gate type. But today is different -- I come with arguments and a concrete proposal that I hope you find convincing.

Argument

Most often, the borrowing signatures are most useful. However, there are cases where their functional equivalent would be nicer to use. I would much rather write:

@guppy
def plus_state() -> qubit:
     return h(qubit())

rather than

@guppy
def plus_state() -> qubit:
    q = qubit()
    h(q)
    return q

Starting to mix two functions for the same gate within my code is so ugly I would refuse to do so. But even discarding this subjective choice: using the two versions is not even an option for user-defined code: if I were to write my custom def my_hadamard, I would have to pick my poison and stick with it.

Concrete proposal

I propose to change the semantics of function definition and function calls in guppy as follows:

1. Every function is functional (i.e. we only keep quantum_functional)

2. However, we keep the current convention in the type signature: linear types have borrow-like semantics by default and must be tagged with @owned to take ownership.

3. When no linear resource is either created or destroyed, the return type can be easily inferred from the function arguments. In such cases specifying the return type and the return statement is optional (this is syntactic sugar). Specifically, an explicit return type and return statement are required if one of the following applies

   • A linear argument to the function is marked @owned
   • Ownership of a callee-created linear resource should be passed to the caller.

   Whenever none of these apply, the return type is inferred to be all linear typed arguments, in the same order.

4. We introduce the equivalent syntactic sugar also at the call site: whenever a function is called and both

   • the function is defined with an implicit return and
   • the outputs of the function are discarded

   are satisfied, we assign the output to the list of linear resources passed to the function.

5. Linear resources passed as function arguments not marked as @owned may not be discarded.

Advantages

• Support both functional and borrowed styles, as is the case currently.
• The borrowed style becomes more limited and is not supported on "complex" function types. This is IMO a feature, types such as def f(q: qubit) -> qubit are just plain confusing. Whenever linear resources are created or discarded, the user is encouraged to think and express explicitly where the resources go.
• These rules are unambiguous because they use the fact that linear types cannot be discarded implicitly. In all cases where syntactic sugar is introduced, any other interpretation of the code would be invalid.
• The type system is simplified: we do not need to introduce Rust-style borrowing and ownership concepts. Borrows can be recast as "syntactic sugar" and ownership as a tag "to consume a qubit".

Examples

@guppy
def cx(ctrl: qubit, target: qubit):
    ...

cx(q0, q1) # ok

# also ok:
def bell_state() -> (qubit, qubit):
    return cx(h(qubit()), qubit())

would be read as

@guppy
def cx(ctrl: qubit, target: qubit) -> (qubit, qubit):
    ...
    return (ctrl, target)

q0, q1 = cx(q0, q1)

def bell_state() -> (qubit, qubit):
    return cx(h(qubit()), qubit())

---

@guppy
def foo(qb: qubit): # implicit: -> qubit
    q = qubit()
    ...
    discard(q)
    # implicit: return qb

---

@guppy
def foo(qb: qubit):
    q = qubit()
    ... # no discard(q)
   # compiler error: you must either discard q or provide an explicit return statement

---

@guppy
def foo(qb: qubit) -> (qubit, qubit):
    q = qubit()
    ... # no discard(q)
   return (qb, q)  # ok; must be specified

foo(qb) # compiler error: this function has an explicit return, so outputs must be assigned explicitly: (qb, q) = foo(qb)

---

@guppy
def foo(qb: qubit @owned) -> qubit:
    return qubit()

foo(qb) # compiler error: this function has an explicit return, so outputs must be assigned explicitly: q = foo(qb)

---

@guppy
def foo(qb: qubit) -> (qubit, f64):
    # An explicit return type on a function that would have been eligible for implicit return    
    return (qb, 3.)

foo(qb) # compiler error: this function has an explicit return, so outputs must be assigned explicitly: q,  _ = foo(qb)

FAQ

Isn't @owned redundant?

It is true that @owned no longer changes the type of the argument -- this is the type simplification that is mentioned earlier. However, it signals the user's intention to consume the qubit. Concretely, it serves three purposes

• It forbids implicit returns
• It allows the callee to discard or measure the qubit
• It documents in the API that this qubit will (may) not be returned. The caller can otherwise assume her qubits are safe from destruction in function calls.