How to generate keys for Qref type?

[jakezweifler]

Related to #7, we want to map TQbit to TQref. In order to solve the no-cloning problem, TQref takes in a key, but how/when should these keys be generated? The key generation is a crucial part of lambda-Q# as it is necessary to ensure there are no unsafe programs.

[k4rtik]

Hi @jakezweifler, if we are restricting ourselves (for now) to the solution presented in the Q-Algol paper, then the keys need to be generated while translating from use declaration in Q# code. You will need to maintain a stack-like data structure (called signature and written as Σ in the paper) to hold these keys/symbols. The operations needed on this signature are push, pop and lookup.

Does that make sense?

[jakezweifler]

Ok, this makes sense but I am still unsure of how to proceed in terms of the type-checking since TQbit (in the Q# grammar) does not take any constructors. So when the key is generated how can it be associated to the type of the qubit?

[k4rtik]

@jakezweifler Indeed, TQbit doesn't require an argument as Q# doesn't distinguish between qubit identities. But while translating we are also trying to infer the identity of qubits, which we can do by adding a new key to the signature on each occurrence of qubit allocation (marked by use for simple cases) in the source language. When we encounter a usage of a qubit variable instead, we need to inspect the context (Γ, that holds the information var:type) to see if we have seen that variable before. For well-formed programs, we should already have an entry in the context, or we can reject the source program as incorrect.

There is also, of course, the third case where we exit the scope of the qubit -- we need to pop the qubit from the signature stack and remove/invalidate all bindings in the context for that type.

For this use case (qubit memory management), you can consider writing a couple of Q# programs manually and add them to the src/examples directory that will help you see the above three scenarios more clearly. A good starting point are the following two bad operations from the paper:

namespace QAlgol {
  operation NewQubit () : Qubit {
    use q = Qubit ();
    return q;
  }

  operation Clone () : Unit {
    use q1 = Qubit ();
    let q2 = q1 ;
    CNOT ( q1 , q2 );
  }
}