-
Notifications
You must be signed in to change notification settings - Fork 5
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Update Type System part of spec wrt "types redux" #401
Changes from 3 commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change | ||||
---|---|---|---|---|---|---|
|
@@ -829,7 +829,7 @@ See [Type System](#type-system) for more on Resources. | |||||
|
||||||
# Import other header files to use their custom types | ||||||
# TODO: allow qualified, and maybe locally-scoped | ||||||
imports: [Quantum] | ||||||
imports: [Quantum, Array] | ||||||
|
||||||
resources: | ||||||
- name: MyGates | ||||||
|
@@ -908,8 +908,17 @@ The declaration of the `params` uses a language that is a distinct, simplified | |||||
form of the [Type System](#type-system) - writing terminals that appear in the YAML in quotes, | ||||||
the value of each member of `params` is given by the following production: | ||||||
``` | ||||||
TypeParam ::= "Type" | "ClassicType" | USize | "List"(TypeParam) | ||||||
TypeParam ::= "Type"("Any"|"Copy"|"Eq") | "USize" | "Resources" | "List"(TypeParam) | "Tuple"([TypeParam]) | Opaque | ||||||
|
||||||
Opaque ::= string<[TypeArgs]> | ||||||
|
||||||
TypeArgs ::= Type(Type) | USize(u64) | Resources | List([TypeArg]) | Tuple([TypeArg]) | ||||||
|
||||||
Type ::= Name<[TypeArg]> | ||||||
``` | ||||||
(We write `[Foo]` to indicate a list of Foo's; and omit `<>` where the contents is the empty list). | ||||||
|
||||||
To use an OpDef as an Op, or a TypeDef as a type, the user must provide a type argument for each type param in the def: a type in the appropriate class, a constant usize, a set of resources, a list or tuple of arguments. | ||||||
|
||||||
**Implementation note** Reading this format into Rust is made easy by `serde` and | ||||||
[serde\_yaml](https://github.com/dtolnay/serde-yaml) (see the | ||||||
|
@@ -980,97 +989,47 @@ indices after the list of node indices? | |||||
|
||||||
## Type System | ||||||
|
||||||
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.) | ||||||
|
||||||
In fully qubit-counted contexts programs take in a number of qubits as input and return the same number, with no discarding. See [quantum resource](#quantum-resource) for more. | ||||||
|
||||||
- User-defined types | ||||||
- Resource management - knowing what plugins a given graph depends on | ||||||
- The next class are "Copyable" types, aka "Classic" types, 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. | ||||||
|
||||||
A grammar of available types is defined below. | ||||||
- The final class are "Equatable" types: these are Copyable types where additionally there is a well-defined notion of equality between values. (While *some* notion of equality is defined on | ||||||
any type with a binary representation, that if the bits are equal then the value is, the converse is not necessarily true - values that are indistinguishable can have different bit representations.) | ||||||
|
||||||
For example, a `float` type would be Copyable, but not Equatable. | ||||||
|
||||||
**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. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I think we should try and avoid footnotes; can you work the footnote text into the paragraph? |
||||||
|
||||||
```haskell | ||||||
Type ::= [Resources]SimpleType | ||||||
-- Rows are ordered lists, not sets | ||||||
# ::= #(SimpleType) | ||||||
#(T) ::= (T)* | ||||||
|
||||||
Resources ::= (Resource)* -- set not list | ||||||
|
||||||
Container(T) ::= Tuple(#(T)) | ||||||
| Array<u64>(T) | ||||||
| NewType(Name, T) | ||||||
| Sum (#(T)) | ||||||
ClassicType ::= USize | ||||||
| Var(X) | ||||||
| String | ||||||
| Graph[R](#, #) | ||||||
| Opaque(Name, #) | ||||||
| Container(ClassicType) | ||||||
SimpleType ::= Qubit | ||||||
| QPaque(Name, #) | ||||||
| Container(SimpleType) -- Sometimes called 'Qontainer' | ||||||
| ClassicType | ||||||
|
||||||
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. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. this |
||||||
| Graph[Resources](#, #) -- monomorphic | ||||||
| Opaque(Name, TypeArgs) -- a (instantiation of a) custom type defined by an extension | ||||||
``` | ||||||
<!-- Graph(TypeParams, #, #, Resources) -- polymorphic, so move TypeParams section here | ||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 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 |
||||||
# | Variable -- refers to a TypeParam bound by an enclosing Graph--> | ||||||
|
||||||
SimpleTypes are the types of *values* which can be sent down wires, | ||||||
except for type variables `Var`. All of the ClassicTypes can also be | ||||||
sent down Static edges. | ||||||
|
||||||
Function signatures are made up of *rows* (\#), which consist of an | ||||||
arbitrary number of SimpleTypes, plus a resource spec. | ||||||
|
||||||
The `USize` type represents 64-bit unsigned integers. | ||||||
|
||||||
ClassicTypes such as `USize` are fixed-size, as is Qubit. | ||||||
`Sum` is a disjoint union tagged by unsigned int; `Tuple`s have | ||||||
statically-known number and type of elements, as does `Array<N>` (where | ||||||
N is a static constant). These types are also fixed-size if their | ||||||
components are. | ||||||
|
||||||
Container types are defined in terms of statically-known element types. | ||||||
Besides `Array<N>`, `Sum` and `Tuple`, these also include the variable-sized | ||||||
types: `Graph`. `NewType` | ||||||
allows named newtypes to be used. Containers are classic (copyable) only | ||||||
if all of their components are classic. | ||||||
|
||||||
Note: any array can be turned into an equivalent tuple, but arrays also | ||||||
support dynamically-indexed `get`. (TODO: Indexed by u64, with panic if | ||||||
out-of-range? Or by known-range `Sum( ()^N )`?) | ||||||
|
||||||
**Row Types** The `#` is a *row type* which consists of zero or more | ||||||
simple types. Types in the row can optionally be given names in metadata | ||||||
i.e. this does not affect behaviour of the HUGR. Row types are used | ||||||
|
||||||
- in the signatures for `Graph` inputs and outputs, and functions | ||||||
- Tuples - the 0-ary Tuple `()` aka `unit` takes no storage | ||||||
- Sums - allowing a bounded nat: `Sum((),(),())` is a ternary value; | ||||||
the 2-ary version takes the place of a boolean type | ||||||
- Arguments to `Opaque` types - where their meaning is | ||||||
extension-defined. | ||||||
|
||||||
### Linearity | ||||||
|
||||||
For expressing and rewriting quantum programs we draw a distinction between | ||||||
arbitrary `SimpleType`s and the subset of `ClassicType`s. Only `ClassicType`s | ||||||
may be used more than once or discarded; the former must always be used | ||||||
exactly once. This leads to a constraint on the HUGR that outgoing ports | ||||||
must have exactly one edge leaving them unless they are `ClassicType`, where | ||||||
outgoing ports may have any number of connected edges (0 is equivalent | ||||||
to a discard). All incoming ports must have exactly one edge connected to them. | ||||||
|
||||||
In fully qubit-counted contexts programs take in a number of qubits | ||||||
as input and return the same number, with no discarding. See | ||||||
[quantum resource](#quantum-resource) for more. | ||||||
|
||||||
### Resources | ||||||
|
||||||
The type of `Graph` has been altered to add | ||||||
*R*: a resource requirement. | ||||||
The *R* here refer to a set | ||||||
of [resources](#resources) which are required to produce a given type. | ||||||
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. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I suppose that other graph signatures such as |
||||||
|
||||||
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. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. "one computation graphs"? |
||||||
|
||||||
Tuples and Sums are Copyable (or Equatable) if all their components are, also are fixed-size if their components are. | ||||||
|
||||||
The majority of types will be defined by extensions including the [standard library](#standard-library). | ||||||
|
||||||
### 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. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 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) There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. OK, makes sense. |
||||||
|
||||||
Keeping track of the resource requirements like this allows extension designers and backends | ||||||
(like tierkreis) to control how/where a module is run. | ||||||
|
||||||
Concretely, if a plugin writer adds a resource | ||||||
|
@@ -1085,16 +1044,7 @@ running different resources. By the same mechanism, Tierkreis can reason | |||||
about where to run different parts of the graph by inspecting their | ||||||
resource requirements. | ||||||
|
||||||
### Type Constraints | ||||||
|
||||||
We will likely also want to add a fixed set of attributes to certain | ||||||
subsets of `TYPE`. In Tierkreis these are called “type constraints”. For | ||||||
example, a potential `HashMap` type can only be constructed when the type that we | ||||||
map from is `Hashable`. For the Hugr, we will need this `Hashable` | ||||||
constraint, as well as a `Classic` constraint. | ||||||
|
||||||
|
||||||
### Resources | ||||||
<!--### Resources | ||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This seemed to duplicate what was written earlier in the "Extension Implementation" section....shall I remove altogether? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yes I think so. |
||||||
|
||||||
On top of the Tierkreis type system, will be a system of Resources. A | ||||||
resource is a collection of operations which are available to use in | ||||||
|
@@ -1107,11 +1057,10 @@ resource they pertain to as a requirement. | |||||
|
||||||
Resources can be added and used by plugin writers. We will also have | ||||||
some built in resources, see | ||||||
[standard library](#standard-library) | ||||||
[standard library](#standard-library)--> | ||||||
|
||||||
Unification will demand that resource constraints are equal and, to make | ||||||
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. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
|
||||||
|
||||||
$\displaystyle{\frac{v : [ \rho ] T}{\textbf{lift} \langle X \rangle (v) : [X, \rho] T}}$ | ||||||
|
||||||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.