circuits 0.1.0.0 → 0.2.0.0

raw patch · 25 files changed

+3933/−1644 lines, 25 filesdep +stm

Dependencies added: stm

Files

• ChangeLog.md +74/−22
• circuits.cabal +23/−25
• other/axioms.md +0/−356
• other/circuits-class.html +87/−0
• other/circuits-module.html +99/−0
• other/symbols.md +0/−238
• readme.md +155/−69
• src/Circuit.hs +175/−67
• src/Circuit/Algebra.hs +406/−0
• src/Circuit/Category.hs +105/−0
• src/Circuit/Channel.hs +466/−0
• src/Circuit/Circuit.hs +0/−145
• src/Circuit/Classes.hs +0/−42
• src/Circuit/Dagger.hs +279/−0
• src/Circuit/Discrete.hs +107/−0
• src/Circuit/Ends.hs +430/−0
• src/Circuit/Free.hs +103/−0
• src/Circuit/Hyper.hs +115/−91
• src/Circuit/Layer.hs +106/−0
• src/Circuit/Loop.hs +261/−0
• src/Circuit/Monoidal.hs +0/−199
• src/Circuit/Net.hs +341/−0
• src/Circuit/Sym.hs +140/−0
• src/Circuit/Tensor.hs +461/−0
• src/Circuit/Traced.hs +0/−390

@@ -1,25 +1,77 @@ # Revision history for circuits -## 0.1.0.0 — 2025-05-26+## 0.2.0.0 — 2026-07-20 -- Initial release (not yet published to Hackage).-- **Circuit** — GADT: Lift, Compose, Knot. Free traced monoidal category with Profunctor instance.-- **Hyper** — final coinductive encoding. Category, Profunctor, Functor instances. Feedback dissolves into the type.-- **Trace** class with `(,)` (lazy knot) and `Either` (iteration) tensors. `Trace (Kleisli IO) Either` via delimited continuations.-- Triangle identity: `reify = lower . encode`. `flatten` for the reverse direction (lossy).-- `ambient` / `ambientBy` — state wire threading through feedback loops.-- Cocartesian combinators in `Circuit.Monoidal`: `coassoc`, `coassoc'`, `coseed`, `coabsorbL`, `coabsorbR`, `coreleaseL`, `coreleaseR`.-- `Braided` class with instances for `(,)` and `Either` — merged with cartesian/cocartesian structure into `Circuit.Monoidal`.-- `cellIO` — stateful `Kleisli IO` arrow via `IORef` for strict accumulators in `(,)`-traced pipelines.-- Removed `Circuit.Queue` and `these` dependency — consolidated into `circuits-io`.-- Removed `Iter`/`loopIter` — duplicates `Trace (Kleisli m) Either`.-- Canonical API uses lowercase names: `lift`, `lower`, `reify`, `encode`, `push`, `run`, `trace`, `untrace`.-- Notation conventions in `other/symbols.md`. No `Circuit.Symbols` module — symbols are prose notation, not Haskell identifiers.-- Narrative arc in `other/`: marks → GADT → Hyper → tensors → Mendler case → making stuff.-- 15+ example cards: parsers, pipes, while-loops, Elgot iteration, delimited continuations, proequipment, ambient, hyper-chain, state, pure-queue, etc.-- Boundary rule: symbols in tables/axioms only; names everywhere else.-- `Step` convention unified with `Trace (->) Either`: `Left` = feedback, `Right` = exit.-- Push is Hyper-only — no direct GADT counterpart.-- Axiom doctests and QuickCheck properties for JSV laws and Hyper embedding/functoriality.-- No Applicative or Monad instances — these collapse feedback structure.-- README: tank mode, Hackage/CI badges, paper link.+Total revamp of the API around a single normal-form GADT and a clearer+separation between syntax and semantics.++*New core vocabulary*++- `Circuit.Loop.Loop t arr a b` is the free traced monoidal category in+  normal form: either `Lift` (a base arrow) or `Knot` (a feedback loop).+  Composition fuses via the `Category` instance, so every value has at most+  one `Knot` at the top.+- `Circuit.Free.Free` is the free category (`Lift`, `Compose`).+- `Circuit.Sym.Sym` is the free symmetric monoidal category (`Lift`,+  `Compose`, `Par`, `Swap`).+- `Circuit.Net.Net` is the free traced PROP with a bimonoid: `Lift`,+  `Compose`, `Par`, `Swap`, `Knot`, `Copy`, `Discard`, `Plus`, `Zero`.+  Wiring stays inspectable for `transpose`, metering, and fusion.+- `Circuit.Hyper.Hyper` is the final coinductive encoding; `encode` and+  `observe` move between `Loop` and `Hyper`.++*Semantics split across two tracks*++- Structural semantics: `Circuit.Category.Category` → `Circuit.Channel.Channel`+  → `Circuit.Channel.Strength` → `Circuit.Channel.Traced`.+- Functorial semantics: `Circuit.Category.Category` → `Circuit.Tensor.Tensor`+  → `Circuit.Tensor.Action`.++*Layer tower*++- `Circuit.Layer.Layer` unifies the free-forgetful folds: `unit`, `run`,+  `bind`, `lower`. `Law`, `Run`, and `Bind` associated types capture what+  each layer needs from its target and source categories.++*Ends, boxes, and queues*++- `Circuit.Ends` replaces the old `Circuit.Box` and `Circuit.Queue` modules.+  Companion/conjoint ends (`Out`, `In`), matched `Ends`, `box`,+  `boxAsymmetric`, `Queue` strategies, `openSTM`, and `openIO` all live here.++*Dagger and bimonoid*++- `Circuit.Dagger` consolidates `CopyDiscard`, `MergeZero`, `Bimonoid`,+  `Dagger`, and `transpose`.++*À-la-carte syntax*++- `Circuit.Algebra` provides compositional signatures (`SigCompose`,+  `SigKnot`, `SigPar`, `SigSwap`, `SigBimonoid`) and direct GADT ↔ syntax+  isomorphisms (`algLoop`, `runAlgLoop`, `algNet`, `runAlgNet`).++*Operators*++- Forward composition is `(.>)`; backward composition is `(.)` from+  `Control.Category`.+- Forward/backward application operators `(|>)` and `(<|)` live in+  `Circuit.Category`.++*Removed*++- `Circuit.Trace` / `Circuit` GADT name retired to `Circuit.Loop`.+- `Circuit.Strength`, `Circuit.Monoidal`, `Circuit.Classes`,+  `Circuit.Adjunction`, `Circuit.Signature`, `Circuit.Box`, `Circuit.Queue`,+  `Circuit.Loopd`, and `Circuit.Dup` are gone; their contents are merged or+  renamed as above.+- `cellIO`, `openCollectSTM`, `openCollectIO`, `openBatchSTM`,+  `openBatchMaybeSTM`, `freeToMon`, `monTranspose`, `AlgSymKnot`,+  `loopToSymKnot`, and the old `traceToAlg` / `algToTrace` names are removed.+  Helpers that are not core API moved to `circuits-examples`.+- The `signature-tests` Cabal test suite is removed; verification is via+  `cabal-docspec` and `cabal check`.++*Examples and companion libraries*++- Example cards moved to the separate `circuits-examples` repository.+- `Circuit.AD` moved to the `circuits-ad` package.

@@ -1,17 +1,17 @@ cabal-version: 3.0 name: circuits-version: 0.1.0.0+version: 0.2.0.0 license: BSD-3-Clause license-file: LICENSE-copyright: Tony Day (c) 2025+copyright: Tony Day (c) 2025-2026 category: control author: Tony Day maintainer: tonyday567@gmail.com homepage: https://github.com/tonyday567/circuits#readme bug-reports: https://github.com/tonyday567/circuits/issues-synopsis: traced categories and circuits+synopsis: first-class circuits description:-  circuits is a Haskell library that makes feedback first-class, by providing Circuit, the initial traced category over a base category, hyperfunctions via Hyper, and combinators and interpreters. It is experimental, but could be a promising approach to programming circuits that is intensional, ergonomic and performant.+  circuits provides a suite of tools that make coding with circuits first-class.  build-type: Simple tested-with:@@ -20,11 +20,10 @@   ghc ==9.14.1  extra-doc-files:-    ChangeLog.md-    readme.md-    LICENSE-    other/symbols.md-    other/axioms.md+  ChangeLog.md+  LICENSE+  other/*.html+  readme.md  source-repository head   type: git@@ -41,28 +40,27 @@     -Wpartial-fields     -Wredundant-constraints -common ghc2024-stanza-  if impl(ghc >=9.10)-    default-language:-      GHC2024-  else-    default-language:-      GHC2021- library   import: ghc-options-stanza-  import: ghc2024-stanza+  default-language: GHC2024   hs-source-dirs: src   exposed-modules:     Circuit-    Circuit.Circuit-    Circuit.Classes+    Circuit.Algebra+    Circuit.Category+    Circuit.Channel+    Circuit.Dagger+    Circuit.Discrete+    Circuit.Ends+    Circuit.Free     Circuit.Hyper-    Circuit.Monoidal-    Circuit.Traced+    Circuit.Layer+    Circuit.Loop+    Circuit.Net+    Circuit.Sym+    Circuit.Tensor    build-depends:     base >=4.18 && <5,--  if impl(ghc)-    build-depends: profunctors >=5.0 && <6,+    profunctors >=5.0 && <6,+    stm >=2.5 && <3,

@@ -1,356 +0,0 @@-# Traced Monoidal Category Axioms--**Summary:** Equational proofs for all five axioms, both tensors. For when-you need to be sure.-**Reference:** https://ncatlab.org/nlab/show/traced+monoidal+category-**See also:** `02-a-knot-recovers-fix.md` (GADT derivation), `src/Circuit/Traced.hs` (Trace instances)--The five Joyal–Street–Verity axioms proved for tensors `(,)` and `Either`-over the base arrow `(->)`. Narrative motivation lives in the arc docs (01–07).--## Preliminaries--```haskell-class Trace arr t where-  trace   :: arr (t a b) (t a c) -> arr b c   -- close the channel-  untrace :: arr b c -> arr (t a b) (t a c)   -- inject into channel-```--For `arr = (->)`:--| Tensor | `trace` | `untrace` |-|--------|---------|-----------|-| `(,)` | `\f b -> let (a, c) = f (a, b) in c` | `fmap` / `second` |-| `Either` | while-loop: `Left` continues, `Right` exits | `fmap` / `right` |--The left-channel convention puts the channel on the left: `t a b` means-channel `a`, payload `b`. So `id ⊗ f` means `first f` for `(,)` and-`left f` for `Either` — both act on the channel component, leaving the-payload untouched.--The two tensors are operationally dual:--- **`(,)`** ties a lazy knot — feedback and output co-occur in a single-  recursive binding. Proofs reduce to substituting the knot.-- **`Either`** runs a while-loop — `Left` re-enters, `Right` exits.-  Proofs compare the reachable states of two state machines.--Every axiom holds for both by the same logical structure, reached by-different computational paths.--## The Five Axioms--**1. Vanishing.** Tracing over the unit does nothing. Nested channels-trace in sequence.-```-(a) tr^I(f) = f           for f : A ⊗ I → B ⊗ I-(b) tr^{X⊗Y}(f) = tr^X(tr^Y(f))   for f : A ⊗ X ⊗ Y → B ⊗ X ⊗ Y-```--**2. Sliding.** A morphism on the channel can slide from one side of `f`-to the other inside the trace.-```-tr^X((id_B ⊗ g) ∘ f) = tr^Y(f ∘ (id_A ⊗ g))-for f : A ⊗ X → B ⊗ Y,  g : Y → X-```--**3. Tightening.** Payload morphisms pass freely through the trace.-```-tr^X((g ⊗ id_X) ∘ f ∘ (h ⊗ id_X)) = g ∘ tr^X(f) ∘ h-for h : A → B,  f : B ⊗ X → C ⊗ X,  g : C → D-```--**4. Strength.** An independent payload wire is invisible to the trace.-```-tr^X(g ⊗ f) = g ⊗ tr^X(f)-for g : A → B,  f : C ⊗ X → D ⊗ X-```--**5. Yanking.** Tracing the braiding is the identity.-```-tr^X(swap_{X,X}) = id_X-```--Yanking is the only axiom that requires a braiding. The other four hold-in any monoidal category with a trace.--## Connection to the Hyperfunction Axioms--Launchbury, Krstic & Sauerwein (2013) state six axioms for hyperfunctions.-`push` is primitive — it prepends a function on the input side of the-feedback channel. The six axioms reduce to three structural roles:--| LKS Axiom | JSV Axiom | Structural role |-|-----------|-----------|-----------------|-| 1–3 | — | Free category (`Lift` + `Compose`) |-| 4 | — | `run (lift f) = fix f` — fixed points of base arrows (Hasegawa Thm 3.1) |-| 5 | — | Push composition: `push f p . push g q = push (f . g) (p . q)`. Push distributes over composition — a homomorphism constraint on the primitive. |-| 6 | Sliding | Feedback (forces `Knot` constructor) |--LKS axioms 1–5 have no direct JSV counterpart — LKS 1–3 fall out of the free-category structure, LKS 4 (`run (lift f) = fix f`) follows from the Hasegawa fixpoint correspondence for base arrows,-and LKS 5 (push composition) constrains how push interacts with composition.-Only LKS 6 (sliding/feedback) maps cleanly to a JSV axiom.--Axioms 4 and 5 introduce no new constructors on the final side. Axiom 4-(`run (lift f) = fix f`) is the key property showing that fixed points of-base arrows are available in the final encoding; it is part of the motivation-for why the initial encoding needs the structure that `Knot` provides.-Only axiom 6 (sliding) forces a new constructor on the initial side.-See `02-a-knot-recovers-fix.md` for the derivation.--## The Mendler Case--In `Circuit`, the sliding axiom is reified as a pattern match in `reify`:--```haskell-reify :: (Category arr, Trace arr t) => Circuit arr t x y -> arr x y-reify (Lift f)             = f-reify (Compose (Knot f) g) = ↪ (f . ↩ (reify g))   -- Mendler-reify (Compose f g)        = reify f . reify g-reify (Knot k)             = ↪ k-```--The Mendler case must appear before the general `Compose` case. Without-it, `Compose (Knot f) g` falls through to `trace f . reify g` — the-naive form that closes the channel immediately, losing the feedback-structure. One pattern match separates a free traced monoidal category-from the degenerate model. For the full story see `02-a-knot-recovers-fix.md` and-`05-no-remorse-once-removed.md`.--## Proofs--### Axiom 1: Vanishing--#### (a) Unit channel is a no-op--**With `(,)` — unit `I = ()`.**--A morphism `f :: ((), a) -> ((), b)` is, under the unit isomorphism,-`f = \((), x) -> ((), g x)` for some `g :: a -> b`.--```haskell-trace f b-  = let (a, c) = f (a, b) in c       -- Trace (->) (,) definition-  = let ((), c) = f ((), b) in c     -- a :: ()-  = let ((), c) = ((), g b) in c     -- definition of f-  = g b-  = trace (Lift g) b                  -- same as a plain Lift-```--The lazy knot has nothing to tie — `()` is determined immediately.--**With `Either` — unit `I = Void`.**--`Either Void a ≅ a` since `Left v` is uninhabited. A morphism-`f :: Either Void a -> Either Void b` can only map `Right x` to-`Right (g x)`.--The while-loop enters at `Right b`. On each step, `f` returns either-`Right c` (exit) or `Left v` — but `Left v` is uninhabited, so the-loop terminates immediately at `g b`. The trace degenerates to plain-function application.--#### (b) Nested channels trace in sequence--**With `(,)`.**--`f :: ((x, y), a) -> ((x, y), b)`. Channel is `(x, y)`, payload is `a`.--**LHS** — trace over `(x, y)` in one lazy knot:-```haskell-trace f a0 = let ((x, y), b) = f ((x, y), a0) in b-```--**RHS** — trace `y` first, then `x`. Reshape `f` via associativity:--```haskell-shuffle   (y, (x, a)) = ((x, y), a)-unshuffle ((x, y), b) = (y, (x, b))-f_Y = unshuffle . f . shuffle   -- channel y, payload (x, a)-```--Inner trace ties `y`, yielding a function of `(x, a0)`. Outer trace-ties `x`. Both find the same fixed point: `((x, y), b) = f ((x, y), a0)`.-Lazy evaluation makes the nested knots equivalent to the single knot.--**With `Either`.**--Channel is `Either a b`. LHS runs one while-loop over the state-`Either a b`. RHS runs two nested loops (trace `b` first, then `a`)-via associativity `Either (Either a b) c ≅ Either a (Either b c)`.-Both reach the same exit state — nested state machines vs one.--The `(,)` and `Either` traces are operationally dual: coinductive lazy-knot vs inductive while-loop. Vanishing holds for both by the same-logical structure, reached by different computational paths.--### Axiom 2: Sliding--`f :: (x, a) -> (y, b)`, `g :: y -> x`. Channel changes from `x` to `y`;-`g` bridges them back.--**With `(,)`.**--LHS — apply `g` to the output channel, trace over `x`:-```haskell-trace (first g . f) a-  = let (x, b) = (first g . f) (x, a) in b-  = let (x, b) = let (y, b') = f (x, a) in (g y, b') in b-  = let (y, b) = f (g y, a) in b             -- substitute x = g y-```--RHS — apply `g` to the input channel, trace over `y`:-```haskell-trace (f . first g) a-  = let (y, b) = (f . first g) (y, a) in b-  = let (y, b) = f (g y, a) in b-```--Both reduce to `\a -> let (y, b) = f (g y, a) in b`. The lazy knot ties-`y` to `g y` from `f`'s output — the same fixed point either side.--**With `Either`.**--`f :: Either x a -> Either y b`, `g :: y -> x`.--LHS — apply `g` to the output channel, trace over `x`:--Enter at `Right b`. On step `s :: Either x a`, call `f s`:-- `Right c` → exit with `c`-- `Left y` → re-enter at `Left (g y)`--RHS — apply `g` to the input channel, trace over `y`:--Enter at `Right b`. On `Right a`, call `f (Right a)`. On `Left y`,-call `f (Left (g y))`.--Both implement the same state machine: each loop step feeds `g`-transformed-values back into `f`. The sequence of states fed to `f` is identical;-the exit condition depends only on `f`'s output. Same result.--### Axiom 3: Tightening--`h :: a -> b`, `f :: (x, b) -> (x, c)`, `g :: c -> d`. Channel `x`-is untouched by `h` and `g` throughout.--**With `(,)`.**--```haskell-trace (second g . f . second h) a-  = let (x, d) = (second g . f . second h) (x, a) in d-  = let (x, d) = second g (f (x, h a)) in d-  = let (x, c) = f (x, h a) in g c-  = g (let (x, c) = f (x, h a) in c)-  = g (trace f (h a))-  = (g . trace f . h) a-```--**With `Either`.**--`h :: a -> b`, `f :: Either x b -> Either x c`, `g :: c -> d`.-`second h` maps `Right a` to `Right (h a)`, leaves `Left x` alone.--The while-loop enters at `Right (h a)`. The channel `x` flows through-`Left` transitions in `f`, never touching `h` or `g`. Exit occurs-when `f` returns `Right c`, at which point `g c` is returned.--Both sides: enter at `Right (h a)`, loop on `f`'s `Left` transitions,-exit with `g c`. `h` and `g` are straight wires — they pass freely-through the trace.--### Axiom 4: Strength--`g :: a -> b` acts on payload `a` independently; `f :: (x, c) -> (x, d)`-runs with the channel `x`. They operate on disjoint parts of the tensor.--**With `(,)`.**--`g ⊗ f` acts on payload `(a, c)` with channel `x`:-```haskell-g `par` f :: (x, (a, c)) -> (x, (b, d))-g `par` f (x, (a, c)) = let (x', d) = f (x, c) in (x', (g a, d))-```--```haskell-trace (g `par` f) (a, c)-  = let (x, (b, d)) = (g `par` f) (x, (a, c)) in (b, d)-  = let (x', d) = f (x, c) in (g a, d)       -- x tied to x' by knot-  = (g a, let (x, d) = f (x, c) in d)-  = (g a, trace f c)-  = (g ⊗ trace f) (a, c)-```--`g` is invisible to the channel — the lazy knot ties only `c`/`d` via `f`.--**With `Either`.**--`g` acts on `Right a`, `f` runs the loop on `Either x c`. `g ⊗ f` maps-`Left x` to `Left x` (channel passes through), `Right (Left a)` to-`Right (Left (g a))` (g on the a-side), and delegates `Right (Right c)`-to `f`.--Both sides: `g` is a straight wire on the `a` component, `trace f`-runs its loop on the `c` component. `g` has no feedback path and-cannot affect when or how the loop exits.--### Axiom 5: Yanking--`swap :: (x, x) -> (x, x)` is the braiding.--**With `(,)`.**--```haskell-trace swap x-  = let (a, c) = swap (a, x) in c-  = let (a, c) = (x, a) in c-  = x-  = id x-```--The lazy knot resolves immediately: `a` is set to `x` from-`swap (a, x) = (x, a)`, and `c = a = x`. One substitution, no recursion.--**With `Either`.**--`swapEither :: Either a b -> Either b a` maps `Left x → Right x`,-`Right x → Left x`.--Enter at `Right x`. `swapEither (Right x) = Left x` — loop.-Re-enter at `Left x`. `swapEither (Left x) = Right x` — exit with `x`.--The while-loop runs exactly two steps. Operationally different from-`(,)` — a two-step state machine vs an immediate lazy substitution —-but the same result.--**Why braiding is required.** The other four axioms involve only the-channel and payload structure — they hold in any monoidal category with-a trace. Yanking requires a morphism `swap : X ⊗ X → X ⊗ X` that is-part of a braiding. In a non-braided monoidal category, no such-morphism is guaranteed to exist, so yanking cannot be stated.--For `(,)` and `Either` in Haskell, both are symmetric monoidal —-`swap` exists and is involutive — so yanking holds.--## Summary--| Axiom | What it says | Key mechanism |-|--------|-------------|---------------|-| Vanishing | Unit channel is a no-op; products nest | Knot with nothing to tie |-| Sliding | Channel bridge commutes past `f` | Same fixed point either side |-| Tightening | Payload morphisms pass through | Channel untouched by `h`, `g` |-| Strength | Independent payload wire is invisible | Disjoint types, no contact |-| Yanking | Tracing a swap is identity | Requires braiding |--The `(,)` and `Either` instances are operationally dual throughout:-lazy knot vs while-loop. Every axiom holds for both by the same logical-structure.--## References--- [Joyal, Street & Verity (1996)](https://doi.org/10.1017/s0305004100074338) — traced monoidal categories-- [Launchbury, Krstic & Sauerwein (2013)](https://doi.org/10.4204/eptcs.129.9) — hyperfunction axioms-- [Hasegawa (1997)](https://doi.org/10.1007/978-1-4471-0865-8_7) — Theorem 3.1: cartesian traces = fixpoints-- [Van der Ploeg & Kiselyov (2014)](https://doi.org/10.1145/2633357.2633360) — Reflection Without Remorse-- `other/02-a-knot-recovers-fix.md` — how the axioms force the GADT-- `other/05-no-remorse-once-removed.md` — Mendler case as `viewl`

