{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Free symmetric monoidal category syntax.
--
-- This module packages the symmetric-monoidal layer on top of the generic
-- free-construction substrate in "Circuit.Syntax". The signature sum is
--
-- @
-- 'SigCompose' ':+:' 'SigPar' w ':+:' 'SigSwap' w
-- @
--
-- where 'SigCompose' provides sequential composition, 'SigPar' w provides
-- parallel composition over the wiring tensor @w@, and 'SigSwap' w provides
-- the symmetry / braiding.
--
-- The 'Tensor' and 'Action' instances are the syntactic constructors:
-- @'Tensor.tensor' f g@ builds a 'SigPar' node and @'Action.braid'@ builds a
-- 'SigSwap' node. Folding uses 'Circuit.Syntax.eval' or
-- 'Circuit.Syntax.evalInto'.
module Circuit.SMC
  ( -- * Free symmetric monoidal category
    SMC,
    lift,

    -- * Dagger mirror
    mirror,

    -- * Constraint synonym used by Net's Layer law
    FreeSMC,

    -- * Signatures (exported for other syntax layers)
    SigPar (..),
    SigSwap (..),
  )
where

import Circuit.Category (Category (..))
import Circuit.Channel (Channel (..), Strength (..), Traced (..))
import Circuit.Dagger qualified as Dg
import Circuit.Syntax
  ( Algebra (..),
    SigCompose (..),
    Syntax (..),
    eval,
    (:+:) (..),
  )
import Circuit.Tensor (Action, Tensor, Unit, Unital)
import Circuit.Tensor qualified as T
import Data.Kind (Type)
import Prelude hiding (id, (.))

-- Signatures

-- | Parallel composition over the wiring tensor @w@.
data SigPar (w :: Type -> Type -> Type) arr rec a b where
  SigPar ::
    rec a b ->
    rec c d ->
    SigPar w arr rec (w a c) (w b d)

instance (Tensor w arr') => Algebra (SigPar w) arr arr' where
  type Ctx (SigPar w) arr arr' = Tensor w arr'
  alg :: forall (rec :: * -> * -> *) a b.
Ctx (SigPar w) arr arr' =>
(forall x y. arr x y -> arr' x y)
-> (forall x y. rec x y -> arr' x y)
-> SigPar w arr rec a b
-> arr' a b
alg forall x y. arr x y -> arr' x y
_ forall x y. rec x y -> arr' x y
rec (SigPar rec a b
f rec c d
g) = arr' a b -> arr' c d -> arr' (w a c) (w b d)
forall a b c d. arr' a b -> arr' c d -> arr' (w a c) (w b d)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k) (d :: k).
Tensor t arr =>
arr a b -> arr c d -> arr (t a c) (t b d)
T.tensor (rec a b -> arr' a b
forall x y. rec x y -> arr' x y
rec rec a b
f) (rec c d -> arr' c d
forall x y. rec x y -> arr' x y
rec rec c d
g)

-- | Symmetric braiding over the wiring tensor @w@.
data SigSwap (w :: Type -> Type -> Type) arr rec a b where
  SigSwap :: SigSwap w arr rec (w a b) (w b a)

instance (Action w arr') => Algebra (SigSwap w) arr arr' where
  type Ctx (SigSwap w) arr arr' = Action w arr'
  alg :: forall (rec :: * -> * -> *) a b.
Ctx (SigSwap w) arr arr' =>
(forall x y. arr x y -> arr' x y)
-> (forall x y. rec x y -> arr' x y)
-> SigSwap w arr rec a b
-> arr' a b
alg forall x y. arr x y -> arr' x y
_ forall x y. rec x y -> arr' x y
_ SigSwap w arr rec a b
SigSwap = arr' a b
arr' (w a b) (w b a)
forall a b. arr' (w a b) (w 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)
T.braid

-- Free symmetric monoidal category

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

-- | Lift a base arrow into the free symmetric monoidal category.
lift :: arr a b -> SMC w arr a b
lift :: forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift = arr a b -> Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) arr a b
forall (arr :: * -> * -> *) a b (sig :: Sig).
arr a b -> Syntax sig arr a b
Lift

-- Instances for the free symmetric monoidal category

instance (Category arr) => Category (SMC w arr) where
  id :: forall a. SMC w arr a a
id = arr a a -> SMC w arr a a
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w 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
  SMC w arr b c
f . :: forall b c a. SMC w arr b c -> SMC w arr a b -> SMC w arr a c
. SMC w arr a b
g = (:+:) SigCompose (SigPar w :+: SigSwap w) arr (SMC w arr) a c
-> Syntax (SigCompose :+: (SigPar w :+: SigSwap 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 (SMC w arr) a c
-> (:+:) SigCompose (SigPar w :+: SigSwap w) arr (SMC 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 (SMC w arr b c -> SMC w arr a b -> SigCompose arr (SMC 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 SMC w arr b c
f SMC w arr a b
g))

instance (Unital w arr) => Unital w (SMC w arr) where
  unitl :: forall a. SMC w arr (w (Unit w) a) a
unitl = arr (w (Unit w) a) a
-> Syntax
     (SigCompose :+: (SigPar w :+: SigSwap w)) arr (w (Unit w) a) a
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift arr (w (Unit w) a) a
forall a. arr (w (Unit w) a) a
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr (t (Unit t) a) a
T.unitl
  unitl' :: forall a. SMC w arr a (w (Unit w) a)
unitl' = arr a (w (Unit w) a)
-> Syntax
     (SigCompose :+: (SigPar w :+: SigSwap w)) arr a (w (Unit w) a)
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift arr a (w (Unit w) a)
forall a. arr a (w (Unit w) a)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr a (t (Unit t) a)
T.unitl'
  unitr :: forall a. SMC w arr (w a (Unit w)) a
unitr = arr (w a (Unit w)) a
-> Syntax
     (SigCompose :+: (SigPar w :+: SigSwap w)) arr (w a (Unit w)) a
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift arr (w a (Unit w)) a
forall a. arr (w a (Unit w)) a
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr (t a (Unit t)) a
T.unitr
  unitr' :: forall a. SMC w arr a (w a (Unit w))
unitr' = arr a (w a (Unit w))
-> Syntax
     (SigCompose :+: (SigPar w :+: SigSwap w)) arr a (w a (Unit w))
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift arr a (w a (Unit w))
forall a. arr a (w a (Unit w))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr a (t a (Unit t))
T.unitr'

instance (Tensor w arr) => Tensor w (SMC w arr) where
  tensor :: forall a b c d.
SMC w arr a b -> SMC w arr c d -> SMC w arr (w a c) (w b d)
tensor SMC w arr a b
f SMC w arr c d
g = (:+:)
  SigCompose (SigPar w :+: SigSwap w) arr (SMC w arr) (w a c) (w b d)
-> Syntax
     (SigCompose :+: (SigPar w :+: SigSwap w)) arr (w a c) (w b d)
forall (sig :: Sig) (arr :: * -> * -> *) a b.
sig arr (Syntax sig arr) a b -> Syntax sig arr a b
Op ((:+:) (SigPar w) (SigSwap w) arr (SMC w arr) (w a c) (w b d)
-> (:+:)
     SigCompose (SigPar w :+: SigSwap w) arr (SMC w arr) (w a c) (w b d)
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 (SMC w arr) (w a c) (w b d)
-> (:+:) (SigPar w) (SigSwap w) arr (SMC w arr) (w a c) (w b d)
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 (SMC w arr a b
-> SMC w arr c d -> SigPar w arr (SMC w arr) (w a c) (w b d)
forall {k} (rec :: * -> * -> *) a b c d (w :: * -> * -> *)
       (arr :: k).
rec a b -> rec c d -> SigPar w arr rec (w a c) (w b d)
SigPar SMC w arr a b
f SMC w arr c d
g)))

instance (Action w arr) => Action w (SMC w arr) where
  braid :: forall a b. SMC w arr (w a b) (w b a)
braid = (:+:)
  SigCompose (SigPar w :+: SigSwap w) arr (SMC w arr) (w a b) (w b a)
-> Syntax
     (SigCompose :+: (SigPar w :+: SigSwap 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) arr (SMC w arr) (w a b) (w b a)
-> (:+:)
     SigCompose (SigPar w :+: SigSwap w) arr (SMC 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 (SMC w arr) (w a b) (w b a)
-> (:+:) (SigPar w) (SigSwap w) arr (SMC 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 (SMC w arr) (w a b) (w b a)
forall {k} {k} (w :: * -> * -> *) (arr :: k) (rec :: k) a b.
SigSwap w arr rec (w a b) (w b a)
SigSwap))

instance (Category arr, Channel t arr) => Channel t (SMC w arr) where
  assoc :: forall a b c. SMC w arr (t (t a b) c) (t a (t b c))
assoc = arr (t (t a b) c) (t a (t b c))
-> SMC w arr (t (t a b) c) (t a (t b c))
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift arr (t (t a b) c) (t a (t b c))
forall a b c. arr (t (t a b) c) (t a (t b c))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t (t a b) c) (t a (t b c))
assoc
  assoc' :: forall a b c. SMC w arr (t a (t b c)) (t (t a b) c)
assoc' = arr (t a (t b c)) (t (t a b) c)
-> SMC w arr (t a (t b c)) (t (t a b) c)
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift arr (t a (t b c)) (t (t a b) c)
forall a b c. arr (t a (t b c)) (t (t a b) c)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t a (t b c)) (t (t a b) c)
assoc'
  slide :: forall a b c. SMC w arr (t a (t b c)) (t b (t a c))
slide = arr (t a (t b c)) (t b (t a c))
-> SMC w arr (t a (t b c)) (t b (t a c))
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift arr (t a (t b c)) (t b (t a c))
forall a b c. arr (t a (t b c)) (t b (t a c))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t a (t b c)) (t b (t a c))
slide

instance (Strength t arr, Action w arr) => Strength t (SMC w arr) where
  strength :: forall b c a. SMC w arr b c -> SMC w arr (t a b) (t a c)
strength SMC w arr b c
f = arr (t a b) (t a c) -> SMC w arr (t a b) (t a c)
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift (arr b c -> arr (t a b) (t a c)
forall b c a. arr b c -> arr (t a b) (t a c)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (b :: k)
       (c :: k) (a :: k).
Strength t arr =>
arr b c -> arr (t a b) (t a c)
strength (SMC w arr b c -> arr b c
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 SMC w arr b c
f))

instance (Traced t arr, Action w arr) => Traced t (SMC w arr) where
  trace :: forall a b c. SMC w arr (t a b) (t a c) -> SMC w arr b c
trace SMC w arr (t a b) (t a c)
body = arr b c -> SMC w arr b c
forall (arr :: * -> * -> *) a b (w :: * -> * -> *).
arr a b -> SMC w arr a b
lift (arr (t a b) (t a c) -> arr b c
forall a b c. arr (t a b) (t a c) -> arr 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 (SMC w arr (t a b) (t a c) -> arr (t a b) (t a c)
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 SMC w arr (t a b) (t a c)
body))

-- Dagger mirror

-- | Mirror an 'SMC' built over 'Dg.Dagger'.
--
-- Reverses composition, transposes each lifted arrow, and leaves 'Circuit.Tensor.tensor'
-- and 'Circuit.Tensor.braid' self-dual. This is the structural transpose of the SMC
-- layer that 'Circuit.Net.mirror' delegates to.
mirror ::
  forall w arr a b.
  SMC w (Dg.Dagger arr) a b ->
  SMC w (Dg.Dagger arr) b a
mirror :: forall (w :: * -> * -> *) (arr :: * -> * -> *) a b.
SMC w (Dagger arr) a b -> SMC w (Dagger arr) b a
mirror (Lift Dagger arr a b
d) = Dagger arr b a
-> Syntax
     (SigCompose :+: (SigPar w :+: SigSwap 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)
  (Dagger arr)
  (Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr))
  a
  b
op) = case (:+:)
  SigCompose
  (SigPar w :+: SigSwap w)
  (Dagger arr)
  (Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr))
  a
  b
op of
  L (SigCompose Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr) b1 b
g Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr) a b1
f) -> (:+:)
  SigCompose
  (SigPar w :+: SigSwap w)
  (Dagger arr)
  (Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr))
  b
  a
-> Syntax
     (SigCompose :+: (SigPar w :+: SigSwap 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)) (Dagger arr))
  b
  a
