From fc111e79f1d4aacc1cfe99ee358a861988be813c Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Wed, 7 Aug 2024 17:51:47 +0100 Subject: [PATCH 1/9] Common up note about exactly one incoming wire --- specification/hugr.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 763e10700..441c9c92d 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -791,15 +791,16 @@ There are two classes of type: `AnyType` $\supset$ `CopyableType`. Types in thes classes are distinguished by whether the runtime values of those types can be implicitly copied or discarded (multiple or 0 links from on output port respectively): -- For the broadest class (`AnyType`), the only operation supported is the identity operation (aka no-op, or `lift` - see [Extension Tracking](#extension-tracking) below). Specifically, we do not require it to be possible to copy or discard all values, hence the requirement that outports of linear type must have exactly one edge. (That is, a type not known to be in the copyable subset). All incoming ports must have exactly one edge. +- For the broadest class (`AnyType`), the only operation supported is the identity operation (aka no-op, or `lift` - see [Extension Tracking](#extension-tracking) below). Specifically, we do not require it to be possible to copy or discard all values, hence the requirement that outports of linear type must have exactly one edge. (That is, a type not known to be in the copyable subset). In fully qubit-counted contexts programs take in a number of qubits as input and return the same number, with no discarding. - The smaller 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 `Const` edges. Note: dataflow inputs (`Value`, `Const` and `Function`) always - require a single connection. + be sent down `Const` edges. + +Note that all dataflow inputs (`Value`, `Const` and `Function`) always require a single connection, regardless of whether the type is `AnyType` or `Copyable`. **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. When writing literal types, we use `#` to distinguish between tuples and rows, e.g. `(int<1>,int<2>)` is a tuple while `Sum(#(int<1>),#(int<2>))` contains two rows. From 5907b633ab0912bdf8e25cdb81ae83d74a06996a Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Wed, 7 Aug 2024 17:53:35 +0100 Subject: [PATCH 2/9] Variables are not bound by Function Types --- specification/hugr.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specification/hugr.md b/specification/hugr.md index 441c9c92d..779f94706 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -813,7 +813,7 @@ Extensions ::= (Extension)* -- a set, not a list Type ::= Sum([#]) -- disjoint union of rows of other types, tagged by unsigned int | Opaque(Name, [TypeArg]) -- a (instantiation of a) custom type defined by an extension | Function(#, #, Extensions) -- monomorphic function: arguments, results, and delta (see below) - | Variable -- refers to a TypeParam bound by the nearest enclosing FuncDefn node, or an enclosing Function Type + | Variable -- refers to a TypeParam bound by an the nearest enclosing FuncDefn node or polymorphic type scheme ``` (We write `[Foo]` to indicate a list of Foo's.) From c592eeee67316714b4db72542235aedaa6ff79d3 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Wed, 7 Aug 2024 17:57:13 +0100 Subject: [PATCH 3/9] Reorder TypeArgs to match TypeParams, correct below->above --- specification/hugr.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 779f94706..1ef750cf2 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -850,11 +850,11 @@ TypeArgs appropriate for the function's TypeParams: ```haskell TypeArg ::= Type(Type) -- could be a variable of kind Type, or contain variable(s) - | Extensions(Extensions) -- may contain TypeArg's of kind Extensions - | Variable -- refers to an enclosing TypeParam (binder) of any kind below | BoundedUSize(u64) + | Extensions(Extensions) -- may contain TypeArg's of kind Extensions | Sequence([TypeArg]) -- fits either a List or Tuple TypeParam | Opaque(Value) + | Variable -- refers to an enclosing TypeParam (binder) of any kind above ``` For example, a Function node declaring a `TypeParam::Opaque("Array", [5, TypeArg::Type(Type::Opaque("usize"))])` From 2aff32fb0168ebef0c8a8fdec47f7c37a3b5fe78 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Wed, 7 Aug 2024 18:14:35 +0100 Subject: [PATCH 4/9] Row Variables section. Need crosslinks in, more examples (elsewhere)? --- specification/hugr.md | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/specification/hugr.md b/specification/hugr.md index 1ef750cf2..2fa262c34 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -869,6 +869,25 @@ a valid type as long as the TypeArgs match the declared TypeParams, which can be (Note that within a polymorphic type scheme, type variables of kind `Sequence` or `Opaque` will only be usable as arguments to Opaque types---see [Extension System](#extension-system).) +#### Row Variables + +Type variables of kind `TypeParam::List(TypeParam::Type(_))` are known as +"row variables" and along with type parameters of the same kinds are given special +treatment, as follows: +* A `TypeParam` of such kind may be instantiated with not just a `TypeArg::List` + but also a single `TypeArg::Type`. (This is purely a notational convenience.) + For example, `Type::Function(usize, unit, )` is equivalent shorthand + for `Type::Function(#(usize), #(unit), )`. +* When a `TypeArg::Sequence` is provided as argument for such a TypeParam, we allow + the elements of the Sequence to be not just types (including variables of kind + `TypeParam::Type(_)`), but also row variables. These are implicitly spliced in + (appending with other elements). + +For example, a polymorphic FuncDefn might declare a row variable X of kind +`TypeParam::List(TypeParam::Type(Copyable))` and have as output a (tuple) type +`Sum([#(X, usize)])`. A call that instantiates said type-parameter with +`TypeArg::Sequence([usize, unit])` would then have output `Sum([#(usize, unit, usize)])`. + ### Extension Tracking The type of `Function` includes a set of [extensions](#extension-system) which are required to execute the graph. From d6838b700c7aee4cadbe5e484260f6b00290406a Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Thu, 8 Aug 2024 10:53:32 +0100 Subject: [PATCH 5/9] Try again re. RowVars --- specification/hugr.md | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 2fa262c34..083961d64 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -879,15 +879,18 @@ treatment, as follows: For example, `Type::Function(usize, unit, )` is equivalent shorthand for `Type::Function(#(usize), #(unit), )`. * When a `TypeArg::Sequence` is provided as argument for such a TypeParam, we allow - the elements of the Sequence to be not just types (including variables of kind - `TypeParam::Type(_)`), but also row variables. These are implicitly spliced in - (appending with other elements). + elements to be a mixture of both types (including variables of kind + `TypeParam::Type(_)`) and also row variables. When such variables are instantiated + (with other Sequences) the elements of the inner Sequence are spliced directly into + the outer (concatenating their elements), eliding the inner (Sequence) wrapper. For example, a polymorphic FuncDefn might declare a row variable X of kind `TypeParam::List(TypeParam::Type(Copyable))` and have as output a (tuple) type `Sum([#(X, usize)])`. A call that instantiates said type-parameter with `TypeArg::Sequence([usize, unit])` would then have output `Sum([#(usize, unit, usize)])`. +Note that since a row variable does not have kind Type, it cannot be used as the type of an edge. + ### Extension Tracking The type of `Function` includes a set of [extensions](#extension-system) which are required to execute the graph. From 9b5ec9c32500229f1b410ef5641f1884c0adf101 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Thu, 8 Aug 2024 10:53:51 +0100 Subject: [PATCH 6/9] RowVar example in declarative syntax --- specification/hugr.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/specification/hugr.md b/specification/hugr.md index 083961d64..d62d49bd5 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -889,6 +889,8 @@ For example, a polymorphic FuncDefn might declare a row variable X of kind `Sum([#(X, usize)])`. A call that instantiates said type-parameter with `TypeArg::Sequence([usize, unit])` would then have output `Sum([#(usize, unit, usize)])`. +See [Declarative Format](#declarative-format) for more examples. + Note that since a row variable does not have kind Type, it cannot be used as the type of an edge. ### Extension Tracking @@ -1170,6 +1172,14 @@ extensions: # outputs would be, in principle: Array(t) # - but default type scheme interpreter does not support such addition # Hence, no signature block => will look up a compute_signature in registry. + - name: TupleConcat + description: "Concatenate two tuples" + params: + a: List[Type] + b: List[Type] + signature: + inputs: Sum([a]), Sum([b]) + outputs: Sum([(a,b)]) # Syntax! Sum([a,b]) would be either-a-or-b, this has one variant - name: GraphOp description: "Involves running an argument Graph. E.g. run it some variable number of times." params: From e67b8ae26faf3ef28baf1df88029804a8dd6a7e1 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Thu, 8 Aug 2024 10:54:20 +0100 Subject: [PATCH 7/9] Updates re. no input extensions --- specification/hugr.md | 53 +++++++++++++++++-------------------------- 1 file changed, 21 insertions(+), 32 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index d62d49bd5..27415d446 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -896,9 +896,12 @@ Note that since a row variable does not have kind Type, it cannot be used as the ### Extension Tracking The type of `Function` includes a set of [extensions](#extension-system) which are required to execute the graph. -Every node in the HUGR is annotated with the set of extensions required to produce its inputs, -and each operation provides (a way to compute) the set of extensions required to execute the node, known as the "delta"; -the union of these two must match the set of extensions on each successor node. +Similarly, every dataflow node in the HUGR has a set of extensions required to execute the node (computed from its operation), also known as the "delta". The delta of any node must be a subset of its parent, +except for FuncDefn's: +* the delta of any child of a FuncDefn, must be a subset of the extensions in the FuncDefn's *type* +* the FuncDefn itself has no delta (trivially a subset of any parent): as no extensions are required +merely to know the code inside a FuncDefn; only a Call actually executes this, and the Call takes the delta +from the called FuncDefn's *type*. Keeping track of the extension requirements like this allows extension designers and third-party tooling to control how/where a module is run. @@ -915,36 +918,24 @@ running different extensions. By the same mechanism, the runtime can reason about where to run different parts of the graph by inspecting their extension requirements. -To allow extension annotations on nodes to be made equal, we will have operations - **lift** and **liftGraph** which can add extension constraints to values. +Special operations **lift** and **liftGraph** can add extension requirements: +* `lift>` is a node with input and output rows `R` and extension-delta `{E}` +* `liftGraph, E: ExtensionSet, O: List>` has one input +$ \vec{I}^{\underrightarrow{\;E\;}}\vec{O} $ and one output $ \vec{I}^{\underrightarrow{\;E \cup N\;}}\vec{O}$. +That is, given a graph, it adds extensions $N$ to the requirements of the graph. -$\displaystyle{\frac{v : [ \rho ] T}{\textbf{lift} \langle X \rangle (v) : [X, \rho] T}}$ +The latter is useful for higher-order operations such as conditionally selecting +one function or another, where the output must have a consistent type (including +the extension-requirements of the function). -**lift** - Takes as a node weight parameter the single extension -**X** which it adds to the -extension requirements of its argument. +# Having these as explicit nodes on the graph allows us to search for the +# point before extensions were added when we want to copy graphs, allowing +# us to get the version with minimal extension requirements. -$\displaystyle{\frac{f : [ \rho ] \textbf{Function}[R](\vec{I}, \vec{O})}{\textbf{liftGraph} \langle X \rangle (f) : [ \rho ] \textbf{Function}[X, R](\vec{I}, \vec{O})}}$ - -**liftGraph** - Like **lift**, takes an -extension X as a constant node -weight parameter. Given a graph, it will add extension -X to the requirements of the -graph. - -Having these as explicit nodes on the graph allows us to search for the -point before extensions were added when we want to copy graphs, allowing -us to get the version with minimal extension requirements. - -Graphs which are almost alike can both be squeezed into a -Conditional-node that selects one or the other, by wrapping them in a -parent graph to correct the inputs/outputs and using the **lift** -function from below. - -Note that here, any letter with vector notation refers to a variable -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`. +# Note that here, any letter with vector notation refers to a variable +# 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`. ### Rewriting Extension Requirements @@ -1623,8 +1614,6 @@ struct HUGR { struct Node{ // parent node index parent: Int, - // The input extensions to the node - input_extensions: Option // name of operation op: String //other op-specific fields From 2c1cb43a07ae2ae57c4b6e8c0142a3f8a0d24428 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Thu, 8 Aug 2024 10:54:52 +0100 Subject: [PATCH 8/9] driveby "in to" -> "into" --- specification/hugr.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specification/hugr.md b/specification/hugr.md index 27415d446..328beb685 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -976,7 +976,7 @@ tooling. These operations cover various flavours: - Instruction sets specific to a target. - Operations that are best expressed in some other format that can be - compiled in to a graph (e.g. ZX). + compiled into a graph (e.g. ZX). - Ephemeral operations used by specific compiler passes. A nice-to-have for this extensibility is a human-friendly format for From 1e85cf2326419f21d1797c3d08d6764ef44e73e8 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Tue, 20 Aug 2024 10:26:17 +0100 Subject: [PATCH 9/9] Review comments --- specification/hugr.md | 26 +++++++++----------------- 1 file changed, 9 insertions(+), 17 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 328beb685..53a71de6e 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -813,7 +813,7 @@ Extensions ::= (Extension)* -- a set, not a list Type ::= Sum([#]) -- disjoint union of rows of other types, tagged by unsigned int | Opaque(Name, [TypeArg]) -- a (instantiation of a) custom type defined by an extension | Function(#, #, Extensions) -- monomorphic function: arguments, results, and delta (see below) - | Variable -- refers to a TypeParam bound by an the nearest enclosing FuncDefn node or polymorphic type scheme + | Variable -- refers to a TypeParam bound by the nearest enclosing FuncDefn node or polymorphic type scheme ``` (We write `[Foo]` to indicate a list of Foo's.) @@ -896,12 +896,13 @@ Note that since a row variable does not have kind Type, it cannot be used as the ### Extension Tracking The type of `Function` includes a set of [extensions](#extension-system) which are required to execute the graph. -Similarly, every dataflow node in the HUGR has a set of extensions required to execute the node (computed from its operation), also known as the "delta". The delta of any node must be a subset of its parent, +Similarly, every dataflow node in the HUGR has a set of extensions required to execute the node (computed from its operation), +also known as the "delta". The delta of any node must be a subset of its parent's delta, except for FuncDefn's: -* the delta of any child of a FuncDefn, must be a subset of the extensions in the FuncDefn's *type* -* the FuncDefn itself has no delta (trivially a subset of any parent): as no extensions are required -merely to know the code inside a FuncDefn; only a Call actually executes this, and the Call takes the delta -from the called FuncDefn's *type*. +* the delta of any child of a FuncDefn must be a subset of the extensions in the FuncDefn's *type* +* the FuncDefn itself has no delta (trivially a subset of any parent): this reflects that the extensions +are not needed to *know* the FuncDefn, only to *execute* it +(by a Call node, whose delta is taken from the called FuncDefn's *type*). Keeping track of the extension requirements like this allows extension designers and third-party tooling to control how/where a module is run. @@ -928,15 +929,6 @@ The latter is useful for higher-order operations such as conditionally selecting one function or another, where the output must have a consistent type (including the extension-requirements of the function). -# Having these as explicit nodes on the graph allows us to search for the -# point before extensions were added when we want to copy graphs, allowing -# us to get the version with minimal extension requirements. - -# Note that here, any letter with vector notation refers to a variable -# 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`. - ### Rewriting Extension Requirements Extension requirements help denote different runtime capabilities. @@ -1169,8 +1161,8 @@ extensions: a: List[Type] b: List[Type] signature: - inputs: Sum([a]), Sum([b]) - outputs: Sum([(a,b)]) # Syntax! Sum([a,b]) would be either-a-or-b, this has one variant + inputs: [[null, Sum(a)], [null, Sum(b)]] # Sums with single variant are tuples + outputs: [[null, Sum([a,b])]] # Tuple of elements of a concatenated with elements of b - name: GraphOp description: "Involves running an argument Graph. E.g. run it some variable number of times." params: