{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

-- | A Moore machine fibered over a polynomial interface @p@.
--
-- @
--   newtype SystemT t arr s p = SystemT (Body t s arr (Dir p) (Pos p))
-- @
--
-- * The base is the state @s@.
-- * The fiber/interface is the polynomial @p@, with positions 'Pos' p and
--   directions 'Dir' p.
-- * The span shape is @s <- (s, Dir p) -> Pos p@.
-- * "Moore" because the observable output 'Pos' p depends on the state @s@,
--   not directly on the current input direction. The direction is consumed to
--   compute the next state; then the position is read from that state.
--
-- For a monomial @Mono i o@:
--
-- @
--   Dir (Mono i o) = i
--   Pos (Mono i o) = o
-- @
--
-- so @System (->) s (Mono i o)@ collapses to the ordinary Moore body
-- @(s, i) -> (s, o)@. The 'mooreSystem' constructor makes this explicit:
-- it takes a transition @s -> a -> s@ and an observation @s -> b@, then
-- packages them as a 'Circuit.Body.Body'.
--
-- For a general polynomial @p@, 'Pos' p and 'Dir' p can be branching: the
-- polynomial layer handles sums and products of interfaces, so 'System' is a
-- Moore machine that can branch, offer choices, or run parallel interfaces,
-- all while 'Circuit.Body.Body' handles the state transition.
--
-- In the BLLL picture (Katis–Sabadini–Walters), an F-Moore machine is an
-- F-algebra @F E -> E@ plus an output @E -> O@. 'System' fits this with
-- state object @E = s@, endofunctor @F = (-) ⊗ Dir p@, transition
-- @d : s ⊗ Dir p -> s@, and output @obs : s -> Pos p@ bundled with the
-- transition in the 'Circuit.Body.Body'.
--
-- 'Circuit.Process.Process' is the pointed monomial special case: where
-- @Process@ is the existential form @∃s. (s, s -> a -> s, s -> b)@, 'System'
-- is the polynomial-lens form of the same idea, with @p@ describing the
-- interactive interface.
--
-- This module defines the system type, conversions between eval and arrow
-- forms, wiring combinators, and higher-level execution combinators.
module Circuit.System
  ( -- * Systems
    SystemT (..),
    System,
    system,
    runSystem,
    mooreSystem,

    -- * Eval / arrow conversion
    SystemEval (..),
    fromEvalSystem,
    toEvalSystem,
    step,

    -- * Monomial helpers
    monoDir,
    monoIn,

    -- * Tensor wiring
    parWiring,

    -- * Channel-pole view of systems
    SomePoles (..),
    runSomePoles,
    systemToPolesWithProbe,
    systemWithSeedToPoles,

    -- * Running monomial systems
    runSystemMono,

    -- * Lenses
    systemAsLens,
    lensAsSystem,
    duplicateSystem,

    -- * Branches
    branchSystem,
    runSystemSum,
    branchSystemHet,
    runSystemSumHet,
    SumStep (..),

    -- * Coalgebras
    Coalgebra (..),
    Step,
    coalgebraToSystem,
    composeCoalgebra,
    systemToCoalgebraMono,
  )
where

import Circuit.Body (Body (..))
import Circuit.Category ((.>))
import Circuit.Poles (HasDual (..), Poles (..))
import Circuit.Poles qualified as Poles
import Circuit.Poly
  ( Dir,
    Eval (..),
    Mono,
    Morphism (..),
    Netlist,
    Poly (..),
    Pos,
    applyLens,
    lens,
    nestedToComp,
    runMorphism,
  )
import Control.Category (id, (.))
import Data.Bifunctor
import Data.Kind (Type)
import Data.Void (Void, absurd)
import Prelude hiding (id, (.))

-- $setup
-- >>> import Circuit.Poly (Eval (..), Mono, Morphism, lens, applyLens)
-- >>> import Circuit.System (System, system, runSystem, mooreSystem, SystemEval (..), toEvalSystem, fromEvalSystem, monoDir, monoIn, parWiring)

-- | 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.
newtype SystemT (t :: Type -> Type -> Type) (arr :: Type -> Type -> Type) s (p :: Poly)
  = SystemT (Body t s arr (Dir p) (Pos p))

-- | Cartesian systems: the state-pairing tensor is @(,)@.
type System = SystemT (,)

-- | Construct a cartesian 'System' from its underlying arrow.
system :: arr (s, Dir p) (s, Pos p) -> System arr s p
system :: forall (arr :: * -> * -> *) s (p :: Poly).
arr (s, Dir p) (s, Pos p) -> System arr s p
system = Body (,) s arr (Dir p) (Pos p) -> System arr s p
forall (t :: * -> * -> *) (arr :: * -> * -> *) s (p :: Poly).
Body t s arr (Dir p) (Pos p) -> SystemT t arr s p
SystemT (Body (,) s arr (Dir p) (Pos p) -> System arr s p)
-> (arr (s, Dir p) (s, Pos p) -> Body (,) s arr (Dir p) (Pos p))
-> arr (s, Dir p) (s, Pos p)
-> System arr s p
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. arr (s, Dir p) (s, Pos p) -> Body (,) s arr (Dir p) (Pos p)
forall {k} {k1} {k2} (t :: k -> k1 -> k2) (ch :: k)
       (arr :: k2 -> k2 -> *) (a :: k1) (b :: k1).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body

-- | Inspect a cartesian 'System' as its underlying arrow.
runSystem :: System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem :: forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem (SystemT (Body arr (s, Dir p) (s, Pos p)
f)) = arr (s, Dir p) (s, Pos p)
f

-- | 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 'Circuit.Process.systemToProcess').
mooreSystem :: (s -> a -> s) -> (s -> b) -> System (->) s (Mono a b)
mooreSystem :: forall s a b. (s -> a -> s) -> (s -> b) -> System (->) s (Mono a b)
mooreSystem s -> a -> s
st s -> b
ex =
  ((s, Dir (Mono a b)) -> (s, Pos (Mono a b)))
-> System (->) s (Mono a b)
forall (arr :: * -> * -> *) s (p :: Poly).
arr (s, Dir p) (s, Pos p) -> System arr s p
system (((s, Dir (Mono a b)) -> (s, Pos (Mono a b)))
 -> System (->) s (Mono a b))
-> ((s, Dir (Mono a b)) -> (s, Pos (Mono a b)))
-> System (->) s (Mono a b)
forall a b. (a -> b) -> a -> b
$ \case
    (s
_, Left Void
v) -> Void -> (s, (b, ()))
forall a. Void -> a
absurd Void
v
    (s
s, Right a
a) ->
      let s' :: s