-> (:+:)
     SigCompose
     (SigPar w :+: SigSwap w)
     (Dagger arr)
     (Syntax (SigCompose :+: (SigPar w :+: SigSwap 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)) (Dagger arr) b1 a
-> Syntax
     (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr) b b1
-> SigCompose
     (Dagger arr)
     (Syntax (SigCompose :+: (SigPar w :+: SigSwap 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)) (Dagger arr) a b1
-> Syntax
     (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr) b1 a
forall (w :: * -> * -> *) (arr :: * -> * -> *) a b.
SMC w (Dagger arr) a b -> SMC w (Dagger arr) b a
mirror Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr) a b1
f) (Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr) b1 b
-> Syntax
     (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr) b b1
forall (w :: * -> * -> *) (arr :: * -> * -> *) a b.
SMC w (Dagger arr) a b -> SMC w (Dagger arr) b a
mirror Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr) b1 b
g)))
  R (L (SigPar Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr) a b
f Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr) c d
g)) -> (:+:)
  SigCompose
  (SigPar w :+: SigSwap w)
  (Dagger arr)
  (Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr))
  b
  a
-> Syntax
     (SigCompose :+: (SigPar w :+: SigSwap 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)
  (Dagger arr)
  (Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr))
  b
  a
-> (:+:)
     SigCompose
     (SigPar w :+: SigSwap w)
     (Dagger arr)
     (Syntax (SigCompose :+: (SigPar w :+: SigSwap 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)) (Dagger arr))
  b
  a
