| Safe Haskell | None |
|---|---|
| Language | GHC2024 |
Free.Agent.Diagram
Description
A monomial System is a lens from its state interface
(systemAsLens: System s p ≅ Poly(S y^S, p)), and box lifts such a
lens into the string-diagram DSL. The result runs one Moore step per
runDiagram call: the forward wire carries state → output, the backward
wire carries input-direction → next state.
Stage 1b: the bend, at the Process layer. A stateful agent decomposes
as a stateless body plus cross-tick feedback: register closes the
state wire with delay making the one-tick lag observable (sound for
strict state, where the lazy cartesian knot would diverge). So:
agent = box + bend + delay ≡ mooreProcess sys s0 = register s0 body
What is still missing is the same wiring inside the
StringDiagram surface itself (a delay box and a trace
combinator over a Process base); the oracles pin the semantics the
surface will need to reproduce.
Stage 2: meetingSkeleton reads a conversation back as a drawing —
the unification claim that the log records the wiring. Stage 2b draws
the full post-DAG: forks and syntheses are visible copy/merge spiders,
routed with SSwap-built permutations.
Synopsis
- agentDiagram :: System (->) s (Mono i o) -> Diagram s s o i
- diagramStep :: System (->) s (Mono i o) -> s -> i -> (s, o)
- diagramSteps :: System (->) s (Mono i o) -> s -> [i] -> [o]
- liftProcess :: (a -> b) -> Process a b
- mooreBody :: System (->) s (Mono i o) -> Process (i, s) (o, s)
- mooreProcess :: System (->) s (Mono i o) -> s -> Process i o
- meetingSkeleton :: [Post a] -> SDiagram
- skeletonLabels :: SDiagram -> [String]
Documentation
agentDiagram :: System (->) s (Mono i o) -> Diagram s s o i Source #
A monomial system as a one-box diagram.
box . systemAsLens: forward wire s → o (state to output), backward
wire i → s (input direction to next state).
diagramStep :: System (->) s (Mono i o) -> s -> i -> (s, o) Source #
One Moore step as a diagram run: (next state, output at current
state). Definitionally (snd (runSystemMono sys s) i, fst (runSystemMono
sys s)) — the oracle pins exactly this.
diagramSteps :: System (->) s (Mono i o) -> s -> [i] -> [o] Source #
Iterate a system over inputs through the diagram, mirroring
iterateSystem (which emits the output of the state after each
transition). Each step runs the diagram twice with the same input: once
to consume (state transition), once to observe (output at the new
state). The backward pass is pure, so the second run is harmless — and
both passes go through runDiagram, so the oracle exercises the bridge
end to end.
liftProcess :: (a -> b) -> Process a b Source #
Lift a pure function to a stateless Process (the box a bend closes).
mooreBody :: System (->) s (Mono i o) -> Process (i, s) (o, s) Source #
The stateless body of a system as a Process: consume the input
(state transition), then read the output of the new state, and emit the
new state on the feedback wire. This matches iterateSystem /
systemAsProcess semantics: the output is read after consuming the
input.
meetingSkeleton :: [Post a] -> SDiagram Source #
The drawing skeleton of a conversation: each post is a box labelled by
its sender, wired by its thread ancestry — "the log is the diagram of
the meeting that produced it". A root is SBox label 0 1 (nothing
feeds it), a reply SBox label 1 1, and a synthesis with m parents is
preceded by a visible merge spider (SSpider m 1); a post cited as
parent by k > 1 later posts forks its output through a visible copy
spider (SSpider 1 k).
One pass over the log, oldest first: the state is the list of live wire
ends (each tagged by the thread edge it feeds, or by the post whose
uncited output it carries to the boundary), and each post emits one
layer — permute the parent wires to the back (adjacent SSwaps), merge,
box, fork. A dangling thread edge (parent not in the log) becomes a
free input wire, present from the left boundary.
skeletonLabels :: SDiagram -> [String] Source #
The box labels of a skeleton, in composition order.