{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans -Wno-partial-fields #-}

-- | The free symmetric monoidal category with a bimonoid over a primitive set.
--
-- 'Net' extends 'SMC' with structural rows for the bimonoid
-- operations: copy, discard, addition, and zero.  Where 'Trace' keeps
-- only 'base' and 'yank' in normal form, 'Net' keeps the wiring
-- inspectable — the difference between wiring you can read backwards and
-- wiring that has been melted into a single loop.
--
-- The bimonoid rows are the dagger's fixed structure: they are owned by
-- "Circuit.Dagger", and 'Bm.BimonoidT' is exactly the precondition that
-- lets 'Net' mirror over 'Dg.Dagger' (see 'mirror').
--
-- @
-- Free = Lift + Compose
-- SMC  = Free + Par + Swap
-- Net  = SMC + Copy + Discard + Plus + Zero
-- @
--
-- 'run' @Net@ interprets a 'Net' to a plain arrow.  'melt' interprets the
-- structural rows into the free 'Trace' syntax.
module Circuit.Net
  ( -- * Net
    Net,

    -- * Smart constructors
    lift,
    braid,

    -- * Conversion
    widen,
    sift,

    -- * Interpretation
    melt,

    -- * Dagger
    mirror,

    -- * Bimonoid syntax fragments (re-exported compatibility aliases)
    AlgRelevant,
    AlgAffine,
    AlgCartesian,
    AlgCoRelevant,
    AlgCoAffine,
    AlgCocartesian,
    AlgBimonoidal,
    AlgNet,
  )
where

import Circuit.Bimonoid
  ( SigCopy (..),
    SigDiscard (..),
    SigPlus (..),
    SigZero (..),
  )
import Circuit.Bimonoid qualified as Bm
import Circuit.Category (Category (..), (.>))
import Circuit.Channel (Channel (..), Strength (..), Traced (..))
import Circuit.Dagger qualified as Dg
import Circuit.Layer (Layer (..), run, (:~>))
import Circuit.SMC (FreeSMC, SMC, SigPar (..), SigSwap (..))
import Circuit.SMC qualified as SMC
import Circuit.Syntax (Algebra (..), SigCompose (..), Syntax (..), evalInto, (:+:) (..))
import Circuit.Tensor (Action, Tensor (..), Unit)
import Circuit.Trace (Trace, base, yank)
import Data.Kind (Type)
import Prelude hiding (id, (.))

-- $setup
-- >>> import Circuit.Dagger qualified as Dg
-- >>> import Circuit.Layer (bind, run, unit)
-- >>> import Circuit.Net
-- >>> import Circuit.Trace (Trace, base, yank)
-- >>> import Circuit.Syntax (eval, evalInto)
-- >>> import Circuit.SMC hiding (lift)
-- >>> import Circuit.SMC qualified as SMC
-- >>> import Circuit.Category ((.))
-- >>> import Prelude hiding (id, (.))

-- | The free symmetric monoidal category with a bimonoid.
--
-- 'Net' is the free 'Syntax' over the signature sum
--
-- @
-- 'SigCompose' ':+:' 'SigPar' w ':+:' 'SigSwap' w ':+:' 'SigCopy' w ':+:' 'SigDiscard' w ':+:' 'SigPlus' w ':+:' 'SigZero' w
-- @
--
-- The 'Lift' constructor embeds a base arrow; the 'Op' constructor holds
-- one of the signature nodes.  Smart constructors 'lift' and 'braid'
-- build the common cases, and 'widen' embeds an entire 'SMC' circuit.
type Net (w :: Type -> Type -> Type) arr =
  Syntax (SigCompose :+: SigPar w :+: SigSwap w :+: SigCopy w :+: SigDiscard w :+: SigPlus w :+: SigZero w) arr

-- | Free relevant symmetric monoidal category over wiring tensor @w@.
type AlgRelevant w arr = Syntax (SigCompose :+: SigPar w :+: SigSwap w :+: SigCopy w) arr

-- | Free affine symmetric monoidal category over wiring tensor @w@.
type AlgAffine w arr = Syntax (SigCompose :+: SigPar w :+: SigSwap w :+: SigDiscard w) arr

-- | Free cartesian symmetric monoidal category over wiring tensor @w@.
type AlgCartesian w arr = Syntax (SigCompose :+: SigPar w :+: SigSwap w :+: SigCopy w :+: SigDiscard w) arr

-- | Free co-relevant symmetric monoidal category over wiring tensor @w@.
type AlgCoRelevant w arr = Syntax (SigCompose :+: SigPar w :+: SigSwap w :+: SigPlus w) arr

-- | Free co-affine symmetric monoidal category over wiring tensor @w@.
type AlgCoAffine w arr = Syntax (SigCompose :+: SigPar w :+: SigSwap w :+: SigZero w) arr

-- | Free cocartesian symmetric monoidal category over wiring tensor @w@.
type AlgCocartesian w arr = Syntax (SigCompose :+: SigPar w :+: SigSwap w :+: SigPlus w :+: SigZero w) arr

-- | Free bimonoidal category over wiring tensor @w@.
type AlgBimonoidal w arr = Syntax (SigCompose :+: SigPar w :+: SigSwap w :+: SigCopy w :+: SigDiscard w :+: SigPlus w :+: SigZero w) arr

-- | Synonym for the full 'Net' syntax.
type AlgNet w arr = Net w arr

-- | The 'Category' instance is the generic free-category instance:
-- 'id' is a lifted identity and composition is a 'SigCompose' node.
instance (Category arr) => Category (Net w arr) where
  id :: forall a. Net w arr a a
id = arr a a
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr
     a
     a
forall (arr :: * -> * -> *) a b (sig :: Sig).
arr a b -> Syntax sig arr a b
Lift arr a a
forall a. arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id
  Net w arr b c
f . :: forall b c a. Net w arr b c -> Net w arr a b -> Net w arr a c
. Net w arr a b
g = (:+:)
  SigCompose
  (SigPar w
   :+: (SigSwap w
        :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
  arr
  (Net w arr)
  a
  c
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr
     a
     c
forall (sig :: Sig) (arr :: * -> * -> *) a b.
sig arr (Syntax sig arr) a b -> Syntax sig arr a b
Op (SigCompose arr (Net w arr) a c
-> (:+:)
     SigCompose
     (SigPar w
      :+: (SigSwap w
           :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
     arr
     (Net w arr)
     a
     c
forall {k} {k1} {k2} {k3} (sig1 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig2 :: k -> k1 -> k2 -> k3 -> *).
sig1 arr rec a b -> (:+:) sig1 sig2 arr rec a b
L (Net w arr b c -> Net w arr a b -> SigCompose arr (Net w arr) a c
forall {k1} {k} (rec :: k1 -> k1 -> *) (b1 :: k1) (b :: k1)
       (a :: k1) (arr :: k).
rec b1 b -> rec a b1 -> SigCompose arr rec a b
SigCompose Net w arr b c
f Net w arr a b
g))

-- | Lift a base arrow into 'Net'.
lift :: arr a b -> Net w arr a b
lift :: forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> Net w arr a b
lift = arr a b
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr
     a
     b
forall (arr :: * -> * -> *) a b (sig :: Sig).
arr a b -> Syntax sig arr a b
Lift

-- | Symmetric braiding in 'Net'.
braid :: Net w arr (w a b) (w b a)
braid :: forall (w :: * -> * -> *) (arr :: * -> * -> *) a b.
Net w arr (w a b) (w b a)
braid = (:+:)
  SigCompose
  (SigPar w
   :+: (SigSwap w
        :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
  arr
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr)
  (w a b)
  (w b a)
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr
     (w a b)
     (w b a)
forall (sig :: Sig) (arr :: * -> * -> *) a b.
sig arr (Syntax sig arr) a b -> Syntax sig arr a b
Op ((:+:)
  (SigPar w)
  (SigSwap w
   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))
  arr
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr)
  (w a b)
  (w b a)
-> (:+:)
     SigCompose
     (SigPar w
      :+: (SigSwap w
           :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
     arr
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        arr)
     (w a b)
     (w b a)
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R ((:+:)
  (SigSwap w)
  (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))
  arr
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr)
  (w a b)
  (w b a)
-> (:+:)
     (SigPar w)
     (SigSwap w
      :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))
     arr
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        arr)
     (w a b)
     (w b a)
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R (SigSwap
  w
  arr
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr)
  (w a b)
  (w b a)
-> (:+:)
     (SigSwap w)
     (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))
     arr
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        arr)
     (w a b)
     (w b a)
forall {k} {k1} {k2} {k3} (sig1 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig2 :: k -> k1 -> k2 -> k3 -> *).
sig1 arr rec a b -> (:+:) sig1 sig2 arr rec a b
L SigSwap
  w
  arr
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr)
  (w a b)
  (w b a)
