A single entry on the shared log, polymorphic in payload.

Routing is by name list: a post delivers to every agent whose name appears in to (the audience). thread is the ancestry edges: [] for a root post, otherwise the PostIds of the posts being replied to or synthesised from. Parents are a set (duplicates discarded) in normalised (sorted) order — the smart constructors keep it so.

Absolute post identity. In the stamped log this is the line id assigned by the single writer. In pure meeting logs it is the position in the oldest-first log, but branches and cone resolve by the id itself, not by position in the passed-in list. Use indexToIdMap to assign ids [0..] from a chronological list.

A fresh root post (no parents).

A reply: the audience is the parent's sender plus the rest of the parent's audience (minus self); the sole thread edge cites the parent's PostId.

A synthesis: one descendant of several parents — the object-level wire-merge dual to merging agents. The ancestry cites every parent id as a normalised set (sorted, duplicates discarded).

Sorted, duplicate-free. The normalised-set primitive of the thread design: parent sets, audiences, and cones are all kept in this form.

Assign positional ids [0..] to a chronological list of posts. This is the convenience bridge from list-shaped logs to the id-resolved branches/cone API.

The label-branches from a post to its conversation roots, resolved by exact PostId. The current post is not in the map; its id is inferred as the id after the largest key in the prior map. Only thread edges strictly less than the current id are resolved (ancestors must be prior posts). A dangling or future id is silently ignored. A root post has one trivial branch; every parent edge contributes its own path. Branches of replies are pure cons:

branches (indexToIdMap prior) (replyTo who i p b)

map (who :) (branches (Map.filterWithKey (k _ -> k < i) (indexToIdMap prior)) p)

>>> let p1 = mkPost "tony" ["grok"] "hi" :: Post String; p2 = mkPost "grok" ["tony"] "hello"; r = replyTo "kimi" 1 p2 "a" in branchesByIndex [p1, p2] r == map ("kimi" :) (branchesByIndex [p1, p2] p2)
True

>>> let p1 = mkPost "tony" ["grok"] "hi" :: Post String; p2 = mkPost "grok" ["tony"] "hello"; r1 = replyTo "kimi" 1 p2 "a"; r2 = replyTo "tony" 2 r1 "b" in branchesByIndex [p1, p2, r1] r2
[["tony","kimi","grok"]]

Convenience wrapper: resolve branches from a chronological list, assigning ids [0..].

The ancestry cone: every name appearing on any branch from a post to its roots, as a normalised set — the "who contributed to this" query, free with the log. Includes the post's own sender.

Cone-union law:

cone (indexToIdMap prior) (synthesis who aud is b)

sortNub (who : concatMap (cone (Map.filterWithKey (k _ -> k < i) (indexToIdMap prior)) . (priorMap Map.!)) is)

>>> let p1 = mkPost "tony" ["grok"] "hi" :: Post String; p2 = mkPost "grok" ["tony"] "hello"; r1 = replyTo "kimi" 1 p2 "a"; prior = [p2, p1, r1] in coneByIndex prior (synthesis "sum" [] [2, 0] "Σ") == sortNub ("sum" : concatMap (coneByIndex prior) [r1, p2])
True

>>> let p1 = mkPost "tony" ["grok"] "hi" :: Post String; p2 = mkPost "grok" ["tony"] "hello"; r1 = replyTo "kimi" 1 p2 "a"; prior = [p2, p1, r1] in coneByIndex prior (synthesis "sum" [] [2, 0] "Σ")
["grok","kimi","sum","tony"]

Convenience wrapper: resolve cone from a chronological list, assigning ids [0..].

The shared append-only log, newest first.

The log is a stream of Posts. Common case: Log [Post]. Generalizing to any f with Cons and Uncons lets the same delivery machinery run over other stream representations while keeping the addressed read as a list.

Empty log.

Agent name on the shared log.

Agent: a Moore machine with free carrier, polymorphic in the base arrow.

