circuits (empty) → 0.1.0.0

raw patch · 12 files changed

+2034/−0 lines, 12 filesdep +basedep +profunctors

Dependencies added: base, profunctors

Files

• ChangeLog.md +25/−0
• LICENSE +29/−0
• circuits.cabal +68/−0
• other/axioms.md +356/−0
• other/symbols.md +238/−0
• readme.md +112/−0
• src/Circuit.hs +143/−0
• src/Circuit/Circuit.hs +145/−0
• src/Circuit/Classes.hs +42/−0
• src/Circuit/Hyper.hs +287/−0
• src/Circuit/Monoidal.hs +199/−0
• src/Circuit/Traced.hs +390/−0

@@ -0,0 +1,25 @@+# Revision history for circuits++## 0.1.0.0 — 2025-05-26++- 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.

@@ -0,0 +1,29 @@+Copyright (c) 2026++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the distribution.++3. Neither the name of the copyright holder nor the names of its+   contributors may be used to endorse or promote products derived+   from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,+INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,+BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS+OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED+AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF+THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH+DAMAGE.

@@ -0,0 +1,68 @@+cabal-version: 3.0+name: circuits+version: 0.1.0.0+license: BSD-3-Clause+license-file: LICENSE+copyright: Tony Day (c) 2025+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+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.++build-type: Simple+tested-with:+  ghc ==9.10.1+  ghc ==9.12.2+  ghc ==9.14.1++extra-doc-files:+    ChangeLog.md+    readme.md+    LICENSE+    other/symbols.md+    other/axioms.md++source-repository head+  type: git+  location: https://github.com/tonyday567/circuits++common ghc-options-stanza+  ghc-options:+    -Wall+    -Wno-unused-imports+    -Wcompat+    -Widentities+    -Wincomplete-record-updates+    -Wincomplete-uni-patterns+    -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+  hs-source-dirs: src+  exposed-modules:+    Circuit+    Circuit.Circuit+    Circuit.Classes+    Circuit.Hyper+    Circuit.Monoidal+    Circuit.Traced++  build-depends:+    base >=4.18 && <5,++  if impl(ghc)+    build-depends: profunctors >=5.0 && <6,

@@ -0,0 +1,356 @@+# 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,238 @@+# 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

@@ -0,0 +1,112 @@+<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>++## ⚙️ Install++```+(m)cabal build circuits+```++Compiles on MicroHS & GHC 9.10+ with `base` & `profunctors`++## 📡 Usage++```haskell+import Circuit++-- Fibonacci via knot-tying+>>> take 5 (trace (\(fibs, ()) -> (0 : 1 : zipWith (+) fibs (drop 1 fibs), fibs)) () :: [Integer])+[0,1,1,2,3]++-- Iteration with Either+>>> let step n = if n < 3 then Left (n + 1) else Right n in trace (either step step) (0 :: Int)+3+```++## 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).++Conversion is given by `reify` and `encode` (and `encodeEither`/`runEither`). The core triangle on observables is `reify . encode = id`.++## 🧭 Pitch++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.++Hyper is the same as the Kidney & Wu construction:++```haskell+newtype Hyper a b = Hyper { invoke :: Hyper b a -> b }+```++From the paper and surrounding literature, we use the hyperfunction axioms and derive a `Circuit`:++```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+```++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.++> 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)++`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`.++`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.++## 📦 Sibling libraries++**circuits-parser** — `Circuit (->) Either f (These a f)` as a parser for a wide variety of f and a.++**circuits-io** — `Circuit (Kleisli IO) Either` as a way to engage with file I/O, sockets, servers, (a)timings & asynchronicity.++**circuits-meter** — circuit measurement and performance.++## 📖 Read++["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.++`other/` — the narrative arc (notation, marks-and-stacks, knot, triangle proof, tensors, Mendler case, examples). For the long version.++`examples/` — cards: parsers, pipes, Elgot iteration, delimited continuations. Paste code blocks into `cabal repl`.++## Contributing++We welcome contributions of any persuasion or fancy. New contributors should open an issue and say hi.++AI / LLM policy++LLMs and agents have been used in the development of this library, including category theory, coding, generation, refactoring, documentation and narrative.++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.++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.++code is code and coders are going to code.++<br>++[![Hackage](https://img.shields.io/hackage/v/circuits.svg)](https://hackage.haskell.org/package/circuits)+[![build](https://github.com/tonyday567/circuits/actions/workflows/haskell-ci.yml/badge.svg)](https://github.com/tonyday567/circuits/actions/workflows/haskell-ci.yml)

