Free traced monoidal category over tensor t.

Lift a base arrow into the free traced category.

Close a feedback loop over the channel tensor t.

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) used to let constrained categories instance this class lawfully; those constraints are now explicit at the instance site rather than inherited from a constraint family.

Law note: the traced-category Sliding axiom is restricted in the premonoidal setting. Benton & Hyland, "Traced Premonoidal Categories" (2003, Def 3.2) replace unrestricted Sliding with Central Sliding: a morphism g may slide past the trace only when g is central. Dually, Centre Preservation says trace f is central whenever f is. This class does not enforce the side-conditions at the type level; lawful instances must guarantee them by construction. See the circuits-axioma sliding oracles for witnesses that the side-condition is not vacuous.

Tensorial strength for a tensor t inside a category arr.

strength tensors a plain morphism with the ambient channel. It is not a syntactic inverse of trace; it is the strength ("tensorial strength") of the tensor t acting on morphisms.

A channel whose interface is the polynomial p.

Internally it is a Moore system with hidden state s. The state is existentially quantified so that different channel constructors can use different state types.

Observe the current output of a (->) channel.

The observation is an Eval p (): a position together with a trivial direction consumer. The position is the channel's current output; the direction consumer is how a future input will advance the channel.

Commit an input direction to a (->) channel, advancing its state.

Identity channel on a monomial interface Mono a a.

Output is the current state; next state is the input direction. An initial state must be supplied because a Moore machine has no input before the first commit.

Constant-output channel on a monomial interface Mono a b.

Output is always b; the state is the constant value and is preserved across commits (the input direction is ignored).

Map a polynomial morphism over a (->) channel.

The forward map transforms positions; the backward map transforms directions. This is the functorial action of Morphism on channels.

A morphism across a tensored channel.

Body t ch arr a b is a morphism arr (t ch a) (t ch b). The channel ch is threaded alongside the payload by the tensor t; it may be state, residual, a stream, or any other value the base arrow arr carries along with the input and output. Composition threads the same channel through both morphisms.

A Body with its channel type hidden.

Compose two bodies at carriers ch and ch' into a body at carrier t ch ch'. This is the body-level building block of horizontal 2-cell algebra and of the Category instance for SomeBody.

The composite is

  assoc .> slide .> strength f .> slide .> strength g .> assoc'

Pointed carrier-tensoring composition for t = (,) and arr = (->).

Seeds pair under the tensor, and the composite can be run with runSomeBody. This is the pointed counterpart to the unpointed cascadeBody.

Run an existentially-packed cartesian body over a list of inputs.

This is the (,) / list specialisation of SomeBody.

Loose 1-cell: a body with its carrier type hidden.

Identity loose 1-cell at the tensor unit carrier.

The carrier is pinned to Unit so that the unit law can be witnessed with the unitor; without the annotation GHC would instantiate the hidden carrier to Any.

Square (indexed 2-cell). The carrier maps compose; the middle body must match (a caller side condition).

Identity square on a body.

Vertical composition of squares.

The middle body must match; this is a caller side condition.

Existential closure of Sq, for stating "there exists a 2-cell".

Eliminator for the existential carrier types of an Intertwiner.

Go down (carrier map) then across (target body).

A nondegenerate intertwiner witness: counter state quotiented by parity. The payload is Char so the carrier slot and payload slot are type-distinct; slot confusion is a type error. These examples exercise both parities and both reset branches. A paired perturbation doctest on acrossThenDown shows the equality can fail, so these agreement cases are not vacuous.

