A dynamical system with interface p, carrier s, over base arrow arr, parameterised by the state-pairing tensor t.

Uncurried netlist form: the state and the current input direction are fed together under t, and the result is the next state together with the current output position. For the monomial Mono i o and t = (,) this is exactly the Moore body arr (s, i) (s, o) after collapsing the unit positions.

The cartesian specialisation SystemT (,) is kept as the type synonym System; use system and runSystem to construct and inspect it.

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).

Helpers for translating between the Eval presentation and the arrow presentation of a (->) system. These extend the netlist view to Sum.

Convert an eval-form (->) system into the arrow form.

Convert an arrow-form (->) system back into eval form.

This is a Moore observation: the position is read from the state alone, with the direction supplied only to compute the next state. Correctness therefore requires that the system be Moore at the call site — the position must not depend on the direction. Internally the direction is probeDir, which is lazily unused for the polynomial shapes where it is defined; any strict forcing of the direction (a bang pattern, seq, or a strict tuple in a user-written body) will turn toEvalSystem into a runtime error rather than a wrong answer.

Run one step: observe the current p-output from state s.

Extract the monomial direction from its 'Either Void' encoding.

Inject a monomial direction into its 'Either Void' encoding.

Place two Moore systems side by side: interface p ⊗ q, state (s, t).

This is the entry point for acyclic wiring over the Dirichlet tensor — boxes in parallel, pins assigned jointly. The wired interface can be mapped with parT (wire-then-map).

An existentially-quantified pair of channel poles over a body, carrying its seed. The shape mirrors SomeBody.

Run an existentially-packed pair of poles over a list of inputs.

This is the (,) / (->) specialisation; SomePoles is parametric in the tensor and arrow so that other shapes can reuse the existential packaging.

Convert a (->) System into companion/conjoint channel poles over Body.

The write pole runs the step and discards the output position; the read pole fabricates an observation by re-stepping the system with the supplied probe direction. This works only when the read can be reasonably approximated by a single probe direction; for an honest Moore observation prefer systemWithSeedToPoles.

Convert a pointed System into companion/conjoint channel poles over Body.

The state carrier is the system's state s and the seed s0 is carried by SomePoles. The write pole steps with the supplied direction; the read pole observes the current state without stepping, using the supplied observation function.

Run a monomial (->) system at a state, exposing the output position and the state-transition function.

The coalgebra-as-lens isomorphism.

A monomial system System (->) s (Mono i o) is exactly a lens S y^S -> Mono i o: the current state s determines the output position o, and each input direction i determines the next state s.

This is the bridge to Spivak's presentation: System s p ≅ Poly(S y^S, p).

Inverse of systemAsLens: build a system from a lens S y^S -> Mono i o.

Comultiplication for an observable system: the output position is the state. The result is a system over the two-step interface Mono o s ◁ Mono o s, so that feeding a pair of inputs (o1, o2) runs the original system for two steps.

Build a system whose interface is the coproduct of two monomial interfaces.

The carrier state selects the active branch at each step. This is the level-2 grammar operator on the span fragment: choice lives in the polynomial interface (Sum) rather than in the carrier-level 'if'.

Run a system with a homogeneous sum-of-monomials interface.

Build a system whose interface is the coproduct of two different monomial interfaces. The carrier state selects the active branch at each step.

Run a heterogeneous sum-interface system.

A single step of a heterogeneous sum-interface system. The GADT encodes the position-dependent input type: the left branch consumes an i1, the right branch consumes an i2.

Spivak's [p,q]-coalgebra. State s is runtime, not a type index.

• act gives the wiring pattern as a polynomial morphism.
• upd takes a state and an input observation in p and returns an output observation in q, i.e. a Step pairing the presented position with its own direction consumer.

A step observation in q, parameterized by state. Eval is already the GADT that pairs each position with its branch-appropriate direction consumer, so it avoids the flat 'Dir q' family that makes sums impossible.

Run a Coalgebra s 'Y q as a System over q.

Sequential composition of two closed coalgebras via the composition product.

Convert a monomial System into a Coalgebra s 'Y (Mono i o).