forall {k} {k1} (w :: * -> * -> *) (arr :: k) (rec :: k1) a1 b1.
SigSwap w arr rec (w a1 b1) (w b1 a1)
SigSwap)))

-- | Include an 'SMC' circuit into 'Net'.
--
-- The injection recurses through the SMC signature sum and rebuilds each node
-- in the larger 'Net' signature sum.  This gives the adjunction between 'SMC'
-- and 'Net' together with 'sift'.
--
-- >>> let m = SMC.lift (+1) . SMC.lift (*2) :: SMC (,) (->) Int Int
-- >>> run (widen m :: Net (,) (->) Int Int) 5
-- 11
--
-- Coherence: 'sift' projects 'widen' back to the original 'SMC'.
--
-- >>> eval (sift (widen m :: Net (,) (->) Int Int)) 5
-- 11
-- >>> eval m 5
-- 11
--
-- Coherence: 'melt' agrees with the function fold on 'SMC' circuits.
--
-- >>> eval (melt (widen m :: Net (,) (->) Int Int) :: Trace (,) (->) Int Int) 5
-- 11
-- >>> eval m 5
-- 11
--
-- Coherence: 'Net' folds through 'widen' match 'SMC' folds.
--
-- >>> let h f = f
-- >>> (bind h (widen m :: Net (,) (->) Int Int) :: Int -> Int) 5
-- 11
-- >>> (evalInto h m :: Int -> Int) 5
-- 11
--
-- Coherence: mirroring commutes with 'widen'.
--
-- >>> let dm = SMC.lift (Dg.Dagger (+1) (subtract 1)) . SMC.lift (Dg.Dagger (*2) (\x -> x `div` 2)) :: SMC (,) (Dg.Dagger (->)) Int Int
-- >>> Dg.front (Dg.transpose (eval dm)) 10
-- 4
-- >>> Dg.front (Dg.transpose (run (widen dm :: Net (,) (Dg.Dagger (->)) Int Int))) 10
-- 4
widen :: SMC w arr a b -> Net w arr a b
widen :: forall (w :: * -> * -> *) (arr :: * -> * -> *) a b.
SMC w arr a b -> Net w arr a b
widen (Lift arr a b
f) = arr a b
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr
     a
     b
