diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -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.
diff --git a/circuits.cabal b/circuits.cabal
--- a/circuits.cabal
+++ b/circuits.cabal
@@ -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,
diff --git a/other/axioms.md b/other/axioms.md
deleted file mode 100644
--- a/other/axioms.md
+++ /dev/null
@@ -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`
diff --git a/other/circuits-class.html b/other/circuits-class.html
new file mode 100644
--- /dev/null
+++ b/other/circuits-class.html
@@ -0,0 +1,87 @@
+
+
+
+
+
+
+
+
+
+circuits — class relationships
+
+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
+
+
+
diff --git a/other/circuits-module.html b/other/circuits-module.html
new file mode 100644
--- /dev/null
+++ b/other/circuits-module.html
@@ -0,0 +1,99 @@
+
+
+
+
+
+
+
+
+
+circuits — module view
+
+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
+
+
+
diff --git a/other/symbols.md b/other/symbols.md
deleted file mode 100644
--- a/other/symbols.md
+++ /dev/null
@@ -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
diff --git a/readme.md b/readme.md
--- a/readme.md
+++ b/readme.md
@@ -1,110 +1,196 @@
⟴ circuits
-## 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
-
-
+`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.
diff --git a/src/Circuit.hs b/src/Circuit.hs
--- a/src/Circuit.hs
+++ b/src/Circuit.hs
@@ -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
diff --git a/src/Circuit/Algebra.hs b/src/Circuit/Algebra.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Algebra.hs
@@ -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
diff --git a/src/Circuit/Category.hs b/src/Circuit/Category.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Category.hs
@@ -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
diff --git a/src/Circuit/Channel.hs b/src/Circuit/Channel.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Channel.hs
@@ -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)
+ )
diff --git a/src/Circuit/Circuit.hs b/src/Circuit/Circuit.hs
deleted file mode 100644
--- a/src/Circuit/Circuit.hs
+++ /dev/null
@@ -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
diff --git a/src/Circuit/Classes.hs b/src/Circuit/Classes.hs
deleted file mode 100644
--- a/src/Circuit/Classes.hs
+++ /dev/null
@@ -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
diff --git a/src/Circuit/Dagger.hs b/src/Circuit/Dagger.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Dagger.hs
@@ -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
diff --git a/src/Circuit/Discrete.hs b/src/Circuit/Discrete.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Discrete.hs
@@ -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
diff --git a/src/Circuit/Ends.hs b/src/Circuit/Ends.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Ends.hs
@@ -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 ())))
diff --git a/src/Circuit/Free.hs b/src/Circuit/Free.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Free.hs
@@ -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
diff --git a/src/Circuit/Hyper.hs b/src/Circuit/Hyper.hs
--- a/src/Circuit/Hyper.hs
+++ b/src/Circuit/Hyper.hs
@@ -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
diff --git a/src/Circuit/Layer.hs b/src/Circuit/Layer.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Layer.hs
@@ -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
diff --git a/src/Circuit/Loop.hs b/src/Circuit/Loop.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Loop.hs
@@ -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)
diff --git a/src/Circuit/Monoidal.hs b/src/Circuit/Monoidal.hs
deleted file mode 100644
--- a/src/Circuit/Monoidal.hs
+++ /dev/null
@@ -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))
diff --git a/src/Circuit/Net.hs b/src/Circuit/Net.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Net.hs
@@ -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)
diff --git a/src/Circuit/Sym.hs b/src/Circuit/Sym.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Sym.hs
@@ -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
diff --git a/src/Circuit/Tensor.hs b/src/Circuit/Tensor.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Tensor.hs
@@ -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'_
diff --git a/src/Circuit/Traced.hs b/src/Circuit/Traced.hs
deleted file mode 100644
--- a/src/Circuit/Traced.hs
+++ /dev/null
@@ -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