{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}

-- | A small string-diagram surface syntax over the Int construction.
--
-- The Int corridor turns a traced monoidal base category into a compact
-- closed category.  For the causal fragment of 'Circuit.Poly' — dependent
-- lenses between monomial interfaces — the resulting diagrams are exactly
-- the usual boxes-and-wires pictures: a wire is a polarity pair, a box is a
-- causal lens, placing diagrams beside each other is tensor, chaining them
-- is composition, and bending a wire back uses the compact-closed cap/cup.
--
-- This module aliases the underlying Int machinery with string-diagram
-- names and runs the diagrams over 'Trace (,) (->)' so that feedback loops
-- are tied into yanked traces.
--
-- The DSL is a /deep embedding/: every value remembers how it was built.
-- That lets us interpret a diagram either as an executable 'IntMorph' (via
-- 'runDiagram') or as an untyped drawing skeleton (via 'skeleton') for a
-- renderer such as @chart-svg@.
--
-- The skeleton also carries hypergraph syntax: multi-port boxes and
-- spiders ('SSpider', with 'sCopy' \/ 'sMerge' \/ 'sDelete' \/ 'sCreate'
-- as the usual generators).  Spiders are drawing-level syntax only —
-- there are deliberately no spider constructors in the typed 'Diagram'
-- GADT, so 'skeleton' never produces one.  Structural comparison of the
-- hyper fragment lives in "Circuit.Diagram.Hyper".
module Circuit.Poly.StringDiagram
  ( -- * String-diagram vocabulary
    Wire,
    Diagram,
    wire,
    box,
    boxLabelled,
    beside,
    thenD,
    bend,
    bend',
    turn,
    unitL,
    unitL',
    unitR,
    unitR',
    assoc,
    assoc',
    swap,
    prismBox,
    traceD,

    -- * Running a diagram
    runDiagram,

    -- * Drawing skeleton (re-exported from "Circuit.Diagram")
    SDiagram (..),
    skeleton,
    sCopy,
    sMerge,
    sDelete,
    sCreate,
  )
where

import Circuit.Category qualified as Cat
import Circuit.Channel (Traced (..))
import Circuit.Diagram (SDiagram (..), sCopy, sCreate, sDelete, sMerge)
import Circuit.Poly (Mono, Morphism, applyLens)
import Circuit.Poly.Int (IN, IntMorph (..))
import Circuit.Poly.Int qualified as Int
import Circuit.Syntax (eval)
import Circuit.Tensor qualified as M
import Circuit.Trace (Trace, base)
import Prelude hiding (id, (.))

-- $setup
-- >>> import Prelude

-- | A wire is a forward type paired with a backward type.
type Wire a da = IN a da

-- | Internal deep embedding of a typed string diagram.
--
-- The constructors mirror the public smart constructors exactly.
data Diagram_ a da b db where
  Wire_ :: Diagram_ a da a da
  Box_ :: String -> Morphism (Mono da a) (Mono db b) -> Diagram_ a da b db
  PrismBox_ ::
    (s -> Either a s) ->
    (a -> s) ->
    Diagram_ s s (Either a s) (Either a s)
  Beside_ ::
    Diagram_ ap am bp bm ->
    Diagram_ cp cm dp dm ->
    Diagram_ (ap, cp) (am, cm) (bp, dp) (bm, dm)
  ThenD_ ::
    Diagram_ ap am bp bm ->
    Diagram_ bp bm cp cm ->
    Diagram_ ap am cp cm
  Bend_ :: Diagram_ (da, a) (a, da) () ()
  Bend'_ :: Diagram_ () () (a, da) (da, a)
  Turn_ :: Diagram_ a da b db -> Diagram_ db b da a
  UnitL_ :: Diagram_ ((), a) ((), da) a da
  UnitL'_ :: Diagram_ a da ((), a) ((), da)
  UnitR_ :: Diagram_ (a, ()) (da, ()) a da
  UnitR'_ :: Diagram_ a da (a, ()) (da, ())
  Assoc_ ::
    Diagram_ (a, (b, c)) (da, (db, dc)) ((a, b), c) ((da, db), dc)
  Assoc'_ ::
    Diagram_ ((a, b), c) ((da, db), dc) (a, (b, c)) (da, (db, dc))
  Swap_ ::
    Diagram_ (a, b) (da, db) (b, a) (db, da)
  Trace_ ::
    Diagram_ (s, a) (s, da) (s, b) (s, db) ->
    Diagram_ a da b db

-- | A string diagram from one bundle of wires to another.
--
-- The base category is 'Trace (,) (->)' so that sequential composition can
-- tie feedback knots.
newtype Diagram a da b db = Diagram (Diagram_ a da b db)