forall (arr :: * -> * -> *) a b (sig :: Sig).
arr a b -> Syntax sig arr a b
Lift arr a b
f
widen (Op (:+:)
  SigCompose
  (SigPar w :+: SigSwap w)
  arr
  (Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) arr)
  a
  b
op) = case (:+:)
  SigCompose
  (SigPar w :+: SigSwap w)
  arr
  (Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) arr)
  a
  b
op of
  L (SigCompose Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) arr b1 b
g Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) arr a b1
f) -> (:+:)
  SigCompose
  (SigPar w
   :+: (SigSwap w
        :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
  arr
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr)
  a
  b
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr
     a
     b
forall (sig :: Sig) (arr :: * -> * -> *) a b.
sig arr (Syntax sig arr) a b -> Syntax sig arr a b
Op (SigCompose
  arr
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr)
  a
  b
-> (:+:)
     SigCompose
     (SigPar w
      :+: (SigSwap w
           :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
     arr
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        arr)
     a
     b
forall {k} {k1} {k2} {k3} (sig1 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig2 :: k -> k1 -> k2 -> k3 -> *).
sig1 arr rec a b -> (:+:) sig1 sig2 arr rec a b
L (Syntax
  (SigCompose
   :+: (SigPar w
        :+: (SigSwap w
             :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
  arr
  b1
  b
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr
     a
     b1
-> SigCompose
     arr
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        arr)
     a
     b
forall {k1} {k} (rec :: k1 -> k1 -> *) (b1 :: k1) (b :: k1)
       (a :: k1) (arr :: k).
rec b1 b -> rec a b1 -> SigCompose arr rec a b
SigCompose (Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) arr b1 b
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr
     b1
     b
forall (w :: * -> * -> *) (arr :: * -> * -> *) a b.
SMC w arr a b -> Net w arr a b
widen Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) arr b1 b
g) (Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) arr a b1
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr
     a
     b1
forall (w :: * -> * -> *) (arr :: * -> * -> *) a b.
SMC w arr a b -> Net w arr a b
widen Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) arr a b1
f)))
  R (L (SigPar Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) arr a1 b1
f Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) arr c d
g)) -> (:+:)
  SigCompose
  (SigPar w
   :+: (SigSwap w
        :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
  arr
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr)
  a
  b
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr
     a
     b
forall (sig :: Sig) (arr :: * -> * -> *) a b.
sig arr (Syntax sig arr) a b -> Syntax sig arr a b
Op ((:+:)
  (SigPar w)
  (SigSwap w
   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))
  arr
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr)
  a
  b
