Wiring diagrams ↔ Lenses (SMC picture, Cartesian semantics)

Controls

Difficulty

Intro Intermediate Advanced

Tip: you can keep this on Intro and still click the “Explain” buttons.

Key claim

SMC is the syntax; cartesian lenses are the semantics for “wiring” when copying/deleting are allowed.

What changes vs “pure SMC”? one sentence

In an arbitrary SMC you don’t get “copy” and “discard” for free; in a cartesian category you do (diagonal + terminal), so a “wiring diagram” can be encoded as plain reindexing data, i.e. a lens in the free cartesian category of arities.

Three mental models pick one

Plumbing: each input gets its value from some earlier output or an external inlet.
Variable management: wiring is selecting/duplicating/dropping variables.
Bidirectional interface: forward picks external outputs; backward supplies internal inputs.

click ports change dropdowns open explainers

Interactive explainer

1) The SMC picture (string diagrams)

This is your starting point: boxes compose ◦ (series) and ⊗ (parallel). The twist is that Myers’ “wiring” usually also permits fanout and discard — which is cartesian structure.

If your “wiring diagrams” allow fanout/weakening, you’ve quietly assumed a cartesian (or at least comonoid‑enriched) monoidal structure.

2) Lenses: forward + backward

Myers packages “interface connection” as a lens in a cartesian category: a forward map plus a backward map that may depend on the forward‑flowing value.

intermediate+

Lens_C((A⁻/A⁺),(B⁻/B⁺)) ≅ C(A⁺,B⁺) × C(A⁺×B⁻,A⁻)

(This is exactly the definition Myers uses before specializing to Arity.)

Why lenses match “wiring” of open systems intermediate

“Forward” tells you what output appears at the outer interface; “backward” tells you how the outer environment’s inputs (plus the already‑computed inner outputs) determine the inner inputs. That is exactly what a wiring pattern does.

3) Arity = free cartesian “variable‑shuffling”

Think: objects are “tuples of wires”. A morphism in Arity is just a way to pick, duplicate, or drop coordinates.

Interactive reindexing

Let I = {a,b}, J = {1,2,3}. Choose a function f : J → I.

f(1) = f(2) = f(3) =

Duplicates = copy; missing = discard; permutation = swap. This is why “cartesian” matters.

Picture: copying & dropping coordinates

intermediate+

We draw wires from coordinate a or b into each output slot 1,2,3.

4) Wiring diagram = lens in Arity (interactive)

A wiring pattern is just two assignment functions: (i) which inner output becomes each outer output, and (ii) where each inner input gets its value from (an inner output or an outer input).

Choose the wiring

Outer output O comes from inner output Inner input i1 reads from Inner input i2 reads from

You’re literally choosing the maps w : B⁺ → A⁺ and w♯ : A⁻ → (A⁺ + B⁻).

In Arity, X^{A⁺}×X^{B⁻} ≅ X^{A⁺+B⁻}, so w♯ is a reindexing recipe.

See it as a wiring diagram

Blue = passforward (outer outputs). Purple = passback (supplying inner inputs from inner outputs or outer inputs).

The “equivalence” you wanted, said plainly intermediate

Your SMC intuition is the correct graphical calculus (series/parallel composition). Myers’ move is that when “wiring” also includes copy/delete, the right underlying algebra is cartesian reindexing; and a lens in the free cartesian category packages exactly the two pieces of wiring data (outer outputs chosen; inner inputs supplied).

Advanced: why “free cartesian” is the cleanest core advanced

In a cartesian monoidal category, every object has a canonical commutative comonoid (Δ, !), so you don’t separately axiomatize “duplication/weakening” as extra structure; the category of arities is then the initial such context, giving the most economical semantics for pure wiring. From there you can extend to typed arities and (via Lawvere theories) wiring with operations.