-- | Forget the types and extract the drawing skeleton.
skeleton :: Diagram a da b db -> SDiagram
skeleton :: forall a da b db. Diagram a da b db -> SDiagram
skeleton (Diagram Diagram_ a da b db
d) = Diagram_ a da b db -> SDiagram
forall a' da' b' db'. Diagram_ a' da' b' db' -> SDiagram
go Diagram_ a da b db
d
  where
    go :: Diagram_ a' da' b' db' -> SDiagram
    go :: forall a' da' b' db'. Diagram_ a' da' b' db' -> SDiagram
go Diagram_ a' da' b' db'
Wire_ = SDiagram
SWire
    go (Box_ String
lbl Morphism (Mono da' a') (Mono db' b')
_) = String -> Int -> Int -> SDiagram
SBox String
lbl Int
1 Int
1
    go (PrismBox_ a' -> Either a a'
_ a -> a'
_) = SDiagram
SPrismBox
    go (Beside_ Diagram_ ap am bp bm
f Diagram_ cp cm dp dm
g) = SDiagram -> SDiagram -> SDiagram
SBeside (Diagram_ ap am bp bm -> SDiagram
forall a' da' b' db'. Diagram_ a' da' b' db' -> SDiagram
go Diagram_ ap am bp bm
f) (Diagram_ cp cm dp dm -> SDiagram
forall a' da' b' db'. Diagram_ a' da' b' db' -> SDiagram
go Diagram_ cp cm dp dm
g)
    go (ThenD_ Diagram_ a' da' bp bm
f Diagram_ bp bm b' db'
g) = SDiagram -> SDiagram -> SDiagram
SThenD (Diagram_ a' da' bp bm -> SDiagram
forall a' da' b' db'. Diagram_ a' da' b' db' -> SDiagram
go Diagram_ a' da' bp bm
f) (Diagram_ bp bm b' db' -> SDiagram
forall a' da' b' db'. Diagram_ a' da' b' db' -> SDiagram
go Diagram_ bp bm b' db'
g)
    go Diagram_ a' da' b' db'
Bend_ = SDiagram
SBend
    go Diagram_ a' da' b' db'
Bend'_ = SDiagram
SBend'
    go (Turn_ Diagram_ db' b' da' a'
f) = SDiagram -> SDiagram
STurn (Diagram_ db' b' da' a' -> SDiagram
forall a' da' b' db'. Diagram_ a' da' b' db' -> SDiagram
go Diagram_ db' b' da' a'
f)
    go Diagram_ a' da' b' db'
UnitL_ = SDiagram
SUnitL
    go Diagram_ a' da' b' db'
UnitL'_ = SDiagram
SUnitL'
    go Diagram_ a' da' b' db'
UnitR_ = SDiagram
SUnitR
    go Diagram_ a' da' b' db'
UnitR'_ = SDiagram
SUnitR'
    go Diagram_ a' da' b' db'
Assoc_ = SDiagram
SAssoc
    go Diagram_ a' da' b' db'
Assoc'_ = SDiagram
SAssoc'
    go Diagram_ a' da' b' db'
Swap_ = SDiagram
SSwap
    go (Trace_ Diagram_ (s, a') (s, da') (s, b') (s, db')
f) = SDiagram -> SDiagram
STrace (Diagram_ (s, a') (s, da') (s, b') (s, db') -> SDiagram
forall a' da' b' db'. Diagram_ a' da' b' db' -> SDiagram
go Diagram_ (s, a') (s, da') (s, b') (s, db')
f)

-- | Convert a deep-embedding diagram back to the executable Int corridor.
toIntMorph :: Diagram a da b db -> IntMorph (,) (Trace (,) (->)) a da b db
toIntMorph :: forall a da b db.
Diagram a da b db -> IntMorph (,) (Trace (,) (->)) a da b db
toIntMorph (Diagram Diagram_ a da b db
d) = case Diagram_ a da b db
d of
  Diagram_ a da b db
Wire_ -> Trace (,) (->) (a, db) (da, b)
-> IntMorph (,) (Trace (,) (->)) a da b db
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
arr (t ap bm) (t am bp) -> IntMorph t arr ap am bp bm
IntMorph (((a, db) -> (da, b)) -> Trace (,) (->) (a, db) (da, b)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (a, db) -> (da, b)
(b, da) -> (da, b)
forall a b. (a, b) -> (b, a)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k).
Action t arr =>
arr (t a b) (t b a)
M.braid)
  Box_ String
_ Morphism (Mono da a) (Mono db b)
m -> Trace (,) (->) (a, db) (da, b)
-> IntMorph (,) (Trace (,) (->)) a da b db
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
arr (t ap bm) (t am bp) -> IntMorph t arr ap am bp bm
IntMorph (((a, db) -> (da, b)) -> Trace (,) (->) (a, db) (da, b)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (\(a
a, db
db) -> let (b
b, db -> da
put) = Morphism (Mono da a) (Mono db b) -> a -> (b, db -> da)
forall da a db b.
Morphism (Mono da a) (Mono db b) -> a -> (b, db -> da)
applyLens Morphism (Mono da a) (Mono db b)
m a
a in (db -> da
put db
db, b
b)))
  PrismBox_ a -> Either a a
