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.

The free boundary K + payload.

A token on the boundary is either a mark from a finite alphabet k or a payload value a. This is the level-0 grammar of process boundaries: marks are the control tokens, payloads are the data.

fmap acts only on the payload side; marks are carried through unchanged.

>>> fmap length (Payload "hi")
Payload 2
>>> fmap length (Mark "halt")
Mark "halt"

True iff the token is a Mark.

True iff the token is a Payload.

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.

Convert a monomial System into a Process machine with a given initial state.

The first input is consumed for the state transition from the supplied initial state, matching the coalgebra intuition of a System.

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.

Run a system for as many steps as there are inputs, emitting one output per input. The output is the state after consuming the input, matching the Process semantics of systemAsProcess.

State after consuming a list of inputs.

List specialization of scanStream.

Run a process over any stream with an Uncons coalgebra and build the output with a Cons algebra.

The first element seeds the hidden channel via inject; each subsequent element steps it via step; each output is extract of the current channel.

List specialization of foldStream.

Run a process over a stream, returning the final output (if any).

List specialization of encodeStream.

Encode a process as a stream-level Trace over arbitrary Uncons/Cons streams.

This is the definitional runner: scanStream is eval composed with encodeStream. The feedback channel carries (Maybe channel, remaining input, accumulated output).

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.

Collect the emitted outputs of a 'Process (Maybe b)' over any stream.

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.

List specialization of processToBodyStream.

View a Process as an existentially-quantified Body.

The process state is exposed as the ambient wire. The initial state is Nothing; the first input is fed to inject to create the real state, and subsequent inputs use step. The output is always extract of the current state.