A sort of kind s, an object of the category of s, known at runtime.

The evidence a sort carries: objecthood.

The finite sets of ports with sorts of kind s, FH (Port xs).

The sorts of the ports of a sorted finite set.

The sort of a port.

A list of sorts, each an object known at runtime.

A list of sorts known at runtime.

The list of sorts as a value.

The sorts of the list, one by one.

The ports of a list of sorts: one for each position, of the sort at that position.

The finite sets whose elements have sorts of kind s: a full subcategory of FINHASK.

A list of sorts known at runtime as a type-level list.

Open hypergraphs with boxes labelled by l and wires of sorts of kind s.

The boundary with a wire for each sort in the list.

A box with a label, attached to nodes of type n by its inputs and its outputs.

Labelled boxes on the nodes of a sorted finite set. Two lists of boxes in a different order describe the same hypergraph, which isomorphic takes into account.

The sorts of the wires of a boundary.

One box with the given label, its inputs the wires of as and its outputs those of bs: a generator of the free hypergraph category.

The open hypergraph with the given nodes, boundaries and boxes. The first argument lists the sorts of the nodes, and a node is referred to by its position in that list, counting from 0. The second and third arguments give, for each wire of as and of bs in order, the node it is attached to, and each box lists the nodes of its inputs and of its outputs. A node that occurs several times joins all those wires and ports. Fails with a message unless every node referred to exists and every wire has a sort isomorphic to that of its node.

The product of a box a from x to y and a box b from y to z has nodes of the sorts x, y and z, with y shared between the boxes:

openHypergraph @'[x] @'[z] [sx, sy, sz] [0] [2] [Box a [0] [1], Box b [1] [2]]

openHypergraph without its checks, with the same arguments: the boundaries must have as many wires as their sorts, every wire and box must be attached to nodes that exist, and every wire must have the sort of its node. Only for hypergraphs that satisfy this by construction, such as those that simplify is given, which trusts the sorts to be equal.

An open hypergraph whose boundaries are known at runtime, for replacing a labelled box.

Replace every box by the diagram assigned to its label. Each replacement must have as many inputs and outputs as the box, in the same order, with isomorphic sorts. All replacements are glued together in one union-find pass. Shared nodes, repeated ports and isolated nodes are kept. Replacement labels are not substituted again.

Adapted from the functor-application construction in §9 of Wilson and Zanasi, Data-Parallel Algorithms for String Diagrams, restricted to an identity object map. This implementation uses maps and union-find rather than the paper's data-parallel representation.

Apply an object map and a generator map to an open hypergraph. Each source sort becomes a list of target sorts, and each box is replaced by a diagram with the expanded inputs and outputs. Every occurrence of a node uses the same expanded nodes, including repeated ports and boundaries. An empty list removes a node; an isolated node expands to one isolated node per target sort. The resulting boundaries are known at runtime, so the result is a SomeHypergraph.

The object map must send isomorphic source sorts to lists of pairwise isomorphic target sorts for composition to be preserved. Replacement boundaries are checked as in substitute.

Adapted from the functor-application construction in §9 of Wilson and Zanasi, Data-Parallel Algorithms for String Diagrams. This implementation uses lists, maps and union-find rather than the paper's data-parallel representation.

substituteWith without comparing sorts. Replacement boundaries must have the sorts specified by the object map, in order. Arity is still checked. For typed primitive translations whose source and replacement ports agree by construction; otherwise use substituteWith.

Whether two open hypergraphs differ only in the names of their nodes, the order of their boxes and their sorts up to isomorphism: a bijection between the nodes that keeps their sorts, agrees with both boundaries and takes the boxes of one to those of the other.

Whether two sorts are isomorphic.

An arrow of the strictified category of s whose lists of sorts are known at runtime, such as the interpretation of a box.

An arrow as one whose sorts are known at runtime.

Interpret a graph using the given wiring, for example readBack copyDiscard interpret graph or readBack (tracedWith permutations) interpret graph. Sorts supplied from outside are compared by DecidableIso; boxes are transported along the resulting isomorphisms. Unsupported incidences or feedback return an error.

Wiring operations, feedback and box scheduling. permutations and copyDiscard reject cycles; frobenius supplies its cup-and-cap trace. tracedWith replaces the feedback policy with the target's trace while keeping the wiring operations and contraction plan. Read-back reduces estimated swap cost; layered also places independent boxes side by side.

Only permutations: every node has one producer and one consumer. Nullary boxes and scalars are allowed; copying, merging and discarding need stronger wiring operations. With tracedWith, isolated loops are traced identities.

Each node has one producer and any number of consumers. Copy when a wire branches and discard it when unused. Boxes with unused outputs still run; copying and discarding need not be natural. Directed cycles are rejected unless tracedWith enables the target's trace. With tracing, nodes without producers feed themselves and their consumers through copying.

Frobenius spiders with sizes from Sized, planned as in frobeniusWith.

Frobenius spiders with the given wire sizes. State boxes are contracted as a tree, using the cheaper of numpy's greedy order and min-fill elimination. Remaining boxes follow a path; nodes are merged and discarded as soon as their other uses allow. This preserves the contraction planner used by einsum. Feedback uses the trace from Frobenius cups and caps. The given sizes also weight swap reduction, including wire routing within state contractions; routing preserves the contraction tree and its eliminated indices.

Use the target's trace for feedback, replacing the wiring's default feedback policy. For example, tracedWith copyDiscard supports copying, discarding and directed cycles.

Place independent boxes side by side with tensor, routing wires between layers. Swap reduction uses the wiring's existing sizes, or Sized when no sizes were supplied. Each crossing is weighted by the product of the wire sizes. Wiring operations and feedback are unchanged. Without this modifier boxes are placed one at a time, with uniform swap costs unless the wiring supplies sizes, as frobenius and frobeniusWith do.

Open hypergraphs whose boxes are arrows of k: the category to run a term of a hypergraph category in, with the arrows it uses made boxes by prim, to simplify it.

The label of a box of SIMPLIFY: the arrow the box was made from, whose sorts are those of the box. Made only by prim, so simplify can trust the sorts. Taking a label out of one hypergraph and attaching it to other nodes with openHypergraph breaks that trust.

An arrow as the label of a box with any sorts. Only for boxes whose sorts are equal to the arrow's by construction, as for unsafeOpenHypergraph.

An arrow of k between lists of objects as one box.

An arrow from the tensor unit as a box with no inputs and one output.

An arrow as a box with one input and one output.

An arrow from a tensor as a box with two inputs and one output.

An arrow from a left-associated tensor as a box with three inputs and one output. Reassociates the right-associated port list to the arrow's input tensor.

Read a primitive graph using the given wiring. Primitive sorts are trusted, so DecidableIso is unnecessary: for example, simplify copyDiscard graph can execute a graph as a Haskell function.

Interpret a primitive graph in its hypergraph target, with wire sizes from Sized. This is simplify with frobenius: every graph is supported and primitive sorts are trusted, so the result needs no Either.

simplifyHypergraph with every box bent into a state on all its wires, its inputs turned into outputs with cups. The read-back then contracts the whole network in the order of planContraction, instead of following the flow from inputs to outputs, and needs no traces for cycles. For computing with a term rather than drawing it, as the result is drawn with cups and caps.