>>> let counter = (Body $ \(n, r) -> let n' = if r then 0 else n + 1 in (n', if odd n' then 'x' else 'y')) :: Body (,) Int (->) Bool Char
>>> let parity = (Body $ \(b, r) -> let b' = not r && not b in (b', if b' then 'x' else 'y')) :: Body (,) Bool (->) Bool Char
>>> let sq = Sq odd counter parity :: Sq (,) (->) Int Bool Bool Char
>>> downThenAcross sq (4, False)
(True,'x')
>>> downThenAcross sq (4, True)
(False,'y')
>>> downThenAcross sq (5, False)
(False,'y')

Go across (source body) then down (carrier map).

Agreement cases for the same witness:

>>> let counter = (Body $ \(n, r) -> let n' = if r then 0 else n + 1 in (n', if odd n' then 'x' else 'y')) :: Body (,) Int (->) Bool Char
>>> let parity = (Body $ \(b, r) -> let b' = not r && not b in (b', if b' then 'x' else 'y')) :: Body (,) Bool (->) Bool Char
>>> let sq = Sq odd counter parity :: Sq (,) (->) Int Bool Bool Char
>>> acrossThenDown sq (4, False)
(True,'x')
>>> acrossThenDown sq (4, True)
(False,'y')
>>> acrossThenDown sq (5, False)
(False,'y')

Perturbation: observe even-ness instead of odd-ness. The two paths now disagree, which proves the agreement cases above are not vacuous.

>>> let badCounter = (Body $ \(n, r) -> let n' = if r then 0 else n + 1 in (n', if even n' then 'x' else 'y')) :: Body (,) Int (->) Bool Char
>>> let bad = Sq odd badCounter parity :: Sq (,) (->) Int Bool Bool Char
>>> downThenAcross bad (4, False)
(True,'x')
>>> acrossThenDown bad (4, False)
(True,'y')

Carrier-tensoring composition of loose 1-cells.

The composite has carrier t ch ch' when the first body has carrier ch and the second has carrier ch'.

Left unitor witness: composing a body with the identity at the unit carrier is isomorphic to the original body.

Right unitor witness.

Indexed left unitor square.

Indexed right unitor square.

Associator witness: carrier bracketing of three composed bodies is isomorphic up to the associator of the tensor.

Indexed associator square.

Right whisker: tensor a square with an identity-on-boundaries 1-cell on the right.

Left whisker: tensor an identity-on-boundaries 1-cell on the left of a square.

Horizontal composition of two squares.

Boundary whisker: apply tight maps to the input and output boundaries of a square. This is the Sq side of the interchange law; the Poles side is iomap on the Moore-split representation.

Close a feedback loop over a component s of the input/output object.

The 1-cell must be of the form Circ t arr (t s a) (t s b): the feedback value s appears as the first component of the tensor in both domain and codomain. The result moves s into the hidden carrier, turning it into state. This is the guarded / state-bootstrapping feedback of KSW, not the immediate fixed-point trace: yanking fails here, which is the expected behaviour for a feedback category.

Implemented by reassociating so that s becomes part of the carrier:

  feedback (Circ (Body f)) = Circ (Body (assoc .> f .> assoc'))

Cartesian systems: the state-pairing tensor is (,).

Construct a cartesian System from its underlying arrow.

Inspect a cartesian System as its underlying arrow.

Build a monomial System from a step and an observation.

This is the pointed-Moore view of a stateful morphism, expressed directly in System terminology. The state transition s -> a -> s and the observation s -> b are explicit; the seed is supplied later (for example by systemToProcess).

The monomial interface: i directions (input), o positions (output).

A morphism p -> q in Poly, encoded as a natural transformation between the evaluated functors.

By the Yoneda / sigma universal property, this is equivalent to a bundle map: a function on positions together with a contravariant family of functions on directions.

Konst and Depend extend the original Poly sketch so that backward maps can depend on the current position, giving point-dependent lenses.

The general point-dependent lens.

Forward pass get :: a -> b; backward pass put :: a -> db -> da depends on the current position.

>>> let l = lens show (\n d -> n + d) :: Morphism (Mono Int Int) (Mono Int String)
>>> let (v, put) = applyLens l 40 in (v, put 2)
("40",42)

Apply a monomial morphism as a lens: (get, put).

Prism: match on a sum-like source, build from the focused branch.

>>> let p = prism (\case Left n -> Left n; Right s -> Right (Right s)) Left :: Morphism (Mono (Either Int String) (Either Int String)) ('Sum (Mono Int Int) (Mono (Either Int String) (Either Int String)))
>>> case runMorphism p (EP (EK (Left 7), EE id)) of ES (Left (EP (EK n, EE k))) -> (n, k 1)
(7,Left 1)

Position set of a polynomial.

For a value of p(x), 'Pos p' is the index type of positions.

Direction set of a polynomial.

For a value of p(x) at a given position, 'Dir p' is the domain of the function into x.

Sum gets a flat direction space Either (Dir p) (Dir q). This is an over-approximation: only the branch selected by the position is in-fibre. It is nonetheless the right shape for dynamics, where the input direction is supplied after the position is observed: a wrong-branch direction is simply off-fibre. The netlist view (Netlist) remains position-dependent and still does not admit a Sum instance.

For Comp, Dir ('Comp p q) = ('Dir p, 'Dir q) is the same flat approximation: the q-position (hence its honest pin set) depends on which p-direction was taken. Exact for Sum-free factors with uniform directions — the monomial fragment.

A stateful process from a to b.

The existential state type s is hidden; the observable interface is the triple inject step extract. Keeping the triple as the primitive (rather than fusing extract into the step) preserves the streaming-statistics invariant that the first output is extract (inject x), before any step.

List specialization of scanStream.

List specialization of foldStream.

Convert a monomial System, an explicit seed, and a state observation into a first-input-seeded Process.

The observation s -> b is applied to the current state to produce each output, including the first output from the seed. The step system is used only for state transitions.

Lift a monomial System and a state observation into a boundary system over Boundary tokens.

Payloads are stepped through the inner system. Marks satisfying the halt predicate freeze the system and produce Nothing thereafter; non-halt marks leave the state unchanged and emit the current output. The halted state remembers the final inner state.

The returned system carries state Either s s: Left is running, Right is halted. This is the core combinator behind mark-driven halt: the finite mark alphabet k carries control tokens, while payloads carry data.

One-tick delay with an initial value.

Output is s0 on the first tick and the input from the previous tick thereafter. This is the primitive that makes register productive: the feedback wire is observable one tick late.

Cross-tick register feedback.

Given an initial feedback value s0 and a process Process (a, s) (b, s), close the s wire so that the s produced at one tick is fed back as input at the next tick. This is the productive, strict-accumulator-safe analogue of the cartesian trace: the delay is explicit in the wiring rather than implicit in a lazy knot.

Compare with the cartesian trace on Process, which ties a lazy knot and diverges for strict state; register keeps strict state cells sound by making the one-tick delay observable.

For bodies whose fixed-point is independent of the initial feedback value (e.g. affine/stateless feedback such as ewmaBody), the same wiring can be expressed by swapping the feedback wire into the active position, applying strength (delay s0), and tracing.

Build a Process from a Mealy-style step.

The output may depend on the current input. The channel internally stores the most recent output so that the Moore-style Process interface is preserved.

List specialization of runMealyStream.

Out is the companion of the identity functor. Covariant in a (sits in the output position).

In is the conjoint of the identity functor. Contravariant in a (sits in the input position).

A matched pair of channel poles: 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, Poles carries an enriched profunctor structure over the base category arr: prefixIn is the left action of arr on In poles, and suffixOut is the right action of arr on Out poles.

Plug an In and an Out of the same payload type together.

close feeds the Out into the In pole, producing a morphism arr a a from the paired payload type.

Yanking: for the unit poles from open, close (conjoint p) (companion p) = id.

Precompose an arr-morphism with an In pole.

Given f :: arr a b and an In pole at type b, produce an In pole at type a. Running the resulting pole first executes f and then commits through the original pole.

This is the left (contravariant) action of the base category on In poles. Specialised to unit poles it is the canonical way to build effectful write poles.

>>> let polesU = open :: Poles (->) () ()
>>> let inA = prefixIn (const ()) (conjoint polesU) :: In (->) Int
>>> commit inA (companion polesU) 42
()

Postcompose an arr-morphism with an Out pole.

Given an Out pole at type a and g :: arr a b, produce an Out pole at type b. Running the resulting pole first emits through the original pole and then executes g on the emitted value.

This is the right (covariant) action of the base category on Out poles. Specialised to unit poles it is the canonical way to build effectful read poles.

>>> let polesU = open :: Poles (->) () ()
>>> let outA = suffixOut (companion polesU) (const 42) :: Out (->) Int
>>> emit outA (conjoint polesU) ()
42

Build a Poles from a write morphism and a read morphism.

write :: arr a bot consumes the input payload and produces the dualising object; read :: arr bot b consumes the dualising object and produces the output payload. The dualising-object poles 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 poles.

Compositional spelling:

poles write receive =
  Poles (prefixIn write (conjoint open)) (suffixOut (companion open) receive)

Specialization of poles for K actions.

write :: a -> m () consumes the input payload; receive :: m b produces the output payload. The dualising-object handling is hidden inside the K wrappers.

Extract the primitive write and read actions from a Poles by plugging each pole with the dualising-object poles.

For a Poles built with poles, this recovers the original write :: arr a bot and receive :: arr bot b.

>>> let p = poles0 (\() -> ()) (const (42 :: Int)) :: Poles (->) () Int
>>> let (write, receive) = splay0 p
>>> (write (), receive ())
((),42)

Forward-composition operator for Poles. p1 >:> p2 = compose p1 p2.

Arrows that have channel poles for a given dualising object bot.

The dualising object is the target of the polar pairing and the object through which the two poles of a Poles are plugged together. In the cartesian case it is the monoidal unit (); for halt-mark / delivery pairings it can be Bool.

The poles are the identity-on-bot morphism split into its two polar halves. The companion is constant; the conjoint delegates to the opposing companion.

These poles require the base arrow to support constant morphisms, so they are captured by this class rather than being definable for all arrows.

The copycat strategy at the dualising object bot.

This is the multiplicative excluded middle bot ⅋ bot⊥ for arrows that have poles at bot: a self-dual channel whose close is the identity on bot. It routes between the two poles without ever deciding which one holds.

The additive excluded middle bot ⊕ bot⊥ — a verdict, now — is not supported; there is no decide :: Either bot bot here, because only the routing witness is provable.

Close a Poles to a plain base-arrow morphism.

A matched pair of free poles (Poles) is a box with one input wire and one output wire. This helper embeds that box into a traced monoidal category by unit-plugging the remaining two slots, giving a plain arr a b: input on the left, output on the right, with the unit plumbing hidden.

>>> let p = poles0 (const ()) (const 42) :: Poles (->) () Int
>>> box @() p ()
42

Asymmetric box with the dualising object exposed on opposite sides.

Uses tensor at the base arrow level. The input carries the dualising object on the right and the output carries it on the left; most users will prefer the dualising-object-normalised box.

>>> let p = poles0 (const ()) (const 42) :: Poles (->) () Int
>>> boxAsymmetric @() p ((), ())
((),42)

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.

>>> run (Lift (+1) :: Free (->) Int Int) 5
6
>>> run (Compose (Lift (+1)) (Lift (*2)) :: Free (->) Int Int) 5
11

Freeze a Free category into its base arrow.

This is a synonym for run Free.

>>> freeze (Lift (+1) :: Free (->) Int Int) 5
6

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.

The kind of Haskell categories: type-to-type hom-sets.

An arrow-to-arrow mapping (a natural transformation between profunctors).

The left direction of the hom-set isomorphism: restrict a map out of the free layer to the generators.

Forward composition. f .> g = g . f

Forward application. x |> f = f x

Backward application. f <| x = f x

Copy a value into a pair.

Laws:

  fst . copy = id              -- left unit
  snd . copy = id              -- right unit
  (copy × id) . copy = (id × copy) . copy  -- coassociativity
  braid . copy = copy            -- cocommutativity

Discard a value.