System arr s (Mono a b) ≅ arr (s, a) (s, b) after collapsing unit positions. Common log case: Agent (->) s (Post a) [Post a] (input = one post, output = list of posts). Agent (K m) s a b is the monadic Moore machine.

State for a pure agent in delivery: free carrier plus an addressed inbox.

Empty carrier and empty inbox for the named agent.

Born empty, conses each received input onto its history.

>>> iterateSystem (tape length) [] [1,2,3 :: Int]
[1,2,3]

Like tape, but also conses the agent's own output onto its history.

This is the internal-monologue construction: an agent's outputs are on the same log as its percepts, visible to its own future turns.

Addressed stream of unread posts for one agent.

The Inbox owns a list of subscribed names and the unread stream. Only posts whose to list intersects the subscription list are peeled by unconsInbox. The common case is a singleton subscription [agentName]; multi-cast wires list several names.

Empty inbox for the subscribed agent(s).

Append a post to the right of the inbox.

Peel the oldest addressed post from the inbox, returning the rest.

Non-matching posts are skipped and discarded. An empty or exhausted inbox returns That with an empty inbox.

Primary owner of the inbox (head of the subscription list).

Full subscription list for the inbox.

Lightweight delivery predicate.

A post delivers when any of the subscribed names appears in the post's to list. Multi-cast is direct: a post addressed to several names reaches each subscriber. A post with to = ["all"] broadcasts to every subscriber; to = [] and to = [""] deliver to no one (discard). This predicate is a small stepping stone toward a relational copy/discard delivery model (FinRel); the full wiring is future work.

Opaque effectful ends: commit an a, emit a b.

Common log case: Shard m [Post] [Post]. Pipeline speaks a stream on commit and emit. Keyboard one-shot:

prefixIn (:[])  -- Post -> [Post] on the conjoint

Emit is an onslaught of posts (empty = quiet / done for that poll).

Same ends shape as Shard — dual seat on the log (journal 013).

Build a Shard from monadic commit and emit actions.

Build log ends (same as shard; dual seat).

State behind an agentShard: free carrier plus a pending emit queue.

Commit parses inputs into the carrier and enqueues one output list per input (the Moore step). Emit flushes the queue — empty means quiet.

Pure parse step: fold committed posts through the coalgebra.

Take the outbox; leave carrier unchanged.

Reinterpret a pure Agent as a list Shard.

agentShard get put sys  ::  Shard m [Post] [Post]

is the change of base from (->) (the Moore coalgebra) into K m ends: commit = parse inputs, emit = flush replies. The interior stays opaque at the Shard boundary — only [Post] in and out.

get / put hold the AgentSeat (e.g. IORef in IO, or State in tests). Example — reply agent over State:

let sys = tape (\hist -> (peek hist) { from = "j", to = [from (peek hist)], body = "ack: " <> body (peek hist) })
    sh  = agentShard get put sys  :: Shard (State (AgentSeat [Post])) [Post] [Post]
in  evalState (runK (close (conjoint sh) (companion sh)) [humanPost]) (AgentSeat [] [])

One closed turn of an agent-as-shard: commit ins, emit replies, new seat.

Pure form of close on agentShard without choosing a monad:

runAgentShard sys seat ins = runState (close (agentShard get put sys) ins) seat

Single-post ends: keyboard / one-out seat.

Obtained by buffering a list Shard on both sides, or by a bare queue (openSTM / openIO).

A tool call from an agent is just a Post: the to list names the tool, body carries the arguments. No extra type — emit that Post on a Port (or post it on the log for the tool agent to watch).

Stream algebra: construct a stream by appending one token on the right.

This is the right-handed dual of Uncons.

Snoc a Post onto a post stream. Specialized alias for snoc.

Ends s f: commit snocs a token; emit flushes the whole stream (parser takeRest — drain policy is "the stream", not a count).

get / put hold the stream buffer.

Ends f s: commit appends a stream; emit peels one token (parser next / uncons). Empty stream is quiet — the buffer is left empty and the returned token is undefined because the polymorphic token type has no empty value. In practice the list Shard layer ensures quiet periods are represented by an empty stream, so this case should not be reached.