-> (:+:)
     SigCompose
     (SigPar w
      :+: (SigSwap w
           :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
     arr
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        arr)
     a
     b
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R (SigPar
  w
  arr
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr)
  a
  b
-> (:+:)
     (SigPar w)
     (SigSwap w
      :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))
     arr
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        arr)
     a
     b
forall {k} {k1} {k2} {k3} (sig1 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig2 :: k -> k1 -> k2 -> k3 -> *).
sig1 arr rec a b -> (:+:) sig1 sig2 arr rec a b
L (Syntax
  (SigCompose
   :+: (SigPar w
        :+: (SigSwap w
             :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
  arr
  a1
  b1
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr
     c
     d
-> SigPar
     w
     arr
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        arr)
     (w a1 c)
     (w b1 d)
forall {k} (rec :: * -> * -> *) a1 b1 c d (w :: * -> * -> *)
       (arr :: k).
rec a1 b1 -> rec c d -> SigPar w arr rec (w a1 c) (w b1 d)
SigPar (Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) arr a1 b1
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr
     a1
     b1
forall (w :: * -> * -> *) (arr :: * -> * -> *) a b.
SMC w arr a b -> Net w arr a b
widen Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) arr a1 b1
f) (Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) arr c d
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr
     c
     d
forall (w :: * -> * -> *) (arr :: * -> * -> *) a b.
SMC w arr a b -> Net w arr a b
widen Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) arr c d
g))))
  R (R SigSwap
  w arr (Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) arr) a b
SigSwap) -> (:+:)
  SigCompose
  (SigPar w
   :+: (SigSwap w
        :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
  arr
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr)
  a
  b
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr
     a
     b
forall (sig :: Sig) (arr :: * -> * -> *) a b.
sig arr (Syntax sig arr) a b -> Syntax sig arr a b
Op ((:+:)
  (SigPar w)
  (SigSwap w
   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))
  arr
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr)
  a
  b
-> (:+:)
     SigCompose
     (SigPar w
      :+: (SigSwap w
           :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
     arr
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        arr)
     a
     b
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R ((:+:)
  (SigSwap w)
  (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))
  arr
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr)
  a
  b
-> (:+:)
     (SigPar w)
     (SigSwap w
      :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))
     arr
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        arr)
     a
     b
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R (SigSwap
  w
  arr
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr)
  a
  b
-> (:+:)
     (SigSwap w)
     (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))
     arr
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        arr)
     a
     b
forall {k} {k1} {k2} {k3} (sig1 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig2 :: k -> k1 -> k2 -> k3 -> *).
sig1 arr rec a b -> (:+:) sig1 sig2 arr rec a b
L SigSwap
  w
  arr
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr)
  a
  b
SigSwap
  w
  arr
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr)
  (w a1 b1)
  (w b1 a1)
forall {k} {k1} (w :: * -> * -> *) (arr :: k) (rec :: k1) a1 b1.
SigSwap w arr rec (w a1 b1) (w b1 a1)
SigSwap)))

-- | Forget the bimonoid rows of a 'Net', keeping only the 'SMC' wiring.
--
-- 'sift' collapses the bimonoid rows into 'SMC.lift' while leaving
-- 'SigCompose' and 'SigPar' inspectable. Together with 'widen' it gives the
-- adjunction between 'SMC' and 'Net'.
-- Note the converse does not hold: @widen . sift ≠ id@ because 'sift'
-- forgets bimonoid structure.
sift ::
  forall w arr a b.
  (Action w arr) =>
  Net w arr a b ->
  SMC w arr a b
sift :: forall (w :: * -> * -> *) (arr :: * -> * -> *) a b.
Action w arr =>
Net w arr a b -> SMC w arr a b
sift = (forall x y.
 arr x y
 -> Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) arr x y)
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr
     a
     b
-> Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) arr a b
forall (arr' :: * -> * -> *) (sig :: Sig) (arr :: * -> * -> *) a b.
(Category arr', Algebra sig arr arr', Ctx sig arr arr') =>
(forall x y. arr x y -> arr' x y) -> Syntax sig arr a b -> arr' a b
evalInto arr x y -> SMC w arr x y
forall x y.
arr x y -> Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) arr x y
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
SMC.lift

-- | Melt the structural rows of a 'Net' into the free 'Trace' syntax.
--
-- The interpretation from the free symmetric monoidal category with
-- bimonoid to the free traced monoidal category.  Structural rows ('SigPar',
-- 'SigCopy', 'SigPlus', etc.) become opaque base-arrow operations wrapped in
-- 'base'; @SigCompose@ uses the 'Category' instance of 'Trace'.
--
-- @'run' @Net = 'Circuit.Syntax.eval' . 'melt'@.
--
-- >>> eval (melt (lift (+1) :: Net (,) (->) Int Int) :: Trace (,) (->) Int Int) 5
-- 6
melt ::
  forall w t arr a b.
  (Traced t arr, Action w arr) =>
  Net w arr a b ->
  Trace t arr a b
melt :: forall (w :: * -> * -> *) (t :: * -> * -> *) (arr :: * -> * -> *) a
       b.
(Traced t arr, Action w arr) =>
Net w arr a b -> Trace t arr a b
melt = (forall x y. arr x y -> Syntax (SigCompose :+: SigYank t) arr x y)
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr
     a
     b
-> Syntax (SigCompose :+: SigYank t) arr a b
forall (arr' :: * -> * -> *) (sig :: Sig) (arr :: * -> * -> *) a b.
(Category arr', Algebra sig arr arr', Ctx sig arr arr') =>
(forall x y. arr x y -> arr' x y) -> Syntax sig arr a b -> arr' a b
evalInto arr x y -> Trace t arr x y
forall x y. arr x y -> Syntax (SigCompose :+: SigYank t) arr x y
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base

-- | Mirror a 'Net' over 'Dg.Dagger'.
--
-- The dagger dualizes the bimonoid rows: 'SigCopy' becomes 'SigPlus',
-- 'SigDiscard' becomes 'SigZero', and vice versa.  Composition is reversed;
-- parallel composition and the braiding are self-dual.
--
-- This operation is total exactly when the base arrow carries a bimonoid
-- on the wiring tensor for every object, i.e. when
-- @'Bm.BimonoidT' w arr x@ holds for all @x@.  That precondition is the
-- tensor-generic form of the 'Dg.Bimonoid' law that makes 'Dagger' and the
-- bimonoid rows presentable as one structure.
mirror ::
  forall w arr a b.
  (forall x. Bm.BimonoidT w arr x) =>
  Net w (Dg.Dagger arr) a b ->
  Net w (Dg.Dagger arr) b a
mirror :: forall (w :: * -> * -> *) (arr :: * -> * -> *) a b.
(forall x. BimonoidT w arr x) =>
Net w (Dagger arr) a b -> Net w (Dagger arr) b a
mirror (Lift Dagger arr a b
d) = Dagger arr b a
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr)
     b
     a
forall (arr :: * -> * -> *) a b (sig :: Sig).
arr a b -> Syntax sig arr a b
Lift (Dagger arr a b -> Dagger arr b a
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
Dagger arr a b -> Dagger arr b a
Dg.transpose Dagger arr a b
d)
mirror (Op (:+:)
  SigCompose
  (SigPar w
   :+: (SigSwap w
        :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  a
  b
op) = case (:+:)
  SigCompose
  (SigPar w
   :+: (SigSwap w
        :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  a
  b
op of
  L (SigCompose Syntax
  (SigCompose
   :+: (SigPar w
        :+: (SigSwap w
             :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
  (Dagger arr)
  b1
  b
g Syntax
  (SigCompose
   :+: (SigPar w
        :+: (SigSwap w
             :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
  (Dagger arr)
  a
  b1
f) -> (:+:)
  SigCompose
  (SigPar w
   :+: (SigSwap w
        :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr)
     b
     a
forall (sig :: Sig) (arr :: * -> * -> *) a b.
sig arr (Syntax sig arr) a b -> Syntax sig arr a b
Op (SigCompose
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     SigCompose
     (SigPar w
      :+: (SigSwap w
           :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig1 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig2 :: k -> k1 -> k2 -> k3 -> *).
sig1 arr rec a b -> (:+:) sig1 sig2 arr rec a b
L (Syntax
  (SigCompose
   :+: (SigPar w
        :+: (SigSwap w
             :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
  (Dagger arr)
  b1
  a
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr)
     b
     b1
-> SigCompose
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k1} {k} (rec :: k1 -> k1 -> *) (b1 :: k1) (b :: k1)
       (a :: k1) (arr :: k).
rec b1 b -> rec a b1 -> SigCompose arr rec a b
SigCompose (Syntax
  (SigCompose
   :+: (SigPar w
        :+: (SigSwap w
             :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
  (Dagger arr)
  a
  b1
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr)
     b1
     a
forall (w :: * -> * -> *) (arr :: * -> * -> *) a b.
(forall x. BimonoidT w arr x) =>
Net w (Dagger arr) a b -> Net w (Dagger arr) b a
mirror Syntax
  (SigCompose
   :+: (SigPar w
        :+: (SigSwap w
             :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
  (Dagger arr)
  a
  b1
f) (Syntax
  (SigCompose
   :+: (SigPar w
        :+: (SigSwap w
             :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
  (Dagger arr)
  b1
  b
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr)
     b
     b1
forall (w :: * -> * -> *) (arr :: * -> * -> *) a b.
(forall x. BimonoidT w arr x) =>
Net w (Dagger arr) a b -> Net w (Dagger arr) b a
mirror Syntax
  (SigCompose
   :+: (SigPar w
        :+: (SigSwap w
             :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
  (Dagger arr)
  b1
  b
g)))
  R (L (SigPar Syntax
  (SigCompose
   :+: (SigPar w
        :+: (SigSwap w
             :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
  (Dagger arr)
  a1
  b1
f Syntax
  (SigCompose
   :+: (SigPar w
        :+: (SigSwap w
             :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
  (Dagger arr)
  c
  d
g)) -> (:+:)
  SigCompose
  (SigPar w
   :+: (SigSwap w
        :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr)
     b
     a
forall (sig :: Sig) (arr :: * -> * -> *) a b.
sig arr (Syntax sig arr) a b -> Syntax sig arr a b
Op ((:+:)
  (SigPar w)
  (SigSwap w
   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     SigCompose
     (SigPar w
      :+: (SigSwap w
           :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R (SigPar
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     (SigPar w)
     (SigSwap w
      :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig1 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig2 :: k -> k1 -> k2 -> k3 -> *).
sig1 arr rec a b -> (:+:) sig1 sig2 arr rec a b
L (Syntax
  (SigCompose
   :+: (SigPar w
        :+: (SigSwap w
             :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
  (Dagger arr)
  b1
  a1
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr)
     d
     c
-> SigPar
     w
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     (w b1 d)
     (w a1 c)
forall {k} (rec :: * -> * -> *) a1 b1 c d (w :: * -> * -> *)
       (arr :: k).
rec a1 b1 -> rec c d -> SigPar w arr rec (w a1 c) (w b1 d)
SigPar (Syntax
  (SigCompose
   :+: (SigPar w
        :+: (SigSwap w
             :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
  (Dagger arr)
  a1
  b1
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr)
     b1
     a1
forall (w :: * -> * -> *) (arr :: * -> * -> *) a b.
(forall x. BimonoidT w arr x) =>
Net w (Dagger arr) a b -> Net w (Dagger arr) b a
mirror Syntax
  (SigCompose
   :+: (SigPar w
        :+: (SigSwap w
             :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
  (Dagger arr)
  a1
  b1
f) (Syntax
  (SigCompose
   :+: (SigPar w
        :+: (SigSwap w
             :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
  (Dagger arr)
  c
  d
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr)
     d
     c
forall (w :: * -> * -> *) (arr :: * -> * -> *) a b.
(forall x. BimonoidT w arr x) =>
Net w (Dagger arr) a b -> Net w (Dagger arr) b a
mirror Syntax
  (SigCompose
   :+: (SigPar w
        :+: (SigSwap w
             :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
  (Dagger arr)
  c
  d
g))))
  R (R (L SigSwap
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  a
  b
SigSwap)) -> (:+:)
  SigCompose
  (SigPar w
   :+: (SigSwap w
        :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr)
     b
     a
forall (sig :: Sig) (arr :: * -> * -> *) a b.
sig arr (Syntax sig arr) a b -> Syntax sig arr a b
Op ((:+:)
  (SigPar w)
  (SigSwap w
   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     SigCompose
     (SigPar w
      :+: (SigSwap w
           :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R ((:+:)
  (SigSwap w)
  (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     (SigPar w)
     (SigSwap w
      :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R (SigSwap
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     (SigSwap w)
     (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig1 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig2 :: k -> k1 -> k2 -> k3 -> *).
sig1 arr rec a b -> (:+:) sig1 sig2 arr rec a b
L SigSwap
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
SigSwap
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  (w b1 a1)
  (w a1 b1)
forall {k} {k1} (w :: * -> * -> *) (arr :: k) (rec :: k1) a1 b1.
SigSwap w arr rec (w a1 b1) (w b1 a1)
SigSwap)))
  R (R (R (L SigCopy
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  a
  b
SigCopy))) -> (:+:)
  SigCompose
  (SigPar w
   :+: (SigSwap w
        :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr)
     b
     a
forall (sig :: Sig) (arr :: * -> * -> *) a b.
sig arr (Syntax sig arr) a b -> Syntax sig arr a b
Op ((:+:)
  (SigPar w)
  (SigSwap w
   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     SigCompose
     (SigPar w
      :+: (SigSwap w
           :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R ((:+:)
  (SigSwap w)
  (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     (SigPar w)
     (SigSwap w
      :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R ((:+:)
  (SigCopy w)
  (SigDiscard w :+: (SigPlus w :+: SigZero w))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     (SigSwap w)
     (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R ((:+:)
  (SigDiscard w)
  (SigPlus w :+: SigZero w)
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     (SigCopy w)
     (SigDiscard w :+: (SigPlus w :+: SigZero w))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R ((:+:)
  (SigPlus w)
  (SigZero w)
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     (SigDiscard w)
     (SigPlus w :+: SigZero w)
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R (SigPlus
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     (SigPlus w)
     (SigZero w)
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig1 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig2 :: k -> k1 -> k2 -> k3 -> *).
sig1 arr rec a b -> (:+:) sig1 sig2 arr rec a b
L SigPlus
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
SigPlus
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  (w a a)
  a
forall {k} (w :: * -> * -> *) (arr :: * -> * -> *) b (rec :: k).
MergeT w arr b =>
SigPlus w arr rec (w b b) b
SigPlus))))))
  R (R (R (R (L SigDiscard
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  a
  b
SigDiscard)))) -> (:+:)
  SigCompose
  (SigPar w
   :+: (SigSwap w
        :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr)
     b
     a
forall (sig :: Sig) (arr :: * -> * -> *) a b.
sig arr (Syntax sig arr) a b -> Syntax sig arr a b
Op ((:+:)
  (SigPar w)
  (SigSwap w
   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     SigCompose
     (SigPar w
      :+: (SigSwap w
           :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R ((:+:)
  (SigSwap w)
  (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     (SigPar w)
     (SigSwap w
      :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R ((:+:)
  (SigCopy w)
  (SigDiscard w :+: (SigPlus w :+: SigZero w))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     (SigSwap w)
     (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R ((:+:)
  (SigDiscard w)
  (SigPlus w :+: SigZero w)
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     (SigCopy w)
     (SigDiscard w :+: (SigPlus w :+: SigZero w))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R ((:+:)
  (SigPlus w)
  (SigZero w)
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     (SigDiscard w)
     (SigPlus w :+: SigZero w)
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R (SigZero
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     (SigPlus w)
     (SigZero w)
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R SigZero
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
SigZero
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  (Unit w)
  a
forall {k} (w :: * -> * -> *) (arr :: * -> * -> *) b (rec :: k).
ZeroT w arr b =>
SigZero w arr rec (Unit w) b
SigZero))))))
  R (R (R (R (R (L SigPlus
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  a
  b
SigPlus))))) -> (:+:)
  SigCompose
  (SigPar w
   :+: (SigSwap w
        :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr)
     b
     a
forall (sig :: Sig) (arr :: * -> * -> *) a b.
sig arr (Syntax sig arr) a b -> Syntax sig arr a b
Op ((:+:)
  (SigPar w)
  (SigSwap w
   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     SigCompose
     (SigPar w
      :+: (SigSwap w
           :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R ((:+:)
  (SigSwap w)
  (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     (SigPar w)
     (SigSwap w
      :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R ((:+:)
  (SigCopy w)
  (SigDiscard w :+: (SigPlus w :+: SigZero w))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     (SigSwap w)
     (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R (SigCopy
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     (SigCopy w)
     (SigDiscard w :+: (SigPlus w :+: SigZero w))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig1 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig2 :: k -> k1 -> k2 -> k3 -> *).
sig1 arr rec a b -> (:+:) sig1 sig2 arr rec a b
L SigCopy
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
SigCopy
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  (w b b)
forall {k} (w :: * -> * -> *) (arr :: * -> * -> *) a (rec :: k).
CopyT w arr a =>
SigCopy w arr rec a (w a a)
SigCopy))))
  R (R (R (R (R (R SigZero
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  a
  b
SigZero))))) -> (:+:)
  SigCompose
  (SigPar w
   :+: (SigSwap w
        :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr)
     b
     a
forall (sig :: Sig) (arr :: * -> * -> *) a b.
sig arr (Syntax sig arr) a b -> Syntax sig arr a b
Op ((:+:)
  (SigPar w)
  (SigSwap w
   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     SigCompose
     (SigPar w
      :+: (SigSwap w
           :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R ((:+:)
  (SigSwap w)
  (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     (SigPar w)
     (SigSwap w
      :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R ((:+:)
  (SigCopy w)
  (SigDiscard w :+: (SigPlus w :+: SigZero w))
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     (SigSwap w)
     (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R ((:+:)
  (SigDiscard w)
  (SigPlus w :+: SigZero w)
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     (SigCopy w)
     (SigDiscard w :+: (SigPlus w :+: SigZero w))
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig2 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig1 :: k -> k1 -> k2 -> k3 -> *).
sig2 arr rec a b -> (:+:) sig1 sig2 arr rec a b
R (SigDiscard
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
-> (:+:)
     (SigDiscard w)
     (SigPlus w :+: SigZero w)
     (Dagger arr)
     (Syntax
        (SigCompose
         :+: (SigPar w
              :+: (SigSwap w
                   :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
        (Dagger arr))
     b
     a
forall {k} {k1} {k2} {k3} (sig1 :: k -> k1 -> k2 -> k3 -> *)
       (arr :: k) (rec :: k1) (a :: k2) (b :: k3)
       (sig2 :: k -> k1 -> k2 -> k3 -> *).
sig1 arr rec a b -> (:+:) sig1 sig2 arr rec a b
L SigDiscard
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  a
SigDiscard
  w
  (Dagger arr)
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     (Dagger arr))
  b
  (Unit w)
forall {k} (w :: * -> * -> *) (arr :: * -> * -> *) a (rec :: k).
DiscardT w arr a =>
SigDiscard w arr rec a (Unit w)
SigDiscard)))))

-- | Free symmetric monoidal category with a bimonoid.
--
-- Structural rows are interpreted in the target category: parallel
-- composition uses 'tensor', braiding uses 'braid', and the bimonoid
-- generators are the images under @h@ of the source dictionaries carried
-- by the 'SigCopy', 'SigDiscard', 'SigPlus', and 'SigZero' constructors.
--
-- [Conditional] 'bind' @h@ interprets bimonoid generators as images under
-- @h@ of the source arrow's dictionaries.  This is the free-PROP fold
-- only when @h@ is a bimonoid homomorphism (automatic for the generator
-- embedding, but must be verified for custom @h@).
instance Layer (Syntax (SigCompose :+: SigPar w :+: SigSwap w :+: SigCopy w :+: SigDiscard w :+: SigPlus w :+: SigZero w)) where
  type Law (Syntax (SigCompose :+: SigPar w :+: SigSwap w :+: SigCopy w :+: SigDiscard w :+: SigPlus w :+: SigZero w)) arr' = FreeSMC w arr'
  type Run (Syntax (SigCompose :+: SigPar w :+: SigSwap w :+: SigCopy w :+: SigDiscard w :+: SigPlus w :+: SigZero w)) arr = Action w arr
  type Bind (Syntax (SigCompose :+: SigPar w :+: SigSwap w :+: SigCopy w :+: SigDiscard w :+: SigPlus w :+: SigZero w)) arr = ()
  unit :: forall (arr :: * -> * -> *).
Category arr =>
arr
:~> Syntax
      (SigCompose
       :+: (SigPar w
            :+: (SigSwap w
                 :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
      arr
unit = arr x y -> Net w arr x y
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> Net w arr a b
lift
  bind ::
    forall arr' arr a b.
    (Law (Syntax (SigCompose :+: SigPar w :+: SigSwap w :+: SigCopy w :+: SigDiscard w :+: SigPlus w :+: SigZero w)) arr') =>
    (arr :~> arr') ->
    Syntax (SigCompose :+: SigPar w :+: SigSwap w :+: SigCopy w :+: SigDiscard w :+: SigPlus w :+: SigZero w) arr a b ->
    arr' a b
  bind :: forall (arr' :: * -> * -> *) (arr :: * -> * -> *) a b.
Law
  (Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w
                     :+: (SigDiscard w :+: (SigPlus w :+: SigZero w)))))))
  arr' =>
(arr :~> arr')
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr
     a
     b
-> arr' a b
bind arr :~> arr'
h = (arr :~> arr')
-> Syntax
     (SigCompose
      :+: (SigPar w
           :+: (SigSwap w
                :+: (SigCopy w :+: (SigDiscard w :+: (SigPlus w :+: SigZero w))))))
     arr
     a
     b
-> arr' a b
forall (arr' :: * -> * -> *) (sig :: Sig) (arr :: * -> * -> *) a b.
(Category arr', Algebra sig arr arr', Ctx sig arr arr') =>
(forall x y. arr x y -> arr' x y) -> Syntax sig arr a b -> arr' a b
evalInto arr x y -> arr' x y
arr :~> arr'
h