Skip to content

Commit

Permalink
remove eq references from spec and example
Browse files Browse the repository at this point in the history
  • Loading branch information
ss2165 committed Jul 25, 2024
1 parent 58bf302 commit f686df1
Show file tree
Hide file tree
Showing 2 changed files with 7 additions and 13 deletions.
2 changes: 1 addition & 1 deletion hugr-core/examples/extension/declarative.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ extensions:
# Parameters are not currently supported.
name: CopyableType
description: A simple type with no parameters
# Types may have a "Eq", "Copyable", or "Any" bound.
# Types may have a "Copyable", or "Any" bound.
# This field is optional and defaults to "Any".
bound: Copyable
operations:
Expand Down
18 changes: 6 additions & 12 deletions specification/hugr.md
Original file line number Diff line number Diff line change
Expand Up @@ -785,24 +785,20 @@ indices after the list of node indices?

## Type System

There are three classes of type: `AnyType` $\supset$ `CopyableType` $\supset$ `EqType`. Types in these classes are distinguished by the operations possible on (runtime) values of those types:
There are two classes of type: `AnyType` $\supset$ `CopyableType`. Types in these
classes are distinguished by whether the runtime values of those types can be implicitly
copied or discard (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.

In fully qubit-counted contexts programs take in a number of qubits as input and return the same number, with no discarding.

- The next class is `CopyableType`, i.e. types holding ordinary classical
- 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.

- 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
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 (defined in an extension) would be a `CopyableType`, but not an `EqType`.

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

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:
Expand All @@ -823,9 +819,7 @@ Tuples are represented as Sum types with a single variant. The type `(int<1>,int

The majority of types will be Opaque ones defined by extensions including the [standard library](#standard-library). However a number of types can be constructed using only the core type constructors: for example the empty tuple type, aka `unit`, with exactly one instance (so 0 bits of data); the empty sum, with no instances; the empty Function type (taking no arguments and producing no results - `void -> void`); and compositions thereof.

Types representing functions are generally `CopyableType`, but not `EqType`. (It is undecidable whether two functions produce the same result for all possible inputs, or similarly whether one computation graph can be rewritten into another by semantic-preserving rewrites).

Sums are `CopyableType` (respectively, `EqType`) if all their components are; they are also fixed-size if their components are.
Sums are `CopyableType` if all their components are; they are also fixed-size if their components are.

### Polymorphism

Expand All @@ -834,7 +828,7 @@ While function *values* passed around the graph at runtime have types that are m
such declarations may include (bind) any number of type parameters, of kinds as follows:

```haskell
TypeParam ::= Type(Any|Copyable|Eq)
TypeParam ::= Type(Any|Copyable)
| BoundedUSize(u64|) -- note optional bound
| Extensions
| List(TypeParam) -- homogeneous, any sized
Expand Down

0 comments on commit f686df1

Please sign in to comment.