Prototype a "lazify-measurement" hugr->hugr pass

[doug-q]

The h-series runtime wants to be lazy in using the results of measurements, to facilitate runtime pipelining.

I suggest we can achieve this with the following:

• create a lazy extension with
  • A custom type Lazy<T>
  • An operation lift<T>: T -> Lazy<T>
  • An operation read<T>: Lazy<T> -> T
• create a "quantum.tket2.lazy" extension with
  • A custom operation measure: Qubit -> (Qubit, Lazy<BOOL_T>)
• Create a hugr-> hugr pass that
• replaces all "quantum.tket2.measure" operations with "quantum.tket2.lazy.measure" operations.
• For all users of the BOOL_T result of "quantum.tket2.measure":
  • For Conditional control input, output-of-DataflowBlock control input, output-of-TailLoop control input, indirect call, call to public function, or custom op input: read the Lazy<BOOL_T> .
  • Otherwise modify the op to take a a Lazy<BOOL_T> and iterate
    Note that here a public function is either a FuncDecl or a function which is the target of LoadFunction

I intend to start with the Lazy<T> type being linear, and adding dup and free functions. I anticipate that lowerings will want to manage waitable "handles". dup will lower to "increment reference count" and free will lower to "decrement reference count". If making it linear ends up being too hard I will switch to non-linear to get something working.

This code should live in tket2-hseries

• #472
• #473
• #474
• #491
• #492

[doug-q]

Further thoughts:

I have implemented the minimum pass in the linked PR. This replaces measure with lazy_measure but instead of delaying the read for as long as possible, does it immediately. I think this is enough to move forward with codegen.

I think we should rename Lazy -> Future. We should remove the Lift operation.

In the lazify-measure pass, for now, we will replace values of type BOOL_T returned from quantum.tket2.measure with values of the sum type BOOL_T + Future<BOOL_T>. When the value is scrutinised (for example the control wire of a Conditional), we will insert a new Conditional node that either forwards the first variant or tket2.future.reads the second variant.

In the future we can introduce a Lazy<T> type, which has a lift (and map etc) operation, and which is lowered to T + Future<T>.

[acl-cqc]

The need for dup here is critical. If we didn't need to dup then we could take Lazy<BOOL_T> as QUBIT and read thereof as measure....

if (given) we do need dup then these Lazys have basically (exactly??) the same interface as Ptrs i.e. https://github.com/CQCL-DEV/hugrverse/issues/21 right?

[doug-q]

The need for dup here is critical. If we didn't need to dup then we could take Lazy<BOOL_T> as QUBIT and read thereof as measure....

if (given) we do need dup then these Lazys have basically (exactly??) the same interface as Ptrs i.e. CQCL-DEV/hugrverse#21 right?

They will lower to reference counted resources, so they are much the same as Ptrs. They replace bools, where out ports may have many uses. We do not necessarily have to make Lazy linear, in the same way we do not necessarily have to make Ptrs linear. If they are linear, then we need dup and free.

They are not exactly the same as Ptrs, they have no write op.

[acl-cqc]

They are not exactly the same as Ptrs, they have no write op.

Ah, yes, true. The writing is captured in the closure of how to compute the value.

And (importantly) this closure, even tho referred to by the non-linear/dup-able Lazy, can capture the linear QUBIT because it can only be called once.

Agreed Lazy/Future is a useful general thing to have. Is it any easier if we do something Qubit/measure-specific? I'm not sure it is (==> this is "develop Future extension", dependent on the Ptr extension - I think this Future effectively wraps some version of Ptr<Sum<QUBIT | Bool>>). Methinks the "push evaluation of lazy things downwards" applies generally and not just to Qubits.

I note also that there is a counterargument that we should do measurement early, to free up qubits for dynamic allocation. The usual instruction-scheduling/register-allocation phase-order problem, one might say ;-) :-(

[doug-q]

They are not exactly the same as Ptrs, they have no write op.

Ah, yes, true. The writing is captured in the closure of how to compute the value.

And (importantly) this closure, even tho referred to by the non-linear/dup-able Lazy, can capture the linear QUBIT because it can only be called once.

To be clear, nothing here constructs a Future<QB_T>, the only future type is Future<BOOL_T>, of course the extension does allow linear type args to Future.
We could disallow linear type args to Future if we decideFuture itself is not linear, or we could have the bound on Future depend on the bound of the type arg.

Agreed Lazy/Future is a useful general thing to have. Is it any easier if we do something Qubit/measure-specific? I'm not sure it is (==> this is "develop Future extension", dependent on the Ptr extension - I think this Future effectively wraps some version of Ptr<Sum<QUBIT | Bool>>).

This Future extension is not dependent on Ptr at all. They lower to different runtime calls. and Future will be represented as some integral index rather than a pointer.

Methinks the "push evaluation of lazy things downwards" applies generally and not just to Qubits.

This is why I have separated the futures and tket2.quantum.lazy extensions.

I note also that there is a counterargument that we should do measurement early, to free up qubits for dynamic allocation. The usual instruction-scheduling/register-allocation phase-order problem, one might say ;-) :-(

Please do see Lazy Measurements on confluence to see how I see this api evolving, in particular a wait_on_multiple_futures op.

I have dreams of introducing a Lazy extension which uses Future to offer a Monadic interface. This is not something one would want for a Ptr.

One can imagine we would would have different kinds of futures(in the future lol), representing different future-like interfaces offered by the runtime. In this world we would identify different kinds of futures by another type param.