Safe Haskell	None
Language	GHC2024

Circuit.Poly.StringDiagram

Contents

String-diagram vocabulary
Running a diagram
Drawing skeleton (re-exported from Circuit.Diagram)

Description

A small string-diagram surface syntax over the Int construction.

The Int corridor turns a traced monoidal base category into a compact closed category. For the causal fragment of Poly — dependent lenses between monomial interfaces — the resulting diagrams are exactly the usual boxes-and-wires pictures: a wire is a polarity pair, a box is a causal lens, placing diagrams beside each other is tensor, chaining them is composition, and bending a wire back uses the compact-closed cap/cup.

This module aliases the underlying Int machinery with string-diagram names and runs the diagrams over 'Trace (,) (->)' so that feedback loops are tied into yanked traces.

The DSL is a deep embedding: every value remembers how it was built. That lets us interpret a diagram either as an executable IntMorph (via runDiagram) or as an untyped drawing skeleton (via skeleton) for a renderer such as chart-svg.

The skeleton also carries hypergraph syntax: multi-port boxes and spiders (SSpider, with sCopy / sMerge / sDelete / sCreate as the usual generators). Spiders are drawing-level syntax only — there are deliberately no spider constructors in the typed Diagram GADT, so skeleton never produces one. Structural comparison of the hyper fragment lives in Circuit.Diagram.Hyper.

Synopsis

type Wire a da = IN a da
data Diagram a da b db
wire :: Diagram a da a da
box :: Morphism (Mono da a) (Mono db b) -> Diagram a da b db
boxLabelled :: String -> Morphism (Mono da a) (Mono db b) -> Diagram a da b db
beside :: Diagram ap am bp bm -> Diagram cp cm dp dm -> Diagram (ap, cp) (am, cm) (bp, dp) (bm, dm)
thenD :: Diagram ap am bp bm -> Diagram bp bm cp cm -> Diagram ap am cp cm
bend :: Diagram (da, a) (a, da) () ()
bend' :: Diagram () () (a, da) (da, a)
turn :: Diagram a da b db -> Diagram db b da a
unitL :: Diagram ((), a) ((), da) a da
unitL' :: Diagram a da ((), a) ((), da)
unitR :: Diagram (a, ()) (da, ()) a da
unitR' :: Diagram a da (a, ()) (da, ())
assoc :: Diagram (a, (b, c)) (da, (db, dc)) ((a, b), c) ((da, db), dc)
assoc' :: Diagram ((a, b), c) ((da, db), dc) (a, (b, c)) (da, (db, dc))
swap :: Diagram (a, b) (da, db) (b, a) (db, da)
prismBox :: (s -> Either a s) -> (a -> s) -> Diagram s s (Either a s) (Either a s)
traceD :: Diagram (s, a) (s, da) (s, b) (s, db) -> Diagram a da b db
runDiagram :: Diagram a da b db -> (a, db) -> (da, b)
data SDiagram
- = SWire
- | SBox String Int Int
- | SSpider Int Int
- | SPrismBox
- | SBeside SDiagram SDiagram
- | SThenD SDiagram SDiagram
- | SBend
- | SBend'
- | STurn SDiagram
- | SUnitL
- | SUnitL'
- | SUnitR
- | SUnitR'
- | SAssoc
- | SAssoc'
- | SSwap
- | STrace SDiagram
skeleton :: Diagram a da b db -> SDiagram
sCopy :: SDiagram
sMerge :: SDiagram
sDelete :: SDiagram
sCreate :: SDiagram

String-diagram vocabulary

type Wire a da = IN a da Source #

A wire is a forward type paired with a backward type.

data Diagram a da b db Source #

A string diagram from one bundle of wires to another.

The base category is 'Trace (,) (->)' so that sequential composition can tie feedback knots.

wire :: Diagram a da a da Source #

The identity diagram: a straight wire.

In the Int construction identity is the symmetry that swaps the forward and backward factors.

box :: Morphism (Mono da a) (Mono db b) -> Diagram a da b db Source #

A box built from a causal dependent lens.

boxLabelled :: String -> Morphism (Mono da a) (Mono db b) -> Diagram a da b db Source #

A labelled box built from a causal dependent lens.

beside :: Diagram ap am bp bm -> Diagram cp cm dp dm -> Diagram (ap, cp) (am, cm) (bp, dp) (bm, dm) Source #

Place two diagrams side by side (tensor product).

thenD :: Diagram ap am bp bm -> Diagram bp bm cp cm -> Diagram ap am cp cm Source #

Chain two diagrams sequentially.

f ">>' g means "first f, then g" — i.e. categorical composition g . f.

bend :: Diagram (da, a) (a, da) () () Source #

