From 3412cb668e3ee2a748c638f03143158caf9f142a Mon Sep 17 00:00:00 2001 From: Seyon Sivarajah Date: Tue, 12 Dec 2023 13:55:09 +0000 Subject: [PATCH 01/10] clarify single input --- specification/hugr.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/specification/hugr.md b/specification/hugr.md index 93e9ceb53..bc4e02191 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1004,7 +1004,11 @@ There are three classes of type: ``AnyType`` $\supset$ ``CopyableType`` $\supset In fully qubit-counted contexts programs take in a number of qubits as input and return the same number, with no discarding. See [quantum extension](#quantum-extension) for more. - - The next class is ``CopyableType``, i.e. types holding ordinary classical data, where values can be copied (and discarded, the 0-ary copy). This allows multiple (or 0) outgoing edges from an outport; also these types can be sent down Static edges. + - The next class is ``CopyableType``, i.e. types holding ordinary classical + data, where values can be copied (and discarded, the 0-ary copy). This + allows multiple (or 0) outgoing edges from an outport; also these types can + be sent down Static edges. Note dataflow inputs (Value and Static) always + require a single a connection. - The final class is ``EqType``: these are copyable types with a well-defined notion of equality between values. (While *some* notion of equality is defined on From ef82c83a9250bd8cb83b484b0885a6d735b0e1a0 Mon Sep 17 00:00:00 2001 From: Seyon Sivarajah Date: Tue, 12 Dec 2023 17:19:00 +0000 Subject: [PATCH 02/10] clarify and consolidate locality --- specification/hugr.md | 88 +++++++++++++++++++++---------------------- 1 file changed, 44 insertions(+), 44 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index bc4e02191..56b3dabec 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -137,22 +137,13 @@ A `Static` edge can only carry a `CopyableType`. For more details see the [Type System](#type-system) section. As well as the type, dataflow edges are also parametrized by a -`Locality`. There are three possible localities: - - - `Local`: Source and target nodes must have the same parent. - - `Ext`: Edges "in" from an ancestor, i.e. where parent(src) == - parenti(dest) for i\>1; see - [Non-local Edges](#non-local-edges). - - `Dom`: Edges from a dominating basic block in a control-flow graph - that is the parent of the source; see - [Non-local Edges](#non-local-edges) +`Locality`, which declares whether the edge crosses levels in the hierarchy. See +[Edge Locality](#edge-locality) for details. ``` AnyType ⊃ CopyableType EdgeKind ::= Hierarchy | Value(Locality, AnyType) | Static(Local | Ext, CopyableType) | Order | ControlFlow - -Locality ::= Local | Ext | Dom ``` Note that a port is associated with a node and zero or more dataflow edges (adjoining @@ -533,50 +524,28 @@ may be a `FuncDefn`, `TailLoop`, `DFG`, `Case` or `DFB` node. | -------------- | ------------ | | Hierarchy | Defines hierarchy; each node has \<=1 parent | | Order, Control | Local (Source + target have same parent) | -| Value | Local, Ext or Dom - see [Non-local edges](#non-local-edges) | -| Static | Local or Ext - see [Non-local edges](#non-local-edges) | - -### Exception Handling - -#### Panic - - - Any operation may panic, e.g. integer divide when denominator is - zero - - Panicking aborts the current graph, and recursively the container - node also panics, etc. - - Nodes that are independent of the panicking node may have executed - or not, at the discretion of the runtime/compiler. - - If there are multiple nodes that may panic where neither has - dependences on the other (including Order edges), it is at the - discretion of the compiler as to which one panics first - -#### `ErrorType` +| Value | Local, Ext or Dom - see [Edge Locality](#edge-locality) | +| Static | Local or Ext - see [Edge Locality](#edge-locality) | - - There is some type of errors, perhaps just a string, or - `Tuple(USize,String)` with some errorcode, that is returned along with - the fact that the graph/program panicked. -#### Catch +### Edge Locality +There are three possible `CopyableType` edge localities: - - At some point we expect to add a first-order `catch` node, somewhat - like a DFG-node. This contains a DSG, and (like a DFG node) has - inputs matching the child DSG; but one output, of type - `Sum(O,ErrorType)` where O is the outputs of the child DSG. - - There is also a higher-order `catch` operation in the Tierkreis - extension, taking a graph argument; and `run_circuit` will return the - same way. + - `Local`: Source and target nodes must have the same parent. + - `Ext`: Edges "in" from a dataflow ancestor. + - `Dom`: Edges from a dominating basic block in a control-flow graph. -#### **Non-local Edges** -**For ``CopyableType`` values only** we allow dataflow edges (i.e. both Value and Static) +We allow non-local dataflow edged n1→n2 where parent(n1) \!= parent(n2) when the edge's locality is: * for Value edges, Ext or Dom; * for Static edges, Ext. + Each of these localities have additional constraints as follows: -1. For Ext edges, ** we require parent(n1) == - parenti(n2) for some i\>1, *and* for Value edges only there must be a order edge from parent(n1) to +1. For Ext edges, we require parent(n1) == + parenti(n2) for some i\>1, *and* for Value edges only there must be a order edge from n1 to parenti-1(n2). The order edge records the @@ -718,6 +687,37 @@ flowchart linkStyle 12,13,14,15,16,17 stroke:#ff3,stroke-width:4px; ``` +### Exception Handling + +#### Panic + + - Any operation may panic, e.g. integer divide when denominator is + zero + - Panicking aborts the current graph, and recursively the container + node also panics, etc. + - Nodes that are independent of the panicking node may have executed + or not, at the discretion of the runtime/compiler. + - If there are multiple nodes that may panic where neither has + dependences on the other (including Order edges), it is at the + discretion of the compiler as to which one panics first + +#### `ErrorType` + + - There is some type of errors, perhaps just a string, or + `Tuple(USize,String)` with some errorcode, that is returned along with + the fact that the graph/program panicked. + +#### Catch + + - At some point we expect to add a first-order `catch` node, somewhat + like a DFG-node. This contains a DSG, and (like a DFG node) has + inputs matching the child DSG; but one output, of type + `Sum(O,ErrorType)` where O is the outputs of the child DSG. + - There is also a higher-order `catch` operation in the Tierkreis + extension, taking a graph argument; and `run_circuit` will return the + same way. + + ### Operation Extensibility #### Goals and constraints From c08d265dbddc611720c2887dbe4f8a0fe4270677 Mon Sep 17 00:00:00 2001 From: Seyon Sivarajah Date: Tue, 12 Dec 2023 17:24:19 +0000 Subject: [PATCH 03/10] clarifications --- specification/hugr.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 56b3dabec..788286342 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -177,7 +177,7 @@ The root node has no non-hierarchy edges (and this supercedes any other requirem edges of specific node types). A _sibling graph_ is a subgraph of the HUGR containing all nodes with -a particular parent, plus any `Order`, `Value` and `ControlFlow` edges between +a particular parent, plus any `Order`, `Value` `Static`, and `ControlFlow` edges between them. #### `Value` edges @@ -197,8 +197,8 @@ these edges; see [operations](#node-operations). #### `Order` edges -`Order` edges represent constraints on ordering that may be specified -explicitly (e.g. for operations that are stateful). These can be seen as +`Order` edges represent explicit constraints on ordering between nodes +(e.g. useful for stateful operations). These can be seen as local value edges of unit type `()`, i.e. that pass no data, and where the source and target nodes must have the same parent. There can be at most one `Order` edge between any two nodes. From ceb3ee5997d1b79cf0dedddc186b7aa5d280a444 Mon Sep 17 00:00:00 2001 From: Seyon Sivarajah Date: Tue, 12 Dec 2023 17:30:58 +0000 Subject: [PATCH 04/10] remove mentions of DSG before definition --- specification/hugr.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 788286342..d8fede7e4 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -337,7 +337,7 @@ control-flow merge. A **TupleSum(T0, T1…TN)** type is an algebraic “sum of products” type, defined as `Sum(Tuple(#T0), Tuple(#T1), ...Tuple(#Tn))` (see [type -system](#type-system)), where `#Ti` is the *i*th Row defining it. +system](#type-system)), where `#Ti` is the *i*th row (sequence of types) defining it. ```mermaid flowchart @@ -395,7 +395,7 @@ The first child is the entry block and must be a `DFB`, with inputs the same as `Exit` node, whose inputs match the outputs of the CFG-node. The remaining children are either `DFB`s or [scoped definitions](#scoped-definitions). -The first output of the DSG contained in a `BasicBlock` has type +The first output of the graph contained in a `BasicBlock` has type `TupleSum(#t0,...#t(n-1))`, where the node has `n` successors, and the remaining outputs are a row `#x`. `#ti` with `#x` appended matches the inputs of successor `i`. @@ -404,7 +404,7 @@ Some normalizations are possible: - If the entry node has no predecessors (i.e. is not a loop header), then its contents can be moved outside the CFG node into a containing - DSG. + graph. - If the entry node has only one successor and that successor is the exit node, the CFG node itself can be removed. @@ -1016,7 +1016,7 @@ There are three classes of type: ``AnyType`` $\supset$ ``CopyableType`` $\supset For example, a `float` type (defined in an extension) would be a ``CopyableType``, but not an ``EqType``. Also, Hugr "classes" loosely correspond to Tierkreis' notion of "constraints". -**Row Types** The `#` is a *row type* which consists of zero or more types. Types in the row can optionally be given names in metadata i.e. this does not affect behaviour of the HUGR. +**Rows** The `#` is a *row* which is a sequence of zero or more types. Types in the row can optionally be given names in metadata i.e. this does not affect behaviour of the HUGR. The Hugr defines a number of type constructors, that can be instantiated into types by providing some collection of types as arguments. The constructors are given in the following grammar: @@ -1024,7 +1024,7 @@ The Hugr defines a number of type constructors, that can be instantiated into ty Extensions ::= (Extension)* -- a set, not a list -Type ::= Tuple(#) -- fixed-arity, heterogenous components +Type ::= Tuple(#) -- fixed-arity, heterogeneous components | Sum(#) -- disjoint union of other types, ??tagged by unsigned int?? | Function[Extensions](#, #) -- monomorphic | Opaque(Name, TypeArgs) -- a (instantiation of a) custom type defined by an extension From 3298710eb1d7cf7dc7837641d732b75daab3b3ed Mon Sep 17 00:00:00 2001 From: Seyon Sivarajah Date: Thu, 14 Dec 2023 17:30:15 +0000 Subject: [PATCH 05/10] update section in extension inference --- specification/hugr.md | 33 +++++++++------------------------ 1 file changed, 9 insertions(+), 24 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index d8fede7e4..c62ca356a 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1088,50 +1088,35 @@ which stands in for a row. Hence, when checking the inputs and outputs align, we’re introducing a *row equality constraint*, rather than the equality constraint of `typeof(b) ~ Bool`. -### Types of built-ins +### Rewriting Extension Requirements -We will provide some built in modules to provide basic functionality. -We will define them in terms of extensions. We have the “builtin” -extension which should always be available when writing hugr plugins. -This includes Conditional and TailLoop nodes, and nodes like `Call`: +Extensions requirements help denote different runtime capabilities. +For example, a quantum computer may not be able to handle arithmetic +while running a circuit, so its use is tracked in the function type so that +rewrites can be performed which remove the arithmetic. -$\displaystyle{\frac{\mathrm{args} : [R] \vec{I}}{\textbf{call} \langle \textbf{Function}[R](\vec{I}, \vec{O}) \rangle (\mathrm{args}) : [R] \vec{O}}}$ - -**Call** - This operation, like **to\_const**, uses its Static graph as -a type parameter. - -On top of that, we're definitely going to want modules which handle -graph-based control flow at runtime, arithmetic and basic quantum -circuits. - -These should all be defined as a part of their own extension -inferface(s). For example, we don’t assume that we can handle arithmetic -while running a circuit, so we track its use in the Graph’s type so that -we can perform rewrites which remove the arithmetic. - -We would expect standard circuits to look something like +Simple circuits may look something like: ``` Function[Quantum](Array(5, Q), (ms: Array(5, Qubit), results: Array(5, Bit))) ``` -A circuit built using our higher-order extension to manage control flow +A circuit built using a higher-order extension to manage control flow could then look like: ``` Function[Quantum, HigherOrder](Array(5, Qubit), (ms: Array(5, Qubit), results: Array(5, Bit))) ``` -So we’d need to perform some graph transformation pass to turn the +So the compiler would need to perform some graph transformation pass to turn the graph-based control flow into a CFG node that a quantum computer could -run, which removes the `HigherOrder` extension requirement: +run, which removes the `HigherOrder` extension requirement. ``` precompute :: Function[](Function[Quantum,HigherOrder](Array(5, Qubit), (ms: Array(5, Qubit), results: Array(5, Bit))), Function[Quantum](Array(5, Qubit), (ms: Array(5, Qubit), results: Array(5, Bit)))) ``` -Before we can run the circuit. ## Replacement and Pattern Matching From 71e6bed11c3a45b1ba1daa13764e82692d5049c7 Mon Sep 17 00:00:00 2001 From: Seyon Sivarajah Date: Thu, 14 Dec 2023 17:31:41 +0000 Subject: [PATCH 06/10] fix table formatting --- specification/hugr.md | 1 - 1 file changed, 1 deletion(-) diff --git a/specification/hugr.md b/specification/hugr.md index c62ca356a..e91424929 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1703,7 +1703,6 @@ Conversions between integers and floats: | Name | Inputs | Outputs | Meaning | | -------------- | --------- | ------------------------ | --------------------- | | `trunc_u` | `float64` | `Sum(int, ErrorType)` | float to unsigned int. Returns an error when the float is non-finite or cannot be exactly stored in N bits. | - | `trunc_s` | `float64` | `Sum(int, ErrorType)` | float to signed int. Returns an error when the float is non-finite or cannot be exactly stored in N bits. | | `convert_u` | `int` | `float64` | unsigned int to float | | `convert_s` | `int` | `float64` | signed int to float | From f3616c633fce4ed46ef9293e66fb442106537182 Mon Sep 17 00:00:00 2001 From: Seyon Sivarajah Date: Thu, 14 Dec 2023 17:35:43 +0000 Subject: [PATCH 07/10] remove to_const reference --- specification/hugr.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index e91424929..fd5edd257 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1734,14 +1734,14 @@ that *v* is lifted to have extension requirement R so that it matches the type of input to the next iterations of the loop. -$\displaystyle{\frac{\Theta : [R] \textbf{Function}[R](\vec{X}, \vec{Y}) \quad \vec{x} : [R] \vec{X}}{\textbf{call\\_indirect}(\Theta, \vec{x}) : [R] \vec{Y}}}$ +$\displaystyle{\frac{\Theta : [R] \textbf{Function}[R](\vec{X}, \vec{Y}) \quad \vec{x} : [R] \vec{X}}{\textbf{call\_indirect}(\Theta, \vec{x}) : [R] \vec{Y}}}$ **CallIndirect** - This has the same feature as **loop**: running a graph requires it’s extensions. -$\displaystyle{\frac{}{\textbf{to\\_const} \langle \textbf{Function}[R](\vec{I}, \vec{O}) \rangle (\mathrm{name}) : [\emptyset] \textbf{Function}[R](\vec{I}, \vec{O})}}$ +$\displaystyle{\frac{}{\textbf{load\_const} \langle \textbf{Function}[R](\vec{I}, \vec{O}) \rangle (\mathrm{name}) : [\emptyset] \textbf{Function}[R](\vec{I}, \vec{O})}}$ -**to_const** - For operations which instantiate a graph (**to\_const** +**load_const** - For operations which instantiate a graph (**load\_const** and **Call**) the functions are given an extra parameter at graph construction time which corresponds to the function type that they are meant to instantiate. This type will be given by a typeless edge from From 5de25953d248cf53d7b057d8bc041d7fce74da1b Mon Sep 17 00:00:00 2001 From: Seyon Sivarajah Date: Thu, 14 Dec 2023 17:38:22 +0000 Subject: [PATCH 08/10] rewroding for clarity --- specification/hugr.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specification/hugr.md b/specification/hugr.md index fd5edd257..ef734af3b 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1338,7 +1338,7 @@ remove it. (If there is an intergraph edge from `n0` to a descendent of ###### `InsertConstIgnore` -Given a `Const` node `c`, and optionally a DSG `P`, add a new +Given a `Const` node `c`, and optionally `P`, a parent of a DSG, add a new `LoadConstant` node `n` as a child of `P` with a `Static` edge from `c` to `n` and no outgoing edges from `n`. Also add an Order edge from the Input node under `P` to `n`. Return the ID of `n`. If `P` is From 2c4c8b5bf39522c2e289b1d0e8a7f33db13aac02 Mon Sep 17 00:00:00 2001 From: Seyon Sivarajah Date: Thu, 14 Dec 2023 17:38:48 +0000 Subject: [PATCH 09/10] integraph -> non-local --- specification/hugr.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specification/hugr.md b/specification/hugr.md index ef734af3b..c1edb167e 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1331,7 +1331,7 @@ nothing (but is not an error). ###### `RemoveOrder` Given nodes `n0` and `n1`, if there is an Order edge from `n0` to `n1`, -remove it. (If there is an intergraph edge from `n0` to a descendent of +remove it. (If there is an non-local edge from `n0` to a descendent of `n1`, this invalidates the hugr. TODO should this be an error?) ##### Insertion and removal of const loads From 7f6ff9cc3fd99988831363426ea64ffa4860bb6c Mon Sep 17 00:00:00 2001 From: Seyon Sivarajah Date: Fri, 15 Dec 2023 12:44:38 +0000 Subject: [PATCH 10/10] Apply suggestions from code review Co-authored-by: Alec Edgington <54802828+cqc-alec@users.noreply.github.com> --- specification/hugr.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index c1edb167e..3c6517dcf 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -536,7 +536,7 @@ There are three possible `CopyableType` edge localities: - `Dom`: Edges from a dominating basic block in a control-flow graph. -We allow non-local dataflow edged +We allow non-local dataflow edges n1→n2 where parent(n1) \!= parent(n2) when the edge's locality is: * for Value edges, Ext or Dom; @@ -1007,8 +1007,8 @@ There are three classes of type: ``AnyType`` $\supset$ ``CopyableType`` $\supset - The next class is ``CopyableType``, i.e. types holding ordinary classical data, where values can be copied (and discarded, the 0-ary copy). This allows multiple (or 0) outgoing edges from an outport; also these types can - be sent down Static edges. Note dataflow inputs (Value and Static) always - require a single a connection. + be sent down Static edges. Note: dataflow inputs (Value and Static) always + require a single connection. - The final class is ``EqType``: these are copyable types with a well-defined notion of equality between values. (While *some* notion of equality is defined on @@ -1090,7 +1090,7 @@ equality constraint of `typeof(b) ~ Bool`. ### Rewriting Extension Requirements -Extensions requirements help denote different runtime capabilities. +Extension requirements help denote different runtime capabilities. For example, a quantum computer may not be able to handle arithmetic while running a circuit, so its use is tracked in the function type so that rewrites can be performed which remove the arithmetic. @@ -1734,12 +1734,12 @@ that *v* is lifted to have extension requirement R so that it matches the type of input to the next iterations of the loop. -$\displaystyle{\frac{\Theta : [R] \textbf{Function}[R](\vec{X}, \vec{Y}) \quad \vec{x} : [R] \vec{X}}{\textbf{call\_indirect}(\Theta, \vec{x}) : [R] \vec{Y}}}$ +$\displaystyle{\frac{\Theta : [R] \textbf{Function}[R](\vec{X}, \vec{Y}) \quad \vec{x} : [R] \vec{X}}{\textbf{call\\_indirect}(\Theta, \vec{x}) : [R] \vec{Y}}}$ **CallIndirect** - This has the same feature as **loop**: running a -graph requires it’s extensions. +graph requires its extensions. -$\displaystyle{\frac{}{\textbf{load\_const} \langle \textbf{Function}[R](\vec{I}, \vec{O}) \rangle (\mathrm{name}) : [\emptyset] \textbf{Function}[R](\vec{I}, \vec{O})}}$ +$\displaystyle{\frac{}{\textbf{load\\_const} \langle \textbf{Function}[R](\vec{I}, \vec{O}) \rangle (\mathrm{name}) : [\emptyset] \textbf{Function}[R](\vec{I}, \vec{O})}}$ **load_const** - For operations which instantiate a graph (**load\_const** and **Call**) the functions are given an extra parameter at graph