match a -> a
build ->
    Trace (,) (->) (a, db) (da, b)
-> IntMorph (,) (Trace (,) (->)) a da b db
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
arr (t ap bm) (t am bp) -> IntMorph t arr ap am bp bm
IntMorph
      ( ((a, db) -> (da, b)) -> Trace (,) (->) (a, db) (da, b)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base
          ( \(a
s, Either a a
e) -> case Either a a
e of
              Left a
a -> (a -> a
build a
a, a -> Either a a
match a
s)
              Right a
s' -> (a
s', a -> Either a a
match a
s)
          )
      )
  Beside_ Diagram_ ap am bp bm
f Diagram_ cp cm dp dm
g -> IntMorph (,) (Trace (,) (->)) ap am bp bm
-> IntMorph (,) (Trace (,) (->)) cp cm dp dm
-> IntMorph
     (,) (Trace (,) (->)) (ap, cp) (am, cm) (bp, dp) (bm, dm)
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm cp cm dp
       dm.
(Action t arr, Channel t arr) =>
IntMorph t arr ap am bp bm
-> IntMorph t arr cp cm dp dm
-> IntMorph t arr (t ap cp) (t am cm) (t bp dp) (t bm dm)
Int.intTensor (Diagram ap am bp bm -> IntMorph (,) (Trace (,) (->)) ap am bp bm
forall a da b db.
Diagram a da b db -> IntMorph (,) (Trace (,) (->)) a da b db
toIntMorph (Diagram_ ap am bp bm -> Diagram ap am bp bm
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram Diagram_ ap am bp bm
f)) (Diagram cp cm dp dm -> IntMorph (,) (Trace (,) (->)) cp cm dp dm
forall a da b db.
Diagram a da b db -> IntMorph (,) (Trace (,) (->)) a da b db
toIntMorph (Diagram_ cp cm dp dm -> Diagram cp cm dp dm
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram Diagram_ cp cm dp dm
g))
  ThenD_ Diagram_ a da bp bm
f Diagram_ bp bm b db
g -> IntMorph (,) (Trace (,) (->)) bp bm b db
-> IntMorph (,) (Trace (,) (->)) a da bp bm
-> IntMorph (,) (Trace (,) (->)) a da b db
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm cp cm.
(Action t arr, Traced t arr) =>
IntMorph t arr bp bm cp cm
-> IntMorph t arr ap am bp bm -> IntMorph t arr ap am cp cm
Int.comp (Diagram bp bm b db -> IntMorph (,) (Trace (,) (->)) bp bm b db
forall a da b db.
Diagram a da b db -> IntMorph (,) (Trace (,) (->)) a da b db
toIntMorph (Diagram_ bp bm b db -> Diagram bp bm b db
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram Diagram_ bp bm b db
g)) (Diagram a da bp bm -> IntMorph (,) (Trace (,) (->)) a da bp bm
forall a da b db.
Diagram a da b db -> IntMorph (,) (Trace (,) (->)) a da b db
toIntMorph (Diagram_ a da bp bm -> Diagram a da bp bm
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram Diagram_ a da bp bm
f))
  Diagram_ a da b db
Bend_ -> Trace (,) (->) (a, db) (da, b)
-> IntMorph (,) (Trace (,) (->)) a da b db
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
arr (t ap bm) (t am bp) -> IntMorph t arr ap am bp bm
IntMorph (((a, db) -> (da, b)) -> Trace (,) (->) (a, db) (da, b)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (\((da
da, a
a), ()) -> ((a
a, da
da), ())))
  Diagram_ a da b db
Bend'_ -> Trace (,) (->) (a, db) (da, b)
-> IntMorph (,) (Trace (,) (->)) a da b db
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
arr (t ap bm) (t am bp) -> IntMorph t arr ap am bp bm
IntMorph (((a, db) -> (da, b)) -> Trace (,) (->) (a, db) (da, b)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (\((), (da
da, a
a)) -> ((), (a
a, da
da))))
  Turn_ Diagram_ db b da a
f -> IntMorph (,) (Trace (,) (->)) db b da a
-> IntMorph (,) (Trace (,) (->)) a da b db
forall a da b db.
IntMorph (,) (Trace (,) (->)) a da b db
-> IntMorph (,) (Trace (,) (->)) db b da a
turnInt (Diagram db b da a -> IntMorph (,) (Trace (,) (->)) db b da a
forall a da b db.
Diagram a da b db -> IntMorph (,) (Trace (,) (->)) a da b db
toIntMorph (Diagram_ db b da a -> Diagram db b da a
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram Diagram_ db b da a
f))
  Diagram_ a da b db
UnitL_ -> Trace (,) (->) (a, db) (da, b)
-> IntMorph (,) (Trace (,) (->)) a da b db
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
arr (t ap bm) (t am bp) -> IntMorph t arr ap am bp bm
IntMorph (((a, db) -> (da, b)) -> Trace (,) (->) (a, db) (da, b)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (IntMorph (,) (->) a da b db -> (a, db) -> (da, b)
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
IntMorph t arr ap am bp bm -> arr (t ap bm) (t am bp)
runIntMorph IntMorph (,) (->) a da b db
IntMorph (,) (->) ((), b) ((), db) b db
forall a b. IntMorph (,) (->) ((), a) ((), b) a b
Int.unitL))
  Diagram_ a da b db
UnitL'_ -> Trace (,) (->) (a, db) (da, b)
-> IntMorph (,) (Trace (,) (->)) a da b db
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
arr (t ap bm) (t am bp) -> IntMorph t arr ap am bp bm
IntMorph (((a, db) -> (da, b)) -> Trace (,) (->) (a, db) (da, b)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (IntMorph (,) (->) a da b db -> (a, db) -> (da, b)
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
IntMorph t arr ap am bp bm -> arr (t ap bm) (t am bp)
runIntMorph IntMorph (,) (->) a da b db
IntMorph (,) (->) a da ((), a) ((), da)
forall a b. IntMorph (,) (->) a b ((), a) ((), b)
Int.unitL'))
  Diagram_ a da b db
UnitR_ -> Trace (,) (->) (a, db) (da, b)
-> IntMorph (,) (Trace (,) (->)) a da b db
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
arr (t ap bm) (t am bp) -> IntMorph t arr ap am bp bm
IntMorph (((a, db) -> (da, b)) -> Trace (,) (->) (a, db) (da, b)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (IntMorph (,) (->) a da b db -> (a, db) -> (da, b)
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
IntMorph t arr ap am bp bm -> arr (t ap bm) (t am bp)
runIntMorph IntMorph (,) (->) a da b db
IntMorph (,) (->) (b, ()) (db, ()) b db
forall a b. IntMorph (,) (->) (a, ()) (b, ()) a b
Int.unitR))
  Diagram_ a da b db
UnitR'_ -> Trace (,) (->) (a, db) (da, b)
-> IntMorph (,) (Trace (,) (->)) a da b db
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
arr (t ap bm) (t am bp) -> IntMorph t arr ap am bp bm
IntMorph (((a, db) -> (da, b)) -> Trace (,) (->) (a, db) (da, b)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (IntMorph (,) (->) a da b db -> (a, db) -> (da, b)
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
IntMorph t arr ap am bp bm -> arr (t ap bm) (t am bp)
runIntMorph IntMorph (,) (->) a da b db
IntMorph (,) (->) a da (a, ()) (da, ())
forall a b. IntMorph (,) (->) a b (a, ()) (b, ())
Int.unitR'))
  Diagram_ a da b db
Assoc_ -> Trace (,) (->) (a, db) (da, b)
-> IntMorph (,) (Trace (,) (->)) a da b db
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
arr (t ap bm) (t am bp) -> IntMorph t arr ap am bp bm
IntMorph (((a, db) -> (da, b)) -> Trace (,) (->) (a, db) (da, b)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (IntMorph (,) (->) a da b db -> (a, db) -> (da, b)
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
IntMorph t arr ap am bp bm -> arr (t ap bm) (t am bp)
runIntMorph IntMorph (,) (->) a da b db
IntMorph
  (,) (->) (a, (b, c)) (da, (db, dc)) ((a, b), c) ((da, db), dc)
forall a b c da db dc.
IntMorph
  (,) (->) (a, (b, c)) (da, (db, dc)) ((a, b), c) ((da, db), dc)
Int.tensorAssoc))
  Diagram_ a da b db
Assoc'_ -> Trace (,) (->) (a, db) (da, b)
-> IntMorph (,) (Trace (,) (->)) a da b db
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
arr (t ap bm) (t am bp) -> IntMorph t arr ap am bp bm
IntMorph (((a, db) -> (da, b)) -> Trace (,) (->) (a, db) (da, b)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (IntMorph (,) (->) a da b db -> (a, db) -> (da, b)
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
IntMorph t arr ap am bp bm -> arr (t ap bm) (t am bp)
runIntMorph IntMorph (,) (->) a da b db
IntMorph
  (,) (->) ((a, b), c) ((da, db), dc) (a, (b, c)) (da, (db, dc))
forall a b c da db dc.
IntMorph
  (,) (->) ((a, b), c) ((da, db), dc) (a, (b, c)) (da, (db, dc))
Int.tensorAssoc'))
  Diagram_ a da b db
Swap_ -> Trace (,) (->) (a, db) (da, b)
-> IntMorph (,) (Trace (,) (->)) a da b db
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
arr (t ap bm) (t am bp) -> IntMorph t arr ap am bp bm
IntMorph (((a, db) -> (da, b)) -> Trace (,) (->) (a, db) (da, b)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (IntMorph (,) (->) a da b db -> (a, db) -> (da, b)
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
IntMorph t arr ap am bp bm -> arr (t ap bm) (t am bp)
runIntMorph IntMorph (,) (->) a da b db
IntMorph (,) (->) (a, b) (da, db) (b, a) (db, da)
forall a b da db. IntMorph (,) (->) (a, b) (da, db) (b, a) (db, da)
Int.intBraid))
  Trace_ Diagram_ (s, a) (s, da) (s, b) (s, db)
f -> IntMorph (,) (Trace (,) (->)) (s, a) (s, da) (s, b) (s, db)
-> IntMorph (,) (Trace (,) (->)) a da b db
forall s a da b db.
IntMorph (,) (Trace (,) (->)) (s, a) (s, da) (s, b) (s, db)
-> IntMorph (,) (Trace (,) (->)) a da b db
traceIntMorph (Diagram (s, a) (s, da) (s, b) (s, db)
-> IntMorph (,) (Trace (,) (->)) (s, a) (s, da) (s, b) (s, db)
forall a da b db.
Diagram a da b db -> IntMorph (,) (Trace (,) (->)) a da b db
toIntMorph (Diagram_ (s, a) (s, da) (s, b) (s, db)
-> Diagram (s, a) (s, da) (s, b) (s, db)
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram Diagram_ (s, a) (s, da) (s, b) (s, db)
f))
  where
    traceIntMorph ::
      IntMorph (,) (Trace (,) (->)) (s, a) (s, da) (s, b) (s, db) ->
      IntMorph (,) (Trace (,) (->)) a da b db
    traceIntMorph :: forall s a da b db.
IntMorph (,) (Trace (,) (->)) (s, a) (s, da) (s, b) (s, db)
-> IntMorph (,) (Trace (,) (->)) a da b db
traceIntMorph (IntMorph Trace (,) (->) ((s, a), (s, db)) ((s, da), (s, b))
body) =
      Trace (,) (->) (a, db) (da, b)
-> IntMorph (,) (Trace (,) (->)) a da b db
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
arr (t ap bm) (t am bp) -> IntMorph t arr ap am bp bm
IntMorph
        ( Trace (,) (->) ((s, s), (a, db)) ((s, s), (da, b))
-> Trace (,) (->) (a, db) (da, b)
forall a b c. Trace (,) (->) (a, b) (a, c) -> Trace (,) (->) b c
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Traced t arr =>
arr (t a b) (t a c) -> arr b c
trace
            ( (((s, da), (s, b)) -> ((s, s), (da, b)))
-> Trace (,) (->) ((s, da), (s, b)) ((s, s), (da, b))
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (\((s
s1, da
s2), (s
da, b
b)) -> ((s
s1, s
da), (da
s2, b
b)))
                Trace (,) (->) ((s, da), (s, b)) ((s, s), (da, b))
-> Trace (,) (->) ((s, a), (s, db)) ((s, da), (s, b))
-> Trace (,) (->) ((s, a), (s, db)) ((s, s), (da, b))
forall b c a.
Trace (,) (->) b c -> Trace (,) (->) a b -> Trace (,) (->) a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
Cat.. Trace (,) (->) ((s, a), (s, db)) ((s, da), (s, b))
body
                Trace (,) (->) ((s, a), (s, db)) ((s, s), (da, b))
-> Trace (,) (->) ((s, s), (a, db)) ((s, a), (s, db))
-> Trace (,) (->) ((s, s), (a, db)) ((s, s), (da, b))
forall b c a.
Trace (,) (->) b c -> Trace (,) (->) a b -> Trace (,) (->) a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
Cat.. (((s, s), (a, db)) -> ((s, a), (s, db)))
-> Trace (,) (->) ((s, s), (a, db)) ((s, a), (s, db))
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (\((s
s1, s
s2), (a
a, db
db)) -> ((s
s1, a
a), (s
s2, db
db)))
            )
        )

-- | The identity diagram: a straight wire.
--
-- In the Int construction identity is the symmetry that swaps the forward
-- and backward factors.
wire :: Diagram a da a da
wire :: forall a da. Diagram a da a da
wire = Diagram_ a da a da -> Diagram a da a da
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram Diagram_ a da a da
forall a da. Diagram_ a da a da
Wire_

-- | A box built from a causal dependent lens.
box :: Morphism (Mono da a) (Mono db b) -> Diagram a da b db
box :: forall da a db b.
Morphism (Mono da a) (Mono db b) -> Diagram a da b db
box = String -> Morphism (Mono da a) (Mono db b) -> Diagram a da b db
forall da a db b.
String -> Morphism (Mono da a) (Mono db b) -> Diagram a da b db
boxLabelled String
"box"

-- | A labelled box built from a causal dependent lens.
boxLabelled :: String -> Morphism (Mono da a) (Mono db b) -> Diagram a da b db
boxLabelled :: forall da a db b.
String -> Morphism (Mono da a) (Mono db b) -> Diagram a da b db
boxLabelled String
lbl Morphism (Mono da a) (Mono db b)
m = Diagram_ a da b db -> Diagram a da b db
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram (String -> Morphism (Mono da a) (Mono db b) -> Diagram_ a da b db
forall da a db b.
String -> Morphism (Mono da a) (Mono db b) -> Diagram_ a da b db
Box_ String
lbl Morphism (Mono da a) (Mono db b)
m)

-- | A prism box: partial access to a sum-shaped position.
--
-- Forward pass @match :: s -> Either a s@; backward pass uses @build :: a -> s@
-- on the matched branch and the identity on the unmatched branch.  Directions
-- are identified with positions, the natural reading for set-valued
-- polynomials.
prismBox ::
  (s -> Either a s) ->
  (a -> s) ->
  Diagram s s (Either a s) (Either a s)
prismBox :: forall s a.
(s -> Either a s)
-> (a -> s) -> Diagram s s (Either a s) (Either a s)
prismBox s -> Either a s
match a -> s
build = Diagram_ s s (Either a s) (Either a s)
-> Diagram s s (Either a s) (Either a s)
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram ((s -> Either a s)
-> (a -> s) -> Diagram_ s s (Either a s) (Either a s)
forall s a.
(s -> Either a s)
-> (a -> s) -> Diagram_ s s (Either a s) (Either a s)
PrismBox_ s -> Either a s
match a -> s
build)

-- | Place two diagrams side by side (tensor product).
beside ::
  Diagram ap am bp bm ->
  Diagram cp cm dp dm ->
  Diagram (ap, cp) (am, cm) (bp, dp) (bm, dm)
beside :: forall ap am bp bm cp cm dp dm.
Diagram ap am bp bm
-> Diagram cp cm dp dm
-> Diagram (ap, cp) (am, cm) (bp, dp) (bm, dm)
beside (Diagram Diagram_ ap am bp bm
f) (Diagram Diagram_ cp cm dp dm
g) = Diagram_ (ap, cp) (am, cm) (bp, dp) (bm, dm)
-> Diagram (ap, cp) (am, cm) (bp, dp) (bm, dm)
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram (Diagram_ ap am bp bm
-> Diagram_ cp cm dp dm
-> Diagram_ (ap, cp) (am, cm) (bp, dp) (bm, dm)
forall a b da db db dc dp dm.
Diagram_ a b da db
-> Diagram_ db dc dp dm
-> Diagram_ (a, db) (b, dc) (da, dp) (db, dm)
Beside_ Diagram_ ap am bp bm
f Diagram_ cp cm dp dm
g)

-- | Chain two diagrams sequentially.
--
-- @f ">>' g@ means "first @f@, then @g@" — i.e. categorical composition
-- @g . f@.
thenD ::
  Diagram ap am bp bm ->
  Diagram bp bm cp cm ->
  Diagram ap am cp cm
thenD :: forall ap am bp bm cp cm.
Diagram ap am bp bm -> Diagram bp bm cp cm -> Diagram ap am cp cm
thenD (Diagram Diagram_ ap am bp bm
f) (Diagram Diagram_ bp bm cp cm
g) = Diagram_ ap am cp cm -> Diagram ap am cp cm
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram (Diagram_ ap am bp bm
-> Diagram_ bp bm cp cm -> Diagram_ ap am cp cm
forall ap am a b cp cm.
Diagram_ ap am a b -> Diagram_ a b cp cm -> Diagram_ ap am cp cm
ThenD_ Diagram_ ap am bp bm
f Diagram_ bp bm cp cm
g)

-- | Hide a feedback wire: trace over the state @s@.
--
-- The body has one extra input/output pair @s@ that is fed back to itself.
traceD ::
  Diagram (s, a) (s, da) (s, b) (s, db) ->
  Diagram a da b db
traceD :: forall s a da b db.
Diagram (s, a) (s, da) (s, b) (s, db) -> Diagram a da b db
traceD (Diagram Diagram_ (s, a) (s, da) (s, b) (s, db)
f) = Diagram_ a da b db -> Diagram a da b db
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram (Diagram_ (s, a) (s, da) (s, b) (s, db) -> Diagram_ a da b db
forall a a da b db.
Diagram_ (a, a) (a, da) (a, b) (a, db) -> Diagram_ a da b db
Trace_ Diagram_ (s, a) (s, da) (s, b) (s, db)
f)

-- | Introduce two wires from nothing to form a cap (unit).
--
-- At object @IN a da@ the cap produces @IN (a, da) (da, a)@.
bend' :: Diagram () () (a, da) (da, a)
bend' :: forall a da. Diagram () () (a, da) (da, a)
bend' = Diagram_ () () (a, da) (da, a) -> Diagram () () (a, da) (da, a)
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram Diagram_ () () (a, da) (da, a)
forall a b. Diagram_ () () (a, b) (b, a)
Bend'_

-- | Bend two wires back to form a cup (counit).
--
-- At object @IN a da@ the cup consumes the dual pair @IN (da, a) (a, da)@.
bend :: Diagram (da, a) (a, da) () ()
bend :: forall da a. Diagram (da, a) (a, da) () ()
bend = Diagram_ (da, a) (a, da) () () -> Diagram (da, a) (a, da) () ()
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram Diagram_ (da, a) (a, da) () ()
forall a b. Diagram_ (a, b) (b, a) () ()
Bend_

-- $snake-equations
--
-- The cap/cup pair on a self-dual finite object satisfies the snake
-- equations up to diagram deformation. For @IN Bool Bool@ both snakes
-- round-trip to the identity wire:
--
-- >>> :{
-- let snakeR :: Diagram Bool Bool Bool Bool
--     snakeR = unitR' `thenD` (wire `beside` bend') `thenD` assoc `thenD` (bend `beside` wire) `thenD` unitL
--     snakeL :: Diagram Bool Bool Bool Bool
--     snakeL = unitL' `thenD` (bend' `beside` wire) `thenD` assoc' `thenD` (wire `beside` bend) `thenD` unitR
--     inputs = [(a, b) | a <- [False, True], b <- [False, True]]
-- in ( and [runDiagram snakeR i == runDiagram wire i | i <- inputs]
--    , and [runDiagram snakeL i == runDiagram wire i | i <- inputs]
--    )
-- :}
-- (True,True)

-- | Turn a diagram around: dual in the compact closed sense.
turn :: Diagram a da b db -> Diagram db b da a
turn :: forall a da b db. Diagram a da b db -> Diagram db b da a
turn (Diagram Diagram_ a da b db
f) = Diagram_ db b da a -> Diagram db b da a
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram (Diagram_ a da b db -> Diagram_ db b da a
forall a da b db. Diagram_ a da b db -> Diagram_ db b da a
Turn_ Diagram_ a da b db
f)

-- | Left unitor: @I \u2297 A -> A@.
unitL :: Diagram ((), a) ((), da) a da
unitL :: forall a da. Diagram ((), a) ((), da) a da
unitL = Diagram_ ((), a) ((), da) a da -> Diagram ((), a) ((), da) a da
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram Diagram_ ((), a) ((), da) a da
forall a da. Diagram_ ((), a) ((), da) a da
UnitL_

-- | Inverse left unitor: @A -> I \u2297 A@.
unitL' :: Diagram a da ((), a) ((), da)
unitL' :: forall a da. Diagram a da ((), a) ((), da)
unitL' = Diagram_ a da ((), a) ((), da) -> Diagram a da ((), a) ((), da)
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram Diagram_ a da ((), a) ((), da)
forall a da. Diagram_ a da ((), a) ((), da)
UnitL'_

-- | Right unitor: @A \u2297 I -> A@.
unitR :: Diagram (a, ()) (da, ()) a da
unitR :: forall a da. Diagram (a, ()) (da, ()) a da
unitR = Diagram_ (a, ()) (da, ()) a da -> Diagram (a, ()) (da, ()) a da
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram Diagram_ (a, ()) (da, ()) a da
forall a da. Diagram_ (a, ()) (da, ()) a da
UnitR_

-- | Inverse right unitor: @A -> A \u2297 I@.
unitR' :: Diagram a da (a, ()) (da, ())
unitR' :: forall a da. Diagram a da (a, ()) (da, ())
unitR' = Diagram_ a da (a, ()) (da, ()) -> Diagram a da (a, ()) (da, ())
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram Diagram_ a da (a, ()) (da, ())
forall a da. Diagram_ a da (a, ()) (da, ())
UnitR'_

-- | Associator: @A \u2297 (B \u2297 C) -> (A \u2297 B) \u2297 C@.
assoc ::
  Diagram (a, (b, c)) (da, (db, dc)) ((a, b), c) ((da, db), dc)
assoc :: forall a b c da db dc.
Diagram (a, (b, c)) (da, (db, dc)) ((a, b), c) ((da, db), dc)
assoc = Diagram_ (a, (b, c)) (da, (db, dc)) ((a, b), c) ((da, db), dc)
-> Diagram (a, (b, c)) (da, (db, dc)) ((a, b), c) ((da, db), dc)
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram Diagram_ (a, (b, c)) (da, (db, dc)) ((a, b), c) ((da, db), dc)
forall a b da db db dc.
Diagram_ (a, (b, da)) (db, (db, dc)) ((a, b), da) ((db, db), dc)
Assoc_

-- | Inverse associator: @(A \u2297 B) \u2297 C -> A \u2297 (B \u2297 C)@.
assoc' ::
  Diagram ((a, b), c) ((da, db), dc) (a, (b, c)) (da, (db, dc))
assoc' :: forall a b c da db dc.
Diagram ((a, b), c) ((da, db), dc) (a, (b, c)) (da, (db, dc))
assoc' = Diagram_ ((a, b), c) ((da, db), dc) (a, (b, c)) (da, (db, dc))
-> Diagram ((a, b), c) ((da, db), dc) (a, (b, c)) (da, (db, dc))
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram Diagram_ ((a, b), c) ((da, db), dc) (a, (b, c)) (da, (db, dc))
forall a b da db db dc.
Diagram_ ((a, b), da) ((db, db), dc) (a, (b, da)) (db, (db, dc))
Assoc'_

-- | Symmetric braiding: @A \u2297 B -> B \u2297 A@.
swap ::
  Diagram (a, b) (da, db) (b, a) (db, da)
swap :: forall a b da db. Diagram (a, b) (da, db) (b, a) (db, da)
swap = Diagram_ (a, b) (da, db) (b, a) (db, da)
-> Diagram (a, b) (da, db) (b, a) (db, da)
forall a da b db. Diagram_ a da b db -> Diagram a da b db
Diagram Diagram_ (a, b) (da, db) (b, a) (db, da)
forall a b da db. Diagram_ (a, b) (da, db) (b, a) (db, da)
Swap_

-- | Run a closed string diagram on a concrete input.
--
-- The input is a forward value together with a backward cotangent; the
-- output is the backward cotangent on the input side together with the
-- forward value on the output side.
runDiagram :: Diagram a da b db -> (a, db) -> (da, b)
runDiagram :: forall a da b db. Diagram a da b db -> (a, db) -> (da, b)
runDiagram Diagram a da b db
d = Syntax (SigCompose :+: SigYank (,)) (->) (a, db) (da, b)
-> (a, db) -> (da, b)
forall (arr :: * -> * -> *) (sig :: Sig) a b.
(Category arr, Algebra sig arr arr, Ctx sig arr arr) =>
Syntax sig arr a b -> arr a b
eval (IntMorph (,) (Trace (,) (->)) a da b db
-> Syntax (SigCompose :+: SigYank (,)) (->) (a, db) (da, b)
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
IntMorph t arr ap am bp bm -> arr (t ap bm) (t am bp)
runIntMorph (Diagram a da b db -> IntMorph (,) (Trace (,) (->)) a da b db
forall a da b db.
Diagram a da b db -> IntMorph (,) (Trace (,) (->)) a da b db
toIntMorph Diagram a da b db
d))

-- Internal helpers (reused from the previous shallow-embedding definitions).

turnInt ::
  IntMorph (,) (Trace (,) (->)) a da b db ->
  IntMorph (,) (Trace (,) (->)) db b da a
turnInt :: forall a da b db.
IntMorph (,) (Trace (,) (->)) a da b db
-> IntMorph (,) (Trace (,) (->)) db b da a
turnInt (IntMorph Trace (,) (->) (a, db) (da, b)
f) = Trace (,) (->) (db, a) (b, da)
-> IntMorph (,) (Trace (,) (->)) db b da a
forall (t :: * -> * -> *) (arr :: * -> * -> *) ap am bp bm.
arr (t ap bm) (t am bp) -> IntMorph t arr ap am bp bm
IntMorph (((da, b) -> (b, da)) -> Trace (,) (->) (da, b) (b, da)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (da, b) -> (b, da)
forall a b. (a, b) -> (b, a)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k).
Action t arr =>
arr (t a b) (t b a)
M.braid Trace (,) (->) (da, b) (b, da)
-> Trace (,) (->) (a, db) (da, b) -> Trace (,) (->) (a, db) (b, da)
forall b c a.
Trace (,) (->) b c -> Trace (,) (->) a b -> Trace (,) (->) a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
Cat.. Trace (,) (->) (a, db) (da, b)
f Trace (,) (->) (a, db) (b, da)
-> Trace (,) (->) (db, a) (a, db) -> Trace (,) (->) (db, a) (b, da)
forall b c a.
Trace (,) (->) b c -> Trace (,) (->) a b -> Trace (,) (->) a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
Cat.. ((db, a) -> (a, db)) -> Trace (,) (->) (db, a) (a, db)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (db, a) -> (a, db)
forall a b. (a, b) -> (b, a)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k).
Action t arr =>
arr (t a b) (t b a)
M.braid)