Bend two wires back to form a cup (counit).

At object IN a da the cup consumes the dual pair IN (da, a) (a, da).

bend' :: Diagram () () (a, da) (da, a) Source #

Introduce two wires from nothing to form a cap (unit).

At object IN a da the cap produces IN (a, da) (da, a).

turn :: Diagram a da b db -> Diagram db b da a Source #

Turn a diagram around: dual in the compact closed sense.

unitL :: Diagram ((), a) ((), da) a da Source #

Left unitor: I u2297 A -> A.

unitL' :: Diagram a da ((), a) ((), da) Source #

Inverse left unitor: A -> I u2297 A.

unitR :: Diagram (a, ()) (da, ()) a da Source #

Right unitor: A u2297 I -> A.

unitR' :: Diagram a da (a, ()) (da, ()) Source #

Inverse right unitor: A -> A u2297 I.

assoc :: Diagram (a, (b, c)) (da, (db, dc)) ((a, b), c) ((da, db), dc) Source #

Associator: A u2297 (B u2297 C) -> (A u2297 B) u2297 C.

assoc' :: Diagram ((a, b), c) ((da, db), dc) (a, (b, c)) (da, (db, dc)) Source #

Inverse associator: (A u2297 B) u2297 C -> A u2297 (B u2297 C).

swap :: Diagram (a, b) (da, db) (b, a) (db, da) Source #

Symmetric braiding: A u2297 B -> B u2297 A.

prismBox :: (s -> Either a s) -> (a -> s) -> Diagram s s (Either a s) (Either a s) Source #

A prism box: partial access to a sum-shaped position.

Forward pass match :: s -> Either a s; backward pass uses build :: a -> s on the matched branch and the identity on the unmatched branch. Directions are identified with positions, the natural reading for set-valued polynomials.

traceD :: Diagram (s, a) (s, da) (s, b) (s, db) -> Diagram a da b db Source #

Hide a feedback wire: trace over the state s.

The body has one extra input/output pair s that is fed back to itself.

Running a diagram

runDiagram :: Diagram a da b db -> (a, db) -> (da, b) Source #

Run a closed string diagram on a concrete input.

The input is a forward value together with a backward cotangent; the output is the backward cotangent on the input side together with the forward value on the output side.

Drawing skeleton (re-exported from Circuit.Diagram)

data SDiagram Source #

Untyped drawing syntax for a string diagram.

This is what a renderer consumes. It discards the Haskell types but keeps the layout structure: boxes, wires, bends, swaps, composition and tensor.

Constructors

SWire	Straight identity wire.
SBox String Int Int	Box with a label, a number of input ports and a number of output ports.
SSpider Int Int	Spider node with an input arity and an output arity (hypergraph junction: all its ports share one wire class).
SPrismBox	Prism box.
SBeside SDiagram SDiagram	Two diagrams side by side (tensor product).
SThenD SDiagram SDiagram	Two diagrams chained (composition).
SBend	Cup (counit): bends two wires back to the unit.
SBend'	Cap (unit): introduces two wires from the unit.
STurn SDiagram	Dual (rotate 180°).
SUnitL	Left unitor `I ⊗ A -> A`.
SUnitL'	Inverse left unitor `A -> I ⊗ A`.
SUnitR	Right unitor `A ⊗ I -> A`.
SUnitR'	Inverse right unitor `A -> A ⊗ I`.
SAssoc	Associator `A ⊗ (B ⊗ C) -> (A ⊗ B) ⊗ C`.
SAssoc'	Inverse associator `(A ⊗ B) ⊗ C -> A ⊗ (B ⊗ C)`.
SSwap	Symmetric braiding `A ⊗ B -> B ⊗ A`.
STrace SDiagram	Trace: hide the last input/output pair as a feedback loop. A value `STrace d` represents a diagram `d` whose last input and last output are connected, removing one port from each boundary.

Instances

Instances details

Eq SDiagram Source #
Instance details Defined in Circuit.Diagram Methods (==) :: SDiagram -> SDiagram -> Bool # (/=) :: SDiagram -> SDiagram -> Bool #
Show SDiagram Source #
Instance details Defined in Circuit.Diagram Methods showsPrec :: Int -> SDiagram -> ShowS # show :: SDiagram -> String # showList :: [SDiagram] -> ShowS #

skeleton :: Diagram a da b db -> SDiagram Source #

Forget the types and extract the drawing skeleton.

sCopy :: SDiagram Source #

Copy spider: one input forked to two outputs.

sMerge :: SDiagram Source #

Merge spider: two inputs joined to one output.

sDelete :: SDiagram Source #

Delete spider: erases one input.

sCreate :: SDiagram Source #

Create spider: produces one output from nothing.