get / put hold the stream buffer.

Token seat around a list Shard: buffer on both ends via stream coalgebra.

portShard getIn putIn getOut putOut sh
  = batchEnds getIn putIn >:> sh >:> unbatchEnds getOut putOut

Flush/drain is not a separate policy knob — it is build-stream (snoc) and peel-stream (uncons), the same syntax as parsers over [s].

Read end of the log: all posts matching any subscription, oldest first.

Traversal is newest-to-oldest; matching posts are prepended, so the accumulator is already oldest-first.

Write end of the log: commit a post.

turn with the agent identity taken from the inbox's first subscription.

For single-subscription inboxes this is the agent's own name; for multi-subscription inboxes use turnAs.

One delivery round: peel one addressed post, step the machine, post each output.

The AgentState carries the free carrier s and an addressed inbox. Only one post is consumed per call; repeated calls drain the inbox. Outputs are committed newest-first via post. When a post is processed, the returned Derivation records the agent name, the input post, and the emitted outputs.

turnAs lets the caller supply the agent identity used in the derivation; this matters when an inbox has multiple subscriptions (card-addressing) and the first subscription is not the agent's own name.

Whether the agent's inbox has an addressed post waiting.

Round-robin turn-loop until no agent has pending deliveries (quiescence).

Roster order is the schedule. Each pass runs turn for every agent that still has pending work at its slot. Passes repeat until a pass starts with nobody pending. Carriers start empty for every name.

Multi-seat-card variant of loop: each agent carries its own subscription list, so several agents can share a card name.

Resumable loop: supply the initial states and inboxes.

Implemented as an Either trace over the roster: each pass is one iteration of the feedback channel, quiescence returns a Right result.

Backwards-compatible wrapper; for explicit subscriptions use loopWithSubs.

Multi-seat-card variant of loopWith.

Transitive unfolding of a meeting.

Each element is one state of the round-robin schedule. Divergence becomes observable (the list is infinite) and loop is simply the last quiescent element. The third component collects one Derivation for every post that was processed by turn across the schedule.

Backwards-compatible wrapper; for explicit subscriptions use loopsSubs.

Multi-seat-card variant of loops.

Resumable loop with a heterogeneous roster: each agent supplies its own initial carrier, while inboxes are still seeded from the shared log.

Backwards-compatible wrapper; for explicit subscriptions use loopHeteroSubs.

Multi-seat-card variant of loopHetero.

The same meeting as a Trace value: yank body over the Either tensor, quiescence returned as a Right payload.

Backwards-compatible wrapper; for explicit subscriptions use meetingLoopSubs.

Multi-seat-card variant of meetingLoop.

Empty carrier and an inbox seeded from the log for the subscribed agent(s).

A roster entry with explicit subscriptions: agent name, subscription names, and the agent itself. The subscription list is the set of names whose posts the agent's inbox should receive; the agent's own name need not be in it.

A node in the meeting's derivation tree.

dChildren is kept flat (empty) in this pass. Building the causal child tree from routed outputs is future work.

Per-agent session assembly: the bodies an agent actually sees.

Run a monomial system for one step.

Consume i, then extract the output from the successor state (Process / iterateSystem timing).

Lift a pure agent into the K arrow of any functor.

This is the change of base from (->) to K m on the agent itself: the same Moore coalgebra, but each step now lives in m.

Run one step of a monadic agent.

STM agent: state is handled transparently inside an STM transaction.

IO agent: the STM boundary has been crossed; state is no longer transparently handled.

Cross from the transparent STM world into the IO boundary.

Seat-level product / await in STM.

Seat-level coproduct / race in STM.

Temporal race under IO: run both branches concurrently, return the first branch to emit a non-empty output, and cancel the loser. If the first branch to finish emits nothing, wait for the other branch. If both emit nothing, the right branch's (empty) result is returned.

This is the honest K-IO refinement of raceS: the winner is whichever step produces a mark first, not the left-biased deterministic rule.

Run one step of an STM agent.

