Symmetric Control Flow Graphs

[zrho]

Quantum computation is a central use case for a HUGR. It appears to me that the ability to
write reversible code would a key feature, e.g. to power compute/uncompute patterns.
Our chosen representation for dataflow graphs
already lends itself quite nicely to this in comparison to other IRs, since it treats
inputs and output completely symmetrically. Reversing a dataflow graph is therefore as
simple as flipping the direction of all the edges and replacing each operation with
its inverse (if it exists, of course).

I would suspect that programs containing control flow graphs would be more difficult to
reverse. But to allow for the possibility, I suggest that we try and keep the encoding
of control flow symmetric as well. To achieve this, we would require the following
adjustments.

At this point, a control flow graph contains DataflowBlock nodes and Exit blocks.
The entry point of the control flow graph is the first DataflowBlock node, while
the exit point is the Exit block. To restore symmetry, I suggest that we introduce
an Entry block as well. This has the additional advantage that we no longer need
to preverse the order of the DataflowBlock nodes in the control flow graph, just
like we don't need to preserve the order of the operations in a dataflow graph.
Moreover, we obtain a nice symmetry between the Entry/Exit nodes of the control
flow graph and the Input/Output nodes of the dataflow graph. Even if we never
get to explore reversibility, these two additional points would make it worthwhile to me.

The second adjustment is to restore symmetry in the inputs and outputs of the
dataflow graphs within the DataflowBlocks. The first output of a DataflowBlock
node is special, and must be a sum type that is used to determine the next block
to jump to. The remaining outputs are additional data that is passed to the next
block, regardless of the branch taken. I quite like this design: it simultaneously
captures a simple conditional jump on a boolean value, with additional information
passed regardless of the branch, and a more complex conditional jump where the branches
can be passed different information. I suggest that the first input of the
dataflow region should similarly be a sum type, indicating the branch taken
to arrive at the block. This not only restores the symmetry in the encoding,
but also provides useful information.

With these changes in place, the IR for control flow becomes entirely symmetric.
This does not automatically make it reversible, but it provides a good starting
point for further exploration once reversible computation becomes a priority.
For instance, the information about the branch taken can be used to power the
assertions of RSSA.

I appreciate that lowering this to LLVM or MLIR might not be entirely trivial,
but I interpret that more as a sign that the IR chosen by those projects is
less suitable for reversible and quantum computation. Accommmodating reversible
computation in a HUGR could therefore be a unique selling point, further motivating
HUGR over trying to build directly upon LLVM or MLIR.

[doug-q]

Nice idea.

I don't see a good way of encoding the predecessor block. The out-edges of a DataflowBlock are ordered(by port), so the tag of a sum type encodes the edge to follow. However all in-edges of a DataflowBlock go to port 0, so how can the input sum value be interpreted as a predecessor?

Given a solution to the above, I don't think lowering this to llvm/mlir would be any more difficult.

[doug-q]

I suppose DataflowBlocks would have multiple in ports, each allowing at most one edge.

This would make mutating CFGs even more annoying, but that's not a deal breaker.

[zrho]

Yes, a port per incoming edge would be the idea. That also makes it symmetric with the way outgoing edges work.

[acl-cqc]

I suggest that the first input of the dataflow region should similarly be a sum type, indicating the branch taken
to arrive at the block

Note that the second part requires the first, but it's the second part that enables reversibility, and this is a non-trivial wellformedness constraint. (I.e. one must ensure that each predecessor sets the appropriate+unique tag.) I don't have anything against non-trivial wellformedness constraints ;) and wouldn't reject them even when make mutation significantly more awkward (removing a predecessor requires not only removing a port, shuffling all subsequent ports along, but also visiting each other predecessor and readjusting the Tag). But it is awkward....

What's the use of this fancy Sum type? Even if all variants contained the same information, say, so you extracted that in order to perform the rest of the block, you'll need to retain the tag and pass that onwards, right? Does(n't) this lead to infinite recursive types when there are loops? (I think there are similar issues with reversal of TailLoop nodes?)

If we require each control flow inport (now we have several) to have a unique predecessor, and then we "log" the extra branch/predecessor information out somehow, that'd be enough to reverse the computation. Of course that extra info is now part of the result, in some awkward format outside the Hugr, so this would not be "nice"....at all...