docs: update spec for Row Variables and no-input-extensions #1402

acl-cqc · 2024-08-08T10:00:03Z

Also some driveby updates e.g. missed in #906.
Closes #1097, #745.

acl-cqc · 2024-08-08T10:00:24Z

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).


This was a driveby commoning up, see below

acl-cqc · 2024-08-08T10:01:08Z

specification/hugr.md

@@ -812,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


This dates back to #906!

Oops, by an the back to by an

acl-cqc · 2024-08-08T10:01:23Z

specification/hugr.md

          | BoundedUSize(u64)
+          | Extensions(Extensions) -- may contain TypeArg's of kind Extensions


just putting in same order as corresponding TypeParams

ss2165 · 2024-08-08T10:01:34Z

I don't think spec should be explicit about inference, I think that is more a feature of the reference implementation.

acl-cqc · 2024-08-08T10:01:59Z

specification/hugr.md

-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*


This is a bit awkward. Suggestions welcome

just remove the comma I think

acl-cqc · 2024-08-08T10:02:31Z

specification/hugr.md

-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.
+# Having these as explicit nodes on the graph allows us to search for the


Any point in keeping these sections I've commented out?

don't think so

acl-cqc · 2024-08-08T10:03:28Z

specification/hugr.md

+      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


Bleurgh. It'd be awkward to write these examples not in the "declarative format", but OTOH I don't think we are really moving in this direction, and it's very unclear how to write these ATM.

I think better just to say what it is in the comment

Suggested change

outputs: Sum([(a,b)]) # Syntax! Sum([a,b]) would be either-a-or-b, this has one variant

outputs: Sum([(a,b)]) # sum with a single variant of type (a, b)

ss2165

thanks!

ss2165 · 2024-08-08T13:23:16Z

specification/hugr.md

-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,


Suggested change

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,

ss2165 · 2024-08-08T13:34:25Z

specification/hugr.md

-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*


just remove the comma I think

ss2165 · 2024-08-08T13:42:49Z

specification/hugr.md

-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.
+# Having these as explicit nodes on the graph allows us to search for the


don't think so

ss2165 · 2024-08-08T13:44:38Z

specification/hugr.md

+      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


I think better just to say what it is in the comment

Suggested change

outputs: Sum([(a,b)]) # Syntax! Sum([a,b]) would be either-a-or-b, this has one variant

outputs: Sum([(a,b)]) # sum with a single variant of type (a, b)

acl-cqc added 8 commits August 8, 2024 10:01

Common up note about exactly one incoming wire

fc111e7

Variables are not bound by Function Types

5907b63

Reorder TypeArgs to match TypeParams, correct below->above

c592eee

Row Variables section. Need crosslinks in, more examples (elsewhere)?

2aff32f

Try again re. RowVars

d6838b7

RowVar example in declarative syntax

9b5ec9c

Updates re. no input extensions

e67b8ae

driveby "in to" -> "into"

2c1cb43

acl-cqc requested a review from a team as a code owner August 8, 2024 10:00

acl-cqc requested a review from aborgna-q August 8, 2024 10:00

acl-cqc commented Aug 8, 2024

View reviewed changes

aborgna-q requested review from ss2165 and removed request for aborgna-q August 8, 2024 10:07

ss2165 approved these changes Aug 8, 2024

View reviewed changes

Review comments

1e85cf2

acl-cqc enabled auto-merge August 20, 2024 09:34

acl-cqc added this pull request to the merge queue Aug 20, 2024

Merged via the queue into main with commit 67f0668 Aug 20, 2024
18 checks passed

acl-cqc deleted the acl/spec_rowvar_exts branch August 20, 2024 09:35

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

docs: update spec for Row Variables and no-input-extensions #1402

docs: update spec for Row Variables and no-input-extensions #1402

acl-cqc commented Aug 8, 2024 •

edited

Loading

acl-cqc Aug 8, 2024

acl-cqc Aug 8, 2024

acl-cqc Aug 20, 2024

acl-cqc Aug 8, 2024

ss2165 commented Aug 8, 2024

acl-cqc Aug 8, 2024

ss2165 Aug 8, 2024

acl-cqc Aug 8, 2024

ss2165 Aug 8, 2024

acl-cqc Aug 8, 2024

ss2165 Aug 8, 2024

ss2165 left a comment

ss2165 Aug 8, 2024

ss2165 Aug 8, 2024

ss2165 Aug 8, 2024

ss2165 Aug 8, 2024

		\| BoundedUSize(u64)
		\| Extensions(Extensions) -- may contain TypeArg's of kind Extensions

	outputs: Sum([(a,b)]) # Syntax! Sum([a,b]) would be either-a-or-b, this has one variant
	outputs: Sum([(a,b)]) # sum with a single variant of type (a, b)

	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,

docs: update spec for Row Variables and no-input-extensions #1402

docs: update spec for Row Variables and no-input-extensions #1402

Conversation

acl-cqc commented Aug 8, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ss2165 commented Aug 8, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ss2165 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

acl-cqc commented Aug 8, 2024 •

edited

Loading