Fold an STM agent over a bundle of inputs within one transaction.

This is the bundle-at-a-time step: one frame consumes a whole [a] and produces the concatenated replies. Factor of runAgentS that stays in STM so it can sit inside a larger transaction (e.g. a self-loop frame).

Run an STM agent over a list of inputs, crossing into IO at the boundary.

Read one token from an STM pole.

Write one token to an STM pole.

Wire an STM agent between an inbox and an outbox, running until quiescence. Quiescence is detected via orElse: if the inbox is empty (retry), the loop returns the current state.

Self-loop: the agent reads from and writes to the same STM end.

Wire an STM agent between an inbox and an outbox, running until quiescence, expressed as a 'Trace Either' value.

Self-loop as a 'Trace Either' citizen.

A bag: finite multiset. Order is forgotten; multiplicity is kept.

Log algebra: a sequence of bags, one bag per turn.

The empty bag.

One element.

Insert one element.

Fold a list into a bag, forgetting order.

Expand a bag into a list in some deterministic order.

Agent behaviour: a pure function from an input stream to an output stream.

Each input post is stepped through the agent; the per-step output lists are concatenated into a single output stream. This is the stream semantics of the Moore coalgebra, independent of any effectful boundary.

Run an agent from an initial carrier to obtain its Behaviour.

State after consuming a list of inputs.

Conditional agent: branch between two agents based on the current state.

This is a level-1 grammar fragment: the carrier can carry a mode, and the agent dispatches to one of two Moore machines depending on that mode. The predicate is evaluated on the carrier before the input is consumed, which is the honest Moore shape: output is a function of state, and the chosen branch's update function determines the next state.

Seat-level product / await: both agents run on the same input; states are paired; emits are concatenated left-to-right.

Seat-level coproduct / race: both agents run on the same input; states are paired; the left emit wins if non-empty, otherwise the right emit wins.

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.

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.

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

How messages are queued between producer and consumer.

A channel policy names the residual mediator that governs an effectful channel. This is the Track-B relocation of the old Queue annotation: the policy is a value passed at allocation time, not a field of the channel type. The constructors match the ?-modality vocabulary from the B0 spike; Linear is the empty-residual default and the only policy on which halt marks are safe.

Open a channel policy as IO Poles.

Open a channel policy as STM Poles.

Open a linear channel as IO Poles.

Linear is the default policy: unbounded FIFO, empty residual, preserves every token in order. This is the effectful face of a linear process.

Open a linear channel as STM Poles.

A channel statically known to be linear.

The index p :: ChannelPolicy a is checked by IsLinear at construction time. Attempting to build a HaltChannel with a non-linear policy fails to typecheck.

Type-level witness that a channel policy is linear.

Only Linear is allowed to carry halt marks; any other policy produces a compile-time type error.

Open a halt-mark channel. This is openLinearChannelSTM with a type-level certificate.

Write a token to a halt-mark channel.

Read a token from a halt-mark channel.

Open a queue strategy as STM Poles.

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.

Open a queue strategy as IO Poles.

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.

Honest sequential composition of two allocated ends via an intermediate queue and a pump.

pipeEnds e1 makeE2 allocates a queue of b values, builds the right end around that queue with makeE2, and starts a pump that moves values from e1 into the right end. The returned Poles uses e1 for input and the built right end for output; the close action cancels the pump.

This is the coend-style composition that composePoles cannot express: the intermediate carrier is a real queue (the residual's home) rather than the unit type, so a multi-read consumer can accumulate inputs before emitting.

Adapt a shard on the commit side (contravariant).

Transform the input before it is committed. One common use is session assembly: prefixShard session changes the payload that the shard posts.

Adapt a shard on the emit side (covariant).

Transform the output after it is emitted. One common use is a transport envelope: suffixShard (map addHeader) decorates every emitted post.

Adapt both sides of a shard at once.

codecShard f g = prefixShard f . suffixShard g.

Sequential composition of shards.

The output of the first shard feeds the input of the second. This is the same shape as connecting two effectful agents in series.

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