@@ -0,0 +1,87 @@+<!DOCTYPE html>+<html>+<head>+  <meta charset="utf-8">+  <script src="https://cdn.jsdelivr.net/npm/mermaid@10/dist/mermaid.min.js"></script>+  <script>+    mermaid.initialize({+      startOnLoad: true,+      theme: 'base',+      themeVariables: {+        primaryColor: '#21252d',+        primaryTextColor: '#c8ccd4',+        primaryBorderColor: '#373c45',+        lineColor: '#c8ccd4',+        secondaryColor: '#21252d',+        tertiaryColor: '#21252d',+        fontFamily: '-apple-system, BlinkMacSystemFont, "Segoe UI", Helvetica, Arial, sans-serif'+      },+      flowchart: {+        curve: 'basis'+      }+    });+  </script>+  <style>+    body {+      background: #1b1e23;+      color: #c8ccd4;+      font-family: -apple-system, BlinkMacSystemFont, 'Segoe UI', Helvetica, Arial, sans-serif;+      padding: 2rem;+    }+    h1 {+      color: #dfe2e8;+    }+    .mermaid {+      background: #21252d;+      border: 1px solid #373c45;+      border-radius: 8px;+      padding: 1rem;+      margin-bottom: 2rem;+    }+  </style>+</head>+<body>+<h1>circuits — class relationships</h1>+<div class="mermaid">+graph LR+  Category["Category"]+  Channel["Channel"]+  Strength["Strength"]+  Traced["Traced"]+  Tensor["Tensor"]+  Action["Action"]++  Free["Free"]+  Sym["Sym"]+  Net["Net"]+  Loop["Loop"]++  Category -.-> Free+  Strength -.-> Loop+  Traced -.-> Loop+  Action -.-> Sym+  Action -.-> Net+  Traced -.-> Net++  Category --> Channel --> Strength --> Traced+  Category --> Tensor --> Action+  Free --> Sym --> Net+  Loop --> Net++  linkStyle 0,1,2,3,4,5 stroke:#C44E8A,stroke-width:2px+  linkStyle 6,7,8,9,10 stroke:#4B7FBD,stroke-width:2px+  linkStyle 11,12,13 stroke:#8FB83A,stroke-width:2px++  style Category fill:#1F7050,stroke:#1F7050,color:#1b1e23+  style Channel fill:#4B7FBD,stroke:#4B7FBD,color:#1b1e23+  style Strength fill:#C44E8A,stroke:#C44E8A,color:#1b1e23+  style Traced fill:#3D3D7A,stroke:#3D3D7A,color:#c8ccd4+  style Tensor fill:#D98A3A,stroke:#D98A3A,color:#1b1e23+  style Action fill:#4B9680,stroke:#4B9680,color:#1b1e23+  style Free fill:#4B9680,stroke:#4B9680,color:#1b1e23+  style Sym fill:#8FB83A,stroke:#8FB83A,color:#1b1e23+  style Net fill:#D98A3A,stroke:#D98A3A,color:#1b1e23+  style Loop fill:#C44E8A,stroke:#C44E8A,color:#1b1e23+</div>+</body>+</html>

@@ -0,0 +1,99 @@+<!DOCTYPE html>+<html>+<head>+  <meta charset="utf-8">+  <script src="https://cdn.jsdelivr.net/npm/mermaid@10/dist/mermaid.min.js"></script>+  <script>+    mermaid.initialize({+      startOnLoad: true,+      theme: 'base',+      themeVariables: {+        primaryColor: '#21252d',+        primaryTextColor: '#c8ccd4',+        primaryBorderColor: '#373c45',+        lineColor: '#c8ccd4',+        secondaryColor: '#21252d',+        tertiaryColor: '#21252d',+        fontFamily: '-apple-system, BlinkMacSystemFont, "Segoe UI", Helvetica, Arial, sans-serif'+      },+      flowchart: {+        curve: 'basis'+      }+    });+  </script>+  <style>+    body {+      background: #1b1e23;+      color: #c8ccd4;+      font-family: -apple-system, BlinkMacSystemFont, 'Segoe UI', Helvetica, Arial, sans-serif;+      padding: 2rem;+    }+    h1 {+      color: #dfe2e8;+    }+    .mermaid {+      background: #21252d;+      border: 1px solid #373c45;+      border-radius: 8px;+      padding: 1rem;+      margin-bottom: 2rem;+    }+  </style>+</head>+<body>+<h1>circuits — module view</h1>+<div class="mermaid">+graph LR+  Category["Circuit.Category"]++  subgraph Channel ["Circuit.Channel"]+    ChannelClass["Channel"]+    Strength["Strength"]+    Traced["Traced"]+  end++  subgraph Tensor ["Circuit.Tensor"]+    TensorClass["Tensor"]+    Action["Action"]+  end++  Free["Circuit.Free"]+  Sym["Circuit.Sym"]+  Net["Circuit.Net"]+  Loop["Circuit.Loop"]+  Hyper["Circuit.Hyper"]+  Dagger["Circuit.Dagger"]+  Ends["Circuit.Ends"]++  Category --> ChannelClass --> Strength --> Traced+  Category --> TensorClass --> Action+  Free --> Sym --> Net+  Loop --> Net+  Loop --> Hyper+  Dagger --> Net+  Ends --> Loop++  linkStyle 0,1,2,3 stroke:#4B7FBD,stroke-width:2px+  linkStyle 4,5 stroke:#4B9680,stroke-width:2px+  linkStyle 6,7 stroke:#8FB83A,stroke-width:2px+  linkStyle 8,9 stroke:#9B6BC0,stroke-width:2px+  linkStyle 10 stroke:#4B96B0,stroke-width:2px++  style Channel fill:transparent,stroke:#4B7FBD,stroke-width:2px,stroke-dasharray: 5 5+  style Tensor fill:transparent,stroke:#D98A3A,stroke-width:2px,stroke-dasharray: 5 5+  style Category fill:#1F7050,stroke:#1F7050,color:#1b1e23+  style ChannelClass fill:#4B7FBD,stroke:#4B7FBD,color:#1b1e23+  style Strength fill:#C44E8A,stroke:#C44E8A,color:#1b1e23+  style Traced fill:#3D3D7A,stroke:#3D3D7A,color:#c8ccd4+  style TensorClass fill:#D98A3A,stroke:#D98A3A,color:#1b1e23+  style Action fill:#4B9680,stroke:#4B9680,color:#1b1e23+  style Free fill:#4B9680,stroke:#4B9680,color:#1b1e23+  style Sym fill:#8FB83A,stroke:#8FB83A,color:#1b1e23+  style Net fill:#D98A3A,stroke:#D98A3A,color:#1b1e23+  style Loop fill:#C44E8A,stroke:#C44E8A,color:#1b1e23+  style Hyper fill:#6B4C8A,stroke:#6B4C8A,color:#c8ccd4+  style Dagger fill:#E07A9E,stroke:#E07A9E,color:#1b1e23+  style Ends fill:#4B96B0,stroke:#4B96B0,color:#1b1e23+</div>+</body>+</html>

@@ -1,238 +0,0 @@-# Notation--**Summary:** The symbols used throughout the arc and examples. Mathematical-notation, used as mathematical notation — no apologies to GHC.-------## The Table--| Symbol | Name | Type | Meaning |-|--------|------|------|---------|-| `↑` | lift | `(a → b) → Circuit arr t a b` | embed a plain arrow |-| `↓` | lower | `Hyper a b → (a → b)` | observe a hyperfunction |-| `⊙` | compose | `cat b c → cat a b → cat a c` | sequential composition |-| `⊲` | push | `(a → b) → Hyper a b → Hyper a b` | prepend a plain function |-| `⥁` | run | `Hyper a a → a` | tie the self-referential knot (recovers fix on lifted arrows) |-| `∥` | ambient | `braid → Circuit arr t a b → Circuit arr t (t s a) (t s b)` | thread state wire alongside |-| `↮` | knot | `arr (t a b) (t a c) → Circuit arr t b c` | feedback loop constructor |-| `↘` | reify | `Circuit arr t x y → arr x y` | interpret to plain arrow |-| `↪` | trace | `arr (t a b) (t a c) → arr b c` | close the feedback channel |-| `↩` | untrace | `arr b c → arr (t a b) (t a c)` | open the feedback channel |-| `⇨` | encode | `Circuit (->) (,) a b → Hyper a b` | initial → final (preserving) |-| `⇦` | flatten | `Hyper a b → Circuit (->) (,) a b` | final → initial (lossy) |-| `⇸` | invoke | `Hyper a b → Hyper b a → b` | apply a hyperfunction to its dual |-| `○` | base | `a → Hyper b a` | constant continuation |-| `↬` | — | `type ↬ = Hyper` | type-level synonym |--The canonical API uses lowercase names (`lift`, `lower`, `reify`, etc.).-The symbols are notation — used in proofs, diagrams, and the arc documents-where the mathematical content should be visible without syntactic noise.-------## Two Registers--**The initial encoding** (`Circuit`) has visible constructors. Its symbols-are construction and elimination forms:--```-↑ f          — constructor: embed f as a Lift-↮ f          — constructor: embed f as a Knot-f ⊙ g        — constructor: Compose f g-↘ c          — eliminator: reify the circuit to a plain arrow-```--**The final encoding** (`Hyper`) has no constructors — only behaviour.-Its symbols are observation and composition:--```-↑ f          — lift f into Hyper (coinductive unrolling)-↓ h          — observe h by severing the feedback channel-⥁ h          — run h by feeding its own dual back-f ⊙ g        — compose: Hyper (\k -> invoke f (g . k))-```--`⊙` and `↑` appear in both registers with the same meaning — compose and-lift are the same operation in both encodings. The difference is what-the type checker sees underneath.-------## The Six Axioms--Written as we mean them, not as GHC requires them:--```-axiom 1   (f ⊙ g) ⊙ h  =  f ⊙ (g ⊙ h)               associativity-axiom 2    f ⊙ ↑ id     =  f  =  ↑ id ⊙ f             identity-axiom 3    ↑ (f . g)    =  ↑ f ⊙ ↑ g                  lift is a functor-axiom 4    ⥁ (↑ f)       =  fix f                      run recovers fix of base arrows-axiom 5    ⊲ f ⊙ ⊲ g    =  ⊲ (f . g)                  push is a homomorphism-axiom 6    ⥁ ((f ⊲ p) ⊙ q)  =  f (⥁ (q ⊙ p))          feedback / sliding-```--Axioms 1–3 are the free category. Axiom 4 is the sanity check on lifted arrows-(run recovers classical fixed points for base arrows). Axiom 5 says push-respects composition. Axiom 6 is the one that isn't free (it forces Knot).-------## The Five JSV Axioms--The Joyal–Street–Verity axioms for a traced monoidal category. Channel-is on the left; payload on the right. `⊗` is the tensor.--```-vanishing    ↪ (id ⊗ f)       =  f                    unit channel is a no-op-sliding      ↪ ((id ⊗ g) ⊙ f) =  ↪ (f ⊙ (id ⊗ g))    channel bridge commutes-tightening   ↪ ((g ⊗ id) ⊙ f ⊙ (h ⊗ id))  =  g ⊙ ↪ f ⊙ h    payload passes through-strength     ↪ (g ⊗ f)        =  g ⊗ ↪ f              independent wire invisible-yanking      ↪ swap            =  id                   tracing a swap is identity-```--For `(,)`, `↪` ties a lazy knot. For `Either`, `↪` runs a while-loop.-The axioms hold for both by the same logical structure.-------## The Triangle--The commuting triangle connecting initial and final encodings:--```-         ⇨-Circuit ────▶ Hyper-    \           │-     \          │ ↓-      \         ▼-       ↘──────▶ arr-```--```-↓ . ⇨  =  ↘-```--Mapping a `Circuit` into `Hyper` and then observing gives the same result-as running the `Circuit` directly. Proved case by case in-[03-hyper-buries-the-knot.md](03-hyper-buries-the-knot.md).-------## The Mendler Identity--The operational form of the sliding axiom in `reify`:--```-↘ (↑ f)           =  f                    faithful embedding-↘ (↮ k)           =  ↪ k                  trace closes the channel-↘ (↮ f ⊙ g)       =  ↪ (f . ↩ (↘ g))     Mendler case: g participates inside-↘ (f ⊙ g)         =  ↘ f . ↘ g            functoriality-```--The third line is the load-bearing one. Without it, `↘ (↮ f ⊙ g)` would-reduce to `↪ f . ↘ g` — closing the channel before `g` participates.-One equation separates the free traced monoidal category from the-degenerate model.-------## The Push/Lift Dual--`push` and `(:)` play the same structural role in different carriers:--```-(:) x . foldr' xs   ≡   push x . foldh' xs-```--`(:)` attaches to the outside of a list. `push` threads into the inside-of a `Hyper`, through the continuation channel. Same shape, flipped-polarity. Both build endofunction chains:--```-foldr'  :: [a → a] → ([a] → [a])       — Endo([a])-foldh'  :: [a → a] → (Hyper a a → Hyper a a)   — Endo(Hyper a a)-```--`push` is not compound in `Hyper` — it is primitive, threading through the-feedback channel.  The GADT has no direct counterpart; `Compose (Lift f) h`-(post-composition on `reify`) is the closest analogue but not equivalent.-------## State Threading--`ambient` (symbol `∥`) threads a state wire through a circuit unchanged.-The braid argument swaps state past the feedback channel:--```-∥ braid (↑ f)    =  ↑ (↩ f)            state tags along via untrace-∥ braid (f ⊙ g)  =  ∥ braid f ⊙ ∥ braid g   state threads both stages-∥ braid (↮ k)    =  ↮ (dimap braid braid (↩ k))   state slides past knot-```--The third equation is the sliding axiom wearing circuit clothes: a state-wire slides past a feedback loop via braiding. This is why `ambient`-requires an explicit braid argument — the braid is the proof that the-state and the channel are independent.-------## Encoding Worked Example--Fibonacci stream via the triangle:--```-fibs :: Circuit (->) (,) () [Int]-fibs = ↮ (\(xs, ()) -> (0 : 1 : zipWith (+) xs (drop 1 xs), xs))---- Run directly:-↘ fibs ()-= ↪ (\(xs, ()) -> (0 : 1 : zipWith (+) xs (drop 1 xs), xs)) ()-= let (xs, ys) = ... in ys      -- lazy knot---- Run via Hyper:-↓ (⇨ fibs) ()-= ↓ (↪ (↑ step)) ()             -- encode (↮ f) = ↪ (↑ f)-= ... same lazy knot ...         -- triangle: ↓ . ⇨ = ↘-```--Both paths reach the same stream. The triangle is not just a diagram —-it is an equality between two ways of running the same program.-------## Factorial via Either--```-fac :: Circuit (->) Either (Int, Int) Int-fac = ↮ step-  where-    step (Right (n, acc))  | n <= 1  =  Right acc-    step (Right (n, acc))            =  Left (n - 1, n * acc)-    step (Left s)                    =  step (Right s)--↘ fac (5, 1)-= ↪ step (5, 1)-= go (Right (5, 1))-= go (Left (4, 5))-= go (Left (3, 20))-= go (Left (2, 60))-= go (Left (1, 120))-= 120-```--`↪` on `Either` is the while-loop. `Left` feeds back; `Right` exits.-The `↮` constructor is the same as for `(,)` — the tensor choice is what-changes the operational character.-------## References--- [01-marks-and-stacks.md](01-marks-and-stacks.md) — the five marks introduced-- [02-a-knot-recovers-fix.md](02-a-knot-recovers-fix.md) — the Mendler identity derived-- [03-hyper-buries-the-knot.md](03-hyper-buries-the-knot.md) — the triangle proved-- [axioms.md](axioms.md) — JSV axioms proved for both tensors-- [Launchbury, Krstic & Sauerwein (2013)](https://doi.org/10.4204/eptcs.129.9) — original LKS axiom system-- [Joyal, Street & Verity (1996)](https://doi.org/10.1017/s0305004100074338) — traced monoidal categories

@@ -1,110 +1,196 @@ <p align="center"><strong>⟴ circuits</strong></p> -## First-Class Feedback--> The free traced monoidal category is the smallest thing you can add to a-> category to get feedback. Not a library of combinators — a single GADT and-> a single coinductive type, a hyperfunction no less, connected by this Galois connection ...->-> ~ What we learned building it--<br>+`circuits` is a toolkit for analysing circuits. A circuit, here, is any+computation that has direction, sequence, and flow: data moves through arrows,+feeds back on itself, and forks or joins along the way. The library gives you+small, composable pieces for building those structures and reasoning about them. -## ⚙️ Install+Solid arrows are enrichment; dashed arrows are the laws a free construction+draws on when it folds. ([open full page](other/circuits-class.html)) -```-(m)cabal build circuits-```+```mermaid+graph LR+  Category["Category"]+  Channel["Channel"]+  Strength["Strength"]+  Traced["Traced"]+  Tensor["Tensor"]+  Action["Action"] -Compiles on MicroHS & GHC 9.10+ with `base` & `profunctors`+  Free["Free"]+  Sym["Sym"]+  Net["Net"]+  Loop["Loop"] -## 📡 Usage+  Category -.-> Free+  Strength -.-> Loop+  Traced -.-> Loop+  Action -.-> Sym+  Action -.-> Net+  Traced -.-> Net -```haskell-import Circuit+  Category --> Channel --> Strength --> Traced+  Category --> Tensor --> Action+  Free --> Sym --> Net+  Loop --> Net --- Fibonacci via knot-tying->>> take 5 (trace (\(fibs, ()) -> (0 : 1 : zipWith (+) fibs (drop 1 fibs), fibs)) () :: [Integer])-[0,1,1,2,3]+  linkStyle 0,1,2,3,4,5 stroke:#C44E8A,stroke-width:2px+  linkStyle 6,7,8,9,10 stroke:#4B7FBD,stroke-width:2px+  linkStyle 11,12,13 stroke:#8FB83A,stroke-width:2px --- Iteration with Either->>> let step n = if n < 3 then Left (n + 1) else Right n in trace (either step step) (0 :: Int)-3+  style Category fill:#1F7050,stroke:#1F7050,color:#1b1e23+  style Channel fill:#4B7FBD,stroke:#4B7FBD,color:#1b1e23+  style Strength fill:#C44E8A,stroke:#C44E8A,color:#1b1e23+  style Traced fill:#3D3D7A,stroke:#3D3D7A,color:#c8ccd4+  style Tensor fill:#D98A3A,stroke:#D98A3A,color:#1b1e23+  style Action fill:#4B9680,stroke:#4B9680,color:#1b1e23+  style Free fill:#4B9680,stroke:#4B9680,color:#1b1e23+  style Sym fill:#8FB83A,stroke:#8FB83A,color:#1b1e23+  style Net fill:#D98A3A,stroke:#D98A3A,color:#1b1e23+  style Loop fill:#C44E8A,stroke:#C44E8A,color:#1b1e23 ``` -## Representations--`Circuit arr t a b` is the initial, inspectable encoding (a GADT with `Lift`, `Compose`, and `Knot`). `Hyper a b` is the final, coinductive encoding in which the feedback channel is structural in the type. The `Trace` class abstracts the tensor, giving lazy knots via `(,)` or iteration via `Either` (with the convention `Left` feeds back, `Right` exits).+The module view groups the classes into their source files and adds the+satellites around the core. ([open full page](other/circuits-module.html)) -Conversion is given by `reify` and `encode` (and `encodeEither`/`runEither`). The core triangle on observables is `reify . encode = id`.+```mermaid+graph LR+  Category["Circuit.Category"] -## 🧭 Pitch+  subgraph Channel ["Circuit.Channel"]+    ChannelClass["Channel"]+    Strength["Strength"]+    Traced["Traced"]+  end -circuits is a rethink of how to interact with a compiler and arrange code-pipelines — circuits — in ways that are intentional, clear, correct and performant.+  subgraph Tensor ["Circuit.Tensor"]+    TensorClass["Tensor"]+    Action["Action"]+  end -Hyper is the same as the Kidney & Wu construction:+  Free["Circuit.Free"]+  Sym["Circuit.Sym"]+  Net["Circuit.Net"]+  Loop["Circuit.Loop"]+  Hyper["Circuit.Hyper"]+  Dagger["Circuit.Dagger"]+  Ends["Circuit.Ends"] -```haskell-newtype Hyper a b = Hyper { invoke :: Hyper b a -> b }-```+  Category --> ChannelClass --> Strength --> Traced+  Category --> TensorClass --> Action+  Free --> Sym --> Net+  Loop --> Net+  Loop --> Hyper+  Dagger --> Net+  Ends --> Loop -From the paper and surrounding literature, we use the hyperfunction axioms and derive a `Circuit`:+  linkStyle 0,1,2 stroke:#4B7FBD,stroke-width:2px+  linkStyle 3,4 stroke:#4B9680,stroke-width:2px+  linkStyle 5,6 stroke:#8FB83A,stroke-width:2px+  linkStyle 7,8 stroke:#9B6BC0,stroke-width:2px+  linkStyle 9 stroke:#4B96B0,stroke-width:2px -```haskell-data Circuit arr t a b where-  Lift    :: arr a b -> Circuit arr t a b-  Compose :: Circuit arr t b c -> Circuit arr t a b -> Circuit arr t a c-  Knot    :: arr (t a b) (t a c) -> Circuit arr t b c+  style Channel fill:transparent,stroke:#4B7FBD,stroke-width:2px,stroke-dasharray: 5 5+  style Tensor fill:transparent,stroke:#D98A3A,stroke-width:2px,stroke-dasharray: 5 5+  style Category fill:#1F7050,stroke:#1F7050,color:#1b1e23+  style ChannelClass fill:#4B7FBD,stroke:#4B7FBD,color:#1b1e23+  style Strength fill:#C44E8A,stroke:#C44E8A,color:#1b1e23+  style Traced fill:#3D3D7A,stroke:#3D3D7A,color:#c8ccd4+  style TensorClass fill:#D98A3A,stroke:#D98A3A,color:#1b1e23+  style Action fill:#4B9680,stroke:#4B9680,color:#1b1e23+  style Free fill:#4B9680,stroke:#4B9680,color:#1b1e23+  style Sym fill:#8FB83A,stroke:#8FB83A,color:#1b1e23+  style Net fill:#D98A3A,stroke:#D98A3A,color:#1b1e23+  style Loop fill:#C44E8A,stroke:#C44E8A,color:#1b1e23+  style Hyper fill:#6B4C8A,stroke:#6B4C8A,color:#c8ccd4+  style Dagger fill:#E07A9E,stroke:#E07A9E,color:#1b1e23+  style Ends fill:#4B96B0,stroke:#4B96B0,color:#1b1e23 ``` -This happens to be the initial traced category over a base category and naturally encodes to a Hyper. To be concrete and on the nose, it's a 2-cell bolted on to the free category. Lifting the trace over a category and abstracting the tensor came later.+## the shape of the library -> Have you used your eyeballs yet and read Bartosz's latest? Original thought is a strong claim and could be awkward.->-> ~ claude ([tank](https://github.com/tonyday567/mg/blob/main/word/tank.md) mode on)+Everything is built over a base arrow that you bring — `(->)`, `Kleisli m`,+matrices over a semiring. The library does not pick a semantics; it adds+structure along two ladders. -`Circuit` covers functions, compositional paths, and feedback loops. `Hyper` is an efficient final encoding where feedback dissolves into the type structure itself. The `Trace` class (in `Circuit.Traced`) abstracts the tensor, giving polymorphic loop semantics: lazy knots with `(,)` or iteration with `Either`. All braided, cartesian and cocartesian structure lives in `Circuit.Monoidal`.+**A ladder of laws.** The type classes form chains out of `Category`:+`Channel → Strength → Traced` (monoidal structure, tensorial strength, feedback+via trace) and `Tensor → Action` (the concrete `(,)` and `Either` machinery).+Each rung is one more law a target category can satisfy. These classes say+nothing about syntax; they are the contracts that folds have to meet. -`other/` traces these ideas from the [Kidney & Wu hyperfunctions](https://doi.org/10.1145/3776649) paper through a narrative arc. `Circuit` is the initial encoding — a GADT-with visible constructors, interpreted by `reify`. `Hyper` is the final-encoding — a coinductive type where feedback dissolves into the structure-itself. The triangle `reify = lower . encode` connects them.+**A deck of languages.** The GADTs form a parallel chain of free constructions,+each rung one enrichment of the last: -## 📦 Sibling libraries+    Free = Lift + Compose+    Sym  = Free + Par + Swap+    Net  = Sym + Knot + Copy + Discard + Plus + Zero -**circuits-parser** — `Circuit (->) Either f (These a f)` as a parser for a wide variety of f and a.+`Free` is the free category; `Sym` the free symmetric monoidal category; `Net`+the free traced PROP with a bimonoid, where every wire is a constructor you can+inspect. `Loop` sits to the side of this chain rather than on it: it is the free+traced monoidal category *in normal form*. Its laws are performed by its+instances, so every value collapses to at most one `Knot` over a base arrow.+`Net` and `Loop` are the two poles of the library — wiring you can read+backwards, and wiring that has been melted into a single loop. `melt` goes from+one to the other. -**circuits-io** — `Circuit (Kleisli IO) Either` as a way to engage with file I/O, sockets, servers, (a)timings & asynchronicity.+**Between the ladders** there is a family of folds. Each free construction can+be evaluated into any target category that satisfies the right laws; the GADT's+constructors are forgotten one at a time. `Layer` captures this pattern+uniformly, and `Algebra` provides the same deck à la carte from signature+functors. -**circuits-meter** — circuit measurement and performance.+In many of the free objects we tag common computation patterns: function+application, composition, tracing, and type tensoring. This bootstraps a+first-class foundation for computational circuits — direction, sequence, and+flow — without baking in a particular semantics too early. -## 📖 Read+Applications and closures can be delayed for analysis and measurement, or+retried. The feedback itself is visible as a wire, not hidden in a closure. -["tracing hyperfunctions"](https://doi.org/10.1145/3776649) — Kidney & Wu (2026). The paper that inspired the core construction. Introduces `Hyper` as a self-dual object in the traced sense and the hyperfunction axioms.+## potential uses -`other/` — the narrative arc (notation, marks-and-stacks, knot, triangle proof, tensors, Mendler case, examples). For the long version.+The core stays small; companion libraries apply it to specific domains. -`examples/` — cards: parsers, pipes, Elgot iteration, delimited continuations. Paste code blocks into `cabal repl`.+| library | what it adds |+|---------|-------------|+| [circuits-ad](https://github.com/tonyday567/circuits-ad) | reverse-mode automatic differentiation, pullbacks, and star-elimination |+| [circuits-examples](https://github.com/tonyday567/circuits-examples) | paste-into-GHCi example cards |+| [circuits-int](https://github.com/tonyday567/circuits-int) | Int construction and polynomial-functor sketches |+| [circuits-io](https://github.com/tonyday567/circuits-io) | sockets, queues, servers, and concrete IO transports |+| [circuits-llm](https://github.com/tonyday567/circuits-llm) | small transformer-style language-model experiments |+| [circuits-mat](https://github.com/tonyday567/circuits-mat) | matrices over a semiring as a traced monoidal category |+| [circuits-meter](https://github.com/tonyday567/circuits-meter) | one-line performance metering and stopwatch pipelines |+| [circuits-parser](https://github.com/tonyday567/circuits-parser) | parser combinators over a coinductive stream decomposition |+| [circuits-pca](https://github.com/tonyday567/circuits-pca) | principal component analysis as a residual-ownership protocol |+| [circuits-repl](https://github.com/tonyday567/circuits-repl) | REPL primitives: commit/emit dual, turns, channels, sessions | -## Contributing+## install -We welcome contributions of any persuasion or fancy. New contributors should open an issue and say hi.+Add `circuits` to your `build-depends`. GHC 9.10+ (tested with 9.14).+Dependencies beyond base: `profunctors` and `stm`. -AI / LLM policy+## examples -LLMs and agents have been used in the development of this library, including category theory, coding, generation, refactoring, documentation and narrative.+The example cards live in the separate+[circuits-examples](https://github.com/tonyday567/circuits-examples) repository.+Each `.md` file is a short, paste-into-GHCi walkthrough with YAML front matter+(`name`, `description`, `tags`). -what we prefer-  ⟜ all code must compile, have and pass doctests, and be reviewable.-  ⟜ if you open a PR, you must be able to explain what the code does and why. "my buddy Grok wrote it" is not an explanation.-  ⟜ do not submit code you have not read, understood, and tested.+Cards are not a secondary dump for outdated material — they are the development+surface of the library. Stable cards document supported API; experimental cards+grow ideas that are not yet in the API. When a card matures, it gets promoted+into `src/` and the public API. -what we do not do-  ⟜ ban AI tools. they are part of the workflow.-  ⟜ accept code that fails the same standards we apply to AI contributions.+## thanks -code is code and coders are going to code.+Built on [Launchbury, Krstic & Sauerwein (2013)](https://doi.org/10.4204/eptcs.129.9)+and [Kidney & Wu (2026)](https://doi.org/10.1145/3776649). The `Hyper` type is+theirs; the normal form that makes it inspectable is ours.++LLMs and agents helped with category theory, coding, refactoring, and+documentation.  <br> 

@@ -11,133 +11,241 @@ -- Use the @(,@) tensor to tie a lazy knot. The feedback value and output -- are produced simultaneously. ----- >>> let powers (ns, ()) = (1 : map (*2) ns, take 5 ns)--- >>> trace powers () :: [Integer]+-- .> let powers (ns, ()) = (1 : map (*2) ns, take 5 ns)+-- .> trace powers () :: [Integer] -- [1,2,4,8,16] -- -- === Iteration ----- Use the 'Either' tensor for loops that terminate.+-- Use the `Either` tensor for loops that terminate. ----- >>> let step n = if n < 5 then Left (n + 1) else Right n--- >>> trace (either step step) (0 :: Int)+-- .> let step n = if n < 5 then Left (n + 1) else Right n+-- .> trace (either step step) (0 :: Int) -- 5 -- -- === Switching between representations ----- 'Circuit' is the inspectable GADT form. 'Hyper' is the efficient final--- encoding. Convert with 'encode' and 'reify'.+-- `Loop` is the inspectable GADT form. @Hyper@ is the final, coinductive+-- encoding. Convert a `Loop` to a @Hyper@ with `encode`, and observe it+-- with `observe` (or eliminate it with `runHyper`). ----- >>> lower (encode (Lift (+1) :: Circuit (->) (,) Int Int)) 41+-- .> observe (encode (Circuit.Loop.Lift (+1) :: Loop (,) (->) Int Int)) 41 -- 42 ----- >>> reify (Knot (\(acc, x) -> (x, acc)) :: Circuit (->) (,) Int Int) 0--- 0--- -- == Overview -- -- This library provides two representations of feedback: ----- * 'Circuit' (in "Circuit.Circuit") — the initial, inspectable GADT encoding.--- * 'Hyper' (in "Circuit.Hyper") — the final, coinductive encoding.+-- * `Loop` (in "Circuit.Loop") — the initial, inspectable GADT encoding.+-- * @Hyper@ (in "Circuit.Hyper") — the final, coinductive encoding. ----- The 'Trace' class (in "Circuit.Traced") abstracts the choice of tensor,--- currently supporting lazy knots with @(,@) and iteration with 'Either'.+-- The `Traced` class (in "Circuit.Channel") abstracts the choice of tensor,+-- currently supporting lazy knots with @(,@) and iteration with `Either`. -- -- All braided, cartesian, and cocartesian structure, plus the general--- 'ambientBy' state-threading combinator, lives in "Circuit.Monoidal".+-- `ambientBy` state-threading combinator, lives in "Circuit.Tensor". -- -- == Core Concepts -- -- * __Tensor__ (@t@): The bifunctor pairing a feedback value with a payload---   inside a 'Knot' (currently @(,@) or 'Either').+--   inside a `Loop` (currently @(,@) or `Either`). -- -- * __Feedback value__: The component that travels around the loop (first---   parameter of the tensor in a 'Knot').+--   parameter of the tensor in a `Loop`). -- -- * __Payload__: The value being transformed and emitted (second parameter --   of the tensor). -- -- * __Feedback channel__: The path the feedback value takes when routed back --   into the next step.+--+-- == Verb glossary+--+-- * __Folds__ eliminate a free construction:+--   `run` (any `Layer`), `freeze` (`Free` to its base arrow),+--   `melt` (`Net` to `Loop`), @sift@ (`Net` to `Sym`),+--   @eval@ / @evalInto@ (@Syntax@ via an algebra).+--+-- * __Injections__ embed one construction into another without eliminating:+--   `unit` (base arrow into a `Layer`), `enrich` (`Loop` into `Net`),+--   @widen@ (`Sym` into `Net`), @algLoop@ / @algNet@ (direct GADT into @Syntax@).+--+-- * __Representation changes__: `encode` (`Loop` to @Hyper@),+--   `observe` / `runHyper` (@Hyper@ to function / fixed point). module Circuit-  ( -- * Circuit-    Circuit (..),-    Wire,-    Step,-    reify,+  ( -- * Loop+    Loop (..),+    Traced,+    Strength,+    -- | Close a feedback loop. See "Circuit.Loop".+    trace,+    -- | Open a feedback loop. See "Circuit.Loop".+    strength, -    -- * Traced-    Trace (..),-    cellIO,+    -- * Channel ends+    Out (..),+    In (..),+    Ends (..),+    close,+    prefixIn,+    suffixOut,+    ends,+    endsK,+    splay,+    HasUnit (..), +    -- * Boxes+    box,+    boxAsymmetric,++    -- * Queues+    Queue (..),+    openSTM,+    openIO,++    -- * Free+    Free,+    freeze,++    -- * Layer tower+    Layer (..),+    Cat2,+    (:~>),+    lower,++    -- * Discrete discharge kit+    compD,+    assocD,+    assocD',+    braidD,+    strengthD,+    traceD,++    -- * Operators+    (.>),+    (|>),+    (<|),++    -- * Dagger (bimonoid + dagger)+    CopyDiscard (..),+    MergeZero (..),+    Dagger (..),+    Bimonoid,+    transpose,++    -- * Sym+    Sym,++    -- * Net+    Net,+    enrich,+    melt,+     -- * Hyper     Hyper (..),     lift,-    lower,+    observe,     base,     push,-    run,+    runHyper,     encode,     encodeEither,+    encodeFree,     runEither,     flatten, -    -- * Monoidal+    -- * Channel     Braided (..),     ambient,-    assoc,-    assoc',-    seed,-    absorb,-    release,-    coassoc,-    coassoc',-    coseed,-    coabsorbL,-    coabsorbR,-    coreleaseL,-    coreleaseR,     ambientBy,+    superpose,++    -- * Channel product+    Tensor (..),+    Action (..),   ) where -import Circuit.Circuit-  ( Circuit (..),-    Step,-    Wire,-    reify,+import Circuit.Category (Ob, (.>), (<|), (|>))+import Circuit.Channel (Strength, Traced)+import Circuit.Channel qualified as Channel+import Circuit.Dagger+  ( Bimonoid,+    CopyDiscard (..),+    Dagger (..),+    MergeZero (..),+    transpose,   )+import Circuit.Discrete+  ( assocD,+    assocD',+    braidD,+    compD,+    strengthD,+    traceD,+  )+import Circuit.Ends+  ( Ends (..),+    HasUnit (..),+    In (..),+    Out (..),+    Queue (..),+    box,+    boxAsymmetric,+    close,+    ends,+    endsK,+    openIO,+    openSTM,+    prefixIn,+    splay,+    suffixOut,+  )+import Circuit.Free+  ( Free (..),+    freeze,+  ) import Circuit.Hyper   ( Hyper (..),     base,     encode,     encodeEither,+    encodeFree,     flatten,     lift,-    lower,+    observe,     push,-    run,     runEither,+    runHyper,   )-import Circuit.Monoidal-  ( Braided (..),-    absorb,-    ambient,-    ambientBy,-    assoc,-    assoc',-    coabsorbL,-    coabsorbR,-    coassoc,-    coassoc',-    coreleaseL,-    coreleaseR,-    coseed,-    release,-    seed,+import Circuit.Layer+  ( Cat2,+    Layer (..),+    lower,+    run,+    (:~>),   )-import Circuit.Traced-  ( Trace (..),-    cellIO,+import Circuit.Loop (Loop (..))+import Circuit.Loop qualified as Loop+import Circuit.Net+  ( Net,+    enrich,+    melt,   )+import Circuit.Sym+import Circuit.Tensor+import Prelude++-- | Close a feedback loop. See "Circuit.Channel".+trace ::+  (Traced t arr, Ob arr a, Ob arr b, Ob arr c, Ob arr (t a b), Ob arr (t a c)) =>+  arr (t a b) (t a c) ->+  arr b c+trace = Channel.trace++-- | Open a feedback loop. See "Circuit.Channel".+strength ::+  (Strength t arr, Ob arr a, Ob arr b, Ob arr c, Ob arr (t a b), Ob arr (t a c)) =>+  arr b c ->+  arr (t a b) (t a c)+strength = Channel.strength

@@ -0,0 +1,406 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Change-of-base algebras for modular circuit syntax.+--+-- A 'Circuit.Layer.Layer' evals a free construction back into the /same/+-- base arrow. An 'Algebra' generalises this by allowing the target+-- category to differ from the source: it interprets syntax built over+-- @arr@ into morphisms of some other category @arr'@. The map+-- @emb :: arr :~> arr'@ handles the base-arrow generators, while+-- @eval@ handles the recursive sub-terms.+--+-- In this picture, 'Syntax sig arr' is the tree, 'Algebra sig arr arr''+-- is the interpreter, 'alg' evaluates a single constructor, and 'eval'+-- evals the whole tree. When @arr' = arr@ and @emb = id@, an 'Algebra'+-- collapses to the single universal eval that 'Layer' captures.+--+-- Each language feature is a signature functor. A GADT is the free+-- construction over a chosen combination of signatures. This makes the+-- design space a lattice: start with the features you need, add more+-- when you need them, and forget them via algebras.+--+-- Signatures expose the design space as a lattice: start with the+-- features you need, add more when you need them, and forget them via+-- algebras. The direct GADTs in "Circuit.Loop" and "Circuit.Net" are+-- the canonical circuit types; this module gives those constructions as+-- compositional syntax.+--+-- The signatures are:+--+-- * @SigCompose@ — sequential composition+-- * @SigKnot@    — feedback / trace over a tensor @t@+-- * @SigPar@     — parallel composition+-- * @SigSwap@    — symmetric braiding+-- * 'SigBimonoid'— copy, discard, plus, zero+--+-- Examples:+--+-- * @'Syntax' @SigCompose@ arr@                              — free category+-- * @'Syntax' (@SigCompose@ ':+:' @SigKnot@ t) arr@          — free traced category+-- * @'Syntax' (@SigCompose@ ':+:' @SigPar@ ':+:' @SigSwap@) arr@ — free monoidal category+-- * @'Syntax' (@SigCompose@ ':+:' @SigKnot@ t ':+:' @SigPar@ ':+:' @SigSwap@ ':+:' 'SigBimonoid') arr@ — Net+module Circuit.Algebra+  ( -- * Signatures+    Sig,+    (:+:) (..),++    -- * Syntax and algebra+    Syntax (..),+    Algebra (..),+    eval,+    evalInto,++    -- * Individual signatures+    SigCompose (..),+    SigKnot (..),+    SigPar (..),+    SigSwap (..),+    SigBimonoid (..),++    -- * Common syntax combinations+    AlgCat,+    AlgLoop,+    AlgSym,+    AlgBimonoidal,+    AlgNet,++    -- * Direct <-> algebra isomorphisms+    algLoop,+    runAlgLoop,+    algNet,+    runAlgNet,+  )+where++import Circuit.Category (Category (..), Discrete (..))+import Circuit.Channel (Channel (..), Strength (..), Traced (..))+import Circuit.Dagger qualified as Dg+import Circuit.Layer (Layer, run)+import Circuit.Loop qualified as C+import Circuit.Net qualified as N+import Circuit.Tensor (Action (..), Tensor (..))+import Data.Kind (Constraint, Type)+import Prelude hiding (id, (.))++-- ---------------------------------------------------------------------------+-- Signature functors++-- | A signature describes a set of constructors for a profunctor.+--+-- * @arr@ — the base arrow (used for constructor constraints)+-- * @rec@ — the recursive arrow type being defined+-- * @a@, @b@ — input and output objects+type Sig = (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type++-- | Coproduct of signatures.+data (sig1 :+: sig2) arr rec a b where+  L :: sig1 arr rec a b -> (sig1 :+: sig2) arr rec a b+  R :: sig2 arr rec a b -> (sig1 :+: sig2) arr rec a b++infixr 6 :+:++-- ---------------------------------------------------------------------------+-- Free construction over a signature.++-- | The free construction over a signature.+data Syntax (sig :: Sig) (arr :: Type -> Type -> Type) a b where+  Lift :: arr a b -> Syntax sig arr a b+  Op :: sig arr (Syntax sig arr) a b -> Syntax sig arr a b++-- | Algebra for a signature. Interprets operations of a signature over+-- source arrow @arr@ into a target arrow @arr'@.+--+-- * @emb@ maps base arrows of the source into the target.+-- * @rec@ maps recursive sub-terms into the target.+class Algebra (sig :: Sig) (arr :: Type -> Type -> Type) (arr' :: Type -> Type -> Type) where+  type Ctx sig arr arr' :: Constraint+  type Ctx sig arr arr' = ()+  alg ::+    (Ctx sig arr arr') =>+    (forall x y. arr x y -> arr' x y) ->+    (forall x y. rec x y -> arr' x y) ->+    sig arr rec a b ->+    arr' a b++-- | Coproduct algebra dispatches to the appropriate component.+instance (Algebra sig1 arr arr', Algebra sig2 arr arr') => Algebra (sig1 :+: sig2) arr arr' where+  type Ctx (sig1 :+: sig2) arr arr' = (Ctx sig1 arr arr', Ctx sig2 arr arr')+  alg emb rec (L op) = alg emb rec op+  alg emb rec (R op) = alg emb rec op++-- | Fold a free construction into a target arrow using its algebra.+--+-- The embedding @emb@ maps base arrows of the source into the target.+-- For folding to the same arrow, use 'eval'.+--+-- This is the à la carte analogue of 'Circuit.Layer.bind': @evalInto emb@+-- folds syntax into a target just as @bind h@ folds a 'Circuit.Layer.Layer'+-- construction. For example, folding 'AlgNet' into 'AlgLoop' is just+-- @'evalInto' 'Lift'@, playing the same role as a structural forgetting map+-- built with @bind unit@.+--+-- A signature like @@SigKnot@ t@ is best read as a type-level tag that tracks+-- which constructors are present in the union; the coproduct @(':+:')@ is the+-- union of those tags.+evalInto ::+  (Category arr', Algebra sig arr arr', Ctx sig arr arr') =>+  (forall x y. arr x y -> arr' x y) ->+  Syntax sig arr a b ->+  arr' a b+evalInto emb (Lift f) = emb f+evalInto emb (Op op) = alg emb (evalInto emb) op++-- | Fold a free construction into its own base arrow.+eval ::+  (Category arr, Algebra sig arr arr, Ctx sig arr arr) =>+  Syntax sig arr a b ->+  arr a b+eval = evalInto id++-- ---------------------------------------------------------------------------+-- Individual signatures++-- | Sequential composition.+data SigCompose arr rec a b where+  SigCompose :: (Ob arr b) => rec b c -> rec a b -> SigCompose arr rec a c++instance Algebra SigCompose arr arr' where+  type Ctx SigCompose arr arr' = Discrete arr'+  alg ::+    forall (rec :: Type -> Type -> Type) (a :: Type) (c :: Type).+    (Ctx SigCompose arr arr') =>+    (forall x y. arr x y -> arr' x y) ->+    (forall x y. rec x y -> arr' x y) ->+    SigCompose arr rec a c ->+    arr' a c+  alg _ rec (SigCompose @_ @b1 @_ @_ @_ g f) =+    withOb @arr' @a $+      withOb @arr' @b1 $+        withOb @arr' @c $+          (rec g . rec f)++-- | Feedback loop / trace over tensor @t@.+data SigKnot (t :: Type -> Type -> Type) arr rec a b where+  SigKnot :: (Ob arr a) => rec (t a b) (t a c) -> SigKnot t arr rec b c++instance (Traced t arr') => Algebra (SigKnot t) arr arr' where+  type Ctx (SigKnot t) arr arr' = (Traced t arr', Discrete arr')+  alg ::+    forall (rec :: Type -> Type -> Type) (b :: Type) (c :: Type).+    (Ctx (SigKnot t) arr arr') =>+    (forall x y. arr x y -> arr' x y) ->+    (forall x y. rec x y -> arr' x y) ->+    SigKnot t arr rec b c ->+    arr' b c+  alg _ rec (SigKnot @_ @a1 @_ @_ @_ @_ f) =+    withOb @arr' @a1 $+      withOb @arr' @b $+        withOb @arr' @c $+          withOb @arr' @(t a1 b) $+            withOb @arr' @(t a1 c) $+              trace (rec f)++-- | Parallel composition.+data SigPar arr rec a b where+  SigPar :: rec a b -> rec c d -> SigPar arr rec (a, c) (b, d)++instance (Tensor (,) arr') => Algebra SigPar arr arr' where+  type Ctx SigPar arr arr' = Tensor (,) arr'+  alg _ rec (SigPar f g) = par (rec f) (rec g)++-- | Symmetric braiding.+data SigSwap arr rec a b where+  SigSwap :: SigSwap arr rec (a, b) (b, a)++instance (Action (,) arr') => Algebra SigSwap arr arr' where+  type Ctx SigSwap arr arr' = Action (,) arr'+  alg _ _ SigSwap = swap++-- | Bimonoid operations: copy, discard, plus, zero.+--+-- Each constructor carries its own 'Dg.Bimonoid' constraint, resolved at+-- pattern-match time rather than in the algebra context.+data SigBimonoid arr rec a b where+  SigCopy :: (Dg.Bimonoid arr a) => SigBimonoid arr rec a (a, a)+  SigDiscard :: (Dg.Bimonoid arr a) => SigBimonoid arr rec a ()+  SigPlus :: (Dg.Bimonoid arr a) => SigBimonoid arr rec (a, a) a+  SigZero :: (Dg.Bimonoid arr a) => SigBimonoid arr rec () a++-- | [Conditional] 'alg' for bimonoid generators sends each generator to the+-- image under @emb@ of the source dictionary. This is the free-PROP fold+-- only when @emb@ is a bimonoid homomorphism; it is automatic for the+-- generator embedding, but must be checked for custom embeddings.+instance Algebra SigBimonoid arr arr' where+  alg ::+    forall rec i o.+    (forall x y. arr x y -> arr' x y) ->+    (forall x y. rec x y -> arr' x y) ->+    SigBimonoid arr rec i o ->+    arr' i o+  alg emb _ SigCopy = emb (Dg.copy :: arr i (i, i))+  alg emb _ SigDiscard = emb (Dg.discard :: arr i ())+  alg emb _ SigPlus = emb (Dg.plus :: arr (o, o) o)+  alg emb _ SigZero = emb (Dg.zero :: arr () o)++-- ---------------------------------------------------------------------------+-- Common syntax combinations++-- | Free category.+type AlgCat arr = Syntax SigCompose arr++-- | Free traced monoidal category over tensor @t@.+type AlgLoop t arr = Syntax (SigCompose :+: SigKnot t) arr++-- | Free monoidal category.+type AlgSym arr = Syntax (SigCompose :+: SigPar :+: SigSwap) arr++-- | Free bimonoidal category.+type AlgBimonoidal arr = Syntax (SigCompose :+: SigPar :+: SigSwap :+: SigBimonoid) arr++-- | Free traced PROP with bimonoid.+type AlgNet t arr = Syntax (SigCompose :+: SigKnot t :+: SigPar :+: SigSwap :+: SigBimonoid) arr++-- ---------------------------------------------------------------------------+-- Instances for signature-based categories++instance (Category arr) => Category (AlgCat arr) where+  type Ob (AlgCat arr) a = Ob arr a+  id = Lift id+  f . g = Op (SigCompose f g)++instance (Category arr) => Category (AlgLoop t arr) where+  type Ob (AlgLoop t arr) a = Ob arr a+  id = Lift id+  f . g = Op (L (SigCompose f g))++instance (Category arr, Channel t arr) => Channel t (AlgLoop t arr) where+  assoc = Lift assoc+  assoc' = Lift assoc'+  slide = Lift slide++instance (Category arr, Traced t arr, Discrete arr) => Strength t (AlgLoop t arr) where+  strength f = Lift (strength (eval f))++instance (Category arr, Traced t arr, Discrete arr) => Traced t (AlgLoop t arr) where+  trace body = Op (R (SigKnot body))++instance (Category arr, Traced t arr, Tensor (,) arr, Discrete arr) => Tensor (,) (AlgLoop t arr) where+  par f g = Lift (par (eval f) (eval g))+  unitl = Lift unitl+  unitl' = Lift unitl'+  unitr = Lift unitr+  unitr' = Lift unitr'++instance (Category arr, Traced t arr, Action (,) arr, Discrete arr) => Action (,) (AlgLoop t arr) where+  swap = Lift swap++instance (Category arr, Channel t arr) => Channel t (AlgCat arr) where+  assoc = Lift assoc+  assoc' = Lift assoc'+  slide = Lift slide++instance (Category arr, Strength t arr, Discrete arr) => Strength t (AlgCat arr) where+  strength f = Lift (strength (eval f))++instance (Category arr, Traced t arr, Discrete arr) => Traced t (AlgCat arr) where+  trace body = Lift (trace (eval body))++-- | A discrete base yields discrete syntax.+--+-- These instances are needed so that 'evalInto Lift' can fold richer syntax+-- into poorer syntax (e.g. 'AlgLoop' into 'AlgCat', 'AlgNet' into 'AlgLoop').+instance (Category arr, Discrete arr) => Discrete (AlgCat arr) where+  withOb @a x = withOb @arr @a x++instance (Category arr, Discrete arr) => Discrete (AlgLoop t arr) where+  withOb @a x = withOb @arr @a x++-- ---------------------------------------------------------------------------+-- Direct <-> algebra isomorphisms++-- | Embed the direct 'C.Loop' GADT into the signature-based form.+algLoop :: forall t arr a b. C.Loop t arr a b -> AlgLoop t arr a b+algLoop (C.Lift f) = Lift f+algLoop (C.Knot f) = Op (R (SigKnot (Lift f)))++-- | Project the signature-based circuit back to the direct GADT.+--+-- @SigCompose@ nodes are interpreted using the 'Category' instance of+-- 'C.Loop', so the result is in normal form (at most one 'C.Knot').+runAlgLoop ::+  forall t a b.+  (Traced t (->)) =>+  AlgLoop t (->) a b ->+  C.Loop t (->) a b+runAlgLoop (Lift f) = C.Lift f+runAlgLoop (Op op) = go op+  where+    go ::+      forall x y.+      (SigCompose :+: SigKnot t) (->) (AlgLoop t (->)) x y ->+      C.Loop t (->) x y+    go (L (SigCompose g f)) = runAlgLoop g . runAlgLoop f+    go (R (SigKnot @_ f)) = C.Knot (run (runAlgLoop f))++-- | Embed the direct 'N.Net' GADT into the signature-based form.+algNet :: forall t arr a b. N.Net t arr a b -> AlgNet t arr a b+algNet (N.Lift f) = Lift f+algNet (N.Compose g f) = Op (L (SigCompose (algNet g) (algNet f)))+algNet (N.Par f g) = Op (R (R (L (SigPar (algNet f) (algNet g)))))+algNet N.Swap = Op (R (R (R (L SigSwap))))+algNet N.Copy = Op (R (R (R (R SigCopy))))+algNet N.Discard = Op (R (R (R (R SigDiscard))))+algNet N.Plus = Op (R (R (R (R SigPlus))))+algNet N.Zero = Op (R (R (R (R SigZero))))+algNet (N.Knot f) = Op (R (L (SigKnot (algNet f))))++-- | Project the signature-based Net back to the direct GADT.+runAlgNet :: forall t arr a b. AlgNet t arr a b -> N.Net t arr a b+runAlgNet = goTop+  where+    goTop :: forall x y. AlgNet t arr x y -> N.Net t arr x y+    goTop (Lift f) = N.Lift f+    goTop (Op op) = goOp op++    goOp :: forall x y. (SigCompose :+: SigKnot t :+: SigPar :+: SigSwap :+: SigBimonoid) arr (AlgNet t arr) x y -> N.Net t arr x y+    goOp (L sc) = goCompose sc+    goOp (R rest) = goKnotOrMore rest++    goCompose :: forall x y. SigCompose arr (AlgNet t arr) x y -> N.Net t arr x y+    goCompose (SigCompose g f) = N.Compose (goTop g) (goTop f)++    goKnotOrMore :: forall x y. (SigKnot t :+: SigPar :+: SigSwap :+: SigBimonoid) arr (AlgNet t arr) x y -> N.Net t arr x y+    goKnotOrMore (L sk) = goKnot sk+    goKnotOrMore (R rest) = goParOrMore rest++    goKnot :: forall x y. SigKnot t arr (AlgNet t arr) x y -> N.Net t arr x y+    goKnot (SigKnot f) = N.Knot (goTop f)++    goParOrMore :: forall x y. (SigPar :+: SigSwap :+: SigBimonoid) arr (AlgNet t arr) x y -> N.Net t arr x y+    goParOrMore (L sp) = goPar sp+    goParOrMore (R rest) = goSwapOrBimonoid rest++    goPar :: forall x y. SigPar arr (AlgNet t arr) x y -> N.Net t arr x y+    goPar (SigPar f g) = N.Par (goTop f) (goTop g)++    goSwapOrBimonoid :: forall x y. (SigSwap :+: SigBimonoid) arr (AlgNet t arr) x y -> N.Net t arr x y+    goSwapOrBimonoid (L SigSwap) = N.Swap+    goSwapOrBimonoid (R sb) = goBimonoid sb++    goBimonoid :: forall x y. SigBimonoid arr (AlgNet t arr) x y -> N.Net t arr x y+    goBimonoid SigCopy = N.Copy+    goBimonoid SigDiscard = N.Discard+    goBimonoid SigPlus = N.Plus+    goBimonoid SigZero = N.Zero

@@ -0,0 +1,105 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Local category hierarchy with object constraints.+--+-- 'Category' is local so morphisms can carry an associated 'Ob'+-- constraint.+--+-- 'Discrete' marks categories whose 'Ob' is trivial for every object+-- (@Ob = ()@). Constrained bases can implement 'Circuit.Loop.Traced'+-- directly, but /hosting/ the free constructions (@Free@, @Sym@, @Loop@,+-- @Net@, and the syntax in "Circuit.Algebra") additionally requires+-- 'Discrete', because compound tensor objects (e.g. @t s a@ inside a+-- 'Loop.Knot') carry no 'Ob' evidence and must be manufactured on demand.+--+-- == Operator convention+--+-- The tip of the operator points in the direction of data flow.+--+-- * @|@ means /apply/ to a value: @('|>')@ feeds a value into a function+--   (forward application, like @&@), and @('<|')@ applies a function+--   to a value (backward application, like @('$')@).+-- * @.@ means /compose/ morphisms: @('.>')@ is forward composition and+--   @('.')@ is backward composition as usual.+module Circuit.Category+  ( Category (..),+    Discrete (..),+    (.>),+    (|>),+    (<|),+  )+where++import Control.Arrow (Kleisli (..))+import Control.Monad ((<=<))+import Data.Kind (Constraint, Type)+import Prelude hiding (id, (.))++-- | A category whose objects may carry a constraint.+--+-- @Ob arr a@ is the evidence required to mention object @a@ in @arr@.+-- Unconstrained categories use the default @()@. Constrained categories+-- specialise the associated type to whatever their objects require.+class Category (arr :: k -> k -> Type) where+  -- | Object constraint for this category.+  type Ob arr (a :: k) :: Constraint++  type Ob arr a = ()++  -- | Identity morphism.+  id :: (Ob arr a) => arr a a++  -- | Composition (right-to-left).+  (.) :: (Ob arr a, Ob arr b, Ob arr c) => arr b c -> arr a b -> arr a c++-- | Categories with a trivial object constraint for every type.+--+-- 'withOb' discharges @Ob arr a@ at an arbitrary @a@. Free constructions+-- that bind an existential object (notably @Loop@ in "Circuit.Loop")+-- use it where a polymorphic @Ob@ constraint cannot be written.+class (Category arr) => Discrete arr where+  withOb :: forall a r. ((Ob arr a) => r) -> r++-- | Forward composition. @f .> g = g . f@+(.>) :: (Category arr, Ob arr a, Ob arr b, Ob arr c) => arr a b -> arr b c -> arr a c+f .> g = g . f+{-# INLINE (.>) #-}++-- | Forward application. @x |> f = f x@+(|>) :: a -> (a -> b) -> b+x |> f = f x+{-# INLINE (|>) #-}++infixl 1 |>++-- | Backward application. @f <| x = f x@+(<|) :: (a -> b) -> a -> b+f <| x = f x+{-# INLINE (<|) #-}++infixr 0 <|++-- | Unconstrained function category.+instance Category (->) where+  type Ob (->) a = ()+  id x = x+  (f . g) x = f (g x)++instance Discrete (->) where+  withOb x = x++-- | Kleisli arrows of a monad (unconstrained objects).+instance (Monad m) => Category (Kleisli m) where+  type Ob (Kleisli m) a = ()+  id = Kleisli pure+  Kleisli f . Kleisli g = Kleisli (f <=< g)++instance (Monad m) => Discrete (Kleisli m) where+  withOb x = x

@@ -0,0 +1,466 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UnboxedTuples #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Structural semantics for traced monoidal categories.+--+-- This module collects the structural superclass chain+-- @Channel → Strength → Traced@ and all base instances for the standard+-- base arrows @(->)@ and @Control.Arrow.Kleisli m@.  These classes+-- describe the monoidal structure, tensorial strength, and feedback-fixing+-- trace that underlie the syntax in "Circuit.Loop".+--+-- 'assoc' and 'assoc'' here reassociate /rightward/ and /leftward/+-- respectively. The monomorphic helpers in "Circuit.Tensor" have the same+-- names but the opposite directions. Also, 'slide' here is the slide+-- @t a (t b c) -> t b (t a c)@; the symmetric braiding @t a b -> t b a@+-- lives in Circuit.Tensor as swap. Where both structures exist,+-- @slide = assoc' .> par swap id .> assoc@.+--+-- Kind-polymorphic: @t@ and @arr@ share object kind (inferred via PolyKinds).+module Circuit.Channel+  ( Channel (..),+    Strength (..),+    strengthD,+    Traced (..),+  )+where++import Circuit.Category (Category (..), Discrete (..))+import Control.Arrow (Kleisli (..))+import Control.Monad.Fix (MonadFix, mfix)+import Data.Bifunctor+import Data.Kind (Type)+import GHC.Exts (PromptTag#, control0#, newPromptTag#, prompt#)+import GHC.IO (IO (..))+import Prelude hiding (id, (.))++-- $setup+-- >> import Circuit.Category ((.>))++-- ===========================================================================+-- Channel+-- ===========================================================================++-- | A monoidal structure on the tensor @t@ internal to the category @arr@.+--+-- Provides the associator and braiding required to reassociate and swap+-- nested tensor values inside an arrow. This is the structure that traced+-- categories inherit as a superclass.+--+-- Object constraints live on 'Category' / 'Traced', not on these structure+-- maps — free constructions over unconstrained bases stay lightweight.+class (Category arr) => Channel t arr where+  -- | Reassociate to the right: @t (t a b) c -> t a (t b c)@.+  assoc :: arr (t (t a b) c) (t a (t b c))++  -- | Inverse reassociation: @t a (t b c) -> t (t a b) c@.+  assoc' :: arr (t a (t b c)) (t (t a b) c)++  -- | Swap the two outer positions, leaving the inner payload in place:+  -- @t a (t b c) -> t b (t a c)@.+  slide :: arr (t a (t b c)) (t b (t a c))++-- | Cartesian monoidal structure for @(,)@.+--+-- .> assoc ((1, 2), 3) :: (Int, (Int, Int))+-- (1,(2,3))+--+-- .> assoc' (1, (2, 3)) :: ((Int, Int), Int)+-- ((1,2),3)+--+-- .> (assoc .> assoc') ((1, 2), 3) :: ((Int, Int), Int)+-- ((1,2),3)+--+-- .> slide (1, (2, 3)) :: (Int, (Int, Int))+-- (2,(1,3))+instance Channel (,) (->) where+  assoc ~(~(a, b), c) = (a, (b, c))+  assoc' ~(a, ~(b, c)) = ((a, b), c)+  slide ~(a, ~(b, c)) = (b, (a, c))++-- | Cocartesian monoidal structure for @Either@.+--+-- .> assoc (Left (Left 1) :: Either (Either Int Bool) Char) :: Either Int (Either Bool Char)+-- Left 1+--+-- .> assoc' (Left 1 :: Either Int (Either Bool Char)) :: Either (Either Int Bool) Char+-- Left (Left 1)+--+-- .> slide (Left 1 :: Either Int (Either Bool Char)) :: Either Bool (Either Int Char)+-- Right (Left 1)+instance Channel Either (->) where+  assoc (Left (Left a)) = Left a+  assoc (Left (Right b)) = Right (Left b)+  assoc (Right c) = Right (Right c)+  assoc' (Left a) = Left (Left a)+  assoc' (Right (Left b)) = Left (Right b)+  assoc' (Right (Right c)) = Right c+  slide (Left a) = Right (Left a)+  slide (Right (Left b)) = Left b+  slide (Right (Right c)) = Right (Right c)++-- ===========================================================================+-- Strength+-- ===========================================================================++-- | Tensorial strength for a tensor @t@ inside a category @arr@.+--+-- 'strength' opens a feedback loop, tensoring a plain morphism with the+-- feedback channel. It is /not/ a syntactic inverse of 'trace'; it is the+-- strength ("tensorial strength") of the tensor @t@ acting on morphisms.+class (Channel t arr) => Strength t arr where+  strength ::+    ( Ob arr a,+      Ob arr b,+      Ob arr c,+      Ob arr (t a b),+      Ob arr (t a c)+    ) =>+    arr b c ->+    arr (t a b) (t a c)++-- | Discrete 'strength': discharge 'Ob' constraints with 'withOb'.+strengthD ::+  forall t arr a b c.+  (Strength t arr, Discrete arr) =>+  arr b c ->+  arr (t a b) (t a c)+strengthD f =+  withOb @arr @a $+    withOb @arr @b $+      withOb @arr @c $+        withOb @arr @(t a b) $+          withOb @arr @(t a c) $+            strength f++-- | Cartesian tensorial strength for @(,)@.+--+-- The implementation uses explicit projections so that the result pair+-- constructor exists before the feedback channel is forced; this keeps+-- fused 'Circuit.Loop.Knot' bodies productive even when the body has a strict+-- top-level pattern on the recursive channel.+--+-- .> strength (+1) (error "forced" :: (Int, Int)) `seq` ()+-- ()+instance Strength (,) (->) where+  strength f p = (fst p, f (snd p))++-- | Either tensorial strength for @Either@.+--+-- 'strength' is the functorial action under 'Either'.+instance Strength Either (->) where+  strength = fmap++-- ===========================================================================+-- Traced+-- ===========================================================================++-- | A trace over a morphism @arr@ and tensor @t@.+--+-- @trace@ closes the feedback loop, eliminating the tensor channel.+-- It extends the 'Strength' structure with the feedback-fixing operation.+--+-- Object constraints on the feedback channel (@a@) let constrained+-- categories (e.g. matrices needing @Finite@ / @KnownNat@) instance+-- this class lawfully.+class (Strength t arr) => Traced t arr where+  trace ::+    ( Ob arr a,+      Ob arr b,+      Ob arr c,+      Ob arr (t a b),+      Ob arr (t a c)+    ) =>+    arr (t a b) (t a c) ->+    arr b c++-- * Cartesian tensor — lazy knot++-- | The cartesian trace ties a lazy knot: the feedback value @a@ and+-- output @c@ are produced simultaneously in a single recursive binding.+--+-- Only works in a lazy setting — the feedback value is a self-referential+-- thunk.  In a strict language this binding is circular and divergent.+-- Haskell's lazy evaluation makes cyclic sharing possible without an+-- explicit fixpoint operator.+--+-- .> :{+-- let powers (ns, ()) =+--       (1 : map (*2) ns, take 5 ns)+-- :}+--+-- .> trace powers () :: [Integer]+-- [1,2,4,8,16]+--+-- .> trace (\(acc, x) -> (acc, x + 1)) 5+-- 6+--+-- Vanishing (a): tracing over the unit does nothing.+--+-- The unit is @()@ for the @(,)@ tensor. The unitor laws say that+-- threading a plain payload through the unit channel is the same as+-- applying the payload morphism directly.+--+-- .> let f = (+1) :: Int -> Int+-- .> trace (unitl' . f . unitl :: ((), Int) -> ((), Int)) 5+-- 6+--+-- .> trace ((unitl' . (+ 3) . unitl) :: ((), Int) -> ((), Int)) 0+-- 3+--+-- Yanking: tracing a swap is the identity.+--+-- .> let swap (x, y) = (y, x)+-- .> trace swap 42+-- 42+--+-- .> trace ((\(a, b) -> (b, a)) :: (Int, Int) -> (Int, Int)) 42+-- 42+--+-- Tightening: payload morphisms pass freely through the trace.+--+-- .> let f (x, a) = (x, a)+-- .> trace ((\(x, a) -> (x, a + 1)) . f . (\(x, a) -> (x, a * 2))) 5+-- 11+--+-- Sliding: a morphism on the channel slides from one side to the other.+--+-- .> let swap (x, y) = (y, x)+-- .> trace ((\(a, b) -> (b, a + 1)) . (\(a, b) -> (b, a)) :: (Int, Int) -> (Int, Int)) 5+-- 6+--+-- .> trace ((\(a, b) -> (b + 1, a)) :: (Int, Int) -> (Int, Int)) 5+-- 6+--+-- Strength: an independent payload wire is invisible to the trace.+--+-- .> let f (x, c) = (x, c + 1)+-- .> let g (x, (a, c)) = (x', (a * 2, d)) where (x', d) = f (x, c)+-- .> trace g (3, 5)+-- (6,6)+--+-- .> trace ((\(x, (p, q)) -> (x, (p + 7, q + 1))) :: (Int, (Int, Int)) -> (Int, (Int, Int))) (0, 5)+-- (7,6)+instance Traced (,) (->) where+  trace f b = let ~(a, c) = f (a, b) in c++-- * Either tensor — iteration++-- | The Either trace iterates: 'Left' feeds back (continue), 'Right'+-- terminates (exit). A compact, under-appreciated pattern for loops in Haskell.+--+-- .> :{+-- let fac (n, acc) | n <= 1    = Right acc+--                  | otherwise = Left (n - 1, n * acc)+-- :}+--+-- .> trace (either fac fac) (5, 1 :: Int)+-- 120+--+-- .> :{+-- let countdown = \case+--       Left n | n > 0 -> Left (n - 1)+--              | otherwise -> Right n+--       Right n | n > 0 -> Left (n - 1)+--               | otherwise -> Right n+-- :}+--+-- .> trace countdown (3 :: Int)+-- 0+--+-- Vanishing (a): tracing over the unit does nothing.+--+-- The unit is 'Data.Void.Void' for the 'Either' tensor. The unitor+-- laws say that threading a plain payload through the unit channel is the+-- same as applying the payload morphism directly.+--+-- .> let f = (+1) :: Int -> Int+-- .> trace (unitl' . f . unitl :: Either Void Int -> Either Void Int) 5+-- 6+--+-- .> trace ((unitl' . (+ 3) . unitl) :: Either Void Int -> Either Void Int) 0+-- 3+--+-- Yanking: tracing a swap is the identity.+--+-- .> :{+-- let swapEither (Left x)  = Right x+--     swapEither (Right x) = Left x+-- :}+--+-- .> trace swapEither 42+-- 42+--+-- .> trace ((\e -> case e of Left a -> Right a; Right a -> Left a) :: Either Int Int -> Either Int Int) 42+-- 42+--+-- Tightening: payload morphisms pass freely through the trace.+--+-- .> let f = fmap ((+1) :: Int -> Int) . fmap ((*2) :: Int -> Int)+-- .> trace (f :: Either Void Int -> Either Void Int) 5+-- 11+--+-- .> trace (fmap ((+1) :: Int -> Int) . fmap ((*2) :: Int -> Int) :: Either Void Int -> Either Void Int) 5+-- 11+instance Traced Either (->) where+  trace f b = go (Right b)+    where+      go x = case f x of+        Right c -> c+        Left a -> go (Left a)++-- ===========================================================================+-- Kleisli m — monoidal structure+-- ===========================================================================++-- | Cartesian monoidal structure for @Kleisli m@ with @(,)@.+instance (Monad m) => Channel (,) (Kleisli m) where+  assoc = Kleisli $ \ ~(~(a, b), c) -> pure (a, (b, c))+  assoc' = Kleisli $ \ ~(a, ~(b, c)) -> pure ((a, b), c)+  slide = Kleisli $ \ ~(a, ~(b, c)) -> pure (b, (a, c))++-- | Cocartesian monoidal structure for @Kleisli m@ with 'Either'.+instance (Monad m) => Channel Either (Kleisli m) where+  assoc = Kleisli $ \case+    Left (Left a) -> pure (Left a)+    Left (Right b) -> pure (Right (Left b))+    Right c -> pure (Right (Right c))+  assoc' = Kleisli $ \case+    Left a -> pure (Left (Left a))+    Right (Left b) -> pure (Left (Right b))+    Right (Right c) -> pure (Right c)+  slide = Kleisli $ \case+    Left a -> pure (Right (Left a))+    Right (Left b) -> pure (Left b)+    Right (Right c) -> pure (Right (Right c))++-- * Kleisli m (,) — lazy knot via MonadFix++-- | Traced for @Kleisli m@ with the cartesian tensor, requiring @MonadFix m@.+--+-- The lazy knot is tied via 'mfix'. The feedback channel is lazy in the+-- recursive binding — the body must not force the feedback value before+-- producing it, or 'mfix' will diverge (just as the pure @(,)@ trace+-- black-holes on strict fields).+--+-- .> :{+-- let fibs = Kleisli $ \(fibs, ()) ->+--       pure (0 : 1 : zipWith (+) fibs (drop 1 fibs), take 3 fibs)+-- :}+--+-- .> runKleisli (trace fibs) ()+-- [0,1,1]+instance (Monad m) => Strength (,) (Kleisli m) where+  strength (Kleisli f) =+    Kleisli+      ( \p -> do+          c <- f (snd p)+          pure (fst p, c)+      )++instance (MonadFix m) => Traced (,) (Kleisli m) where+  trace (Kleisli f) =+    Kleisli+      ( \b -> do+          (_, c) <- mfix $ \ ~(s, _) -> f (s, b)+          pure c+      )++-- * Kleisli m Either — iteration for any Monad++-- | Traced for @Kleisli m@ with the 'Either' tensor, for any @Monad m@.+--+-- Iterates by feeding 'Left' back into the step function until a 'Right'+-- is produced. Uses plain recursion — builds stack proportional to+-- iteration count.+--+-- .> :{+-- let countTo target = Kleisli $ \case+--       Left n | n < target -> pure (Left (n + 1))+--              | otherwise  -> pure (Right n)+--       Right ()            -> pure (Left 0)+-- :}+--+-- .> runKleisli (trace (countTo (3 :: Int))) ()+-- 3+--+-- This instance is @OVERLAPPABLE@: the IO-specific instance below takes+-- priority for @IO@, providing constant-stack iteration via delimited+-- continuations.+instance (Monad m) => Strength Either (Kleisli m) where+  strength (Kleisli f) =+    Kleisli $ \case+      Left a -> pure (Left a)+      Right b -> Right <$> f b++instance {-# OVERLAPPABLE #-} (Monad m) => Traced Either (Kleisli m) where+  trace (Kleisli f) =+    Kleisli $ \b -> go (Right b)+    where+      go x =+        f x >>= \case+          Right c -> pure c+          Left a -> go (Left a)++-- * Kleisli IO Either — delimited continuations (constant stack)++-- | GHC delimited-continuation primops.+data PromptTag a = PromptTag (PromptTag# a)++-- | Create a new prompt tag for delimited continuations.+newPromptTag :: IO (PromptTag a)+newPromptTag =+  IO+    ( \s ->+        case newPromptTag# s of+          (# s', t #) -> (# s', PromptTag t #)+    )++-- | Run an IO computation under a prompt boundary.+prompt :: PromptTag a -> IO a -> IO a+prompt (PromptTag t) (IO m) = IO (prompt# t m)++-- | Captures the continuation up to the nearest prompt with the matching tag.+control0 :: forall a b. PromptTag a -> ((IO b -> IO a) -> IO a) -> IO b+control0 (PromptTag t) f = IO (control0# t arg)+  where+    arg f# s = case f (\(IO x) -> IO (f# x)) of IO m -> m s++-- | Traced for @Kleisli IO@ with 'Either' tensor.+--+-- Each iteration re-establishes the prompt boundary. When @control0@+-- fires on @Left a@, it captures the continuation, wraps it around+-- the next loop step, and jumps back to the prompt — constant stack.+--+-- .> :{+-- let exit42 = Kleisli $ \case+--       Right () -> pure (Right (42 :: Int))+-- :}+--+-- .> runKleisli (trace exit42) ()+-- 42+instance {-# OVERLAPPING #-} Traced Either (Kleisli IO) where+  trace (Kleisli body) =+    Kleisli+      ( \initial -> do+          tag <- newPromptTag+          let go x =+                prompt tag $+                  body x+                    >>= ( \case+                            Right c -> pure c+                            Left a -> control0 tag (\k -> k (go (Left a)))+                        )+          go (Right initial)+      )

@@ -1,145 +0,0 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE UndecidableInstances #-}---- | The free traced monoidal category.------ @Circuit arr t a b@ is the initial encoding of a traced monoidal category--- over a base morphism @arr@ with a supplied tensor @t@ for the category. The three constructors encode:------   - `Lift`: embedding of a base arrow (strict monoidal functor)---   - `Compose`: sequential composition (category structure)---   - `Knot`: introduces a feedback channel (trace structure)------ For example, a `Circuit (->) (,)` is the initial traced monoidal cartesian category over Haskell functions.------ == Core Concepts------ * __Tensor__ (@t@): The bifunctor that pairs a feedback value with a payload---   inside a 'Knot'. The two tensors provided are @(,)@ (simultaneous / lazy---   sharing) and 'Either' (sequential / iteration).------ * __Feedback value__: The component that travels around the loop (the first---   parameter of the tensor inside a 'Knot').------ * __Payload__: The component that is transformed and emitted by the circuit---   (the second parameter of the tensor).------ * __Feedback channel__: The path the feedback value takes when it is routed---   back into the next step of the computation. In a 'Knot' the channel type---   is carried by the tensor @t@.------ These concepts are independent of any particular base arrow @arr@. They--- describe the structure of feedback itself.------ The `reify` function interprets any `Circuit` to a plain arrow via--- the `Trace` instance on @t@. For encoding into 'Circuit.Hyper', see--- 'Circuit.Hyper.encode' and 'Circuit.Hyper.encodeEither'.-module Circuit.Circuit-  ( -- * Circuit-    Circuit (..),--    -- * Type aliases-    Wire,-    Step,--    -- * Operators-    reify,-  )-where--import Circuit.Traced (Trace (..))-import Prelude hiding (id, (.))--#ifdef __GLASGOW_HASKELL__-import Control.Category-import Data.Bifunctor-import Data.Profunctor-#else-import Circuit.Classes-#endif---- $setup--- >>> import Control.Category ((>>>))--- >>> import Data.Profunctor (dimap)--- >>> import Prelude hiding (id, (.))---- | The free traced monoidal category over base morphism @arr@ and tensor @t@.------ Three constructors:------   * 'Lift' — embed a base arrow.---   * 'Compose' — sequential composition.---   * 'Knot' — feedback loop via the tensor.-data Circuit arr t a b where-  -- | Lift embeds a base arrow (strict monoidal functor).-  ---  -- >>> reify (Lift (+1) :: Circuit (->) (,) Int Int) 5-  -- 6-  Lift :: arr a b -> Circuit arr t a b-  -- | Compose performs sequential composition (category structure).-  ---  -- >>> reify (Lift (+1) >>> Lift (*2) :: Circuit (->) (,) Int Int) 5-  -- 12-  Compose :: Circuit arr t b c -> Circuit arr t a b -> Circuit arr t a c-  -- | Knot ties a feedback loop. The tensor @t@ carries the channel type.-  ---  -- >>> reify (Knot (\(acc, x) -> (x, acc)) :: Circuit (->) (,) Int Int) 42-  -- 42-  Knot :: arr (t a b) (t a c) -> Circuit arr t b c---- | A traced circuit over plain functions with the cartesian tensor.------ @Wire a b = Circuit (->) (,) a b@------ The @(,)@ tensor ties a lazy knot: output and feedback are produced--- simultaneously.-type Wire = Circuit (->) (,)---- | A traced circuit over plain functions with the cocartesian tensor.------ @Step a b = Circuit (->) Either a b@------ The @Either@ tensor iterates: @Left@ feeds back (continue),--- @Right@ terminates (exit).-type Step = Circuit (->) Either--instance (Category arr) => Category (Circuit arr t) where-  id = Lift id-  (.) = Compose--instance Functor (Circuit (->) t a) where-  fmap f = Compose (Lift f)---- | Profunctor instance for Circuit.------ Maps over both ends of the arrow. For @Compose@, the map is applied--- to the input of the left sub-circuit and the output of the right--- sub-circuit, leaving the intermediate type aligned.------ >>> reify (dimap (+ 1) (+ 1) (Lift (* 2) :: Circuit (->) (,) Int Int)) 5--- 13-instance (Profunctor arr, Bifunctor t) => Profunctor (Circuit arr t) where-  dimap f g (Lift h) = Lift (dimap f g h)-  dimap f g (Compose h k) = Compose (dimap id g h) (dimap f id k)-  dimap f g (Knot k) = Knot (dimap (second f) (second g) k)-  lmap f (Lift h) = Lift (lmap f h)-  lmap f (Compose h k) = Compose (lmap id h) (lmap f k)-  lmap f (Knot k) = Knot (lmap (second f) k)-  rmap g (Lift h) = Lift (rmap g h)-  rmap g (Compose h k) = Compose (rmap g h) (rmap id k)-  rmap g (Knot k) = Knot (rmap (second g) k)---- | Interpret a Circuit to a plain arrow.------ This is the canonical map out of the free (initial) traced monoidal--- category.  The interesting case is when a @Knot@ appears on the left--- of a @Compose@: this is exactly where the sliding axiom of traced--- monoidal categories is enforced (the Mendler case).------ >>> reify (Lift (+1) :: Circuit (->) (,) Int Int) 5--- 6-reify :: (Category arr, Trace arr t) => Circuit arr t x y -> arr x y-reify (Lift f) = f-reify (Compose (Knot f) g) = trace (f . untrace (reify g))-reify (Compose f g) = reify f . reify g-reify (Knot k) = trace k

@@ -1,42 +0,0 @@-{-# LANGUAGE CPP #-}---- | On GHC, Category, Bifunctor, and Profunctor come from packages.--- On other compilers (e.g. MicroHs), we define them locally.-module Circuit.Classes where--#ifndef __GLASGOW_HASKELL__--import Prelude hiding (id, (.))--class Category cat where-  id :: cat a a-  (.) :: cat b c -> cat a b -> cat a c--instance Category (->) where-  id x = x-  (f . g) x = f (g x)--class Bifunctor p where-  bimap :: (a -> b) -> (c -> d) -> p a c -> p b d-  first :: (a -> b) -> p a c -> p b c-  second :: (b -> c) -> p a b -> p a c-  bimap f g = first f . second g-  first f = bimap f id-  second = bimap id--instance Bifunctor (,) where-  bimap f g (a, b) = (f a, g b)--instance Bifunctor Either where-  bimap f _ (Left a) = Left (f a)-  bimap _ g (Right b) = Right (g b)--class Profunctor p where-  dimap :: (a -> b) -> (c -> d) -> p b c -> p a d-  lmap :: (a -> b) -> p b c -> p a c-  rmap :: (b -> c) -> p a b -> p a c-  dimap f g = lmap f . rmap g-  lmap f = dimap f id-  rmap = dimap id--#endif

@@ -0,0 +1,279 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++-- | The dagger/bimonoid layer of circuit wiring.+--+-- This module collects the algebraic structure that every wire carries in a+-- circuit category:+--+-- * 'CopyDiscard' — the comonoid on channel objects (fan-out of values).+-- * 'MergeZero' — the monoid on channel objects (fan-in of contributions).+-- * 'Bimonoid' — both together, the precondition for 'Circuit.Net.transpose'.+-- * @Dagger@ — the free dagger category over a base arrow, pairing a forward+--   arrow with a backward arrow.  'transpose' is the dagger operation.+--+-- The four structural rows of 'Circuit.Net' ('Circuit.Net.Copy',+-- 'Circuit.Net.Discard', 'Circuit.Net.Plus', 'Circuit.Net.Zero') are exactly+-- the generators of this bimonoid.  In a dagger setting,+-- copy and add are adjoint, as are discard and zero.  @Dagger@ makes that+-- duality explicit: a dagger wire's forward direction copies while its+-- backward direction adds.+module Circuit.Dagger+  ( -- * CopyDiscard+    CopyDiscard (..),++    -- * MergeZero+    MergeZero (..),++    -- * Bimonoid+    Bimonoid,++    -- * Dagger+    Dagger (..),+    transpose,+  )+where++import Circuit.Category (Category (..), Discrete (..), (.>))+import Circuit.Channel (Channel (..), Strength (..), Traced (..))+import Circuit.Tensor (Action (..), Tensor (..))+import Prelude hiding (id, (.))++-- $setup+-- >> import Circuit.Dagger+-- >> import Circuit.Tensor (Action (..), Tensor (..))+-- >> import Circuit.Channel (Traced (..))+-- >> import Circuit.Category (Category (..), Discrete (..), (.>))+-- >> import Prelude hiding (id, (.))++-- ---------------------------------------------------------------------------+-- MergeZero: monoid structure on channel objects+-- ---------------------------------------------------------------------------++-- | A commutative monoid on channel objects.+--+-- Not the same as arithmetic '+'; this is the operation by which parallel+-- contributions to the same wire combine.  Fan-out on the forward pass+-- becomes fan-in (summation) on the backward pass.+class MergeZero arr a where+  -- | Combine two values of the channel type.+  plus :: arr (a, a) a++  -- | The neutral element.+  zero :: arr () a++-- | The unit type carries the trivial monoid.+--+-- .> plus ((), ()) :: ()+-- ()+-- .> zero () :: ()+-- ()+instance MergeZero (->) () where+  plus _ = ()+  {-# INLINE plus #-}+  zero _ = ()+  {-# INLINE zero #-}++-- | Numeric carriers.  'plus' is addition, 'zero' is 0.+--+-- .> plus (1, 2) :: Int+-- 3+-- .> zero () :: Int+-- 0+-- .> plus (1.0, 2.0) :: Double+-- 3.0+-- .> zero () :: Double+-- 0.0+instance MergeZero (->) Int where+  plus = uncurry (+)+  {-# INLINE plus #-}+  zero _ = 0+  {-# INLINE zero #-}++instance MergeZero (->) Integer where+  plus = uncurry (+)+  {-# INLINE plus #-}+  zero _ = 0+  {-# INLINE zero #-}++instance MergeZero (->) Double where+  plus = uncurry (+)+  {-# INLINE plus #-}+  zero _ = 0+  {-# INLINE zero #-}++instance MergeZero (->) Float where+  plus = uncurry (+)+  {-# INLINE plus #-}+  zero _ = 0+  {-# INLINE zero #-}++-- | Boolean monoid under disjunction.+--+-- Idempotent because @True || True = True@.+--+-- .> plus (True, False) :: Bool+-- True+-- .> zero () :: Bool+-- False+instance MergeZero (->) Bool where+  plus = uncurry (||)+  {-# INLINE plus #-}+  zero _ = False+  {-# INLINE zero #-}++-- | Componentwise 'plus' on pairs.+--+-- .> plus ((3, 4), (5, 6)) :: (Int, Int)+-- (8,10)+instance (MergeZero (->) a, MergeZero (->) b) => MergeZero (->) (a, b) where+  plus ((a, b), (a', b')) = (plus (a, a'), plus (b, b'))+  {-# INLINE plus #-}+  zero u = (zero u, zero u)+  {-# INLINE zero #-}++-- | Lists via elementwise 'plus', padded with 'zero'.+--+-- For lists of unequal length, the shorter list is implicitly extended+-- with the element 'zero'. The unit is the empty list.+--+-- .> plus ([1, 2], [3, 4, 5]) :: [Int]+-- [4,6,5]+-- .> plus ([], [3, 4, 5]) :: [Int]+-- [3,4,5]+instance (MergeZero (->) a) => MergeZero (->) [a] where+  plus (xs, ys) = go xs ys+    where+      go [] [] = []+      go [] (y : ys') = plus (zero (), y) : go [] ys'+      go (x : xs') [] = plus (x, zero ()) : go xs' []+      go (x : xs') (y : ys') = plus (x, y) : go xs' ys'+  {-# INLINE plus #-}+  zero _ = []+  {-# INLINE zero #-}++-- ---------------------------------------------------------------------------+-- CopyDiscard: comonoid structure on channel objects+-- ---------------------------------------------------------------------------++-- | A cocommutative comonoid on channel objects.+--+-- Laws:+--+-- @+--   fst . copy = id              -- left unit+--   snd . copy = id              -- right unit+--   (copy × id) . copy = (id × copy) . copy  -- coassociativity+--   swap . copy = copy            -- cocommutativity+-- @+class CopyDiscard arr a where+  -- | Copy a value into a pair.+  copy :: arr a (a, a)++  -- | Discard a value.+  discard :: arr a ()++-- | Both the comonoid and monoid on a channel object.+--+-- A constraint synonym — no instance required.  On a cartesian base arrow,+-- every type carries both structures.  This is the precondition for+-- 'Circuit.Net.transpose' to be total.+type Bimonoid arr a = (CopyDiscard arr a, MergeZero arr a)++-- | Every type copies for free in a cartesian category (Fox's theorem).+--+-- .> copy (42 :: Int)+-- (42,42)+-- .> discard (42 :: Int)+-- ()+instance CopyDiscard (->) a where+  copy a = (a, a)+  {-# INLINE copy #-}+  discard _ = ()+  {-# INLINE discard #-}++-- ---------------------------------------------------------------------------+-- Dagger: the free dagger category over a base arrow+-- ---------------------------------------------------------------------------++-- | The free dagger category over a base arrow.+--+-- @Dagger arr a b@ is a pair of arrows @arr a b@ (forward) and+-- @arr b a@ (backward).  Composition is covariant forward, contravariant+-- backward: @Dagger f g . Dagger f' g' = Dagger (f . f') (g' . g)@.+--+-- .> let d = Dagger (+1) (subtract 1) :: Dagger (->) Int Int+-- .> front d 5+-- 6+-- .> back d 6+-- 5+data Dagger arr a b = Dagger+  { -- | The forward direction.+    front :: arr a b,+    -- | The backward direction.+    back :: arr b a+  }++-- | The dagger operation: swap forward and backward.+--+-- Involutive: @transpose . transpose = id@.+transpose :: Dagger arr a b -> Dagger arr b a+transpose (Dagger f g) = Dagger g f++instance (Category arr) => Category (Dagger arr) where+  type Ob (Dagger arr) a = Ob arr a+  id = Dagger id id+  {-# INLINE id #-}+  Dagger f g . Dagger f' g' = Dagger (f . f') (g' . g)+  {-# INLINE (.) #-}++-- | Dagger of a discrete base is discrete.+instance (Discrete arr) => Discrete (Dagger arr) where+  withOb @a x = withOb @arr @a x++instance (Strength t arr) => Strength t (Dagger arr) where+  strength (Dagger f g) = Dagger (strength f) (strength g)+  {-# INLINE strength #-}++instance (Traced t arr) => Traced t (Dagger arr) where+  trace (Dagger f g) = Dagger (trace f) (trace g)+  {-# INLINE trace #-}++-- | Forward copy, backward add — the bimonoid self-duality.+instance (CopyDiscard arr a, MergeZero arr a) => CopyDiscard (Dagger arr) a where+  copy = Dagger copy plus+  {-# INLINE copy #-}+  discard = Dagger discard zero+  {-# INLINE discard #-}++-- | Forward add, backward copy.+instance (CopyDiscard arr a, MergeZero arr a) => MergeZero (Dagger arr) a where+  plus = Dagger plus copy+  {-# INLINE plus #-}+  zero = Dagger zero discard+  {-# INLINE zero #-}++instance (Tensor t arr) => Tensor t (Dagger arr) where+  par (Dagger f g) (Dagger f' g') = Dagger (par f f') (par g g')+  {-# INLINE par #-}+  unitl = Dagger unitl unitl'+  {-# INLINE unitl #-}+  unitl' = Dagger unitl' unitl+  {-# INLINE unitl' #-}+  unitr = Dagger unitr unitr'+  {-# INLINE unitr #-}+  unitr' = Dagger unitr' unitr+  {-# INLINE unitr' #-}++instance (Action t arr) => Action t (Dagger arr) where+  swap = Dagger swap swap+  {-# INLINE swap #-}++-- | Lift monoidal structure through @Dagger@.+instance (Channel t arr) => Channel t (Dagger arr) where+  assoc = Dagger assoc assoc'+  assoc' = Dagger assoc' assoc+  slide = Dagger slide slide

@@ -0,0 +1,107 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}++-- | Discharge kit for authors of 'Discrete' categories and @Layer@ targets.+--+-- Free folds often need 'Ob' evidence at existential or compound objects+-- (intermediate composition objects, tensor products, feedback channels).+-- When the base category is 'Discrete', 'withOb' can manufacture that+-- evidence, but the resulting ladders are noisy. The helpers below package+-- the common patterns so instance authors do not rewrite them.+module Circuit.Discrete+  ( -- * Composition+    compD,++    -- * Channel structure+    assocD,+    assocD',+    braidD,++    -- * Strength and trace+    strengthD,+    traceD,+  )+where++import Circuit.Category (Category (..), Discrete (..))+import Circuit.Channel (Channel (..), Strength (..), Traced (..), strengthD)+import Prelude hiding (id, (.))++-- | Discrete composition: compose two arrows while discharging 'Ob'+-- constraints with 'withOb'.+compD ::+  forall arr a b c.+  (Discrete arr) =>+  arr b c ->+  arr a b ->+  arr a c+compD f g =+  withOb @arr @a $+    withOb @arr @b $+      withOb @arr @c $+        f . g++-- | Discrete associator: reassociate leftward while discharging 'Ob'+-- constraints.+assocD ::+  forall t arr a b c.+  (Channel t arr, Discrete arr) =>+  arr (t (t a b) c) (t a (t b c))+assocD =+  withOb @arr @a $+    withOb @arr @b $+      withOb @arr @c $+        withOb @arr @(t a b) $+          withOb @arr @(t b c) $+            withOb @arr @(t (t a b) c) $+              withOb @arr @(t a (t b c)) $+                assoc++-- | Discrete associator inverse: reassociate rightward while discharging+-- 'Ob' constraints.+assocD' ::+  forall t arr a b c.+  (Channel t arr, Discrete arr) =>+  arr (t a (t b c)) (t (t a b) c)+assocD' =+  withOb @arr @a $+    withOb @arr @b $+      withOb @arr @c $+        withOb @arr @(t a b) $+          withOb @arr @(t b c) $+            withOb @arr @(t a (t b c)) $+              withOb @arr @(t (t a b) c) $+                assoc'++-- | Discrete braiding: slide a wire past a nested pair while discharging+-- 'Ob' constraints.+braidD ::+  forall t arr a b c.+  (Channel t arr, Discrete arr) =>+  arr (t a (t b c)) (t b (t a c))+braidD =+  withOb @arr @a $+    withOb @arr @b $+      withOb @arr @c $+        withOb @arr @(t b c) $+          withOb @arr @(t a c) $+            withOb @arr @(t a (t b c)) $+              withOb @arr @(t b (t a c)) $+                slide++-- | Discrete trace: eliminate a feedback loop while discharging 'Ob'+-- constraints.+traceD ::+  forall t arr a b c.+  (Traced t arr, Discrete arr) =>+  arr (t a b) (t a c) ->+  arr b c+traceD f =+  withOb @arr @a $+    withOb @arr @b $+      withOb @arr @c $+        withOb @arr @(t a b) $+          withOb @arr @(t a c) $+            trace f

@@ -0,0 +1,430 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}++-- | Free channel ends over a base arrow, plus concrete box and queue helpers.+--+-- A channel has exactly two ends:+--+--   * @Out@ — the companion (read / emit end), covariant in the payload.+--   * @In@  — the conjoint (write / commit end), contravariant in the payload.+--+-- @Ends@ is the record that pairs one @In@ with one @Out@.  The ends are+-- defined purely in terms of the base arrow @arr@.+--+-- 'open' produces a matched pair; 'close' plugs the pair back together by+-- feeding the @Out@ into the @In@.+--+-- This module also provides the concrete helpers built on top of channel+-- ends:+--+--   * 'box' and 'boxAsymmetric' — embed an @Ends@ into a plain 'Loop'.+--   * 'Queue' strategies and STM / IO @Ends@ constructors ('openSTM',+--     'openIO').+module Circuit.Ends+  ( -- * Channel ends (bi-polar contract)+    Out (..),+    In (..),++    -- * Matched pair+    Ends (..),++    -- * Counit+    close,++    -- * Prefixing an action to an @In@+    prefixIn,++    -- * Suffixing an action to an @Out@+    suffixOut,++    -- * Build an @Ends@ from primitive actions+    ends,+    endsK,++    -- * Extract primitive actions from an @Ends@+    splay,++    -- * Unit ends (requires constant morphisms)+    HasUnit (..),++    -- * Boxes+    box,+    boxAsymmetric,++    -- * Queue strategies+    Queue (..),++    -- * STM @Ends@+    openSTM,++    -- * IO @Ends@+    openIO,+  )+where++import Circuit.Category (Category (..), Discrete (..), (.>))+import Circuit.Loop (Loop (..))+import Circuit.Tensor (Tensor (..), Unit)+import Control.Applicative+import Control.Arrow (Kleisli (..))+import Control.Concurrent.STM+import Control.Monad (void)+import Prelude hiding (id, (.))++-- $setup+-- >> :set -XTypeApplications+-- >> import Circuit.Category ((.>))+-- >> import Circuit.Ends+-- >> import Circuit.Layer (run)+-- >> import Control.Arrow (Kleisli(..), runKleisli)+-- >> import Control.Concurrent.STM (STM, atomically)++-- ---------------------------------------------------------------------------+-- Channel ends — the companion and conjoint of the identity functor.+-- ---------------------------------------------------------------------------++-- | @Out@ is the companion of the identity functor.  Covariant in @a@+-- (sits in the output position).+newtype Out arr a = Out+  { -- | Emit through the companion, supplying the other end.+    emit :: forall x. In arr x -> arr x a+  }++-- | @In@ is the conjoint of the identity functor.  Contravariant in+-- @a@ (sits in the input position).+newtype In arr a = In+  { -- | Commit through the conjoint, supplying the other end.+    commit :: forall x. Out arr x -> arr a x+  }++-- | A matched pair of channel ends: one @In@ and one @Out@.+--+-- This is the bi-polar communication contract.  The conjoint (@In@)+-- consumes payloads of type @a@; the companion (@Out@) produces payloads+-- of type @b@.  For symmetric channels such as queues @a = b@.+--+-- Together with 'prefixIn' and 'suffixOut', @Ends@ carries an /enriched/+-- profunctor structure over the base category @arr@: 'prefixIn' is the+-- left action of @arr@ on @In@ ends, and 'suffixOut' is the right action+-- of @arr@ on @Out@ ends.+data Ends arr a b = Ends+  { -- | Write end (producer), the conjoint.+    conjoint :: In arr a,+    -- | Read end  (consumer), the companion.+    companion :: Out arr b+  }++-- | Plug an @In@ and an @Out@ of the same payload type together.+--+-- 'close' feeds the @Out@ into the @In@ end, producing a morphism+-- @arr a a@ from the paired payload type.+--+-- Yanking: for the unit ends from 'open',+-- @close (conjoint ends) (companion ends) = id@.+close :: In arr a -> Out arr a -> arr a a+close contra = commit contra++-- | Precompose an @arr@-morphism with an @In@ end.+--+-- Given @f :: arr a b@ and an @In@ end at type @b@, produce an @In@ end+-- at type @a@.  Running the resulting end first executes @f@ and then+-- commits through the original end.+--+-- This is the left (contravariant) action of the base category on @In@+-- ends.  Specialised to unit ends it is the canonical way to build+-- effectful write ends.+--+-- .> let endsU = open :: Ends (->) () ()+-- .> let inA = prefixIn (const ()) (conjoint endsU) :: In (->) Int+-- .> commit inA (companion endsU) 42+-- ()+prefixIn :: forall arr a b. (Discrete arr) => arr a b -> In arr b -> In arr a+prefixIn f i = In $ \(o :: Out arr x) -> withOb @arr @a $ withOb @arr @b $ withOb @arr @x $ f .> commit i o++-- | Postcompose an @arr@-morphism with an @Out@ end.+--+-- Given an @Out@ end at type @a@ and @g :: arr a b@, produce an @Out@+-- end at type @b@.  Running the resulting end first emits through the+-- original end and then executes @g@ on the emitted value.+--+-- This is the right (covariant) action of the base category on @Out@+-- ends.  Specialised to unit ends it is the canonical way to build+-- effectful read ends.+--+-- .> let endsU = open :: Ends (->) () ()+-- .> let outA = suffixOut (companion endsU) (const 42) :: Out (->) Int+-- .> emit outA (conjoint endsU) ()+-- 42+suffixOut :: forall arr a b. (Discrete arr) => Out arr a -> arr a b -> Out arr b+suffixOut o g = Out $ \(i :: In arr x) -> withOb @arr @x $ withOb @arr @a $ withOb @arr @b $ emit o i .> g++-- ---------------------------------------------------------------------------+-- Unit ends+-- ---------------------------------------------------------------------------++-- | Arrows that have unit channel ends for a given unit object @u@.+--+-- The unit ends are the identity-on-@u@ morphism split into its two+-- polar halves.  The companion is constant; the conjoint delegates to+-- the opposing companion.+--+-- These ends require the base arrow to support constant morphisms, so+-- they are captured by this class rather than being definable for all+-- arrows.+class (Category arr) => HasUnit u arr where+  -- | The monoidal unit as channel ends.+  --+  -- === Yank+  --+  -- >>> let ends = open :: Ends (->) () ()+  -- >>> close (conjoint ends) (companion ends) ()+  -- ()+  --+  -- === Unit plug+  --+  -- >>> let endsA = open :: Ends (->) () ()+  -- >>> let endsU = open :: Ends (->) () ()+  -- >>> commit (conjoint endsA) (companion endsU) ()+  -- ()+  -- >>> emit (companion endsA) (conjoint endsU) ()+  -- ()+  open :: Ends arr u u++-- | Build an @Ends@ from a write morphism and a read morphism.+--+-- @write :: arr a ()@ consumes the input payload and produces the unit;+-- @read :: arr () b@ consumes the unit and produces the output payload.+-- The unit ends wire the two halves together.+--+-- This is the canonical way to turn a pair of primitive channel actions+-- into a matched pair of @In@ and @Out@ ends.+--+-- Compositional spelling:+--+-- @+-- ends write receive =+--   Ends (prefixIn write (conjoint open)) (suffixOut (companion open) receive)+-- @+ends ::+  forall arr a b.+  (Discrete arr, HasUnit () arr) =>+  arr a () ->+  arr () b ->+  Ends arr a b+ends write receive =+  Ends+    (prefixIn write (conjoint open))+    (suffixOut (companion open) receive)++-- | Specialization of 'ends' for @Kleisli@ actions.+--+-- @write :: a -> m ()@ consumes the input payload; @receive :: m b@+-- produces the output payload. The unit handling is hidden inside the+-- @Kleisli@ wrappers.+endsK ::+  forall m a b.+  (Monad m) =>+  (a -> m ()) ->+  m b ->+  Ends (Kleisli m) a b+endsK write receive = ends (Kleisli write) (Kleisli $ const receive)++-- | Extract the primitive write and read actions from an @Ends@ by+-- plugging each end with the unit ends.+--+-- For an @Ends@ built with 'ends', this recovers the original+-- @write :: arr a ()@ and @receive :: arr () b@.+--+-- .> let e = ends (\() -> ()) (const (42 :: Int)) :: Ends (->) () Int+-- .> let (write, receive) = splay e+-- .> (write (), receive ())+-- ((),42)+splay ::+  forall arr a b.+  (HasUnit () arr) =>+  Ends arr a b ->+  (arr a (), arr () b)+splay e =+  ( commit (conjoint e) (companion (open :: Ends arr () ())),+    emit (companion e) (conjoint (open :: Ends arr () ()))+  )++-- | Unit ends for @(->)@ with unit @()@.+--+-- The companion is the constant function returning @()@; the conjoint+-- recursively emits through the supplied companion.+instance HasUnit () (->) where+  open = Ends inU outU+    where+      outU = Out $ \_ -> const ()+      inU = In $ \o -> emit o inU++-- | Unit ends for @Kleisli@ @m@ with unit @()@.+--+-- Same shape as the @(->)@ instance, but the constant companion returns+-- @()@ in the monad.+instance (Monad m) => HasUnit () (Kleisli m) where+  open = Ends inU outU+    where+      outU = Out $ \_ -> Kleisli $ \_ -> pure ()+      inU = In $ \o -> emit o inU++-- ---------------------------------------------------------------------------+-- Boxes+-- ---------------------------------------------------------------------------++-- | String-diagram boxes from channel ends.+--+-- A matched pair of free ends (@Ends@) is a box with one input wire and+-- one output wire.  The helpers below embed that box into a traced+-- monoidal category by unit-plugging the remaining two slots.++-- | Embed an @Ends@ into a plain @Loop t arr a b@.+--+-- Connects the two channel ends through the unit object, giving a plain+-- @Loop t arr a b@. This is the version most users expect: input on the+-- left, output on the right, with the unit plumbing hidden.+--+-- .> let e = ends (const ()) (const 42) :: Ends (->) () Int+-- .> run (box @(,) e) ()+-- 42+box ::+  forall t arr a b.+  (HasUnit (Unit t) arr, Ob arr a, Ob arr b, Ob arr (Unit t)) =>+  Ends arr a b ->+  Loop t arr a b+box ends' =+  Lift $+    commit (conjoint ends') (companion (open :: Ends arr (Unit t) (Unit t)))+      .> emit (companion ends') (conjoint (open :: Ends arr (Unit t) (Unit t)))++-- | Asymmetric box with units exposed on opposite sides.+--+-- Uses 'par' at the base arrow level and lifts the result with 'Lift'.+-- The input carries the unit on the right and the output carries the unit+-- on the left; most users will prefer the unit-normalised 'box'.+--+-- .> let e = ends (const ()) (const 42) :: Ends (->) () Int+-- .> run (boxAsymmetric @(,) e) ((), ())+-- ((),42)+boxAsymmetric ::+  forall t arr a b.+  (HasUnit (Unit t) arr, Tensor t arr) =>+  Ends arr a b ->+  Loop t arr (t a (Unit t)) (t (Unit t) b)+boxAsymmetric ends' =+  Lift $+    par+      (commit (conjoint ends') (companion open))+      (emit (companion ends') (conjoint open))++-- ---------------------------------------------------------------------------+-- Queue strategies and STM @Ends@+-- ---------------------------------------------------------------------------++-- | How messages are queued between producer and consumer.+data Queue a+  = -- | Unbounded FIFO queue.+    Unbounded+  | -- | Bounded FIFO with backpressure (write blocks when full).+    Bounded Int+  | -- | Single-slot buffer (write blocks when full).+    Single+  | -- | Single-slot buffer, overwrite-on-full.+    -- Write always succeeds; read empties.+    SwapQ+  | -- | Always holds the latest value (overwrites, never blocks).+    Latest a+  | -- | Like @Bounded@ but drops oldest when full.+    Newest Int+  deriving (Show, Eq)++-- ---------------------------------------------------------------------------+-- STM ends+-- ---------------------------------------------------------------------------++-- | Internal STM primitive for a queue strategy.+--+-- Returns the raw write/read actions used by 'openSTM'.  Not exported;+-- the canonical API is 'openSTM'.+endsSTM :: Queue a -> STM (a -> STM (), STM a)+endsSTM = \case+  Bounded n -> do+    q <- newTBQueue (fromIntegral n)+    pure (writeTBQueue q, readTBQueue q)+  Unbounded -> do+    q <- newTQueue+    pure (writeTQueue q, readTQueue q)+  Single -> do+    m <- newEmptyTMVar+    pure (putTMVar m, takeTMVar m)+  SwapQ -> do+    v <- newEmptyTMVar+    let write x = tryPutTMVar v x >>= \case True -> pure (); False -> void (swapTMVar v x)+    pure (write, takeTMVar v)+  Latest a -> do+    t <- newTVar a+    pure (writeTVar t, readTVar t)+  Newest n -> do+    q <- newTBQueue (fromIntegral n)+    let write x = writeTBQueue q x <|> (tryReadTBQueue q *> write x)+    pure (write, readTBQueue q)++-- ---------------------------------------------------------------------------+-- IO @Ends@+-- ---------------------------------------------------------------------------++-- | Open a queue strategy as STM @Ends@.+--+-- Allocates STM primitives and returns a matched pair of ends sharing+-- the same mutable channel.  Both ends live in 'STM', so you can compose+-- operations across channels in a single 'atomically' block.+--+-- === Unbounded+--+-- .> let endsU = open :: Ends (Kleisli STM) () ()+-- .> ends <- atomically (openSTM Unbounded :: STM (Ends (Kleisli STM) Int Int))+-- .> atomically $ runKleisli (commit (conjoint ends) (companion endsU)) 42+-- .> atomically $ runKleisli (emit (companion ends) (conjoint endsU)) ()+-- 42+--+-- Multi-op compose in one 'atomically' (both writes + read):+--+-- .> ends <- atomically (openSTM Unbounded :: STM (Ends (Kleisli STM) Int Int))+-- .> atomically $ runKleisli (commit (conjoint ends) (companion endsU)) 1 >> runKleisli (commit (conjoint ends) (companion endsU)) 2 >> runKleisli (emit (companion ends) (conjoint endsU)) ()+-- 1+--+-- 'close' recovers the value through the queue:+--+-- .> ends <- atomically (openSTM Unbounded :: STM (Ends (Kleisli STM) Int Int))+-- .> atomically $ runKleisli (close (conjoint ends) (companion ends)) 7+-- 7+--+-- === SwapQ (overwrite on write)+--+-- .> ends <- atomically (openSTM SwapQ :: STM (Ends (Kleisli STM) Int Int))+-- .> atomically $ runKleisli (commit (conjoint ends) (companion endsU)) 1 >> runKleisli (commit (conjoint ends) (companion endsU)) 2 >> runKleisli (emit (companion ends) (conjoint endsU)) ()+-- 2+openSTM :: Queue a -> STM (Ends (Kleisli STM) a a)+openSTM q = do+  (write, read') <- endsSTM q+  pure (endsK write read')++-- | Open a queue strategy as IO @Ends@.+--+-- Like 'openSTM', but each primitive operation is wrapped in its own+-- 'atomically'.  You cannot batch multiple writes or a write-plus-read+-- into a single STM transaction; for that use 'openSTM' and wrap in+-- 'atomically' yourself.+--+-- .> let endsU = open :: Ends (Kleisli IO) () ()+-- .> ends <- openIO Unbounded :: IO (Ends (Kleisli IO) Int Int)+-- .> runKleisli (commit (conjoint ends) (companion endsU)) 42+-- .> runKleisli (emit (companion ends) (conjoint endsU)) ()+-- 42+openIO :: Queue a -> IO (Ends (Kleisli IO) a a)+openIO q = do+  e <- atomically (openSTM q)+  let (Kleisli write, Kleisli receive) = splay e+  pure (endsK (atomically . write) (atomically (receive ())))

@@ -0,0 +1,103 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -Wno-orphans #-}++-- | The free category over a base arrow.+--+-- The two constructors are 'Lift', which embeds a base arrow, and+-- 'Compose', which sequences two free morphisms.  The universal fold out+-- of 'Free' is 'run'.+module Circuit.Free+  ( Free (..),+    freeze,+  )+where++import Circuit.Category (Category (..), Discrete (..))+import Circuit.Channel (Channel (..), Strength (..), Traced (..))+import Circuit.Layer (Layer (..), (:~>))+import Prelude hiding (id, (.))++-- $setup+-- >> import Circuit.Free+-- >> import Circuit.Layer (run)+-- >> import Prelude hiding (id, (.))++-- | The free category over a base arrow @arr@.+--+-- Two constructors:+--+--   * 'Lift' — embed a base arrow.+--   * 'Compose' — sequential composition.+--+-- .> run (Lift (+1) :: Free (->) Int Int) 5+-- 6+-- .> run (Compose (Lift (+1)) (Lift (*2)) :: Free (->) Int Int) 5+-- 11+data Free arr a b where+  -- | Embed a base arrow.+  Lift :: arr a b -> Free arr a b+  -- | Sequential composition.+  --+  -- The 'Ob' constraint on the intermediate object @b@ is carried in the+  -- constructor so folding does not need a 'Discrete' base.+  Compose :: (Ob arr b) => Free arr b c -> Free arr a b -> Free arr a c++instance (Category arr) => Category (Free arr) where+  type Ob (Free arr) a = Ob arr a+  id = Lift id+  (.) = Compose++-- | A discrete base yields a discrete free category.+instance (Discrete arr) => Discrete (Free arr) where+  withOb @a x = withOb @arr @a x++-- | Layer instance for the free category.+--+-- 'Compose' carries the intermediate 'Ob' evidence of the /source/+-- category, but folding into a target category @arr'@ still needs to+-- manufacture the corresponding 'Ob arr' b' evidence.  That is exactly+-- what 'Discrete arr'' provides, so 'Law' is 'Discrete'.+instance Layer Free where+  type Law Free arr' = Discrete arr'+  type Run Free arr = Category arr+  type Bind Free arr = ()+  unit = Lift+  run (Lift f) = f+  run (Compose g f) = run g . run f+  bind :: forall arr' arr a b. (Law Free arr', Ob arr a, Ob arr b, Ob arr' a, Ob arr' b) => (arr :~> arr') -> Free arr a b -> arr' a b+  bind h (Lift f) = h f+  bind h (Compose @_ @b1 g f) = withOb @arr' @b1 (bind h g . bind h f)++-- | Freeze a 'Free' category into its base arrow.+--+-- This is a synonym for 'run' @Free@.+--+-- .> freeze (Lift (+1) :: Free (->) Int Int) 5+-- 6+freeze :: (Category arr, Ob arr a, Ob arr b) => Free arr a b -> arr a b+freeze (Lift f) = f+freeze (Compose g f) = freeze g . freeze f++-- | Lift the 'Channel' structure through 'Free'.+instance (Channel t arr) => Channel t (Free arr) where+  assoc = Lift assoc+  assoc' = Lift assoc'+  slide = Lift slide++-- | Lift the 'Strength' class through 'Free'.+--+-- A morphism is frozen before tensoring with the feedback channel.+instance (Strength t arr) => Strength t (Free arr) where+  strength = Lift . strength . freeze++-- | Lift the 'Traced' class through 'Free'.+--+-- A loop body in @Free arr@ is frozen before calling the base 'trace'.+instance (Traced t arr) => Traced t (Free arr) where+  trace = Lift . trace . freeze

@@ -1,4 +1,4 @@-{-# LANGUAGE CPP #-}+{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-}  -- | Hyperfunctions: final encoding of traced monoidal categories.@@ -7,8 +7,8 @@ -- defined by its dual: to produce a result of type @b@ you must supply -- a continuation of type @Hyper b a@. ----- 'Hyper' is the /final/ (coinductive) encoding of a traced monoidal--- category. Its dual, 'Circuit' (see "Circuit.Circuit"), is the+-- @Hyper@ is the /final/ (coinductive) encoding of a traced monoidal+-- category. Its dual, 'Loop' (see "Circuit.Loop"), is the -- corresponding /initial/ (inductive) encoding. The feedback channel -- is not represented by an extra constructor; it is structural in the -- type itself.@@ -18,53 +18,53 @@      -- * Construction and elimination     lift,-    lower,+    observe,     base,     push,-    run,+    runHyper,      -- * Encoding     encode,+    encodeFree,     encodeEither,     runEither,     flatten,   ) where -import Circuit.Circuit (Circuit (..), reify)-import Circuit.Traced (Trace (..))-import Prelude hiding (id, (.))--#ifdef __GLASGOW_HASKELL__-import Control.Category+import Circuit.Category (Category (..), Discrete (..), (.>))+import Circuit.Channel (Channel (..), Strength (..), Traced (..))+import Circuit.Free qualified as F+import Circuit.Layer (Layer, bind, run, (:~>))+import Circuit.Loop (Loop (..))+import Data.Bifunctor (second) import Data.Profunctor-#else-import Circuit.Classes-#endif+import Prelude hiding (id, (.))  -- $setup--- >>> import Prelude hiding (id, (.))--- >>> import Control.Category--- >>> import Data.Profunctor--- >>> import Circuit.Traced (Trace (..))--- >>> import Circuit.Circuit (Circuit (..), reify)--- >>> let h = lift (+1) :: Hyper Int Int--- >>> let f1 = (*2) :: Int -> Int--- >>> let g1 = (+10) :: Int -> Int--- >>> let f2 = (+3) :: Int -> Int--- >>> let g2 = (*100) :: Int -> Int+-- >> import Prelude hiding (id, (.))+-- >> import Circuit.Category (Category (..), Discrete (..), (.>))+-- >> import Data.Profunctor+-- >> import Circuit.Channel (Traced (..))+-- >> import Circuit.Loop (Loop (..))+-- >> import Circuit.Layer (run)+-- >> let h = lift (+1) :: Hyper Int Int+-- >> let f1 = (*2) :: Int -> Int+-- >> let g1 = (+10) :: Int -> Int+-- >> let f2 = (+3) :: Int -> Int+-- >> let g2 = (*100) :: Int -> Int  -- | A hyperfunction from @a@ to @b@. ----- A 'Hyper' is completely determined by its dual. To get a @b@ you must+-- A @Hyper@ is completely determined by its dual. To get a @b@ you must -- provide a continuation that can itself produce an @a@. -- -- Two small examples: ----- >>> lower (lift (+1)) 41+-- .> observe (lift (+1)) 41 -- 42 ----- >>> run (Hyper $ \k -> invoke k (Hyper $ \_ -> 0) + 1)+-- .> runHyper (Hyper $ \k -> invoke k (Hyper $ \_ -> 0) + 1) -- 1 newtype Hyper a b = Hyper   { -- | Feed a continuation of type @Hyper b a@ into the hyperfunction.@@ -75,11 +75,11 @@  -- | Embed a plain function into a hyperfunction. ----- This is where the coinductive character of 'Hyper' lives:+-- This is where the coinductive character of @Hyper@ lives: -- @lift f@ creates a hyperfunction by recursively pushing @f@ onto -- every future continuation that will ever be supplied. ----- >>> lower (lift (+1)) 5+-- .> observe (lift (+1)) 5 -- 6 lift :: (a -> b) -> Hyper a b lift f = push f (lift f)@@ -90,14 +90,14 @@ -- (@invoke h (Hyper (const a))@), asking: "what output do you produce -- when the feedback channel feeds back the input @a@?" ----- >>> lower (lift reverse) "hello"+-- .> observe (lift reverse) "hello" -- "olleh"-lower :: Hyper a b -> (a -> b)-lower h a = invoke h (Hyper (const a))+observe :: Hyper a b -> (a -> b)+observe h a = invoke h (Hyper (const a))  -- | Ignores the input and returns a constant value. ----- >>> lower (base 42) undefined+-- .> observe (base 42) undefined -- 42 base :: a -> Hyper b a base a = Hyper (const a)@@ -108,42 +108,39 @@ -- eventually produces. This threads @f@ through the continuation, -- enabling feedback-aware composition. ----- >>> lower (push (+1) (lift (*2))) 5+-- .> observe (push (+1) (lift (*2))) 5 -- 6 push :: (a -> b) -> Hyper a b -> Hyper a b push f h = Hyper (\k -> f (invoke k h))  -- | Close the self-referential loop. ----- @run h@ feeds the hyperfunction back into itself, tying the knot.--- This is the fundamental way to eliminate a 'Hyper'.+-- @runHyper h@ feeds the hyperfunction back into itself, tying the knot.+-- This is the fundamental way to eliminate a @Hyper@. ----- >>> run (Hyper $ \_ -> 42 :: Int)+-- .> runHyper (Hyper $ \_ -> 42 :: Int) -- 42 ----- >>> run (Hyper $ \h -> invoke h (Hyper $ \_ -> 0) + 1) :: Int+-- .> runHyper (Hyper $ \h -> invoke h (Hyper $ \_ -> 0) + 1) :: Int -- 1-run :: Hyper a a -> a-run h = invoke h (Hyper run)+runHyper :: Hyper a a -> a+runHyper h = invoke h (Hyper runHyper)  -- * Properties  -- Faithful embedding: observation recovers the original arrow. ----- prop> \x -> lower (lift (+1)) (x :: Int) == x + 1+-- prop> \x -> observe (lift (+1)) (x :: Int) == x + 1  -- Functoriality: lift respects composition. ----- prop> \x -> lower (lift (*2) . lift (+1)) (x :: Int) == (x + 1) * 2+-- prop> \x -> observe (lift (*2) . lift (+1)) (x :: Int) == (x + 1) * 2 --- * Trace+-- * Loop --- | 'Trace' instance for 'Hyper' with the @(,)@ tensor.+-- | 'Loop' instance for @Hyper@ with the @(,)@ tensor. ----- Transcribes the lazy-knot trace from @(->)@ into Hyper's continuation--- language. Where @Trace (->) (,)@ can write @let (a, c) = f (a, b) in c@--- directly, Hyper must route the self-reference through explicit 'Hyper'--- values:+-- Routes the self-reference through explicit @Hyper@ values: -- --   1. @invoke body cont@ calls the body, which will eventually ask @cont@ --      for an @(a, b)@ — the feedback pair.@@ -153,48 +150,66 @@ --   3. @invoke k (Hyper (const (snd pair)))@ converts the output @c@ to a --      @b@ for @cont@'s return type — purely type plumbing. ----- Law: @lower (trace (lift f)) x = trace \@ (->) f x@------ >>> import Circuit.Traced (Trace (..))--- >>> let body = lift (\(xs, ()) -> (0:xs, take 3 xs))--- >>> lower (trace body) ()+-- .> import Circuit.Channel (Traced (..))+-- .> let body = lift (\(xs, ()) -> (0:xs, take 3 xs))+-- .> observe (trace body) () -- [0,0,0]-instance Trace Hyper (,) where+instance Channel (,) Hyper where+  assoc = lift $ \((a, b), c) -> (a, (b, c))+  assoc' = lift $ \(a, (b, c)) -> ((a, b), c)+  slide = lift $ \(a, (b, c)) -> (b, (a, c))++instance Strength (,) Hyper where+  strength h = lift (second (observe h))++instance Traced (,) Hyper where   trace body = Hyper $ \k ->     let pair = invoke body cont         cont = Hyper $ \_ ->           let a_val = invoke k (Hyper (const (snd pair)))            in (fst pair, a_val)      in snd pair-  untrace = lift . fmap . lower --- * Encoding Circuit into Hyper+-- * Encoding Loop into Hyper --- | Encode a Circuit into a Hyper. Symbol: @(⇨)@.+-- | Encode a Free into a Hyper. ----- This is the unique traced functor from the initial object (Circuit)--- to the final object (Hyper), satisfying the commuting triangle--- @lower . encode = reify@.+-- The lift of the canonical fold 'run' into the final encoding. ----- The @Knot@ case uses Hyper's own @Trace (,)@ instance — a coinductive--- lazy knot that preserves the feedback structure inside Hyper.--- For an Either-loop encoding, see 'encodeEither'.+-- Law: @'observe' . 'encodeFree' = 'run'@ — the two interpreters+-- from Free agree. ----- >>> import Circuit.Circuit (Circuit (..), reify)--- >>> lower (encode (Lift (+1) :: Circuit (->) (,) Int Int)) 5+-- .> import Circuit.Free qualified as F+-- .> observe (encodeFree (F.Lift (+1))) 5 -- 6-encode :: Circuit (->) (,) a b -> Hyper a b+encodeFree :: F.Free (->) a b -> Hyper a b+encodeFree (F.Lift f) = lift f+encodeFree (F.Compose f g) = encodeFree f . encodeFree g++-- | Encode a Loop into a Hyper.+--+-- This is the unique traced functor from the initial object ('Loop')+-- to the final object (@Hyper@), satisfying the commuting triangle+-- @'observe' . 'encode' = 'run'@.+--+-- 'Lift' constructors embed directly via 'lift'; 'Knot' constructors+-- become 'trace' over a hyperfunction.+--+-- .> import Circuit.Layer (run)+-- .> import Circuit.Loop (Loop (..))+-- .> observe (encode (Lift (+1) :: Loop (,) (->) Int Int)) 5+-- 6+encode :: Loop (,) (->) a b -> Hyper a b encode (Lift f) = lift f-encode (Compose f g) = encode f . encode g encode (Knot f) = trace (lift f)  -- | Encode an Either-loop as a self-referential Hyper. ----- Whereas 'encode' handles the @(,)@ tensor using Hyper's own Trace+-- Whereas 'encode' handles the @(,)@ tensor using Hyper's own Loop -- instance, this preserves the Either-loop state in the function domain. -- @Left a@ feeds back; @Right c@ terminates with output. ----- >>> :{+-- .> :{ -- let step = \case --       Right n | n < 3 -> Left (n + 1) --       Right n         -> Right n@@ -202,7 +217,7 @@ --       Left n          -> Right n -- :} ----- >>> runEither step (0 :: Int)+-- .> runEither step (0 :: Int) -- 3 encodeEither :: (Either a b -> Either a c) -> Hyper (Either a b -> c) (Either a b -> c) encodeEither f = h@@ -217,11 +232,10 @@  -- | Run an 'encodeEither'-encoded circuit from initial input @b@. ----- @runEither@ is to @encodeEither@ what @run . lift@ is to plain functions:--- 'encodeEither' embeds the Either state machine into Hyper, @run@ ties the--- self-referential knot, and @Right b@ injects the initial state.+-- 'encodeEither' embeds the Either state machine into Hyper, @runHyper@ ties+-- the self-referential knot, and @Right b@ injects the initial state. ----- >>> :{+-- .> :{ -- let step = \case --       Right n | n < 3 -> Left (n + 1) --       Right n         -> Right n@@ -229,55 +243,65 @@ --       Left n          -> Right n -- :} ----- >>> runEither step (0 :: Int)+-- .> runEither step (0 :: Int) -- 3 runEither :: (Either a b -> Either a c) -> b -> c-runEither f b = run (encodeEither f) (Right b)+runEither f b = runHyper (encodeEither f) (Right b) --- | Flatten a Hyper to a Circuit by observing it.+-- | Flatten a Hyper to a Loop by observing it. -- -- This is the forgetful map from the final encoding to the initial encoding. -- All feedback structure is lost; only the observable behaviour remains. ----- >>> let h = lift (+ 1)--- >>> reify (flatten h) 5+-- .> let h = lift (+ 1)+-- .> run (flatten h) 5 -- 6 -- -- Flatten then encode is not identity — the feedback structure is gone: ----- >>> let h = lift (+ 1)--- >>> lower (encode (flatten h)) 5+-- .> let h = lift (+ 1)+-- .> observe (encode (flatten h)) 5 -- 6-flatten :: Hyper a b -> Circuit (->) (,) a b-flatten h = Lift (lower h)+flatten :: Hyper a b -> Loop (,) (->) a b+flatten h = Lift (observe h)  -- * Instances  instance Category Hyper where+  type Ob Hyper a = ()   id = lift id   f . g = Hyper $ \h -> invoke f (g . h) --- | 'Profunctor' instance for 'Hyper'.+-- | 'Profunctor' instance for @Hyper@. ----- 'rmap' is not a composition of 'push'; it acts directly on the--- hyperfunction's output. 'dimap' routes both input and output--- through the continuation structure.+-- 'dimap' routes both input and output through the continuation+-- structure. -- -- Profunctor identity: dimap id id = id ----- prop> \x -> lower (dimap id id h) (x :: Int) == x + 1+-- .> observe (dimap id id h) 5+-- 6 -- -- Profunctor composition: dimap f g . dimap f' g' = dimap (f' . f) (g . g') ----- prop> \x -> lower (dimap f1 g1 (dimap f2 g2 h)) (x :: Int) == lower (dimap (f2 . f1) (g1 . g2) h) x+-- .> observe (dimap f1 g1 (dimap f2 g2 h)) 5+-- 1410+-- .> observe (dimap (f2 . f1) (g1 . g2) h) 5+-- 1410 -- -- lmap f = dimap f id ----- prop> \x -> lower (lmap ((*2) :: Int -> Int) h) (x :: Int) == lower (dimap ((*2) :: Int -> Int) id h) x+-- .> observe (lmap ((*2) :: Int -> Int) h) 5+-- 11+-- .> observe (dimap ((*2) :: Int -> Int) id h) 5+-- 11 -- -- rmap g = dimap id g ----- prop> \x -> lower (rmap ((*2) :: Int -> Int) h) (x :: Int) == lower (dimap id ((*2) :: Int -> Int) h) x+-- .> observe (rmap ((*2) :: Int -> Int) h) 5+-- 12+-- .> observe (dimap id ((*2) :: Int -> Int) h) 5+-- 12 instance Profunctor Hyper where   dimap f g h = Hyper $ g . invoke h . dimap g f   lmap f h = Hyper $ invoke h . rmap f

@@ -0,0 +1,106 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++-- | The free-layer / free-forgetful adjunction tower.+--+-- Each layer @f@ is a free construction over a base arrow:+--+-- * @run@ @Free@       — free category+-- * @run@ @Sym@        — free symmetric monoidal category+-- * @run@ @(Loop t)@  — free traced monoidal category+-- * @run@ @(Net t)@    — free traced PROP with bimonoid+--+-- 'Law' says what the /target/ category must satisfy to receive a 'bind'+-- fold; 'Run' says what the /base/ category must satisfy for a same-category+-- 'run'; and 'Bind' captures any extra source constraints needed when the+-- free syntax has structural rows that do not carry all 'Ob' evidence.+--+-- The hom-set isomorphism is stated once, generically:+--+-- @+--   bind h . unit = h              (β)+--   bind unit      = id            (η)+--   run            = bind id       (coherence, where both sides are defined)+-- @+--+-- Composition of layers is just nesting — no new operator, no bespoke+-- coherence lemmas.+module Circuit.Layer+  ( -- * Free-layer class+    Cat2,+    (:~>),+    Layer (..),++    -- * Derived vocabulary+    lower,+  )+where++import Circuit.Category (Category (..))+import Data.Kind (Constraint, Type)+import Prelude hiding (id, (.))++-- $setup+-- >> import Circuit.Category (Category(..))+-- >> import Circuit.Free (Free)++-- | The kind of Haskell categories: type-to-type hom-sets.+type Cat2 = Type -> Type -> Type++-- | An arrow-to-arrow mapping (a natural transformation between+-- profunctors).+type arr :~> arr' = forall x y. arr x y -> arr' x y++-- | A free construction over a base arrow.+--+-- * 'unit' includes the generators.+-- * 'run' folds the free syntax back into the same base category.+-- * 'bind' folds the free syntax into any 'Law'-abiding target.+class Layer (f :: Cat2 -> Cat2) where+  -- | What the target category must satisfy to receive a 'bind' fold.+  -- 'run' only needs the base category's own object constraints.+  type Law f (arr' :: Cat2) :: Constraint++  -- | What the base category must satisfy to receive a 'run' fold back into+  -- itself.  Defaults to no extra constraints.+  type Run f (arr :: Cat2) :: Constraint++  type Run f arr = ()++  -- | Extra constraints the /source/ category must satisfy for a 'bind'+  -- fold.  Defaults to no extra constraints; instances with structural+  -- rows that do not carry all needed 'Ob' evidence may require @Discrete@.+  --+  -- For example, 'Sym.Par' reuses the base 'Tensor.par' method, which is+  -- deliberately 'Ob'-free; because 'par = Par' has no object dictionaries+  -- to stash in the constructor, the source category must be @Discrete@ so+  -- the missing evidence can be manufactured on demand.+  type Bind f (arr :: Cat2) :: Constraint++  type Bind f arr = ()++  -- | Include a base arrow as a single generator.+  unit :: (Category arr) => arr :~> f arr++  -- | Fold the free syntax into the same base category.+  --+  -- Implemented directly by each instance so that constrained categories+  -- (e.g. matrices) do not need a @Discrete@ instance for same-category+  -- folds.+  run :: (Run f arr, Ob arr a, Ob arr b) => f arr a b -> arr a b++  -- | The universal fold out of the free construction into any+  -- 'Law'-abiding target category.+  bind ::+    (Law f arr', Bind f arr, Ob arr a, Ob arr b, Ob arr' a, Ob arr' b) =>+    (arr :~> arr') ->+    f arr a b ->+    arr' a b++-- | The left direction of the hom-set isomorphism: restrict a map out of+-- the free layer to the generators.+lower :: (Layer f, Category arr) => (f arr :~> arr') -> (arr :~> arr')+lower g = g . unit

@@ -0,0 +1,261 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wno-orphans #-}++-- | The free traced monoidal category, in existential normal form.+--+-- @Loop t arr a b@ is the free traced monoidal category over a base+-- morphism @arr@ with tensor @t@. The two constructors encode:+--+--   * 'Lift' — a plain base arrow.+--   * 'Knot' — a feedback loop with a hidden feedback channel.+--+-- The laws of traced monoidal categories are performed by the 'Category'+-- and 'Traced' instances, so every value is already in normal form: at most+-- one 'Knot' at the top, over a base-arrow body.+--+-- For example, a @Loop (,) (->)@ is the initial traced monoidal cartesian+-- category over Haskell functions.+--+-- = Introduce / resolve+--+-- The vocabulary in this module follows the introduce/resolve pattern:+--+--   * 'Knot' introduces feedback; 'trace' resolves it. This is the gold+--     type-changing pair; composition fuses 'Knot's.+--+-- The polar channel ends (@Out@, @In@), their counit (@close@), and+-- their unit (@open@) all live in "Circuit.Ends".+--+-- == Interpreting a 'Loop'+--+-- Use 'run' or 'bind' to interpret a 'Loop' into a target category.  The+-- 'Category' and 'Traced' instances of the target discharge the knot; for+-- @(->)@ this is lazy knot-tying, and for 'Either' it is iteration.+--+-- == Core Concepts+--+-- * __Tensor__ (@t@): The bifunctor that pairs a feedback value with a payload.+--   The two tensors provided are @(,)@ (simultaneous / lazy sharing) and+--   'Either' (sequential / iteration).+--+-- * __Feedback value__: The component that travels around the loop (the first+--   parameter of the tensor inside a 'Knot' body).+--+-- * __Payload__: The component that is transformed and emitted (the second+--   parameter of the tensor inside a 'Knot' body).+--+-- * __Feedback channel__: The hidden type @s@ in a 'Knot'. It is the value+--   the abstraction hides.+module Circuit.Loop+  ( -- * Loop+    Loop (..),++    -- * Layer witness+    FreeLoop,+  )+where++import Circuit.Category (Category (..), Discrete (..), (.>))+import Circuit.Channel (Channel (..), Strength (..), Traced (..))+import Circuit.Layer (Layer (..), run, (:~>))+import Control.Arrow (Kleisli (..))+import Data.Bifunctor (Bifunctor (..))+import Data.Kind (Type)+import Data.Profunctor+import Prelude hiding (id, (.))++-- $setup+-- >>> import Circuit.Layer (run)++-- | The free traced monoidal category over base morphism @arr@ and tensor @t@,+-- in existential normal form.+--+-- Two constructors:+--+--   * 'Lift' — a plain base arrow.+--   * 'Knot' — a feedback loop with hidden channel @s@.+data Loop (t :: Type -> Type -> Type) arr a b where+  -- | A plain base arrow.+  Lift :: arr a b -> Loop t arr a b+  -- | Tie a feedback loop. The tensor @t@ carries the hidden channel type @s@.+  --+  -- The argument is the base arrow itself, /not/ a 'Lift'-wrapped stage.+  -- The constructor carries the 'Ob' evidence for the feedback channel in+  -- the /source/ category.  Folding into a different target still needs+  -- 'Discrete' to manufacture the corresponding 'Ob' evidence there.+  Knot :: (Ob arr s) => arr (t s a) (t s b) -> Loop t arr a b++-- $examples+--+-- >>> run (Lift (+1) :: Loop (,) (->) Int Int) 5+-- 6+--+-- >>> run (Knot (\(acc, x) -> (x, acc)) :: Loop (,) (->) Int Int) 42+-- 42+--+-- For the @(,)@ tensor the channel value is self-referential, so the body+-- must use an irrefutable pattern or otherwise avoid forcing the channel+-- before producing its constructor:+--+-- >>> run (Knot (\ ~(ns, ()) -> (0 : ns, take 3 ns)) :: Loop (,) (->) () [Int]) ()+-- [0,0,0]++instance (Strength t arr, Discrete arr) => Category (Loop t arr) where+  type Ob (Loop t arr) a = Ob arr a+  id :: forall a. (Ob arr a) => Loop t arr a a+  id = Lift id+  (.) :: forall a b c. (Ob arr a, Ob arr b, Ob arr c) => Loop t arr b c -> Loop t arr a b -> Loop t arr a c+  Lift f . Lift g = Lift (f . g)+  Knot @_ @s @_ @_ @_ f . Lift g =+    withOb @arr @(t s a) $+      withOb @arr @(t s b) $+        withOb @arr @(t s c) $+          Knot (f . strength g)+  Lift f . Knot @_ @s @_ @_ @_ g =+    withOb @arr @(t s a) $+      withOb @arr @(t s b) $+        withOb @arr @(t s c) $+          Knot (strength f . g)+  Knot @_ @s2 @_ @_ @_ f . Knot @_ @s1 @_ @_ @_ g =+    withOb @arr @(t s2 s1) $+      withOb @arr @(t (t s2 s1) a) $+        withOb @arr @(t s2 (t s1 a)) $+          withOb @arr @(t s2 (t s1 b)) $+            withOb @arr @(t s2 (t s1 c)) $+              withOb @arr @(t s1 a) $+                withOb @arr @(t s1 b) $+                  withOb @arr @(t s1 (t s2 b)) $+                    withOb @arr @(t s2 b) $+                      withOb @arr @(t s2 c) $+                        withOb @arr @(t s1 (t s2 c)) $+                          withOb @arr @(t (t s2 s1) c) $+                            Knot (assoc .> strength g .> slide .> strength f .> slide .> assoc')++-- | A discrete base yields a discrete free traced category.+instance (Strength t arr, Discrete arr) => Discrete (Loop t arr) where+  withOb @a x = withOb @arr @a x++instance (Profunctor arr, Bifunctor t) => Profunctor (Loop t arr) where+  dimap f g (Lift h) = Lift (dimap f g h)+  dimap f g (Knot h) = Knot (dimap (second f) (second g) h)+  lmap f (Lift h) = Lift (lmap f h)+  lmap f (Knot h) = Knot (lmap (second f) h)+  rmap g (Lift h) = Lift (rmap g h)+  rmap g (Knot h) = Knot (rmap (second g) h)++instance (Bifunctor t) => Functor (Loop t (->) a) where+  fmap f (Lift g) = Lift (f . g)+  fmap f (Knot g) = Knot (second f . g)++-- | Lift the 'Channel' structure of the base arrow into 'Loop t arr'.+--+-- The 'withOb' ladder is written out inline rather than using+-- 'Circuit.Discrete.assocD' / @Circuit.Discrete.braidD@ because importing that kit here would+-- create a cycle: 'Circuit.Discrete' needs 'Traced' (and hence this module).+instance (Strength t arr, Discrete arr) => Channel t (Loop t arr) where+  assoc :: forall a b c. Loop t arr (t (t a b) c) (t a (t b c))+  assoc =+    Lift $+      withOb @arr @a $+        withOb @arr @b $+          withOb @arr @c $+            withOb @arr @(t a b) $+              withOb @arr @(t b c) $+                withOb @arr @(t (t a b) c) $+                  withOb @arr @(t a (t b c)) $+                    assoc+  assoc' :: forall a b c. Loop t arr (t a (t b c)) (t (t a b) c)+  assoc' =+    Lift $+      withOb @arr @a $+        withOb @arr @b $+          withOb @arr @c $+            withOb @arr @(t a b) $+              withOb @arr @(t b c) $+                withOb @arr @(t a (t b c)) $+                  withOb @arr @(t (t a b) c) $+                    assoc'+  slide :: forall a b c. Loop t arr (t a (t b c)) (t b (t a c))+  slide =+    Lift $+      withOb @arr @a $+        withOb @arr @b $+          withOb @arr @c $+            withOb @arr @(t b c) $+              withOb @arr @(t a c) $+                withOb @arr @(t a (t b c)) $+                  withOb @arr @(t b (t a c)) $+                    slide++-- | Lift the 'Strength' class through 'Loop t'.+instance (Strength t arr, Discrete arr) => Strength t (Loop t arr) where+  strength :: forall a b c. (Ob arr a, Ob arr b, Ob arr c, Ob arr (t a b), Ob arr (t a c)) => Loop t arr b c -> Loop t arr (t a b) (t a c)+  strength (Lift f) =+    Lift $+      withOb @arr @a $+        withOb @arr @b $+          withOb @arr @c $+            withOb @arr @(t a b) $+              withOb @arr @(t a c) $+                strength f+  strength (Knot @_ @s @_ @_ @_ f) =+    withOb @arr @(t s (t a b)) $+      withOb @arr @(t a (t s b)) $+        withOb @arr @(t a (t s c)) $+          withOb @arr @(t s b) $+            withOb @arr @(t s c) $+              withOb @arr @(t s (t a c)) $+                Knot (slide .> strength f .> slide)++-- | Lift the 'Traced' class through 'Loop t'.+--+-- 'trace' hides a wire as a 'Knot'.+instance (Traced t arr, Discrete arr) => Traced t (Loop t arr) where+  trace ::+    forall a b c.+    (Ob arr a) =>+    Loop t arr (t a b) (t a c) ->+    Loop t arr b c+  trace (Lift f) = Knot f+  trace (Knot @_ @s @_ @_ @_ f) =+    withOb @arr @(t (t s a) b) $+      withOb @arr @(t s (t a b)) $+        withOb @arr @(t s (t a c)) $+          withOb @arr @(t (t s a) c) $+            withOb @arr @(t s a) $+              Knot (assoc .> f .> assoc')++-- | 'Traced' plus 'Discrete' — required to fold free 'Loop'+-- (existential feedback channels need trivial 'Ob' on every type).+class (Traced t arr, Discrete arr) => FreeLoop t arr++instance (Traced t arr, Discrete arr) => FreeLoop t arr++-- | Free traced monoidal category.+instance Layer (Loop t) where+  type Law (Loop t) arr' = FreeLoop t arr'+  type Run (Loop t) arr = (Traced t arr, Discrete arr)+  type Bind (Loop t) arr = ()+  unit = Lift+  run :: forall arr a b. (Run (Loop t) arr, Ob arr a, Ob arr b) => Loop t arr a b -> arr a b+  run (Lift f) = f+  run (Knot @_ @s @_ @_ @_ f) =+    withOb @arr @(t s a) $+      withOb @arr @(t s b) $+        trace f+  bind :: forall arr arr' a b. (Law (Loop t) arr', Ob arr' a, Ob arr' b) => (arr :~> arr') -> Loop t arr a b -> arr' a b+  bind h (Lift f) = h f+  bind h (Knot @_ @s @_ @_ @_ f) =+    withOb @arr' @s $+      withOb @arr' @(t s a) $+        withOb @arr' @(t s b) $+          trace (h f)

@@ -1,199 +0,0 @@-{-# LANGUAGE CPP #-}---- | Monoidal structure for the tensors used in traced categories.------ This module collects the braided, cartesian, and cocartesian structure--- over the standard tensors @(,)@ and 'Either', along with the general--- 'ambientBy' combinator for threading additional state wires.------ The goal is to keep the core 'Circuit' GADT and 'reify' mechanism--- independent of these structural details.-module Circuit.Monoidal-  ( Braided (..),-    ambient,-    assoc,-    assoc',-    seed,-    absorb,-    release,-    coassoc,-    coassoc',-    coseed,-    coabsorbL,-    coabsorbR,-    coreleaseL,-    coreleaseR,-    ambientBy,-  )-where--#ifdef __GLASGOW_HASKELL__-import Data.Profunctor (Profunctor, dimap)-import Data.Bifunctor (Bifunctor (..))-#else-import Circuit.Classes (Profunctor, Bifunctor (..))-#endif--import Circuit.Circuit (Circuit (..))-import Circuit.Traced (Trace (..))---- ===========================================================================--- BRAIDING--- ===========================================================================---- | A symmetric braiding for a bifunctor tensor.------ The braid swaps a wire past a nested pair:------ @---   t x (t y z)  ->  t y (t x z)--- @------ For @(,)@ this is the cartesian slide.  For @Either@ it is the--- coproduct slide.  Both are derived from the associator and swap.-class (Bifunctor t) => Braided t where-  braid :: t x (t y z) -> t y (t x z)---- | Cartesian slide: @(x, (y, z)) -> (y, (x, z))@.-instance Braided (,) where-  braid (x, (y, z)) = (y, (x, z))---- | Coproduct slide.------ >>> braid (Left "hi" :: Either String (Either Int Bool))--- Right (Left "hi")-instance Braided Either where-  braid (Left x) = Right (Left x)-  braid (Right (Left y)) = Left y-  braid (Right (Right z)) = Right (Right z)---- | Thread a state wire through a circuit using the canonical braid.------ This is 'ambientBy' with the braid supplied by the 'Braided' instance.-ambient ::-  (Profunctor arr, Trace arr t, Braided t) =>-  Circuit arr t a b -> Circuit arr t (t s a) (t s b)-ambient = ambientBy braid---- ===========================================================================--- CARTESIAN STRUCTURE ((,))--- ===========================================================================---- | Associator: @(a, (b, c)) -> ((a, b), c)@.-assoc :: (a, (b, c)) -> ((a, b), c)-assoc (a, (b, c)) = ((a, b), c)---- | Inverse associator: @((a, b), c) -> (a, (b, c))@.-assoc' :: ((a, b), c) -> (a, (b, c))-assoc' ((a, b), c) = (a, (b, c))---- | Introduce a state wire alongside a payload.------ Given an initial state and a payload value, produce a paired value--- suitable for feeding into a circuit threaded with 'ambientBy'.-seed :: s -> a -> (s, a)-seed s a = (s, a)---- | Move a value from the payload into the state wire.------ @absorb f = first (uncurry f) . assoc@-absorb :: (t -> s -> s') -> (s, (t, b)) -> (s', b)-absorb f (s, (t, b)) = (f t s, b)---- | Move a value from the state wire into the payload.------ @release f = assoc' . first f@-release :: (s -> (s', t)) -> (s, b) -> (s', (t, b))-release f (s, b) = let (s', t) = f s in (s', (t, b))---- ===========================================================================--- COCARTESIAN STRUCTURE (Either)--- ===========================================================================---- | Coassociator for sums.------ >>> coassoc (Left 1 :: Either Int (Either Bool Char))--- Left (Left 1)-coassoc :: Either a (Either b c) -> Either (Either a b) c-coassoc (Left a) = Left (Left a)-coassoc (Right (Left b)) = Left (Right b)-coassoc (Right (Right c)) = Right c---- | Inverse coassociator.------ >>> coassoc' (Left (Left 1) :: Either (Either Int Bool) Char)--- Left 1-coassoc' :: Either (Either a b) c -> Either a (Either b c)-coassoc' (Left (Left a)) = Left a-coassoc' (Left (Right b)) = Right (Left b)-coassoc' (Right c) = Right (Right c)---- | Tag a state value onto whichever branch of the sum is active.------ >>> coseed "st" (Left 42 :: Either Int Char)--- Left ("st",42)-coseed :: s -> Either a b -> Either (s, a) (s, b)-coseed s = bimap (s,) (s,)---- | If the left branch is taken, move a value from the payload into the state wire.------ >>> coabsorbL (+) (Left (10, (3, 'x')) :: Either (Int, (Int, Char)) Bool)--- Left (13,'x')-coabsorbL :: (t -> s -> s') -> Either (s, (t, a)) b -> Either (s', a) b-coabsorbL f (Left (s, (t, a))) = Left (f t s, a)-coabsorbL _ (Right b) = Right b---- | If the right branch is taken, move a value from the payload into the state wire.------ >>> coabsorbR (+) (Right (10, (3, 'x')) :: Either Bool (Int, (Int, Char)))--- Right (13,'x')-coabsorbR :: (t -> s -> s') -> Either a (s, (t, b)) -> Either a (s', b)-coabsorbR f (Right (s, (t, b))) = Right (f t s, b)-coabsorbR _ (Left a) = Left a---- | If the left branch is taken, move a value from the state wire into the payload.------ >>> coreleaseL (\s -> (s+1, s*2)) (Left (5, 99) :: Either (Int, Int) Char)--- Left (6,(10,99))-coreleaseL :: (s -> (s', t)) -> Either (s, a) b -> Either (s', (t, a)) b-coreleaseL f (Left (s, a)) = let (s', t) = f s in Left (s', (t, a))-coreleaseL _ (Right b) = Right b---- | If the right branch is taken, move a value from the state wire into the payload.------ >>> coreleaseR (\s -> (s+1, s*2)) (Right (5, 99) :: Either Char (Int, Int))--- Right (6,(10,99))-coreleaseR :: (s -> (s', t)) -> Either a (s, b) -> Either a (s', (t, b))-coreleaseR f (Right (s, b)) = let (s', t) = f s in Right (s', (t, b))-coreleaseR _ (Left a) = Left a---- ===========================================================================--- GENERAL AMBIENT STATE THREADING--- ===========================================================================---- | Thread a state wire through a Circuit.------ 'ambientBy' threads an additional state component alongside a circuit--- without the circuit having to mention it. The state wire is braided--- past the feedback channel so it travels "ambiently".------ The @braid@ function swaps the state wire past the feedback channel:--- @t x (t s a) -> t s (t x a)@. For @(,)@, this is--- @\\(x, (s, a)) -> (s, (x, a))@.------ >>> import Circuit.Circuit (Circuit(..), reify)--- >>> let braid (x, (s, a)) = (s, (x, a))--- >>> Circuit.Circuit.reify (ambientBy braid (Lift (+1) :: Circuit (->) (,) Int Int)) ("st", 5)--- ("st",6)------ >>> let step (xs, ()) = (0 : xs, take 3 xs)--- >>> Circuit.Circuit.reify (ambientBy braid (Knot step)) ("st", ())--- ("st",[0,0,0])-ambientBy ::-  (Profunctor arr, Trace arr t) =>-  (forall x y z. t x (t y z) -> t y (t x z)) ->-  Circuit arr t a b ->-  Circuit arr t (t s a) (t s b)-ambientBy _br (Lift f) = Lift (untrace f)-ambientBy br (Compose f g) = Compose (ambientBy br f) (ambientBy br g)-ambientBy br (Knot k) = Knot (dimap br br (untrace k))

@@ -0,0 +1,341 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wno-orphans #-}++-- | The free traced PROP with a bimonoid over a primitive set.+--+-- 'Net' extends 'C.Loop' with structural rows for the monoidal and+-- bimonoid operations: parallel composition, copy, discard, addition,+-- and zero.  Where 'C.Loop' keeps only 'C.Lift' and 'C.Knot' in normal+-- form, 'Net' keeps the wiring inspectable — the difference between+-- wiring you can read backwards and wiring that has been melted into a+-- single loop.+--+-- @+-- Free = Lift + Compose+-- Sym  = Free + Par + Swap+-- Net  = Sym + Knot + Copy + Discard + Plus + Zero+-- @+--+-- 'run' @Net@ interprets a 'Net' to a plain arrow.  'melt' interprets the+-- structural rows into the normal form of 'C.Loop'.+module Circuit.Net+  ( -- * Net+    Net (..),++    -- * Transposition+    transpose,++    -- * Conversion+    enrich,+    widen,+    sift,++    -- * Interpretation+    melt,++    -- * Free Net constraint+    FreeNet,+  )+where++import Circuit.Category (Category (..), Discrete (..), (.>))+import Circuit.Channel (Traced (..))+import Circuit.Dagger qualified as Dg+import Circuit.Layer (Layer (..), (:~>))+import Circuit.Layer qualified as Layer+import Circuit.Loop qualified as C+import Circuit.Sym qualified as M+import Circuit.Tensor (Action (..), Tensor (..))+import Data.Kind (Type)+import Prelude hiding (id, (.))++-- $setup+-- >> import Circuit.Dagger qualified as Dg+-- >> import Circuit.Layer (bind, run, unit)+-- >> import Circuit.Sym qualified as M+-- >> import Circuit.Net+-- >> import Circuit.Loop (Loop (Knot))+-- >> import Circuit.Loop qualified as C+-- >> import Prelude hiding (id, (.))++-- | The free traced PROP with a bimonoid.+--+-- Four families of constructor:+--+--   * __Sequential__ — @Lift@, @Compose@.+--   * __Monoidal__ — 'Par', 'Swap' (parallel composition, braiding).+--   * __Bimonoid__ — 'Copy', 'Discard' (comonoid), 'Plus', 'Zero' (monoid).+--   * __Feedback__ — 'Knot', with a 'Net' body so 'transpose' can reach inside.+--+-- 'Dg.CopyDiscard' and 'Dg.MergeZero' (via 'Dg.Bimonoid') constraints ride as dictionary arguments on the+-- constructors that need them — laws in the typeclass holes, evidence on+-- the GADT rows.+--+-- The wiring monoidal structure ('Par' / 'Swap') is cartesian: it always+-- uses @(,)@. Only the feedback tensor carried by 'Knot' is polymorphic+-- in @t@. This is why 'Net' is a PROP over the cartesian wiring category+-- with feedback supplied by the traced tensor.+--+-- 'Net' extends 'C.Loop' inspectably. 'enrich' embeds a 'Loop' into+-- 'Net', and 'melt' collapses it back; 'melt' . 'enrich' = 'id'.+data Net (t :: Type -> Type -> Type) arr a b where+  -- | Embed a base arrow.+  Lift :: arr a b -> Net t arr a b+  -- | Sequential composition.+  --+  -- The 'Ob' constraint on the intermediate object @b@ is carried in the+  -- constructor so folding does not need a 'Discrete' base.+  Compose :: (Ob arr b) => Net t arr b c -> Net t arr a b -> Net t arr a c+  -- | Parallel composition (monoidal product).+  Par :: Net t arr a b -> Net t arr c d -> Net t arr (a, c) (b, d)+  -- | Symmetric braiding.+  Swap :: Net t arr (a, b) (b, a)+  -- | Copy: fan-out.  Requires both comonoid and monoid ('Dg.Bimonoid').+  Copy :: (Dg.Bimonoid arr a) => Net t arr a (a, a)+  -- | Discard: erase.  Requires 'Dg.Bimonoid'.+  Discard :: (Dg.Bimonoid arr a) => Net t arr a ()+  -- | Plus: fan-in.  Requires 'Dg.Bimonoid'.+  Plus :: (Dg.Bimonoid arr a) => Net t arr (a, a) a+  -- | Zero: the neutral element.  Requires 'Dg.Bimonoid'.+  Zero :: (Dg.Bimonoid arr a) => Net t arr () a+  -- | Feedback loop.  The body is a 'Net', not an opaque base arrow —+  -- so 'transpose' can reach inside and swap 'Copy' ↔ 'Plus' within+  -- the loop.+  --+  -- The constructor carries the 'Ob' evidence for the feedback channel in+  -- the /source/ category.+  Knot :: (Ob arr s) => Net t arr (t s a) (t s b) -> Net t arr a b++-- | The 'Category' instance preserves inspectable wiring.+--+-- Composition uses the explicit @Compose@ constructor, so 'Copy',+-- 'Plus', 'Par', and 'Knot' stay visible.  'melt' collapses the+-- structure when the normal form is needed.+--+-- Composition uses the explicit @Compose@ constructor so structural+-- rows remain inspectable.  'melt' collapses them to the normal form of+-- 'C.Loop' when needed.+instance (Category arr) => Category (Net t arr) where+  type Ob (Net t arr) a = Ob arr a+  id = Lift id+  g . f = Compose g f++-- | A discrete base yields a discrete free traced PROP.+instance (Category arr, Discrete arr) => Discrete (Net t arr) where+  withOb @a x = withOb @arr @a x++-- | Transpose a 'Net' — the backward circuit as inspectable syntax.+--+-- The structural rows are self-dual under transposition:+-- @Compose@ reverses, 'Par' transposes componentwise, 'Copy' ↔ 'Plus',+-- 'Discard' ↔ 'Zero', 'Knot' ↔ 'Knot' (recurring into the body).+--+-- @Lift@ transposes via 'Dg.Dagger' field swap — only nets over+-- 'Dg.Dagger' are transposable, since the forward\/backward pairing is+-- structural in the base arrow.+--+-- Law: @transpose . transpose = id@.+--+-- .> import Circuit.Dagger qualified as Dg+-- .> let n1 = Lift (Dg.Dagger (+1) (subtract 1)) :: Net (,) (Dg.Dagger (->)) Int Int+-- .> let n2 = Lift (Dg.Dagger (+1) (subtract 1)) `Compose` Lift (Dg.Dagger (+1) (subtract 1)) :: Net (,) (Dg.Dagger (->)) Int Int+-- .> Dg.front (run (transpose (transpose n1))) 5+-- 6+-- .> Dg.front (run (transpose (transpose n2))) 5+-- 7+--+-- Asymmetric factors catch the direction of @Compose@ reversal:+-- forward is @(*2) . (+1)@, backward is @(subtract 1) . (`div` 2)@.+--+-- .> let n3 = Lift (Dg.Dagger (+1) (subtract 1)) `Compose` Lift (Dg.Dagger (*2) (\x -> x `div` 2)) :: Net (,) (Dg.Dagger (->)) Int Int+-- .> Dg.front (run (transpose n3)) 10+-- 4+transpose ::+  Net t (Dg.Dagger arr) a b ->+  Net t (Dg.Dagger arr) b a+transpose = \case+  Lift (Dg.Dagger f g) -> Lift (Dg.Dagger g f)+  Compose g f -> Compose (transpose f) (transpose g)+  Par f g -> Par (transpose f) (transpose g)+  Swap -> Swap+  Copy -> Plus+  Plus -> Copy+  Discard -> Zero+  Zero -> Discard+  Knot f -> Knot (transpose f)++-- | Upgrade a 'C.Loop' to a 'Net' — constructor-to-constructor.+--+-- 'C.Loop' is the normal form 'C.Lift' / 'C.Knot' over a base-arrow body;+-- 'Net' keeps the same information but can hold more structure.+-- 'C.Lift' lifts to 'Net.Lift'; 'C.Knot' lifts to 'Net.Knot' around a+-- @Lift@ body.+enrich :: C.Loop t arr a b -> Net t arr a b+enrich (C.Lift f) = Lift f+enrich (C.Knot f) = Knot (Lift f)++-- | Include a 'M.Sym' circuit into 'Net' — constructor-to-constructor.+--+-- 'Net' duplicates the four rows of 'M.Sym' (@Lift@, @Compose@, 'Par',+-- 'Swap') so that structural wiring stays inspectable.  This is the+-- injection of the 'Sym' layer into the 'Net' layer.+--+-- .> let m = M.Lift (+1) `M.Compose` M.Lift (*2) :: M.Sym (->) Int Int+-- .> run (widen m :: Net (,) (->) Int Int) 5+-- 11+--+-- Coherence: 'sift' projects 'widen' back to the original 'Sym'.+--+-- .> run (sift (widen m :: Net (,) (->) Int Int)) 5+-- 11+-- .> run m 5+-- 11+--+-- Coherence: 'melt' agrees with the function fold on 'Sym' circuits.+--+-- .> run (melt (widen m :: Net (,) (->) Int Int)) 5+-- 11+-- .> let h f = f+-- .> (bind h m :: Int -> Int) 5+-- 11+--+-- Coherence: 'Net' folds through 'widen' match 'Sym' folds.+--+-- .> let h f = f+-- .> (bind h (widen m :: Net (,) (->) Int Int) :: Int -> Int) 5+-- 11+-- .> (bind h m :: Int -> Int) 5+-- 11+--+-- Coherence: transposition commutes with 'widen'.+--+-- .> let dm = M.Lift (Dg.Dagger (+1) (subtract 1)) `M.Compose` M.Lift (Dg.Dagger (*2) (\x -> x `div` 2)) :: M.Sym (Dg.Dagger (->)) Int Int+-- .> Dg.front (run (transpose (widen dm :: Net (,) (Dg.Dagger (->)) Int Int))) 10+-- 4+widen :: M.Sym arr a b -> Net t arr a b+widen (M.Lift f) = Lift f+widen (M.Compose g f) = Compose (widen g) (widen f)+widen (M.Par f g) = Par (widen f) (widen g)+widen M.Swap = Swap++-- | Forget the feedback and bimonoid rows of a 'Net', keeping only the+-- 'M.Sym' wiring.+--+-- 'sift' collapses 'Knot' and the bimonoid rows into 'M.Lift' while+-- leaving @Compose@, 'Par', and 'Swap' inspectable. Together with 'widen'+-- it gives the adjunction between 'M.Sym' and 'Net'.+-- Note the converse does not hold: @widen . sift ≠ id@ because 'sift'+-- forgets knots and bimonoid structure.+sift ::+  forall t arr a b.+  (Traced t arr, Action (,) arr, Discrete arr) =>+  Net t arr a b ->+  M.Sym arr a b+sift (Lift f) = M.Lift f+sift (Compose g f) = M.Compose (sift g) (sift f)+sift (Par f g) = M.Par (sift f) (sift g)+sift Swap = M.Swap+sift Copy = M.Lift Dg.copy+sift Discard = M.Lift Dg.discard+sift Plus = M.Lift Dg.plus+sift Zero = M.Lift Dg.zero+sift n@(Knot @_ @s @_ @_ @_ _) =+  withOb @arr @a $+    withOb @arr @b $+      withOb @arr @(t s a) $+        withOb @arr @(t s b) $+          M.Lift (Layer.run (melt n))++-- | Melt the structural rows of a 'Net' into the normal form of 'C.Loop'.+--+-- The interpretation from the free traced PROP with bimonoid to the free+-- traced monoidal category.  Structural rows ('Par', 'Copy', 'Plus',+-- etc.) become opaque base-arrow operations wrapped in 'C.Lift'; @Compose@+-- and 'C.Knot' use the 'Category' and 'Traced' instances of 'C.Loop'.+--+-- @'run' @Net = 'run' . 'melt'@.+--+-- .> run (melt (Lift (+1) :: Net (,) (->) Int Int)) 5+-- 6+melt ::+  forall t arr a b.+  (Traced t arr, Action (,) arr, Discrete arr) =>+  Net t arr a b ->+  C.Loop t arr a b+melt (Lift f) = C.Lift f+melt (Compose @_ @b1 @_ @_ @_ g f) =+  withOb @arr @a $+    withOb @arr @b1 $+      withOb @arr @b $+        (melt g . melt f)+melt (Par f g) = par (melt f) (melt g)+melt Swap = C.Lift swap+melt Copy = C.Lift Dg.copy+melt Discard = C.Lift Dg.discard+melt Plus = C.Lift Dg.plus+melt Zero = C.Lift Dg.zero+melt (Knot @_ @s @_ @_ @_ f) =+  withOb @arr @a $+    withOb @arr @b $+      withOb @arr @(t s a) $+        withOb @arr @(t s b) $+          trace (melt f)++-- | 'Traced' + 'Action' + 'Discrete' — free 'Net' fold needs trivial 'Ob'.+class (Traced t arr, Action (,) arr, Discrete arr) => FreeNet t arr++instance (Traced t arr, Action (,) arr, Discrete arr) => FreeNet t arr++-- | Free traced PROP with a bimonoid.+--+-- Structural rows are interpreted in the target category: parallel+-- composition uses 'par', braiding uses 'swap', and the bimonoid+-- generators are the images under @h@ of the source dictionaries carried+-- by the 'Copy', 'Discard', 'Plus', and 'Zero' constructors.+--+-- [Conditional] 'bind' @h@ interprets bimonoid generators as images under+-- @h@ of the source arrow's dictionaries.  This is the free-PROP fold+-- only when @h@ is a bimonoid homomorphism (automatic for the generator+-- embedding, but must be verified for custom @h@).+instance Layer (Net t) where+  type Law (Net t) arr' = FreeNet t arr'+  type Run (Net t) arr = (Traced t arr, Action (,) arr, Discrete arr)+  type Bind (Net t) arr = Discrete arr+  unit = Lift+  run = Layer.run . melt+  bind :: forall arr' arr a b. (Law (Net t) arr', Bind (Net t) arr, Ob arr a, Ob arr b, Ob arr' a, Ob arr' b) => (arr :~> arr') -> Net t arr a b -> arr' a b+  bind h (Lift f) = h f+  bind h (Compose @_ @b1 @_ @_ @_ g f) =+    withOb @arr @b1 $+      withOb @arr' @b1 $+        (bind h g . bind h f)+  bind h (Par @_ @_ @a1 @b1 @c @d f g) =+    withOb @arr @a1 $+      withOb @arr @b1 $+        withOb @arr @c $+          withOb @arr @d $+            withOb @arr' @a1 $+              withOb @arr' @b1 $+                withOb @arr' @c $+                  withOb @arr' @d $+                    par (bind h f) (bind h g)+  bind _ Swap = swap+  bind h Copy = h Dg.copy+  bind h Discard = h Dg.discard+  bind h Plus = h Dg.plus+  bind h Zero = h Dg.zero+  bind h (Knot @_ @s @_ @_ @_ f) =+    withOb @arr @s $+      withOb @arr @(t s a) $+        withOb @arr @(t s b) $+          withOb @arr' @s $+            withOb @arr' @(t s a) $+              withOb @arr' @(t s b) $+                trace (bind h f)

@@ -0,0 +1,140 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++-- | The free symmetric monoidal category over a base arrow.+--+-- 'Sym' extends the free category (@Circuit.Free.Free@) with explicit+-- monoidal product ('Par') and symmetry ('Swap') syntax.  It is the+-- intermediate layer between @Circuit.Free.Free@ and @Circuit.Net.Net@:+--+-- @+-- Free = Lift + Compose+-- Sym  = Free + Par + Swap+-- Net  = Sym + Knot + Copy + Discard + Plus + Zero+-- @+--+-- The tensor is fixed to @(,)@, matching 'Circuit.Tensor.Action'.+module Circuit.Sym+  ( Sym (..),++    -- * Free monoidal constraint+    FreeSym,+  )+where++import Circuit.Category (Category (..), Discrete (..), (.>))+import Circuit.Channel (Channel (..), Strength (..), Traced (..))+import Circuit.Layer (Layer (..), run, (:~>))+import Circuit.Tensor (Action (..), Tensor (..))+import Prelude hiding (id, (.))++-- $setup+-- >> import Circuit.Layer (run)+-- >> import Circuit.Tensor (Action (..), Tensor (..))+-- >> import Prelude hiding (id, (.))++-- | The free symmetric monoidal category over a base arrow @arr@.+--+-- Four constructors:+--+--   * 'Lift' — embed a base arrow.+--   * 'Compose' — sequential composition.+--   * 'Par' — tensor product of morphisms (parallel composition).+--   * 'Swap' — symmetry / braiding.+data Sym arr a b where+  -- | Embed a base arrow.+  Lift :: arr a b -> Sym arr a b+  -- | Sequential composition.+  --+  -- The 'Ob' constraint on the intermediate object @b@ is carried in the+  -- constructor so folding does not need a 'Discrete' base.+  Compose :: (Ob arr b) => Sym arr b c -> Sym arr a b -> Sym arr a c+  -- | Tensor product of morphisms (parallel composition on disjoint wires).+  Par :: Sym arr a b -> Sym arr c d -> Sym arr (a, c) (b, d)+  -- | Symmetric braiding.+  Swap :: Sym arr (a, b) (b, a)++-- | 'Sym' is a category.+instance (Category arr) => Category (Sym arr) where+  type Ob (Sym arr) a = Ob arr a+  id = Lift id+  (.) = Compose++-- | A discrete base yields a discrete free monoidal category.+instance (Category arr, Discrete arr) => Discrete (Sym arr) where+  withOb @a x = withOb @arr @a x++-- | 'Sym' has a tensor structure whose tensor is @(,)@.+--+-- This is the syntactic instance: 'Par' is its own interpretation.+-- The unitors require the base arrow to have its own cartesian unitors.+instance (Tensor (,) arr) => Tensor (,) (Sym arr) where+  par = Par+  unitl = Lift unitl+  unitl' = Lift unitl'+  unitr = Lift unitr+  unitr' = Lift unitr'++-- | 'Sym' has a symmetric braiding.+--+-- This is the syntactic instance: 'Swap' is its own interpretation.+instance (Tensor (,) arr) => Action (,) (Sym arr) where+  swap = Swap++-- | Lift the 'Channel' structure through 'Sym'.+instance (Category arr, Channel t arr) => Channel t (Sym arr) where+  assoc = Lift assoc+  assoc' = Lift assoc'+  slide = Lift slide++-- | 'Action' plus 'Discrete' so free 'Sym' can fold intermediate objects.+--+-- Sequential structure is folded with the target's category composition.+class (Action (,) arr, Discrete arr) => FreeSym arr++instance (Action (,) arr, Discrete arr) => FreeSym arr++instance Layer Sym where+  type Law Sym arr' = FreeSym arr'+  type Run Sym arr = (Action (,) arr, Discrete arr)+  type Bind Sym arr = Discrete arr+  unit = Lift+  run :: forall arr a b. (Run Sym arr, Ob arr a, Ob arr b) => Sym arr a b -> arr a b+  run (Lift f) = f+  run (Compose g f) = run g . run f+  run (Par (f :: Sym arr a1 b1) (g :: Sym arr c d)) =+    withOb @arr @a1 $+      withOb @arr @b1 $+        withOb @arr @c $+          withOb @arr @d $+            par (run f) (run g)+  run Swap = swap+  bind :: forall arr' arr a b. (Law Sym arr', Bind Sym arr, Ob arr a, Ob arr b, Ob arr' a, Ob arr' b) => (arr :~> arr') -> Sym arr a b -> arr' a b+  bind h (Lift f) = h f+  bind h (Compose @_ @b1 g f) = withOb @arr' @b1 (bind h g . bind h f)+  bind h (Par (f :: Sym arr a1 b1) (g :: Sym arr c d)) =+    withOb @arr @a1 $+      withOb @arr @b1 $+        withOb @arr @c $+          withOb @arr @d $+            withOb @arr' @a1 $+              withOb @arr' @b1 $+                withOb @arr' @c $+                  withOb @arr' @d $+                    par (bind h f) (bind h g)+  bind _ Swap = swap++-- | Lift the 'Strength' structure through 'Sym'.+instance (Strength t arr, Action (,) arr, Discrete arr) => Strength t (Sym arr) where+  strength = Lift . strength . run++-- | Lift the 'Traced' structure through 'Sym'.+--+-- Loop bodies are 'run' into the base arrow before tracing, just as for+-- @Free@.+instance (Traced t arr, Action (,) arr, Discrete arr) => Traced t (Sym arr) where+  trace = Lift . trace . run

@@ -0,0 +1,461 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wno-orphans #-}+{-# OPTIONS_GHC -Wno-unused-top-binds #-}++-- | Channel structure for the tensors used in traced categories.+--+-- This module collects the braided, cartesian, and cocartesian structure+-- over the standard tensors @(,)@ and 'Either', along with the general+-- 'ambientBy' combinator for threading additional state wires.+--+-- The goal is to keep the core 'Loop' GADT and 'run' mechanism+-- independent of these structural details.+--+-- Note: the monomorphic 'assocL' and 'assocR' helpers below reassociate+-- /leftward/ and /rightward/ respectively — the opposite direction to+-- 'Circuit.Channel.assoc' and 'Circuit.Channel.assoc''. The 'slide'+-- from 'Braided' is the slide @t a (t b c) -> t b (t a c)@; 'swap' here+-- is the symmetric braiding @t a b -> t b a@. They cohere as+-- @slide = assocR '.>' par swap id '.>' assocL@ wherever the 'Tensor'+-- and 'Action' structure is available.+--+-- 'Tensor' / 'Action' are kind-polymorphic.+module Circuit.Tensor+  ( Braided (..),+    ambient,+    ambientBy,+    superpose,++    -- * Channel product on base arrows+    Unit,+    Tensor (..),+    Action (..),++    -- * Cartesian / cocartesian associators+    assocL,+    assocR,+    coassoc,+    coassoc',+  )+where++import Circuit.Category (Category (..), Discrete (..), (.>))+import Circuit.Channel (Strength (..), Traced (..), strengthD)+import Circuit.Discrete (assocD, assocD', braidD)+import Circuit.Layer (run)+import Circuit.Loop (Loop (..))+import Control.Arrow (Kleisli (..))+import Control.Monad (Monad)+import Data.Bifunctor (Bifunctor (..))+import Data.Kind (Type)+import Data.Profunctor (Profunctor, dimap)+import Data.Void (Void, absurd)+import Prelude hiding (id, (.))++-- $setup+-- >> :set -XLambdaCase+-- >> import Circuit.Layer (run)+-- >> import Circuit.Loop (Loop (..))+-- >> import Control.Arrow (Kleisli (..), runKleisli)+-- >> import Data.Functor.Identity (Identity)+-- >> import Prelude hiding (id, (.))++-- ===========================================================================+-- BRAIDING+-- ===========================================================================++-- | A braiding for a bifunctor tensor.+--+-- The slide swaps a wire past a nested pair:+--+-- @+--   t x (t y z)  ->  t y (t x z)+-- @+--+-- For @(,)@ this is the cartesian slide.  For @Either@ it is the+-- coproduct slide.  Both are derived from the associator and swap.+class (Bifunctor t) => Braided t where+  slide :: t x (t y z) -> t y (t x z)++-- | Cartesian slide: @(x, (y, z)) -> (y, (x, z))@.+instance Braided (,) where+  slide ~(x, ~(y, z)) = (y, (x, z))++-- | Coproduct slide.+--+-- .> slide (Left "hi" :: Either String (Either Int Bool))+-- Right (Left "hi")+instance Braided Either where+  slide (Left x) = Right (Left x)+  slide (Right (Left y)) = Left y+  slide (Right (Right z)) = Right (Right z)++-- | Thread a state wire through a circuit using the canonical slide.+--+-- This is 'ambientBy' with the slide supplied by the 'Braided' instance.+ambient ::+  (Braided t, Strength t (->)) =>+  Loop t (->) a b ->+  Loop t (->) (t s a) (t s b)+ambient = ambientBy slide++-- ===========================================================================+-- CARTESIAN STRUCTURE ((,))+-- ===========================================================================++-- | Leftward associator: @(a, (b, c)) -> ((a, b), c)@.+assocL :: (a, (b, c)) -> ((a, b), c)+assocL ~(a, ~(b, c)) = ((a, b), c)++-- | Rightward associator: @((a, b), c) -> (a, (b, c))@.+assocR :: ((a, b), c) -> (a, (b, c))+assocR ~(~(a, b), c) = (a, (b, c))++-- | Introduce a state wire alongside a payload.+--+-- Given an initial state and a payload value, produce a paired value+-- suitable for feeding into a circuit threaded with 'ambientBy'.+seed :: s -> a -> (s, a)+seed s a = (s, a)++-- | Move a value from the payload into the state wire.+--+-- @absorb f = first (uncurry f) . assocL@+absorb :: (t -> s -> s') -> (s, (t, b)) -> (s', b)+absorb f (s, (t, b)) = (f t s, b)++-- | Move a value from the state wire into the payload.+--+-- @release f = assocR . first f@+release :: (s -> (s', t)) -> (s, b) -> (s', (t, b))+release f (s, b) = let (s', t) = f s in (s', (t, b))++-- ===========================================================================+-- COCARTESIAN STRUCTURE (Either)+-- ===========================================================================++-- | Coassociator for sums.+--+-- .> coassoc (Left 1 :: Either Int (Either Bool Char))+-- Left (Left 1)+coassoc :: Either a (Either b c) -> Either (Either a b) c+coassoc (Left a) = Left (Left a)+coassoc (Right (Left b)) = Left (Right b)+coassoc (Right (Right c)) = Right c++-- | Inverse coassociator.+--+-- .> coassoc' (Left (Left 1) :: Either (Either Int Bool) Char)+-- Left 1+coassoc' :: Either (Either a b) c -> Either a (Either b c)+coassoc' (Left (Left a)) = Left a+coassoc' (Left (Right b)) = Right (Left b)+coassoc' (Right c) = Right (Right c)++-- | Tag a state value onto whichever branch of the sum is active.+--+-- .> coseed "st" (Left 42 :: Either Int Char)+-- Left ("st",42)+coseed :: s -> Either a b -> Either (s, a) (s, b)+coseed s = bimap (s,) (s,)++-- | If the left branch is taken, move a value from the payload into the state wire.+--+-- .> coabsorbL (+) (Left (10, (3, 7)) :: Either (Int, (Int, Int)) Bool)+-- Left (13,7)+coabsorbL :: (t -> s -> s') -> Either (s, (t, a)) b -> Either (s', a) b+coabsorbL f (Left (s, (t, a))) = Left (f t s, a)+coabsorbL _ (Right b) = Right b++-- | If the right branch is taken, move a value from the payload into the state wire.+--+-- .> coabsorbR (+) (Right (10, (3, 7)) :: Either Bool (Int, (Int, Int)))+-- Right (13,7)+coabsorbR :: (t -> s -> s') -> Either a (s, (t, b)) -> Either a (s', b)+coabsorbR f (Right (s, (t, b))) = Right (f t s, b)+coabsorbR _ (Left a) = Left a++-- | If the left branch is taken, move a value from the state wire into the payload.+--+-- .> coreleaseL (\s -> (s+1, s*2)) (Left (5, 99) :: Either (Int, Int) Char)+-- Left (6,(10,99))+coreleaseL :: (s -> (s', t)) -> Either (s, a) b -> Either (s', (t, a)) b+coreleaseL f (Left (s, a)) = let (s', t) = f s in Left (s', (t, a))+coreleaseL _ (Right b) = Right b++-- | If the right branch is taken, move a value from the state wire into the payload.+--+-- .> coreleaseR (\s -> (s+1, s*2)) (Right (5, 99) :: Either Char (Int, Int))+-- Right (6,(10,99))+coreleaseR :: (s -> (s', t)) -> Either a (s, b) -> Either a (s', (t, b))+coreleaseR f (Right (s, b)) = let (s', t) = f s in Right (s', (t, b))+coreleaseR _ (Left a) = Left a++-- ===========================================================================+-- GENERAL AMBIENT STATE THREADING+-- ===========================================================================++-- | Thread a state wire through a Circuit.+--+-- 'ambientBy' threads an additional state component alongside a circuit+-- without the circuit having to mention it. The state wire is slid+-- past the feedback channel so it travels "ambiently".+--+-- The @slide@ function swaps the state wire past the feedback channel:+-- @t x (t s a) -> t s (t x a)@. For @(,)@, this is+-- @\(x, (s, a)) -> (s, (x, a))@.+--+-- .> import Circuit.Layer (run)+-- .> import Circuit.Loop (Loop(..))+-- .> let slide (x, (s, a)) = (s, (x, a))+-- .> run (ambientBy slide (Lift (+1) :: Loop (,) (->) Int Int)) ("st", 5)+-- ("st",6)+--+-- .> let step (xs, ()) = (0 : xs, take 3 xs)+-- .> run (ambientBy slide (Knot step)) ("st", ())+-- ("st",[0,0,0])+ambientBy ::+  (Strength t (->)) =>+  (forall x y z. t x (t y z) -> t y (t x z)) ->+  Loop t (->) a b ->+  Loop t (->) (t s a) (t s b)+ambientBy _br (Lift f) = Lift (strength f)+ambientBy br (Knot k) = Knot (dimap br br (strength k))++-- ===========================================================================+-- Tensor / Action — tensor action on morphisms+-- ===========================================================================++-- | The unit object for a tensor @t@.+--+-- @t@ is an object-level bifunctor (@Either@, @(,)@, type-level @(+)@, …)+-- with kind @k -> k -> k@, not a morphism tensor.+type family Unit (t :: k -> k -> k) :: k++-- | The tensor action of @t@ on a category @arr@, without braiding.+--+-- 'par' is the tensor product of morphisms (parallel composition on+-- disjoint wires). 'unitl' and 'unitr' witness that the tensor has a unit+-- object. This is the planar fragment: 'Tensor' only provides the+-- associator and unitors, not a braiding.+--+-- Kind-polymorphic: @t@ and @arr@ share object kind (inferred via PolyKinds).+class (Category arr) => Tensor t arr where+  -- | Parallel composition: run two arrows on disjoint wires.+  --+  -- >>> par ((+1) :: Int -> Int) ((*2) :: Int -> Int) (3, 4)+  -- (4,8)+  par :: arr a b -> arr c d -> arr (t a c) (t b d)++  -- | Left unitor: @I ⊗ a -> a@.+  unitl :: arr (t (Unit t) a) a++  -- | Inverse left unitor: @a -> I ⊗ a@.+  unitl' :: arr a (t (Unit t) a)++  -- | Right unitor: @a ⊗ I -> a@.+  unitr :: arr (t a (Unit t)) a++  -- | Inverse right unitor: @a -> a ⊗ I@.+  unitr' :: arr a (t a (Unit t))++-- | The action of a tensor @t@ on a category @arr@, extended with a+-- symmetric braiding.+--+-- This is the self-action of a symmetric monoidal category: @t@ acts on+-- @arr@ by taking morphisms to morphisms over paired objects, and 'swap'+-- provides the symmetry.+class (Tensor t arr) => Action t arr where+  -- | Symmetric braiding.+  --+  -- >>> swap (3, 4) :: (Int, Int)+  -- (4,3)+  swap :: arr (t a b) (t b a)++type instance Unit (,) = ()++-- | Cartesian tensor action on functions.+--+-- Laws: 'unitl' = 'snd', 'unitl'' = @((),)@, 'unitr' = 'fst', 'unitr'' = @(,) ()@.+instance Tensor (,) (->) where+  par f g (a, c) = (f a, g c)+  {-# INLINE par #-}+  unitl ~((), a) = a+  {-# INLINE unitl #-}+  unitl' a = ((), a)+  {-# INLINE unitl' #-}+  unitr ~(a, ()) = a+  {-# INLINE unitr #-}+  unitr' a = (a, ())+  {-# INLINE unitr' #-}++-- | Cartesian symmetry on functions.+instance Action (,) (->) where+  swap (a, b) = (b, a)+  {-# INLINE swap #-}++-- | Cartesian tensor on @Kleisli@ (effectful sequential product).+instance (Monad m) => Tensor (,) (Kleisli m) where+  par (Kleisli f) (Kleisli g) =+    Kleisli $ \(a, c) -> do+      b <- f a+      d <- g c+      pure (b, d)+  {-# INLINE par #-}+  unitl = Kleisli $ \((), a) -> pure a+  {-# INLINE unitl #-}+  unitl' = Kleisli $ \a -> pure ((), a)+  {-# INLINE unitl' #-}+  unitr = Kleisli $ \(a, ()) -> pure a+  {-# INLINE unitr #-}+  unitr' = Kleisli $ \a -> pure (a, ())+  {-# INLINE unitr' #-}++instance (Monad m) => Action (,) (Kleisli m) where+  swap = Kleisli $ \(a, b) -> pure (b, a)+  {-# INLINE swap #-}++type instance Unit Either = Void++-- | Coproduct tensor action on functions.+--+-- .> par ((+1) :: Int -> Int) ((*2) :: Int -> Int) (Left 3 :: Either Int Int)+-- Left 4+--+-- .> par ((+1) :: Int -> Int) ((*2) :: Int -> Int) (Right 3 :: Either Int Int)+-- Right 6+instance Tensor Either (->) where+  par = bimap+  {-# INLINE par #-}+  unitl = either absurd id+  {-# INLINE unitl #-}+  unitl' = Right+  {-# INLINE unitl' #-}+  unitr = either id absurd+  {-# INLINE unitr #-}+  unitr' = Left+  {-# INLINE unitr' #-}++-- | Coproduct symmetry on functions.+--+-- .> swap (Left 3 :: Either Int Int) :: Either Int Int+-- Right 3+instance Action Either (->) where+  swap = \case+    Left a -> Right a+    Right b -> Left b+  {-# INLINE swap #-}++-- | Coproduct tensor action on @Kleisli@ @m@.+--+-- .> import Control.Arrow (Kleisli(..), runKleisli)+-- .> let f = Kleisli (\n -> pure (n + 1)) :: Kleisli IO Int Int+-- .> let g = Kleisli (\n -> pure (n * 2)) :: Kleisli IO Int Int+-- .> runKleisli (par f g) (Left 3 :: Either Int Int)+-- Left 4+-- .> runKleisli (par f g) (Right 3 :: Either Int Int)+-- Right 6+instance (Monad m) => Tensor Either (Kleisli m) where+  par (Kleisli f) (Kleisli g) =+    Kleisli $ \case+      Left a -> Left <$> f a+      Right c -> Right <$> g c+  {-# INLINE par #-}+  unitl = Kleisli $ either absurd pure+  {-# INLINE unitl #-}+  unitl' = Kleisli $ pure . Right+  {-# INLINE unitl' #-}+  unitr = Kleisli $ either pure absurd+  {-# INLINE unitr #-}+  unitr' = Kleisli $ pure . Left+  {-# INLINE unitr' #-}++-- | Coproduct symmetry on @Kleisli@ @m@.+instance (Monad m) => Action Either (Kleisli m) where+  swap = Kleisli $ pure . swap+  {-# INLINE swap #-}++-- | Lift 'Tensor'/'Action' through 'Loop'.+--+-- This is the single lawful instance: it evaluates each 'Loop' branch+-- independently with 'run' and combines the results using the base arrow's+-- tensor. It is correct and black-hole-free, but does not fuse feedback+-- loops. For the fused superposition of two 'Knot's, use 'superpose'.+instance (Tensor t arr, Traced t' arr, Discrete arr) => Tensor t (Loop t' arr) where+  par :: forall a b c d. Loop t' arr a b -> Loop t' arr c d -> Loop t' arr (t a c) (t b d)+  par f g =+    Lift $+      withOb @arr @a $+        withOb @arr @b $+          withOb @arr @c $+            withOb @arr @d $+              par (run f) (run g)+  unitl = Lift unitl+  unitl' = Lift unitl'+  unitr = Lift unitr+  unitr' = Lift unitr'++instance (Action t arr, Traced t' arr, Discrete arr) => Action t (Loop t' arr) where+  swap = Lift swap++-- | Fused parallel composition for 'Loop' when the feedback tensor matches.+--+-- Two 'Knot's in parallel superpose into one 'Knot' over a paired channel,+-- satisfying the superposing axiom of traced monoidal categories:+--+-- @superpose (trace f) (trace g) = trace (pre . par f g . post)@+--+-- where @pre@ and @post@ rearrange the paired channel via associators+-- and braiding. This preserves sharing for recursive circuits; the lawful+-- 'Tensor' instance falls back to independent evaluation.+--+-- .> let k1 = Circuit.Loop.Knot (\(ns, _) -> (1 : ns, take 3 ns)) :: Circuit.Loop.Loop (,) (->) [Int] [Int]+-- .> let k2 = Circuit.Loop.Knot (\(ns, _) -> (2 : ns, take 3 ns))+-- .> Circuit.Layer.run (superpose k1 k2) ([], [])+-- ([1,1,1],[2,2,2])+--+-- The same fusion works for @Kleisli@, preserving sharing across the+-- recursive channels under @MonadFix@.+--+-- .> let k1 = Circuit.Loop.Knot (Kleisli $ \(ns, _) -> pure (1 : ns, take 3 ns)) :: Circuit.Loop.Loop (,) (Kleisli Identity) [Int] [Int]+-- .> let k2 = Circuit.Loop.Knot (Kleisli $ \(ns, _) -> pure (2 : ns, take 3 ns))+-- .> runKleisli (Circuit.Layer.run (superpose k1 k2)) ([], [])+-- Identity ([1,1,1],[2,2,2])+superpose ::+  forall t arr a b c d.+  (Tensor t arr, Strength t arr, Discrete arr) =>+  Loop t arr a b ->+  Loop t arr c d ->+  Loop t arr (t a c) (t b d)+superpose x y = case (x, y) of+  (Knot @_ @s @_ @_ @_ f, Knot @_ @s1 @_ @_ @_ g) ->+    withOb @arr @(t s s1) $ Knot $ pre .>> par f g .>> post+  (Knot @_ @_ @_ @_ @_ f, Lift g) -> Knot $ assoc'_ .>> par f g .>> assoc_+  (Lift f, Knot @_ @_ @_ @_ @_ g) -> Knot $ braid_ .>> par f g .>> braid_+  (Lift f, Lift g) -> Lift (par f g)+  where+    (.>>) :: forall x y z. arr x y -> arr y z -> arr x z+    (.>>) f' g' = withOb @arr @x $ withOb @arr @y $ withOb @arr @z $ g' . f'++    assoc_ :: forall x y z. arr (t (t x y) z) (t x (t y z))+    assoc_ = assocD++    assoc'_ :: forall x y z. arr (t x (t y z)) (t (t x y) z)+    assoc'_ = assocD'++    braid_ :: forall x y z. arr (t x (t y z)) (t y (t x z))+    braid_ = braidD++    pre, post :: forall u v w x. arr (t (t u v) (t w x)) (t (t u w) (t v x))+    pre = assoc_ .>> strengthD braid_ .>> assoc'_+    post = assoc_ .>> strengthD braid_ .>> assoc'_

@@ -1,390 +0,0 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE FlexibleInstances #-}-#ifdef __GLASGOW_HASKELL__-{-# LANGUAGE MagicHash #-}-{-# LANGUAGE UnboxedTuples #-}-#endif---- | Close and open feedback loops in a monoidal category.------ A 'Trace' instance for a tensor @t@ specifies how to thread a value--- through a feedback channel:------   * 'trace' closes the channel — eliminates the tensor and produces---     a plain morphism. This is where the loop semantics live.------   * 'untrace' opens the channel — lifts a plain morphism into the---     tensor, leaving the feedback value untouched.------ The trace laws (traced monoidal category axioms):------ 1. __Naturality (tightening)__. Morphisms that don't touch the traced---    wire pass through freely.------      @trace (untrace f . g . untrace h) = f . trace g . h@------ 2. __Dinaturality (sliding)__. A morphism on the traced wire can slide---    from one side of the trace to the other.------      @trace (g . untrace f) = trace (untrace f . g)@------ 3. __Vanishing__.------      * Unit: @trace (untrace f) = f@---      * Tensor: @trace (trace g) = trace (assoc . g . assoc')@------ 4. __Yanking__. Tracing a swap is identity.------      @trace swap = id@------ And for 'trace' and 'untrace' specifically: @'trace' . 'untrace' = 'id'@.--- 'untrace' is a section of 'trace'; round-tripping through--- @'untrace' . 'trace'@ only recovers morphisms that were already of the--- form @'untrace' f@.------ Two tensor semantics are provided, corresponding to the standard--- traced monoidal structures:------ [@(,)@] A single lazy recursive binding.  @trace f b@ produces--- @let (a, c) = f (a, b) in c@ — the feedback value @a@ and the--- output @c@ are co-defined.  This is cyclic sharing, not iteration:--- the body executes once with a self-referential channel.--- Only works in a lazy setting — the feedback value is a self-referential--- thunk.  In a strict language this binding is circular and divergent.------ [@Either@] A while-loop.  @Left a@ feeds back into another iteration;--- @Right c@ terminates.  The loop runs until a 'Right' is produced.------ For effectful arrows, both tensors lift to 'Kleisli' @m@:------   * @'MonadFix' m => 'Trace' ('Kleisli' m) (,)@ ties the lazy knot---     via 'mfix'.------   * @'Monad' m => 'Trace' ('Kleisli' m) 'Either'@ iterates via---     plain recursion.  For 'IO' specifically, an overlapping instance---     uses GHC's delimited-continuation primops ('prompt#', 'control0#')---     for constant stack space.------ /References:/------   * Hasegawa (1997) — cartesian (cyclic-sharing) vs computational---     (iterative) traces.  The @(,)@/@Either@ distinction.------   * Kidney & Wu (2026) — hyperfunctions, producer-consumer pattern.------   * Joyal, Street & Verity (1996) — traced monoidal categories.-module Circuit.Traced-  ( Trace (..),-    cellIO,-  )-where--#ifdef __GLASGOW_HASKELL__-import Control.Arrow (Kleisli (..))-import Control.Monad.Fix (MonadFix, mfix)-import Data.IORef-import GHC.Exts (PromptTag#, control0#, newPromptTag#, prompt#)-import GHC.IO (IO (..))-#endif---- $setup--- >>> import Control.Arrow (Kleisli (..), second)--- >>> import Control.Category ((>>>))--- >>> import Data.Either (fromRight)--- >>> import Circuit.Traced---- | A trace over a morphism @arr@ and tensor @t@.------ @trace@ closes the feedback loop, eliminating the tensor channel.--- @untrace@ opens the loop, lifting a plain morphism into the tensor.-class Trace arr t where-  trace :: arr (t a b) (t a c) -> arr b c-  untrace :: arr b c -> arr (t a b) (t a c)---- * Cartesian tensor — lazy knot---- | The cartesian trace ties a lazy knot: the feedback value @a@ and--- output @c@ are produced simultaneously in a single recursive binding.------ Only works in a lazy setting — the feedback value is a self-referential--- thunk.  In a strict language this binding is circular and divergent.--- Haskell's lazy evaluation makes cyclic sharing possible without--- mutation or explicit suspension primitives.------ >>> :{--- let powers (ns, ()) =---       (1 : map (*2) ns, take 5 ns)--- :}------ >>> trace powers () :: [Integer]--- [1,2,4,8,16]------ >>> trace (\(acc, x) -> (acc, x + 1)) 5--- 6------ Vanishing (a): tracing over the unit does nothing.------ Note: using @()@ as the channel type hits a GHC black-hole detection--- because @()@ has only one constructor. We test with 'Int' as the--- channel instead — the channel value is unconstrained, so the trace--- degenerates to plain function application.------ >>> let f (x, a) = (x, a + 1)--- >>> trace f 5--- 6------ prop> \n -> trace ((\(x, a) -> (x, a + n)) :: ((Int, Int) -> (Int, Int))) (0 :: Int) == (n :: Int)------ Yanking: tracing a swap is the identity.------ >>> let swap (x, y) = (y, x)--- >>> trace swap 42--- 42------ prop> \x -> trace ((\(a, b) -> (b, a)) :: ((Int, Int) -> (Int, Int))) (x :: Int) == x------ Tightening: payload morphisms pass freely through the trace.------ >>> let f (x, a) = (x, a)--- >>> trace (second (+1) . f . second (*2)) 5--- 11------ prop> \x -> trace (second ((+1) :: Int -> Int) . (id :: ((Int, Int) -> (Int, Int))) . second ((*2) :: Int -> Int)) (x :: Int) == x * 2 + 1------ Sliding: a morphism on the channel slides from one side to the other.------ >>> let swap (x, y) = (y, x)--- >>> trace (second (+1) . swap) 5--- 6------ >>> trace (swap . second (+1)) 5--- 6------ prop> \x -> trace (second ((+1) :: Int -> Int) . ((\(a, b) -> (b, a)) :: ((Int, Int) -> (Int, Int)))) (x :: Int) == trace (((\(a, b) -> (b, a)) :: ((Int, Int) -> (Int, Int))) . second ((+1) :: Int -> Int)) x------ Strength: an independent payload wire is invisible to the trace.------ >>> let f (x, c) = (x, c + 1)--- >>> let g (x, (a, c)) = (x', (a * 2, d)) where (x', d) = f (x, c)--- >>> trace g (3, 5)--- (6,6)------ prop> \a c -> trace ((\(x, (p, q)) -> (x, (p + a, q + 1))) :: ((Int, (Int, Int)) -> (Int, (Int, Int)))) (0 :: Int, c :: Int) == (a :: Int, c + 1)-instance Trace (->) (,) where-  trace f b = let (a, c) = f (a, b) in c-  untrace = fmap---- * Either tensor — iteration---- | The Either trace iterates: 'Left' feeds back (continue), 'Right'--- terminates (exit). A compact, under-appreciated pattern for loops in Haskell.------ >>> :{--- let fac (n, acc) | n <= 1    = Right acc---                  | otherwise = Left (n - 1, n * acc)--- :}------ >>> trace (either fac fac) (5, 1 :: Int)--- 120------ >>> :{--- let countdown = \case---       Left n | n > 0 -> Left (n - 1)---              | otherwise -> Right n---       Right n | n > 0 -> Left (n - 1)---               | otherwise -> Right n--- :}------ >>> trace countdown (3 :: Int)--- 0------ Vanishing (a): tracing over the unit does nothing.------ >>> let f = Right . (+1) . fromRight undefined--- >>> trace f 5--- 6------ prop> \n -> trace ((Right . (+ n) . fromRight (undefined :: Int)) :: (Either () Int -> Either () Int)) (0 :: Int) == (n :: Int)------ Yanking: tracing a swap is the identity.------ >>> :{--- let swapEither (Left x)  = Right x---     swapEither (Right x) = Left x--- :}------ >>> trace swapEither 42--- 42------ prop> \x -> trace ((\e -> case e of Left a -> Right a; Right a -> Left a) :: (Either Int Int -> Either Int Int)) (x :: Int) == x------ Tightening: payload morphisms pass freely through the trace.------ >>> let f = fmap ((+1) :: Int -> Int) . fmap ((*2) :: Int -> Int)--- >>> trace (f :: Either () Int -> Either () Int) 5--- 11------ prop> \x -> trace (fmap ((+1) :: Int -> Int) . fmap ((*2) :: Int -> Int) :: Either () Int -> Either () Int) (x :: Int) == x * 2 + 1-instance Trace (->) Either where-  trace f b = go (Right b)-    where-      go x = case f x of-        Right c -> c-        Left a -> go (Left a)-  untrace = fmap--#ifdef __GLASGOW_HASKELL__---- * Kleisli m (,) — lazy knot via MonadFix---- | Trace for 'Kleisli' @m@ with the cartesian tensor, requiring @'MonadFix' m@.------ The lazy knot is tied via 'mfix'. The feedback channel is lazy in the--- recursive binding — the body must not force the feedback value before--- producing it, or 'mfix' will diverge (just as the pure @(,)@ trace--- black-holes on strict fields).------ >>> :{--- let fibs = Kleisli $ \(fibs, ()) ->---       pure (0 : 1 : zipWith (+) fibs (drop 1 fibs), take 3 fibs)--- :}------ >>> runKleisli (trace fibs) ()--- [0,1,1]-instance MonadFix m => Trace (Kleisli m) (,) where-  trace (Kleisli f) =-    Kleisli-      ( \b -> do-          (_, c) <- mfix $ \ ~(s, _) -> f (s, b)-          pure c-      )--  untrace (Kleisli f) =-    Kleisli-      ( \(a, b) -> do-          c <- f b-          pure (a, c)-      )---- * Kleisli m Either — iteration for any Monad---- | Trace for 'Kleisli' @m@ with the 'Either' tensor, for any @'Monad' m@.------ Iterates by feeding 'Left' back into the step function until a 'Right'--- is produced. Uses plain recursion — builds stack proportional to--- iteration count.------ >>> :{--- let countTo target = Kleisli $ \case---       Left n | n < target -> pure (Left (n + 1))---              | otherwise  -> pure (Right n)---       Right ()            -> pure (Left 0)--- :}------ >>> runKleisli (trace (countTo (3 :: Int))) ()--- 3------ This instance is @OVERLAPPABLE@: the IO-specific instance below takes--- priority for 'IO', providing constant-stack iteration via delimited--- continuations.-instance {-# OVERLAPPABLE #-} Monad m => Trace (Kleisli m) Either where-  trace (Kleisli f) =-    Kleisli $ \b -> go (Right b)-      where-        go x = f x >>= \case-          Right c -> pure c-          Left a -> go (Left a)--  untrace (Kleisli f) =-    Kleisli $ \case-      Left a -> pure (Left a)-      Right b -> Right <$> f b---- * Kleisli IO Either — delimited continuations (constant stack)---- | GHC delimited-continuation primops.-data PromptTag a = PromptTag (PromptTag# a)---- | Create a new prompt tag for delimited continuations.-newPromptTag :: IO (PromptTag a)-newPromptTag =-  IO-    ( \s ->-        case newPromptTag# s of-          (# s', t #) -> (# s', PromptTag t #)-    )---- | Run an IO computation under a prompt boundary.-prompt :: PromptTag a -> IO a -> IO a-prompt (PromptTag t) (IO m) = IO (prompt# t m)---- | Captures the continuation up to the nearest prompt with the matching tag.-control0 :: forall a b. PromptTag a -> ((IO b -> IO a) -> IO a) -> IO b-control0 (PromptTag t) f = IO (control0# t arg)-  where-    arg f# s = case f (\(IO x) -> IO (f# x)) of IO m -> m s---- | Trace for 'Kleisli' 'IO' with 'Either' tensor.------ Each iteration re-establishes the prompt boundary. When @control0@--- fires on @Left a@, it captures the continuation, wraps it around--- the next loop step, and jumps back to the prompt — constant stack.------ >>> :{--- let exit42 = Kleisli $ \case---       Right () -> pure (Right (42 :: Int))--- :}------ >>> runKleisli (trace exit42) ()--- 42-instance {-# OVERLAPPING #-} Trace (Kleisli IO) Either where-  trace (Kleisli body) =-    Kleisli-      ( \initial -> do-          tag <- newPromptTag-          let go x =-                prompt tag $-                  body x-                    >>= ( \case-                            Right c -> pure c-                            Left a -> control0 tag (\k -> k (go (Left a)))-                        )-          go (Right initial)-      )--  untrace (Kleisli f) =-    Kleisli-      ( \case-          Left a -> pure (Left a)-          Right b -> Right <$> f b-      )---- * Stateful stages via IORef---- | Create a stateful 'Kleisli' 'IO' arrow backed by 'IORef'.------ Allocates a mutable reference once, then each invocation reads the--- current state, applies the transfer function, writes the new state--- back, and returns the output. The 'IORef' is hidden inside the--- arrow — callers see a pure @Kleisli IO a b@.------ This breaks the circular dependency that 'MonadFix' requires for--- the 'Trace' @(,)@ instance: the feedback value is stored in the--- mutable cell rather than being self-referential. Strict accumulators--- (counters, frequency tables, running sums) work without diverging.-cellIO-  :: s-  -- ^ initial state-  -> (s -> a -> IO (s, b))-  -- ^ transfer: current state and input yield next state and output-  -> IO (Kleisli IO a b)-cellIO s0 step = do-  ref <- newIORef s0-  pure $-    Kleisli $ \a -> do-      s <- readIORef ref-      (s', b) <- step s a-      writeIORef ref s'-      pure b--#endif