-> (:+:)
     (SigPar w)
     (SigSwap w)
     (Dagger arr)
     (Syntax (SigCompose :+: (SigPar w :+: SigSwap 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)) (Dagger arr) b a
-> Syntax
     (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr) d c
-> SigPar
     w
     (Dagger arr)
     (Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr))
     (w b d)
     (w a c)
forall {k} (rec :: * -> * -> *) a b c d (w :: * -> * -> *)
       (arr :: k).
rec a b -> rec c d -> SigPar w arr rec (w a c) (w b d)
SigPar (Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr) a b
-> Syntax
     (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr) b a
forall (w :: * -> * -> *) (arr :: * -> * -> *) a b.
SMC w (Dagger arr) a b -> SMC w (Dagger arr) b a
mirror Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr) a b
f) (Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr) c d
-> Syntax
     (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr) d c
forall (w :: * -> * -> *) (arr :: * -> * -> *) a b.
SMC w (Dagger arr) a b -> SMC w (Dagger arr) b a
mirror Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr) c d
g))))
  R (R SigSwap
  w
  (Dagger arr)
  (Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr))
  a
  b
SigSwap) -> (:+:)
  SigCompose
  (SigPar w :+: SigSwap w)
  (Dagger arr)
  (Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr))
  b
  a
-> Syntax
     (SigCompose :+: (SigPar w :+: SigSwap 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)
  (Dagger arr)
  (Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr))
  b
  a
-> (:+:)
     SigCompose
     (SigPar w :+: SigSwap w)
     (Dagger arr)
     (Syntax (SigCompose :+: (SigPar w :+: SigSwap 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)) (Dagger arr))
  b
  a
-> (:+:)
     (SigPar w)
     (SigSwap w)
     (Dagger arr)
     (Syntax (SigCompose :+: (SigPar w :+: SigSwap 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)) (Dagger arr))
  b
  a
SigSwap
  w
  (Dagger arr)
  (Syntax (SigCompose :+: (SigPar w :+: SigSwap w)) (Dagger arr))
  (w b a)
  (w a b)
forall {k} {k} (w :: * -> * -> *) (arr :: k) (rec :: k) a b.
SigSwap w arr rec (w a b) (w b a)
SigSwap))

-- Constraint synonym used by Net's Layer law

-- | Free 'SMC' folds target any category with @w@-monoidal action.
class (Action w arr) => FreeSMC w arr

instance (Action w arr) => FreeSMC w arr