s' = s -> a -> s
st s
s a
a
       in (s
s', (s -> b
ex s
s', ()))

-- | Extract the monomial direction from its 'Either Void' encoding.
monoDir :: Dir (Mono i o) -> i
monoDir :: forall i o. Dir (Mono i o) -> i
monoDir (Right i
i) = i
i
monoDir (Left Void
v) = Void -> i
forall a. Void -> a
absurd Void
v

-- | Inject a monomial direction into its 'Either Void' encoding.
monoIn :: i -> Dir (Mono i o)
monoIn :: forall i o. i -> Dir (Mono i o)
monoIn = i -> Either Void i
i -> Dir ('Prod ('Const o) ('Exp i))
forall a b. b -> Either a b
Right

-- | Convert an eval-form @(->)@ system into the arrow form.
fromEvalSystem :: (SystemEval p) => (s -> Eval p s) -> System (->) s p
fromEvalSystem :: forall (p :: Poly) s.
SystemEval p =>
(s -> Eval p s) -> System (->) s p
fromEvalSystem s -> Eval p s
f = ((s, Dir p) -> (s, Pos p)) -> System (->) s p
forall (arr :: * -> * -> *) s (p :: Poly).
arr (s, Dir p) (s, Pos p) -> System arr s p
system (((s, Dir p) -> (s, Pos p)) -> System (->) s p)
-> ((s, Dir p) -> (s, Pos p)) -> System (->) s p
forall a b. (a -> b) -> a -> b
$ \(s
s, Dir p
d) ->
  let (Pos p
pos, Dir p -> s
next) = Eval p s -> (Pos p, Dir p -> s)
forall x. Eval p x -> (Pos p, Dir p -> x)
forall (p :: Poly) x.
SystemEval p =>
Eval p x -> (Pos p, Dir p -> x)
evalToSystem (s -> Eval p s
f s
s)
   in (Dir p -> s
next Dir p
d, Pos p
pos)

-- | 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.
toEvalSystem :: forall p s. (SystemEval p) => System (->) s p -> s -> Eval p s
toEvalSystem :: forall (p :: Poly) s.
SystemEval p =>
System (->) s p -> s -> Eval p s
toEvalSystem System (->) s p
sys s
s = Pos p -> (Dir p -> s) -> Eval p s
forall x. Pos p -> (Dir p -> x) -> Eval p x
forall (p :: Poly) x.
SystemEval p =>
Pos p -> (Dir p -> x) -> Eval p x
evalFromSystem Pos p
pos (\Dir p
d -> (s, Pos p) -> s
forall a b. (a, b) -> a
fst (System (->) s p -> (s, Dir p) -> (s, Pos p)
forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem System (->) s p
sys (s
s, Dir p
d)))
  where
    pos :: Pos p
pos = (s, Pos p) -> Pos p
forall a b. (a, b) -> b
snd (System (->) s p -> (s, Dir p) -> (s, Pos p)
forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem System (->) s p
sys (s
s, forall (p :: Poly). SystemEval p => Dir p
probeDir @p))

-- | Run one step: observe the current @p@-output from state @s@.
step :: (SystemEval p) => System (->) s p -> s -> Eval p s
step :: forall (p :: Poly) s.
SystemEval p =>
System (->) s p -> s -> Eval p s
step = System (->) s p -> s -> Eval p s
forall (p :: Poly) s.
SystemEval p =>
System (->) s p -> s -> Eval p s
toEvalSystem

-- | Helpers for translating between the 'Eval' presentation and the arrow
-- presentation of a @(->)@ system.  These extend the netlist view to 'Sum'.
class SystemEval (p :: Poly) where
  evalToSystem :: Eval p x -> (Pos p, Dir p -> x)
  evalFromSystem :: Pos p -> (Dir p -> x) -> Eval p x
  probeDir :: Dir p

instance SystemEval 'Y where
  evalToSystem :: forall x. Eval 'Y x -> (Pos 'Y, Dir 'Y -> x)
evalToSystem (EY x
x) = ((), \() -> x
x)
  evalFromSystem :: forall x. Pos 'Y -> (Dir 'Y -> x) -> Eval 'Y x
evalFromSystem () Dir 'Y -> x
k = x -> Eval 'Y x
forall x. x -> Eval 'Y x
EY (Dir 'Y -> x
k ())
  probeDir :: Dir 'Y
probeDir = ()

instance SystemEval ('Const a) where
  evalToSystem :: forall x.
Eval ('Const a) x -> (Pos ('Const a), Dir ('Const a) -> x)
evalToSystem (EK c
c) = (c
Pos ('Const a)
c, Void -> x
Dir ('Const a) -> x
forall a. Void -> a
absurd)
  evalFromSystem :: forall x.
Pos ('Const a) -> (Dir ('Const a) -> x) -> Eval ('Const a) x
evalFromSystem Pos ('Const a)
c Dir ('Const a) -> x
_ = a -> Eval ('Const a) x
forall c x. c -> Eval ('Const c) x
EK a
Pos ('Const a)
c
  probeDir :: Dir ('Const a)
probeDir = [Char] -> Void
forall a. HasCallStack => [Char] -> a
error [Char]
"probeDir Const"

instance SystemEval ('Exp a) where
  evalToSystem :: forall x. Eval ('Exp a) x -> (Pos ('Exp a), Dir ('Exp a) -> x)
evalToSystem (EE a -> x
f) = ((), a -> x
Dir ('Exp a) -> x
f)
  evalFromSystem :: forall x. Pos ('Exp a) -> (Dir ('Exp a) -> x) -> Eval ('Exp a) x
evalFromSystem () = (a -> x) -> Eval ('Exp a) x
(Dir ('Exp a) -> x) -> Eval ('Exp a) x
forall a x. (a -> x) -> Eval ('Exp a) x
EE
  probeDir :: Dir ('Exp a)
probeDir = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"probeDir Exp"

instance (SystemEval p, SystemEval q) => SystemEval ('Sum p q) where
  evalToSystem :: forall x.
Eval ('Sum p q) x -> (Pos ('Sum p q), Dir ('Sum p q) -> x)
evalToSystem (ES (Left Eval p1 x
v)) =
    let (Pos p1
i, Dir p1 -> x
f) = Eval p1 x -> (Pos p1, Dir p1 -> x)
forall x. Eval p1 x -> (Pos p1, Dir p1 -> x)
forall (p :: Poly) x.
SystemEval p =>
Eval p x -> (Pos p, Dir p -> x)
evalToSystem Eval p1 x
v
     in (Pos p -> Either (Pos p) (Pos q)
forall a b. a -> Either a b
Left Pos p
Pos p1
i, (Dir p -> x) -> (Dir q -> x) -> Either (Dir p) (Dir q) -> x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Dir p -> x
Dir p1 -> x
f (x -> Dir q -> x
forall a b. a -> b -> a
const x
forall a. a
offFibre))
  evalToSystem (ES (Right Eval q x
w)) =
    let (Pos q
j, Dir q -> x
g) = Eval q x -> (Pos q, Dir q -> x)
forall x. Eval q x -> (Pos q, Dir q -> x)
forall (p :: Poly) x.
SystemEval p =>
Eval p x -> (Pos p, Dir p -> x)
evalToSystem Eval q x
w
     in (Pos q -> Either (Pos p) (Pos q)
forall a b. b -> Either a b
Right Pos q
Pos q
j, (Dir p -> x) -> (Dir q -> x) -> Either (Dir p) (Dir q) -> x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (x -> Dir p -> x
forall a b. a -> b -> a
const x
forall a. a
offFibre) Dir q -> x
Dir q -> x
g)
  evalFromSystem :: forall x.
Pos ('Sum p q) -> (Dir ('Sum p q) -> x) -> Eval ('Sum p q) x
evalFromSystem (Left Pos p
i) Dir ('Sum p q) -> x
k = Either (Eval p x) (Eval q x) -> Eval ('Sum p q) x
forall (p1 :: Poly) x (q :: Poly).
Either (Eval p1 x) (Eval q x) -> Eval ('Sum p1 q) x
ES (Eval p x -> Either (Eval p x) (Eval q x)
forall a b. a -> Either a b
Left (Pos p -> (Dir p -> x) -> Eval p x
forall x. Pos p -> (Dir p -> x) -> Eval p x
forall (p :: Poly) x.
SystemEval p =>
Pos p -> (Dir p -> x) -> Eval p x
evalFromSystem Pos p
i (Either (Dir p) (Dir q) -> x
Dir ('Sum p q) -> x
k (Either (Dir p) (Dir q) -> x)
-> (Dir p -> Either (Dir p) (Dir q)) -> Dir p -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Dir p -> Either (Dir p) (Dir q)
forall a b. a -> Either a b
Left)))
  evalFromSystem (Right Pos q
j) Dir ('Sum p q) -> x
k = Either (Eval p x) (Eval q x) -> Eval ('Sum p q) x
forall (p1 :: Poly) x (q :: Poly).
Either (Eval p1 x) (Eval q x) -> Eval ('Sum p1 q) x
ES (Eval q x -> Either (Eval p x) (Eval q x)
forall a b. b -> Either a b
Right (Pos q -> (Dir q -> x) -> Eval q x
forall x. Pos q -> (Dir q -> x) -> Eval q x
forall (p :: Poly) x.
SystemEval p =>
Pos p -> (Dir p -> x) -> Eval p x
evalFromSystem Pos q
j (Either (Dir p) (Dir q) -> x
Dir ('Sum p q) -> x
k (Either (Dir p) (Dir q) -> x)
-> (Dir q -> Either (Dir p) (Dir q)) -> Dir q -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Dir q -> Either (Dir p) (Dir q)
forall a b. b -> Either a b
Right)))
  probeDir :: Dir ('Sum p q)
  probeDir :: Dir ('Sum p q)
probeDir = Dir p -> Either (Dir p) (Dir q)
forall a b. a -> Either a b
Left (forall (p :: Poly). SystemEval p => Dir p
probeDir @p)

instance (SystemEval p, SystemEval q) => SystemEval ('Prod p q) where
  evalToSystem :: forall x.
Eval ('Prod p q) x -> (Pos ('Prod p q), Dir ('Prod p q) -> x)
evalToSystem (EP (Eval p1 x
u, Eval q x
v)) =
    let (Pos p1
i, Dir p1 -> x
f) = Eval p1 x -> (Pos p1, Dir p1 -> x)
forall x. Eval p1 x -> (Pos p1, Dir p1 -> x)
forall (p :: Poly) x.
SystemEval p =>
Eval p x -> (Pos p, Dir p -> x)
evalToSystem Eval p1 x
u
        (Pos q
j, Dir q -> x
g) = Eval q x -> (Pos q, Dir q -> x)
forall x. Eval q x -> (Pos q, Dir q -> x)
forall (p :: Poly) x.
SystemEval p =>
Eval p x -> (Pos p, Dir p -> x)
evalToSystem Eval q x
v
     in ((Pos p
Pos p1
i, Pos q
Pos q
j), (Dir p -> x) -> (Dir q -> x) -> Either (Dir p) (Dir q) -> x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Dir p -> x
Dir p1 -> x
f Dir q -> x
Dir q -> x
g)
  evalFromSystem :: forall x.
Pos ('Prod p q) -> (Dir ('Prod p q) -> x) -> Eval ('Prod p q) x
evalFromSystem (Pos p
i, Pos q
j) Dir ('Prod p q) -> x
k =
    (Eval p x, Eval q x) -> Eval ('Prod p q) x
forall (p1 :: Poly) x (q :: Poly).
(Eval p1 x, Eval q x) -> Eval ('Prod p1 q) x
EP (Pos p -> (Dir p -> x) -> Eval p x
forall x. Pos p -> (Dir p -> x) -> Eval p x
forall (p :: Poly) x.
SystemEval p =>
Pos p -> (Dir p -> x) -> Eval p x
evalFromSystem Pos p
i (Either (Dir p) (Dir q) -> x
Dir ('Prod p q) -> x
k (Either (Dir p) (Dir q) -> x)
-> (Dir p -> Either (Dir p) (Dir q)) -> Dir p -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Dir p -> Either (Dir p) (Dir q)
forall a b. a -> Either a b
Left), Pos q -> (Dir q -> x) -> Eval q x
forall x. Pos q -> (Dir q -> x) -> Eval q x
forall (p :: Poly) x.
SystemEval p =>
Pos p -> (Dir p -> x) -> Eval p x
evalFromSystem Pos q
j (Either (Dir p) (Dir q) -> x
Dir ('Prod p q) -> x
k (Either (Dir p) (Dir q) -> x)
-> (Dir q -> Either (Dir p) (Dir q)) -> Dir q -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Dir q -> Either (Dir p) (Dir q)
forall a b. b -> Either a b
Right))
  probeDir :: Dir ('Prod p q)
  probeDir :: Dir ('Prod p q)
probeDir = Dir p -> Either (Dir p) (Dir q)
forall a b. a -> Either a b
Left (forall (p :: Poly). SystemEval p => Dir p
probeDir @p)

instance (SystemEval p, SystemEval q) => SystemEval ('Tensor p q) where
  evalToSystem :: forall x.
Eval ('Tensor p q) x -> (Pos ('Tensor p q), Dir ('Tensor p q) -> x)
evalToSystem (ET (Pos p1, Pos q)
pos (Dir p1, Dir q) -> x
f) = ((Pos p1, Pos q)
Pos ('Tensor p q)
pos, (Dir p1, Dir q) -> x
Dir ('Tensor p q) -> x
f)
  evalFromSystem :: forall x.
Pos ('Tensor p q)
-> (Dir ('Tensor p q) -> x) -> Eval ('Tensor p q) x
evalFromSystem = (Pos p, Pos q) -> ((Dir p, Dir q) -> x) -> Eval ('Tensor p q) x
Pos ('Tensor p q)
-> (Dir ('Tensor p q) -> x) -> Eval ('Tensor p q) x
forall (p1 :: Poly) (q :: Poly) x.
(Pos p1, Pos q) -> ((Dir p1, Dir q) -> x) -> Eval ('Tensor p1 q) x
ET
  probeDir :: Dir ('Tensor p q)
  probeDir :: Dir ('Tensor p q)
probeDir = (forall (p :: Poly). SystemEval p => Dir p
probeDir @p, forall (p :: Poly). SystemEval p => Dir p
probeDir @q)

instance (SystemEval p, SystemEval q) => SystemEval ('Comp p q) where
  evalToSystem :: forall x.
Eval ('Comp p q) x -> (Pos ('Comp p q), Dir ('Comp p q) -> x)
evalToSystem (EC (Pos p1, Dir p1 -> Pos q)
pos (Dir p1, Dir q) -> x
f) = ((Pos p1, Dir p1 -> Pos q)
Pos ('Comp p q)
pos, (Dir p1, Dir q) -> x
Dir ('Comp p q) -> x
f)
  evalFromSystem :: forall x.
Pos ('Comp p q) -> (Dir ('Comp p q) -> x) -> Eval ('Comp p q) x
evalFromSystem = (Pos p, Dir p -> Pos q)
-> ((Dir p, Dir q) -> x) -> Eval ('Comp p q) x
Pos ('Comp p q) -> (Dir ('Comp p q) -> x) -> Eval ('Comp p q) x
forall (p1 :: Poly) (q :: Poly) x.
(Pos p1, Dir p1 -> Pos q)
-> ((Dir p1, Dir q) -> x) -> Eval ('Comp p1 q) x
EC
  probeDir :: Dir ('Comp p q)
  probeDir :: Dir ('Comp p q)
probeDir = (forall (p :: Poly). SystemEval p => Dir p
probeDir @p, forall (p :: Poly). SystemEval p => Dir p
probeDir @q)

offFibre :: a
offFibre :: forall a. a
offFibre = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"off-fibre direction"

-- | 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).
parWiring :: System (->) s p -> System (->) t q -> System (->) (s, t) (Tensor p q)
parWiring :: forall s (p :: Poly) t (q :: Poly).
System (->) s p
-> System (->) t q -> System (->) (s, t) ('Tensor p q)
parWiring System (->) s p
sp System (->) t q
sq =
  (((s, t), Dir ('Tensor p q)) -> ((s, t), Pos ('Tensor p q)))
-> System (->) (s, t) ('Tensor p q)
forall (arr :: * -> * -> *) s (p :: Poly).
arr (s, Dir p) (s, Pos p) -> System arr s p
system ((((s, t), Dir ('Tensor p q)) -> ((s, t), Pos ('Tensor p q)))
 -> System (->) (s, t) ('Tensor p q))
-> (((s, t), Dir ('Tensor p q)) -> ((s, t), Pos ('Tensor p q)))
-> System (->) (s, t) ('Tensor p q)
forall a b. (a -> b) -> a -> b
$ \((s
s, t
t), (Dir p
dp, Dir q
dq)) ->
    let (s
s', Pos p
posP) = System (->) s p -> (s, Dir p) -> (s, Pos p)
forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem System (->) s p
sp (s
s, Dir p
dp)
        (t
t', Pos q
posQ) = System (->) t q -> (t, Dir q) -> (t, Pos q)
forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem System (->) t q
sq (t
t, Dir q
dq)
     in ((s
s', t
t'), (Pos p
posP, Pos q
posQ))

-- * Channel-pole view of systems

-- | An existentially-quantified pair of channel poles over a body, carrying
-- its seed. The shape mirrors 'Circuit.Body.SomeBody'.
data SomePoles t arr a b where
  SomePoles :: s -> Poles (Body t s arr) a b -> SomePoles t arr a b

-- | 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.
runSomePoles :: SomePoles (,) (->) a b -> [a] -> [b]
runSomePoles :: forall a b. SomePoles (,) (->) a b -> [a] -> [b]
runSomePoles (SomePoles s
s0 Poles (Body (,) s (->)) a b
p) [a]
xs =
  let (Body (,) s (->) a ()
write, Body (,) s (->) () b
receive) = Poles (Body (,) s (->)) a b
-> (Body (,) s (->) a (), Body (,) s (->) () b)
forall (arr :: * -> * -> *) a b.
HasDual () arr =>
Poles arr a b -> (arr a (), arr () b)
Poles.splay0 Poles (Body (,) s (->)) a b
p
      Body (s, a) -> (s, b)
f = Body (,) s (->) a ()
write Body (,) s (->) a () -> Body (,) s (->) () b -> Body (,) s (->) a b
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> Body (,) s (->) () b
receive
      (s
_, [b]
bs) = ((s, [b]) -> a -> (s, [b])) -> (s, [b]) -> [a] -> (s, [b])
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\(s
s, [b]
acc) a
a -> let (s
s', b
b) = (s, a) -> (s, b)
f (s
s, a
a) in (s
s', b
b b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [b]
acc)) (s
s0, []) [a]
xs
   in [b] -> [b]
forall a. [a] -> [a]
reverse [b]
bs

-- | Shared write pole for a @(->)@ system over @(,)@: run the step and discard
-- the output position.
systemWriteBody :: System (->) s p -> Body (,) s (->) (Dir p) ()
systemWriteBody :: forall s (p :: Poly). System (->) s p -> Body (,) s (->) (Dir p) ()
systemWriteBody System (->) s p
sys = ((s, Dir p) -> (s, ())) -> Body (,) s (->) (Dir p) ()
forall {k} {k1} {k2} (t :: k -> k1 -> k2) (ch :: k)
       (arr :: k2 -> k2 -> *) (a :: k1) (b :: k1).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body (((s, Dir p) -> (s, ())) -> Body (,) s (->) (Dir p) ())
-> ((s, Dir p) -> (s, ())) -> Body (,) s (->) (Dir p) ()
forall a b. (a -> b) -> a -> b
$ \(s
s, Dir p
d) -> ((s, Pos p) -> s
forall a b. (a, b) -> a
fst (System (->) s p -> (s, Dir p) -> (s, Pos p)
forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem System (->) s p
sys (s
s, Dir p
d)), ())

-- | 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'.
systemToPolesWithProbe :: Dir p -> System (->) s p -> Poles (Body (,) s (->)) (Dir p) (Pos p)
systemToPolesWithProbe :: forall (p :: Poly) s.
Dir p -> System (->) s p -> Poles (Body (,) s (->)) (Dir p) (Pos p)
systemToPolesWithProbe Dir p
probe System (->) s p
sys =
  Body (,) s (->) (Dir p) ()
-> Body (,) s (->) () (Pos p)
-> Poles (Body (,) s (->)) (Dir p) (Pos p)
forall (arr :: * -> * -> *) a b.
HasDual () arr =>
arr a () -> arr () b -> Poles arr a b
Poles.poles0
    (System (->) s p -> Body (,) s (->) (Dir p) ()
forall s (p :: Poly). System (->) s p -> Body (,) s (->) (Dir p) ()
systemWriteBody System (->) s p
sys)
    (((s, ()) -> (s, Pos p)) -> Body (,) s (->) () (Pos p)
forall {k} {k1} {k2} (t :: k -> k1 -> k2) (ch :: k)
       (arr :: k2 -> k2 -> *) (a :: k1) (b :: k1).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body (((s, ()) -> (s, Pos p)) -> Body (,) s (->) () (Pos p))
-> ((s, ()) -> (s, Pos p)) -> Body (,) s (->) () (Pos p)
forall a b. (a -> b) -> a -> b
$ \(s
s, ()) -> System (->) s p -> (s, Dir p) -> (s, Pos p)
forall (arr :: * -> * -> *) s (p :: Poly).
System arr s p -> arr (s, Dir p) (s, Pos p)
runSystem System (->) s p
sys (s
s, Dir p
probe))

-- | 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.
systemWithSeedToPoles :: s -> (s -> Pos p) -> System (->) s p -> SomePoles (,) (->) (Dir p) (Pos p)
systemWithSeedToPoles :: forall s (p :: Poly).
s
-> (s -> Pos p)
-> System (->) s p
-> SomePoles (,) (->) (Dir p) (Pos p)
systemWithSeedToPoles s
s0 s -> Pos p
ex System (->) s p
sys =
  s
-> Poles (Body (,) s (->)) (Dir p) (Pos p)
-> SomePoles (,) (->) (Dir p) (Pos p)
forall {k1} {k2} s (t :: * -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (a :: k1) (b :: k1).
s -> Poles (Body t s arr) a b -> SomePoles t arr a b
SomePoles s
s0 (Poles (Body (,) s (->)) (Dir p) (Pos p)
 -> SomePoles (,) (->) (Dir p) (Pos p))
-> Poles (Body (,) s (->)) (Dir p) (Pos p)
-> SomePoles (,) (->) (Dir p) (Pos p)
forall a b. (a -> b) -> a -> b
$
    Body (,) s (->) (Dir p) ()
-> Body (,) s (->) () (Pos p)
-> Poles (Body (,) s (->)) (Dir p) (Pos p)
forall (arr :: * -> * -> *) a b.
HasDual () arr =>
arr a () -> arr () b -> Poles arr a b
Poles.poles0
      (System (->) s p -> Body (,) s (->) (Dir p) ()
forall s (p :: Poly). System (->) s p -> Body (,) s (->) (Dir p) ()
systemWriteBody System (->) s p
sys)
      (((s, ()) -> (s, Pos p)) -> Body (,) s (->) () (Pos p)
forall {k} {k1} {k2} (t :: k -> k1 -> k2) (ch :: k)
       (arr :: k2 -> k2 -> *) (a :: k1) (b :: k1).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body (((s, ()) -> (s, Pos p)) -> Body (,) s (->) () (Pos p))
-> ((s, ()) -> (s, Pos p)) -> Body (,) s (->) () (Pos p)
forall a b. (a -> b) -> a -> b
$ \(s
s, ()) -> (s
s, s -> Pos p
ex s
s))

-- | Run a monomial @(->)@ system at a state, exposing the output position and
-- the state-transition function.
runSystemMono :: System (->) s (Mono i o) -> s -> (o, i -> s)
runSystemMono :: forall s i o. System (->) s (Mono i o) -> s -> (o, i -> s)
runSystemMono System (->) s (Mono i o)
sys s
s = case System (->) s (Mono i o) -> s -> Eval (Mono i o) s
forall (p :: Poly) s.
SystemEval p =>
System (->) s p -> s -> Eval p s
toEvalSystem System (->) s (Mono i o)
sys s
s of EP (EK c
o, EE a -> s
f) -> (o
c
o, i -> s
a -> s
f)

-- | 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)@.
systemAsLens :: System (->) s (Mono i o) -> Morphism (Mono s s) (Mono i o)
systemAsLens :: forall s i o.
System (->) s (Mono i o) -> Morphism (Mono s s) (Mono i o)
systemAsLens System (->) s (Mono i o)
sys = (s -> o) -> (s -> i -> s) -> Morphism (Mono s s) (Mono i o)
forall a b db da.
(a -> b) -> (a -> db -> da) -> Morphism (Mono da a) (Mono db b)
lens s -> o
get s -> i -> s
put
  where
    get :: s -> o
get s
s = (o, i -> s) -> o
forall a b. (a, b) -> a
fst (System (->) s (Mono i o) -> s -> (o, i -> s)
forall s i o. System (->) s (Mono i o) -> s -> (o, i -> s)
runSystemMono System (->) s (Mono i o)
sys s
s)
    put :: s -> i -> s
put s
s = (o, i -> s) -> i -> s
forall a b. (a, b) -> b
snd (System (->) s (Mono i o) -> s -> (o, i -> s)
forall s i o. System (->) s (Mono i o) -> s -> (o, i -> s)
runSystemMono System (->) s (Mono i o)
sys s
s)

-- | Inverse of 'systemAsLens': build a system from a lens @S y^S -> Mono i o@.
lensAsSystem :: Morphism (Mono s s) (Mono i o) -> System (->) s (Mono i o)
lensAsSystem :: forall s i o.
Morphism (Mono s s) (Mono i o) -> System (->) s (Mono i o)
lensAsSystem Morphism (Mono s s) (Mono i o)
m = (s -> Eval (Mono i o) s) -> System (->) s (Mono i o)
forall (p :: Poly) s.
SystemEval p =>
(s -> Eval p s) -> System (->) s p
fromEvalSystem ((s -> Eval (Mono i o) s) -> System (->) s (Mono i o))
-> (s -> Eval (Mono i o) s) -> System (->) s (Mono i o)
forall a b. (a -> b) -> a -> b
$ \s
s ->
  case Morphism (Mono s s) (Mono i o) -> s -> (o, i -> s)
forall da a db b.
Morphism (Mono da a) (Mono db b) -> a -> (b, db -> da)
applyLens Morphism (Mono s s) (Mono i o)
m s
s of
    (o
o, i -> s
put) -> (Eval ('Const o) s, Eval ('Exp i) s) -> Eval (Mono i o) s
forall (p1 :: Poly) x (q :: Poly).
(Eval p1 x, Eval q x) -> Eval ('Prod p1 q) x
EP (o -> Eval ('Const o) s
forall c x. c -> Eval ('Const c) x
EK o
o, (i -> s) -> Eval ('Exp i) s
forall a x. (a -> x) -> Eval ('Exp a) x
EE i -> s
put)

-- | 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.
duplicateSystem :: System (->) s (Mono o s) -> System (->) s ('Comp (Mono o s) (Mono o s))
duplicateSystem :: forall s o.
System (->) s (Mono o s)
-> System (->) s ('Comp (Mono o s) (Mono o s))
duplicateSystem System (->) s (Mono o s)
sys =
  (s -> Eval ('Comp (Mono o s) (Mono o s)) s)
-> System (->) s ('Comp (Mono o s) (Mono o s))
forall (p :: Poly) s.
SystemEval p =>
(s -> Eval p s) -> System (->) s p
fromEvalSystem ((s -> Eval ('Comp (Mono o s) (Mono o s)) s)
 -> System (->) s ('Comp (Mono o s) (Mono o s)))
-> (s -> Eval ('Comp (Mono o s) (Mono o s)) s)
-> System (->) s ('Comp (Mono o s) (Mono o s))
forall a b. (a -> b) -> a -> b
$ \s
s ->
    let (s
s0, o -> s
nextStep) = System (->) s (Mono o s) -> s -> (s, o -> s)
forall s i o. System (->) s (Mono i o) -> s -> (o, i -> s)
runSystemMono System (->) s (Mono o s)
sys s
s
        nextEval :: o -> Eval (Mono o s) s
nextEval o
o =
          let (s
s1, o -> s
step1) = System (->) s (Mono o s) -> s -> (s, o -> s)
forall s i o. System (->) s (Mono i o) -> s -> (o, i -> s)
runSystemMono System (->) s (Mono o s)
sys (o -> s
nextStep o
o)
           in (Eval ('Const s) s, Eval ('Exp o) s) -> Eval (Mono o s) s
forall (p1 :: Poly) x (q :: Poly).
(Eval p1 x, Eval q x) -> Eval ('Prod p1 q) x
EP (s -> Eval ('Const s) s
forall c x. c -> Eval ('Const c) x
EK s
s1, (o -> s) -> Eval ('Exp o) s
forall a x. (a -> x) -> Eval ('Exp a) x
EE o -> s
step1)
     in Eval (Mono o s) (Eval (Mono o s) s)
-> Eval ('Comp (Mono o s) (Mono o s)) s
forall (p :: Poly) (q :: Poly) x.
(Netlist p, Netlist q) =>
Eval p (Eval q x) -> Eval ('Comp p q) x
nestedToComp ((Eval ('Const s) (Eval (Mono o s) s),
 Eval ('Exp o) (Eval (Mono o s) s))
-> Eval (Mono o s) (Eval (Mono o s) s)
forall (p1 :: Poly) x (q :: Poly).
(Eval p1 x, Eval q x) -> Eval ('Prod p1 q) x
EP (s -> Eval ('Const s) (Eval (Mono o s) s)
forall c x. c -> Eval ('Const c) x
EK s
s0, (o -> Eval (Mono o s) s) -> Eval ('Exp o) (Eval (Mono o s) s)
forall a x. (a -> x) -> Eval ('Exp a) x
EE o -> Eval (Mono o s) s
nextEval))

-- | 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'.
branchSystem ::
  (s -> Bool) ->
  System (->) s (Mono i o) ->
  System (->) s (Mono i o) ->
  System (->) s ('Sum (Mono i o) (Mono i o))
branchSystem :: forall s i o.
(s -> Bool)
-> System (->) s (Mono i o)
-> System (->) s (Mono i o)
-> System (->) s ('Sum (Mono i o) (Mono i o))
branchSystem s -> Bool
cond System (->) s (Mono i o)
sysL System (->) s (Mono i o)
sysR =
  (s -> Eval ('Sum (Mono i o) (Mono i o)) s)
-> System (->) s ('Sum (Mono i o) (Mono i o))
forall (p :: Poly) s.
SystemEval p =>
(s -> Eval p s) -> System (->) s p
fromEvalSystem ((s -> Eval ('Sum (Mono i o) (Mono i o)) s)
 -> System (->) s ('Sum (Mono i o) (Mono i o)))
-> (s -> Eval ('Sum (Mono i o) (Mono i o)) s)
-> System (->) s ('Sum (Mono i o) (Mono i o))
forall a b. (a -> b) -> a -> b
$ \s
s ->
    if s -> Bool
cond s
s
      then Either (Eval (Mono i o) s) (Eval (Mono i o) s)
-> Eval ('Sum (Mono i o) (Mono i o)) s
forall (p1 :: Poly) x (q :: Poly).
Either (Eval p1 x) (Eval q x) -> Eval ('Sum p1 q) x
ES (Eval (Mono i o) s -> Either (Eval (Mono i o) s) (Eval (Mono i o) s)
forall a b. a -> Either a b
Left (System (->) s (Mono i o) -> s -> Eval (Mono i o) s
forall (p :: Poly) s.
SystemEval p =>
System (->) s p -> s -> Eval p s
toEvalSystem System (->) s (Mono i o)
sysL s
s))
      else Either (Eval (Mono i o) s) (Eval (Mono i o) s)
-> Eval ('Sum (Mono i o) (Mono i o)) s
forall (p1 :: Poly) x (q :: Poly).
Either (Eval p1 x) (Eval q x) -> Eval ('Sum p1 q) x
ES (Eval (Mono i o) s -> Either (Eval (Mono i o) s) (Eval (Mono i o) s)
forall a b. b -> Either a b
Right (System (->) s (Mono i o) -> s -> Eval (Mono i o) s
forall (p :: Poly) s.
SystemEval p =>
System (->) s p -> s -> Eval p s
toEvalSystem System (->) s (Mono i o)
sysR s
s))

-- | Run a system with a homogeneous sum-of-monomials interface.
runSystemSum ::
  System (->) s ('Sum (Mono i o) (Mono i o)) ->
  s ->
  (Either o o, i -> s)
runSystemSum :: forall s i o.
System (->) s ('Sum (Mono i o) (Mono i o))
-> s -> (Either o o, i -> s)
runSystemSum System (->) s ('Sum (Mono i o) (Mono i o))
sys s
s = case System (->) s ('Sum (Mono i o) (Mono i o))
-> s -> Eval ('Sum (Mono i o) (Mono i o)) s
forall (p :: Poly) s.
SystemEval p =>
System (->) s p -> s -> Eval p s
toEvalSystem System (->) s ('Sum (Mono i o) (Mono i o))
sys s
s of
  ES (Left (EP (EK c
o, EE a -> s
f))) -> (o -> Either o o
forall a b. a -> Either a b
Left o
c
o, i -> s
a -> s
f)
  ES (Right (EP (EK c
o, EE a -> s
f))) -> (o -> Either o o
forall a b. b -> Either a b
Right o
c
o, i -> s
a -> s
f)

-- | 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@.
data SumStep s o1 i1 o2 i2 where
  SumStepL :: o1 -> (i1 -> s) -> SumStep s o1 i1 o2 i2
  SumStepR :: o2 -> (i2 -> s) -> SumStep s o1 i1 o2 i2

-- | Build a system whose interface is the coproduct of two /different/
-- monomial interfaces.  The carrier state selects the active branch at each
-- step.
branchSystemHet ::
  (s -> Bool) ->
  System (->) s (Mono i1 o1) ->
  System (->) s (Mono i2 o2) ->
  System (->) s ('Sum (Mono i1 o1) (Mono i2 o2))
branchSystemHet :: forall s i1 o1 i2 o2.
(s -> Bool)
-> System (->) s (Mono i1 o1)
-> System (->) s (Mono i2 o2)
-> System (->) s ('Sum (Mono i1 o1) (Mono i2 o2))
branchSystemHet s -> Bool
cond System (->) s (Mono i1 o1)
sysL System (->) s (Mono i2 o2)
sysR =
  (s -> Eval ('Sum (Mono i1 o1) (Mono i2 o2)) s)
-> System (->) s ('Sum (Mono i1 o1) (Mono i2 o2))
forall (p :: Poly) s.
SystemEval p =>
(s -> Eval p s) -> System (->) s p
fromEvalSystem ((s -> Eval ('Sum (Mono i1 o1) (Mono i2 o2)) s)
 -> System (->) s ('Sum (Mono i1 o1) (Mono i2 o2)))
-> (s -> Eval ('Sum (Mono i1 o1) (Mono i2 o2)) s)
-> System (->) s ('Sum (Mono i1 o1) (Mono i2 o2))
forall a b. (a -> b) -> a -> b
$ \s
s ->
    if s -> Bool
cond s
s
      then Either (Eval (Mono i1 o1) s) (Eval (Mono i2 o2) s)
-> Eval ('Sum (Mono i1 o1) (Mono i2 o2)) s
forall (p1 :: Poly) x (q :: Poly).
Either (Eval p1 x) (Eval q x) -> Eval ('Sum p1 q) x
ES (Eval (Mono i1 o1) s
-> Either (Eval (Mono i1 o1) s) (Eval (Mono i2 o2) s)
forall a b. a -> Either a b
Left (System (->) s (Mono i1 o1) -> s -> Eval (Mono i1 o1) s
forall (p :: Poly) s.
SystemEval p =>
System (->) s p -> s -> Eval p s
toEvalSystem System (->) s (Mono i1 o1)
sysL s
s))
      else Either (Eval (Mono i1 o1) s) (Eval (Mono i2 o2) s)
-> Eval ('Sum (Mono i1 o1) (Mono i2 o2)) s
forall (p1 :: Poly) x (q :: Poly).
Either (Eval p1 x) (Eval q x) -> Eval ('Sum p1 q) x
ES (Eval (Mono i2 o2) s
-> Either (Eval (Mono i1 o1) s) (Eval (Mono i2 o2) s)
forall a b. b -> Either a b
Right (System (->) s (Mono i2 o2) -> s -> Eval (Mono i2 o2) s
forall (p :: Poly) s.
SystemEval p =>
System (->) s p -> s -> Eval p s
toEvalSystem System (->) s (Mono i2 o2)
sysR s
s))

-- | Run a heterogeneous sum-interface system.
runSystemSumHet ::
  System (->) s ('Sum (Mono i1 o1) (Mono i2 o2)) ->
  s ->
  SumStep s o1 i1 o2 i2
runSystemSumHet :: forall s i1 o1 i2 o2.
System (->) s ('Sum (Mono i1 o1) (Mono i2 o2))
-> s -> SumStep s o1 i1 o2 i2
runSystemSumHet System (->) s ('Sum (Mono i1 o1) (Mono i2 o2))
sys s
s = case System (->) s ('Sum (Mono i1 o1) (Mono i2 o2))
-> s -> Eval ('Sum (Mono i1 o1) (Mono i2 o2)) s
forall (p :: Poly) s.
SystemEval p =>
System (->) s p -> s -> Eval p s
toEvalSystem System (->) s ('Sum (Mono i1 o1) (Mono i2 o2))
sys s
s of
  ES (Left (EP (EK c
o, EE a -> s
f))) -> o1 -> (i1 -> s) -> SumStep s o1 i1 o2 i2
forall o1 i1 s o2 i2. o1 -> (i1 -> s) -> SumStep s o1 i1 o2 i2
SumStepL o1
c
o i1 -> s
a -> s
f
  ES (Right (EP (EK c
o, EE a -> s
f))) -> o2 -> (i2 -> s) -> SumStep s o1 i1 o2 i2
forall o2 i2 s o1 i1. o2 -> (i2 -> s) -> SumStep s o1 i1 o2 i2
SumStepR o2
c
o i2 -> s
a -> s
f

-- | 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.
type Step s q = Eval q s

-- | 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.
data Coalgebra s p q = Coalgebra
  { forall s (p :: Poly) (q :: Poly).
Coalgebra s p q -> s -> Morphism p q
act :: s -> Morphism p q,
    forall s (p :: Poly) (q :: Poly).
Coalgebra s p q -> s -> Eval p s -> Step s q
upd :: s -> Eval p s -> Step s q
  }

-- | Run a @Coalgebra s 'Y q@ as a 'System' over @q@.
coalgebraToSystem :: (SystemEval q) => Coalgebra s 'Y q -> System (->) s q
coalgebraToSystem :: forall (q :: Poly) s.
SystemEval q =>
Coalgebra s 'Y q -> System (->) s q
coalgebraToSystem Coalgebra s 'Y q
coal = (s -> Eval q s) -> System (->) s q
forall (p :: Poly) s.
SystemEval p =>
(s -> Eval p s) -> System (->) s p
fromEvalSystem ((s -> Eval q s) -> System (->) s q)
-> (s -> Eval q s) -> System (->) s q
forall a b. (a -> b) -> a -> b
$ \s
s -> Coalgebra s 'Y q -> s -> Eval 'Y s -> Eval q s
forall s (p :: Poly) (q :: Poly).
Coalgebra s p q -> s -> Eval p s -> Step s q
upd Coalgebra s 'Y q
coal s
s (s -> Eval 'Y s
forall x. x -> Eval 'Y x
EY s
s)

-- | Convert a monomial 'System' into a @Coalgebra s 'Y (Mono i o)@.
systemToCoalgebraMono :: System (->) s (Mono i o) -> Coalgebra s 'Y (Mono i o)
systemToCoalgebraMono :: forall s i o. System (->) s (Mono i o) -> Coalgebra s 'Y (Mono i o)
systemToCoalgebraMono System (->) s ('Prod ('Const o) ('Exp i))
sys =
  Coalgebra
    { act :: s -> Morphism 'Y ('Prod ('Const o) ('Exp i))
act = \s
s -> let (o
o, i -> s
_) = System (->) s ('Prod ('Const o) ('Exp i)) -> s -> (o, i -> s)
forall s i o. System (->) s (Mono i o) -> s -> (o, i -> s)
runSystemMono System (->) s ('Prod ('Const o) ('Exp i))
sys s
s in Eval ('Prod ('Const o) ('Exp i)) ()
-> Morphism 'Y ('Prod ('Const o) ('Exp i))
forall (q :: Poly). Eval q () -> Morphism 'Y q
Point ((Eval ('Const o) (), Eval ('Exp i) ())
-> Eval ('Prod ('Const o) ('Exp i)) ()
forall (p1 :: Poly) x (q :: Poly).
(Eval p1 x, Eval q x) -> Eval ('Prod p1 q) x
EP (o -> Eval ('Const o) ()
forall c x. c -> Eval ('Const c) x
EK o
o, (i -> ()) -> Eval ('Exp i) ()
forall a x. (a -> x) -> Eval ('Exp a) x
EE (() -> i -> ()
forall a b. a -> b -> a
const ()))),
      upd :: s -> Eval 'Y s -> Step s ('Prod ('Const o) ('Exp i))
upd = \s
s Eval 'Y s
_ -> System (->) s ('Prod ('Const o) ('Exp i))
-> s -> Step s ('Prod ('Const o) ('Exp i))
forall (p :: Poly) s.
SystemEval p =>
System (->) s p -> s -> Eval p s
toEvalSystem System (->) s ('Prod ('Const o) ('Exp i))
sys s
s
    }

-- | Sequential composition of two closed coalgebras via the composition product.
composeCoalgebra ::
  (Netlist p, Netlist q) =>
  Coalgebra s 'Y p ->
  Coalgebra t 'Y q ->
  Coalgebra (s, t) 'Y (Comp p q)
composeCoalgebra :: forall (p :: Poly) (q :: Poly) s t.
(Netlist p, Netlist q) =>
Coalgebra s 'Y p
-> Coalgebra t 'Y q -> Coalgebra (s, t) 'Y ('Comp p q)
composeCoalgebra Coalgebra s 'Y p
coalP Coalgebra t 'Y q
coalQ =
  Coalgebra
    { act :: (s, t) -> Morphism 'Y ('Comp p q)
act = \(s
s, t
t) ->
        let pPoint :: Eval p ()
pPoint = Morphism 'Y p -> forall x. Eval 'Y x -> Eval p x
forall (p :: Poly) (q :: Poly).
Morphism p q -> forall x. Eval p x -> Eval q x
runMorphism (Coalgebra s 'Y p -> s -> Morphism 'Y p
forall s (p :: Poly) (q :: Poly).
Coalgebra s p q -> s -> Morphism p q
act Coalgebra s 'Y p
coalP s
s) (() -> Eval 'Y ()
forall x. x -> Eval 'Y x
EY ())
            qPoint :: Eval q ()
qPoint = Morphism 'Y q -> forall x. Eval 'Y x -> Eval q x
forall (p :: Poly) (q :: Poly).
Morphism p q -> forall x. Eval p x -> Eval q x
runMorphism (Coalgebra t 'Y q -> t -> Morphism 'Y q
forall s (p :: Poly) (q :: Poly).
Coalgebra s p q -> s -> Morphism p q
act Coalgebra t 'Y q
coalQ t
t) (() -> Eval 'Y ()
forall x. x -> Eval 'Y x
EY ())
         in Eval ('Comp p q) () -> Morphism 'Y ('Comp p q)
forall (q :: Poly). Eval q () -> Morphism 'Y q
Point (Eval p (Eval q ()) -> Eval ('Comp p q) ()
forall (p :: Poly) (q :: Poly) x.
(Netlist p, Netlist q) =>
Eval p (Eval q x) -> Eval ('Comp p q) x
nestedToComp ((() -> Eval q ()) -> Eval p () -> Eval p (Eval q ())
forall a b. (a -> b) -> Eval p a -> Eval p b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Eval q () -> () -> Eval q ()
forall a b. a -> b -> a
const Eval q ()
qPoint) Eval p ()
pPoint)),
      upd :: (s, t) -> Eval 'Y (s, t) -> Step (s, t) ('Comp p q)
upd = \(s
s, t
t) Eval 'Y (s, t)
_ ->
        let pVal :: Step s p
pVal = Coalgebra s 'Y p -> s -> Eval 'Y s -> Step s p
forall s (p :: Poly) (q :: Poly).
Coalgebra s p q -> s -> Eval p s -> Step s q
upd Coalgebra s 'Y p
coalP s
s (s -> Eval 'Y s
forall x. x -> Eval 'Y x
EY s
s)
            qVal :: Step t q
qVal = Coalgebra t 'Y q -> t -> Eval 'Y t -> Step t q
forall s (p :: Poly) (q :: Poly).
Coalgebra s p q -> s -> Eval p s -> Step s q
upd Coalgebra t 'Y q
coalQ t
t (t -> Eval 'Y t
forall x. x -> Eval 'Y x
EY t
t)
         in Eval p (Eval q (s, t)) -> Step (s, t) ('Comp p q)
forall (p :: Poly) (q :: Poly) x.
(Netlist p, Netlist q) =>
Eval p (Eval q x) -> Eval ('Comp p q) x
nestedToComp ((s -> Eval q (s, t)) -> Step s p -> Eval p (Eval q (s, t))
forall a b. (a -> b) -> Eval p a -> Eval p b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\s
s' -> (t -> (s, t)) -> Step t q -> Eval q (s, t)
forall a b. (a -> b) -> Eval q a -> Eval q b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (s
s',) Step t q
qVal) Step s p
pVal)
    }