Update Type System part of spec wrt "types redux" #401
Conversation
specification/hugr.md
Outdated
|
|
||
|
|
||
| ### Resources | ||
| <!--### Resources |
There was a problem hiding this comment.
This seemed to duplicate what was written earlier in the "Extension Implementation" section....shall I remove altogether?
| ``` | ||
| <!-- Graph(TypeParams, #, #, Resources) -- polymorphic, so move TypeParams section here |
There was a problem hiding this comment.
Not going here yet, until #285 fully resolved; if we do do this, we probably want to restructure so that Type System comes before Extension
specification/hugr.md
Outdated
| The type system will resemble the tierkreis type system, but with some | ||
| extensions. Namely, the things the tierkreis type system is missing are: | ||
| There are three classes of type, distinguished by the operations possible on (runtime) values of that type. (These loosely correspond to Tierkreis' notion of "constraints".) | ||
| - For the broadest class ("Any" type), the only operation supported is the identity operation (aka no-op, or `lift` - see [Resource Tracking](#resource-tracking) below). Specifically, these values cannot necessarily be copied or discarded, hence the linearity requirement that outports of these types must have exactly one edge. (All incoming ports must have exactly one edge connected to them.) |
There was a problem hiding this comment.
| - For the broadest class ("Any" type), the only operation supported is the identity operation (aka no-op, or `lift` - see [Resource Tracking](#resource-tracking) below). Specifically, these values cannot necessarily be copied or discarded, hence the linearity requirement that outports of these types must have exactly one edge. (All incoming ports must have exactly one edge connected to them.) | |
| - For the broadest class ("Any" type), the only operation supported is the identity operation (aka no-op, or `lift` - see [Resource Tracking](#resource-tracking) below). Specifically, these values cannot necessarily be copied or discarded, hence the requirement that outports of linear types must have exactly one edge. (All incoming ports must have exactly one edge connected to them.) |
specification/hugr.md
Outdated
|
|
||
| **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. | ||
|
|
||
| The core does not define any types** , only type constructors (that must be instantiated into types by providing some collection of types as arguments). These are given in the following grammar: |
There was a problem hiding this comment.
I think we should try and avoid footnotes; can you work the footnote text into the paragraph?
specification/hugr.md
Outdated
| Graphs are annotated with the resources that they need to run and, when | ||
| run, their outputs are annotated with those resources. Keeping track of | ||
| the resource requirements of graphs allows plugin designers and backends | ||
| ** the empty tuple type, aka `unit`, with exactly one instance (so 0 bits of data); the empty sum, with no instances; and the empty Graph (void -> void), are the only "leaf" types here. |
There was a problem hiding this comment.
I suppose that other graph signatures such as Sum((), ()) --> Sum((), ()) are also possible leaf nodes (not just void -> void)? Maybe even non-empty ones, such as "rotate the Tuple"? (I mean they can be defined without reference to any extension, but perhaps you mean something different...)
specification/hugr.md
Outdated
| the resource requirements of graphs allows plugin designers and backends | ||
| ** the empty tuple type, aka `unit`, with exactly one instance (so 0 bits of data); the empty sum, with no instances; and the empty Graph (void -> void), are the only "leaf" types here. | ||
|
|
||
| Graphs are Copyable, but not Equatable (as they represent functions: it is undecidable whether two functions produce the same result for all possible inputs, or similarly whether one computation graphs can be rewritten into another by semantic-preserving rewrites). |
There was a problem hiding this comment.
"one computation graphs"?
|
|
||
| ### Resource Tracking | ||
|
|
||
| The type of `Graph` includes a set of resources (that is, [Extensions](#extension-implementation)) which are required to execute the graph. Every node in the HUGR is annotated with the set of resources required to produce its inputs, and the set of resources required to execute the node; the union of these two must match the set of resources on each successor node. |
There was a problem hiding this comment.
| The type of `Graph` includes a set of resources (that is, [Extensions](#extension-implementation)) which are required to execute the graph. Every node in the HUGR is annotated with the set of resources required to produce its inputs, and the set of resources required to execute the node; the union of these two must match the set of resources on each successor node. | |
| The type of `Graph` includes a set of resources (that is, [Extensions](#extension-implementation)) which are required to execute the graph. Every node in the HUGR is annotated with the set of resources required to produce its inputs, and the set of resources required to execute the node; the union of these two must be a superset of the set of resources on each successor node. |
?
I'm thinking e.g. of a quantum node whose outputs are just some bits for classical post-processing (not requiring the quantum resource).
There was a problem hiding this comment.
I think you'd demarcate the part you want to run into the quantum computer in a separate graph, and then run in via a (Tierkreis, so probably higher-order) run_remote node (i.e. that takes a Graph[Quantum](...) and yet itself only needs Tierkreis resources). We don't want resource requirements to be dropped/forgotten or we'd conclude the containing graph could run anywhere when it actually needs quantum hardware...
specification/hugr.md
Outdated
|
|
||
|
|
||
| ### Resources | ||
| <!--### Resources |
specification/hugr.md
Outdated
| it so, we will have an operations called **lift** and **liftGraph** | ||
| which can add a resource constraints to values. | ||
| To allow resource annotations on nodes to be made equal, we will have operations | ||
| **lift** and **liftGraph** which can add a resource constraints to values. |
There was a problem hiding this comment.
| **lift** and **liftGraph** which can add a resource constraints to values. | |
| **lift** and **liftGraph** which can add resource constraints to values. |
|
Thanks Alec, many good points there. Feel free to take over, or merge when ready, @ss2165 and @aborgna-q too. |
| Resources ::= (Resource)* -- a set, not a list | ||
|
|
||
| Type ::= Tuple(#) -- fixed-arity, heterogenous components | ||
| | Sum(#) -- disjoint union of other types, ??tagged by unsigned int?? |
There was a problem hiding this comment.
this tagged by unsigned int was in here (a bit further down) before, and relates to the implementation and/or the tag operation, defined elsewhere. So this might want rewording. can be tagged by USize perhaps? or remove it, either with an implementation note elsewhere, or in whatever part of the prelude that defines the tag op ?
Not done function polymorphism, and have not added array (or indeed prelude) to standard library. @ss2165 were you in the process of doing that?