@@ -0,0 +1,143 @@+-- | Circuit: free traced monoidal categories and hyperfunctions.+--+-- == Usage+--+-- @+-- import Circuit+-- @+--+-- === Lazy feedback (knot-tying)+--+-- 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]+-- [1,2,4,8,16]+--+-- === Iteration+--+-- 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)+-- 5+--+-- === Switching between representations+--+-- 'Circuit' is the inspectable GADT form. 'Hyper' is the efficient final+-- encoding. Convert with 'encode' and 'reify'.+--+-- >>> lower (encode (Lift (+1) :: Circuit (->) (,) 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.+--+-- The 'Trace' class (in "Circuit.Traced") 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".+--+-- == Core Concepts+--+-- * __Tensor__ (@t@): The bifunctor pairing a feedback value with a payload+--   inside a 'Knot' (currently @(,@) or 'Either').+--+-- * __Feedback value__: The component that travels around the loop (first+--   parameter of the tensor in a 'Knot').+--+-- * __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.+module Circuit+  ( -- * Circuit+    Circuit (..),+    Wire,+    Step,+    reify,++    -- * Traced+    Trace (..),+    cellIO,++    -- * Hyper+    Hyper (..),+    lift,+    lower,+    base,+    push,+    run,+    encode,+    encodeEither,+    runEither,+    flatten,++    -- * Monoidal+    Braided (..),+    ambient,+    assoc,+    assoc',+    seed,+    absorb,+    release,+    coassoc,+    coassoc',+    coseed,+    coabsorbL,+    coabsorbR,+    coreleaseL,+    coreleaseR,+    ambientBy,+  )+where++import Circuit.Circuit+  ( Circuit (..),+    Step,+    Wire,+    reify,+  )+import Circuit.Hyper+  ( Hyper (..),+    base,+    encode,+    encodeEither,+    flatten,+    lift,+    lower,+    push,+    run,+    runEither,+  )+import Circuit.Monoidal+  ( Braided (..),+    absorb,+    ambient,+    ambientBy,+    assoc,+    assoc',+    coabsorbL,+    coabsorbR,+    coassoc,+    coassoc',+    coreleaseL,+    coreleaseR,+    coseed,+    release,+    seed,+  )+import Circuit.Traced+  ( Trace (..),+    cellIO,+  )

@@ -0,0 +1,145 @@+{-# 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

@@ -0,0 +1,42 @@+{-# 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,287 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Hyperfunctions: final encoding of traced monoidal categories.+--+-- A hyperfunction (following Kidney & Wu) is a value that is completely+-- 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+-- corresponding /initial/ (inductive) encoding. The feedback channel+-- is not represented by an extra constructor; it is structural in the+-- type itself.+module Circuit.Hyper+  ( -- * Hyper+    Hyper (..),++    -- * Construction and elimination+    lift,+    lower,+    base,+    push,+    run,++    -- * Encoding+    encode,+    encodeEither,+    runEither,+    flatten,+  )+where++import Circuit.Circuit (Circuit (..), reify)+import Circuit.Traced (Trace (..))+import Prelude hiding (id, (.))++#ifdef __GLASGOW_HASKELL__+import Control.Category+import Data.Profunctor+#else+import Circuit.Classes+#endif++-- $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++-- | A hyperfunction from @a@ to @b@.+--+-- 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+-- 42+--+-- >>> run (Hyper $ \k -> invoke k (Hyper $ \_ -> 0) + 1)+-- 1+newtype Hyper a b = Hyper+  { -- | Feed a continuation of type @Hyper b a@ into the hyperfunction.+    invoke :: Hyper b a -> b+  }++-- * Construction and elimination++-- | Embed a plain function into a hyperfunction.+--+-- 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+-- 6+lift :: (a -> b) -> Hyper a b+lift f = push f (lift f)++-- | Extract a plain function from a hyperfunction.+--+-- Supplies the hyperfunction with a constant continuation+-- (@invoke h (Hyper (const a))@), asking: "what output do you produce+-- when the feedback channel feeds back the input @a@?"+--+-- >>> lower (lift reverse) "hello"+-- "olleh"+lower :: Hyper a b -> (a -> b)+lower h a = invoke h (Hyper (const a))++-- | Ignores the input and returns a constant value.+--+-- >>> lower (base 42) undefined+-- 42+base :: a -> Hyper b a+base a = Hyper (const a)++-- | Push a plain function onto a hyperfunction.+--+-- The function @f@ is applied to whatever value the hyperfunction+-- eventually produces. This threads @f@ through the continuation,+-- enabling feedback-aware composition.+--+-- >>> lower (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'.+--+-- >>> run (Hyper $ \_ -> 42 :: Int)+-- 42+--+-- >>> run (Hyper $ \h -> invoke h (Hyper $ \_ -> 0) + 1) :: Int+-- 1+run :: Hyper a a -> a+run h = invoke h (Hyper run)++-- * Properties++-- Faithful embedding: observation recovers the original arrow.+--+-- prop> \x -> lower (lift (+1)) (x :: Int) == x + 1++-- Functoriality: lift respects composition.+--+-- prop> \x -> lower (lift (*2) . lift (+1)) (x :: Int) == (x + 1) * 2++-- * Trace++-- | 'Trace' 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:+--+--   1. @invoke body cont@ calls the body, which will eventually ask @cont@+--      for an @(a, b)@ — the feedback pair.+--   2. @cont@ captures @a@ from @body@'s output (@fst pair@) and feeds it+--      back as the first component of its return. This is the knot: @a@+--      cycles through @body → pair → cont → body@.+--   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) ()+-- [0,0,0]+instance Trace 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++-- | Encode a Circuit into a Hyper. Symbol: @(⇨)@.+--+-- This is the unique traced functor from the initial object (Circuit)+-- to the final object (Hyper), satisfying the commuting triangle+-- @lower . encode = reify@.+--+-- 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'.+--+-- >>> import Circuit.Circuit (Circuit (..), reify)+-- >>> lower (encode (Lift (+1) :: Circuit (->) (,) Int Int)) 5+-- 6+encode :: Circuit (->) (,) 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+-- 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+--       Left n  | n < 3 -> Left (n + 1)+--       Left n          -> Right n+-- :}+--+-- >>> runEither step (0 :: Int)+-- 3+encodeEither :: (Either a b -> Either a c) -> Hyper (Either a b -> c) (Either a b -> c)+encodeEither f = h+  where+    h =+      Hyper+        ( \k s ->+            case f s of+              Right c -> c+              Left a -> invoke k h (Left a)+        )++-- | 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.+--+-- >>> :{+-- let step = \case+--       Right n | n < 3 -> Left (n + 1)+--       Right n         -> Right n+--       Left n  | n < 3 -> Left (n + 1)+--       Left n          -> Right n+-- :}+--+-- >>> runEither step (0 :: Int)+-- 3+runEither :: (Either a b -> Either a c) -> b -> c+runEither f b = run (encodeEither f) (Right b)++-- | Flatten a Hyper to a Circuit 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+-- 6+--+-- Flatten then encode is not identity — the feedback structure is gone:+--+-- >>> let h = lift (+ 1)+-- >>> lower (encode (flatten h)) 5+-- 6+flatten :: Hyper a b -> Circuit (->) (,) a b+flatten h = Lift (lower h)++-- * Instances++instance Category Hyper where+  id = lift id+  f . g = Hyper $ \h -> invoke f (g . h)++-- | '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.+--+-- Profunctor identity: dimap id id = id+--+-- prop> \x -> lower (dimap id id h) (x :: Int) == x + 1+--+-- 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+--+-- lmap f = dimap f id+--+-- prop> \x -> lower (lmap ((*2) :: Int -> Int) h) (x :: Int) == lower (dimap ((*2) :: Int -> Int) id h) x+--+-- rmap g = dimap id g+--+-- prop> \x -> lower (rmap ((*2) :: Int -> Int) h) (x :: Int) == lower (dimap id ((*2) :: Int -> Int) h) x+instance Profunctor Hyper where+  dimap f g h = Hyper $ g . invoke h . dimap g f+  lmap f h = Hyper $ invoke h . rmap f+  rmap f h = Hyper $ f . invoke h . lmap f++instance Functor (Hyper a) where+  fmap = rmap

@@ -0,0 +1,199 @@+{-# 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,390 @@+{-# 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