{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-unused-top-binds #-}

-- | Tensor action and braiding for traced categories.
--
-- This module collects the cartesian and cocartesian structure over the
-- standard tensors @(,)@ and 'Either', plus the tensor action on morphisms.
--
-- The goal is to keep the core 'Trace' syntax and 'Circuit.Syntax.eval' fold
-- independent of these structural details.
--
-- Note: the monomorphic 'assocL' and 'assocR' helpers below reassociate
-- /leftward/ and /rightward/ respectively — the opposite direction to
-- 'Circuit.Channel.assoc' and 'Circuit.Channel.assoc''.
--
-- 'Tensor' / 'Action' are kind-polymorphic.
module Circuit.Tensor
  ( -- * Fused parallel composition
    superpose,

    -- * Schedule bias (also used by additive disjunction)
    Bias (..),

    -- * Channel product on base arrows
    Unit,
    Unital (..),
    Tensor (..),
    Action (..),
    TensorSeed (..),

    -- * Distributivity of two tensors (multiplicative over additive)
    Distributive (..),

    -- * Cartesian / cocartesian associators
    assocL,
    assocR,
    coassoc,
    coassoc',
    coseed,
    coabsorbL,
    coabsorbR,
    coreleaseL,
    coreleaseR,
  )
where

import Circuit.Category (Category (..), K (..), (.>))
import Circuit.Channel (Strength (..), Traced (..))
import Circuit.Channel qualified as Ch
import Circuit.Syntax (Syntax (..), eval, (:+:) (..))
import Circuit.Trace (SigYank (..), Trace, base, yank)
import Control.Monad (Monad)
import Data.Bifunctor (Bifunctor (..))
import Data.Kind (Type)
import Data.These (These (..))
import Data.Void (Void, absurd)
import Prelude hiding (id, (.))

-- $setup
-- >>> :set -XLambdaCase
-- >>> import Circuit.Trace (Trace, base, yank)
-- >>> import Circuit.Syntax (eval)
-- >>> import Circuit.Category (K (..), runK)
-- >>> import Data.Functor.Identity (Identity)
-- >>> import Prelude hiding (id, (.))

-- * Schedule bias

-- | Bias for ordered choice in scheduling and additive disjunction.
--
-- 'LeftFirst' and 'RightFirst' are used by shared-medium fusion in
-- "Circuit.Shared" and by additive disjunction in "Circuit.Poles".
data Bias = LeftFirst | RightFirst
  deriving (Bias -> Bias -> Bool
(Bias -> Bias -> Bool) -> (Bias -> Bias -> Bool) -> Eq Bias
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Bias -> Bias -> Bool
== :: Bias -> Bias -> Bool
$c/= :: Bias -> Bias -> Bool
/= :: Bias -> Bias -> Bool
Eq, Int -> Bias -> ShowS
[Bias] -> ShowS
Bias -> String
(Int -> Bias -> ShowS)
-> (Bias -> String) -> ([Bias] -> ShowS) -> Show Bias
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Bias -> ShowS
showsPrec :: Int -> Bias -> ShowS
$cshow :: Bias -> String
show :: Bias -> String
$cshowList :: [Bias] -> ShowS
showList :: [Bias] -> ShowS
Show)

-- * Cartesian structure ((,))

-- | Leftward associator: @(a, (b, c)) -> ((a, b), c)@.
assocL :: (a, (b, c)) -> ((a, b), c)
assocL :: forall a b c. (a, (b, c)) -> ((a, b), c)
assocL ~(a
a, ~(b
b, c
c)) = ((a
a, b
b), c
c)

-- | Rightward associator: @((a, b), c) -> (a, (b, c))@.
assocR :: ((a, b), c) -> (a, (b, c))
assocR :: forall a b c. ((a, b), c) -> (a, (b, c))
assocR ~(~(a
a, b
b), c
c) = (a
a, (b
b, c
c))

-- Introduce a channel wire alongside a payload.
seed :: s -> a -> (s, a)
seed :: forall s a. s -> a -> (s, a)
seed s
s a
a = (s
s, a
a)

-- Move a value from the payload into the channel wire.
--
-- absorb f = first (uncurry f) . assocL
absorb :: (t -> s -> s') -> (s, (t, b)) -> (s', b)
absorb :: forall t s s' b. (t -> s -> s') -> (s, (t, b)) -> (s', b)
absorb t -> s -> s'
f (s
s, (t
t, b
b)) = (t -> s -> s'
f t
t s
s, b
b)

-- Move a value from the channel wire into the payload.
--
-- release f = assocR . first f
release :: (s -> (s', t)) -> (s, b) -> (s', (t, b))
release :: forall s s' t b. (s -> (s', t)) -> (s, b) -> (s', (t, b))
release s -> (s', t)
f (s
s, b
b) = let (s'
s', t
t) = s -> (s', t)
f s
s in (s'
s', (t
t, b
b))

-- * Cocartesian structure (Either)

-- | Coassociator for sums.
--
-- >>> coassoc (Left 1 :: Either Int (Either Bool Char))
-- Left (Left 1)
coassoc :: Either a (Either b c) -> Either (Either a b) c
coassoc :: forall a b c. Either a (Either b c) -> Either (Either a b) c
coassoc (Left a
a) = Either a b -> Either (Either a b) c
forall a b. a -> Either a b
Left (a -> Either a b
forall a b. a -> Either a b
Left a
a)
coassoc (Right (Left b
b)) = Either a b -> Either (Either a b) c
forall a b. a -> Either a b
Left (b -> Either a b
forall a b. b -> Either a b
Right b
b)
coassoc (Right (Right c
c)) = c -> Either (Either a b) c
forall a b. b -> Either a b
Right c
c

-- | Inverse coassociator.
--
-- >>> coassoc' (Left (Left 1) :: Either (Either Int Bool) Char)
-- Left 1
coassoc' :: Either (Either a b) c -> Either a (Either b c)
coassoc' :: forall a b c. Either (Either a b) c -> Either a (Either b c)
coassoc' (Left (Left a
a)) = a -> Either a (Either b c)
forall a b. a -> Either a b
Left a
a
coassoc' (Left (Right b
b)) = Either b c -> Either a (Either b c)
forall a b. b -> Either a b
Right (b -> Either b c
forall a b. a -> Either a b
Left b
b)
coassoc' (Right c
c) = Either b c -> Either a (Either b c)
forall a b. b -> Either a b
Right (c -> Either b c
forall a b. b -> Either a b
Right c
c)

-- | Tag a channel value onto whichever branch of the sum is active.
--
-- >>> coseed "st" (Left 42 :: Either Int Char)
-- Left ("st",42)
coseed :: s -> Either a b -> Either (s, a) (s, b)
coseed :: forall s a b. s -> Either a b -> Either (s, a) (s, b)
coseed s
s = (a -> (s, a))
-> (b -> (s, b)) -> Either a b -> Either (s, a) (s, b)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (s
s,) (s
s,)

-- | If the left branch is taken, move a value from the payload into the channel wire.
--
-- >>> coabsorbL (+) (Left (10, (3, 7)) :: Either (Int, (Int, Int)) Bool)
-- Left (13,7)
coabsorbL :: (t -> s -> s') -> Either (s, (t, a)) b -> Either (s', a) b
coabsorbL :: forall t s s' a b.
(t -> s -> s') -> Either (s, (t, a)) b -> Either (s', a) b
coabsorbL t -> s -> s'
f (Left (s
s, (t
t, a
a))) = (s', a) -> Either (s', a) b
forall a b. a -> Either a b
Left (t -> s -> s'
f t
t s
s, a
a)
coabsorbL t -> s -> s'
_ (Right b
b) = b -> Either (s', a) b
forall a b. b -> Either a b
Right b
b

-- | If the right branch is taken, move a value from the payload into the channel wire.
--
-- >>> coabsorbR (+) (Right (10, (3, 7)) :: Either Bool (Int, (Int, Int)))
-- Right (13,7)
coabsorbR :: (t -> s -> s') -> Either a (s, (t, b)) -> Either a (s', b)
coabsorbR :: forall t s s' a b.
(t -> s -> s') -> Either a (s, (t, b)) -> Either a (s', b)
coabsorbR t -> s -> s'
f (Right (s
s, (t
t, b
b))) = (s', b) -> Either a (s', b)
forall a b. b -> Either a b
Right (t -> s -> s'
f t
t s
s, b
b)
coabsorbR t -> s -> s'
_ (Left a
a) = a -> Either a (s', b)
forall a b. a -> Either a b
Left a
a

-- | If the left branch is taken, move a value from the channel wire into the payload.
--
-- >>> coreleaseL (\s -> (s+1, s*2)) (Left (5, 99) :: Either (Int, Int) Char)
-- Left (6,(10,99))
coreleaseL :: (s -> (s', t)) -> Either (s, a) b -> Either (s', (t, a)) b
coreleaseL :: forall s s' t a b.
(s -> (s', t)) -> Either (s, a) b -> Either (s', (t, a)) b
coreleaseL s -> (s', t)
f (Left (s
s, a
a)) = let (s'
s', t
t) = s -> (s', t)
f s
s in (s', (t, a)) -> Either (s', (t, a)) b
forall a b. a -> Either a b
Left (s'
s', (t
t, a
a))
coreleaseL s -> (s', t)
_ (Right b
b) = b -> Either (s', (t, a)) b
forall a b. b -> Either a b
Right b
b

-- | If the right branch is taken, move a value from the channel wire into the payload.
--
-- >>> coreleaseR (\s -> (s+1, s*2)) (Right (5, 99) :: Either Char (Int, Int))
-- Right (6,(10,99))
coreleaseR :: (s -> (s', t)) -> Either a (s, b) -> Either a (s', (t, b))
coreleaseR :: forall s s' t a b.
(s -> (s', t)) -> Either a (s, b) -> Either a (s', (t, b))
coreleaseR s -> (s', t)
f (Right (s
s, b
b)) = let (s'
s', t
t) = s -> (s', t)
f s
s in (s', (t, b)) -> Either a (s', (t, b))
forall a b. b -> Either a b
Right (s'
s', (t
t, b
b))
coreleaseR s -> (s', t)
_ (Left a
a) = a -> Either a (s', (t, b))
forall a b. a -> Either a b
Left a
a

-- * Tensor / Action — tensor action on morphisms

-- | The unit object for a tensor @t@.
--
-- @t@ is an object-level bifunctor (@Either@, @(,)@, type-level @(+)@, …)
-- with kind @k -> k -> k@, not a morphism tensor.
type family Unit (t :: k -> k -> k) :: k

-- | Value-level pairing for a tensor @t@.
--
-- 'Tensor' gives the action of @t@ on morphisms; 'TensorSeed' names the
-- canonical way to combine two values into a value of type @t a b@.  It is
-- needed by constructions (such as 'Circuit.Body.SomeBody') that store a
-- concrete channel value alongside a body.
--
-- Not every tensor has a canonical pairing: @(,)@ has the pair constructor,
-- but 'Either' has no unbiased way to combine @a@ and @b@ into
-- @Either a b@.  Consequently 'TensorSeed' is a separate class.
class TensorSeed (t :: Type -> Type -> Type) where
  seedPair :: a -> b -> t a b

-- | Cartesian pairing.
instance TensorSeed (,) where
  seedPair :: forall s a. s -> a -> (s, a)
seedPair = (,)
  {-# INLINE seedPair #-}

-- | The unit object structure of a tensor @t@ on a category @arr@.
--
-- 'unitl' and 'unitr' witness that the tensor has a unit object. This is
-- the planar fragment without the morphism-level tensor product: arrows
-- that are merely unital can introduce and eliminate the unit, but cannot
-- parallel-compose two arbitrary morphisms.
--
-- Splitting this out from 'Tensor' matters for premonoidal arrows such as
-- @Circuit.Prob@: the unitors are deterministic and embed cleanly, while
-- the general tensor product @tensor@ is not canonical.
--
-- Kind-polymorphic: @t@ and @arr@ share object kind (inferred via PolyKinds).
class (Category arr) => Unital t arr where
  -- | Left unitor: @I ⊗ a -> a@.
  unitl :: arr (t (Unit t) a) a

  -- | Inverse left unitor: @a -> I ⊗ a@.
  unitl' :: arr a (t (Unit t) a)

  -- | Right unitor: @a ⊗ I -> a@.
  unitr :: arr (t a (Unit t)) a

  -- | Inverse right unitor: @a -> a ⊗ I@.
  unitr' :: arr a (t a (Unit t))

-- | The tensor action of @t@ on a category @arr@, without braiding.
--
-- 'tensor' is the tensor product of morphisms (parallel composition on
-- disjoint wires). The unitors live in the 'Unital' superclass.
--
-- Kind-polymorphic: @t@ and @arr@ share object kind (inferred via PolyKinds).
class (Unital t arr) => Tensor t arr where
  -- | Parallel composition: run two arrows on disjoint wires.
  --
  -- >>> tensor ((+1) :: Int -> Int) ((*2) :: Int -> Int) (3, 4)
  -- (4,8)
  tensor :: arr a b -> arr c d -> arr (t a c) (t b d)

-- | The action of a tensor @t@ on a category @arr@, extended with a
-- symmetric braiding.
--
-- This is the self-action of a symmetric monoidal category: @t@ acts on
-- @arr@ by taking morphisms to morphisms over paired objects, and 'braid'
-- provides the symmetry.
class (Tensor t arr) => Action t arr where
  -- | Symmetric braiding.
  --
  -- >>> braid (3, 4) :: (Int, Int)
  -- (4,3)
  braid :: arr (t a b) (t b a)

-- * Distributivity

-- | Distributivity of a multiplicative tensor @d@ over an additive tensor @t@.
--
-- In a distributive monoidal category the product distributes over the sum:
-- @d a (t b c) ≅ t (d a b) (d a c)@ and @d (t a b) c ≅ t (d a c) (d b c)@,
-- and the additive unit is annihilated: @d a (Unit t) ≅ Unit t@.
--
-- For @d = (,)@ and @t = Either@ this is the ordinary distributivity of
-- cartesian product over coproduct, with @(a, Void) ≅ Void@.
class (Tensor d arr, Tensor t arr) => Distributive d t arr where
  -- | Left distributor: @d a (t b c) -> t (d a b) (d a c)@.
  distl :: arr (d a (t b c)) (t (d a b) (d a c))

  -- | Inverse left distributor.
  distl' :: arr (t (d a b) (d a c)) (d a (t b c))

  -- | Right distributor: @d (t a b) c -> t (d a c) (d b c)@.
  distr :: arr (d (t a b) c) (t (d a c) (d b c))

  -- | Inverse right distributor.
  distr' :: arr (t (d a c) (d b c)) (d (t a b) c)

  -- | Left annihilator: @d a (Unit t) -> Unit t@.
  annih :: arr (d a (Unit t)) (Unit t)

  -- | Inverse left annihilator.
  annih' :: arr (Unit t) (d a (Unit t))

type instance Unit (,) = ()

-- | Cartesian unit structure on functions.
--
-- Laws: 'unitl' = 'snd', 'unitl'' = @((),)@, 'unitr' = 'fst', 'unitr'' = @(,) ()@.
instance Unital (,) (->) where
  unitl :: forall a. (Unit (,), a) -> a
unitl ~((), a
a) = a
a
  {-# INLINE unitl #-}
  unitl' :: forall a. a -> (Unit (,), a)
unitl' a
a = ((), a
a)
  {-# INLINE unitl' #-}
  unitr :: forall a. (a, Unit (,)) -> a
unitr ~(a
a, ()) = a
a
  {-# INLINE unitr #-}
  unitr' :: forall a. a -> (a, Unit (,))
unitr' a
a = (a
a, ())
  {-# INLINE unitr' #-}

-- | Cartesian tensor action on functions.
instance Tensor (,) (->) where
  tensor :: forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
tensor a -> b
f c -> d
g (a
a, c
c) = (a -> b
f a
a, c -> d
g c
c)
  {-# INLINE tensor #-}

-- | Cartesian symmetry on functions.
instance Action (,) (->) where
  braid :: forall a b. (a, b) -> (b, a)
braid (a
a, b
b) = (b
b, a
a)
  {-# INLINE braid #-}

-- | Distributivity of @(,)@ over 'Either' on functions.
--
-- >>> distl ('x', Left 1 :: Either Int Bool) :: Either (Char, Int) (Char, Bool)
-- Left ('x',1)
--
-- >>> distl ('x', Right True) :: Either (Char, Int) (Char, Bool)
-- Right ('x',True)
instance Distributive (,) Either (->) where
  distl :: forall a b c. (a, Either b c) -> Either (a, b) (a, c)
distl (a
a, Left b
b) = (a, b) -> Either (a, b) (a, c)
forall a b. a -> Either a b
Left (a
a, b
b)
  distl (a
a, Right c
c) = (a, c) -> Either (a, b) (a, c)
forall a b. b -> Either a b
Right (a
a, c
c)
  {-# INLINE distl #-}
  distl' :: forall a b c. Either (a, b) (a, c) -> (a, Either b c)
distl' = \case
    Left (a
a, b
b) -> (a
a, b -> Either b c
forall a b. a -> Either a b
Left b
b)
    Right (a
a, c
c) -> (a
a, c -> Either b c
forall a b. b -> Either a b
Right c
c)
  {-# INLINE distl' #-}
  distr :: forall a b c. (Either a b, c) -> Either (a, c) (b, c)
distr (Left a
a, c
c) = (a, c) -> Either (a, c) (b, c)
forall a b. a -> Either a b
Left (a
a, c
c)
  distr (Right b
b, c
c) = (b, c) -> Either (a, c) (b, c)
forall a b. b -> Either a b
Right (b
b, c
c)
  {-# INLINE distr #-}
  distr' :: forall a c b. Either (a, c) (b, c) -> (Either a b, c)
distr' = \case
    Left (a
a, c
c) -> (a -> Either a b
forall a b. a -> Either a b
Left a
a, c
c)
    Right (b
b, c
c) -> (b -> Either a b
forall a b. b -> Either a b
Right b
b, c
c)
  {-# INLINE distr' #-}
  annih :: forall a. (a, Unit Either) -> Unit Either
annih = Void -> Void
forall a. Void -> a
absurd (Void -> Void) -> ((a, Void) -> Void) -> (a, Void) -> Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. (a, Void) -> Void
forall a b. (a, b) -> b
snd
  {-# INLINE annih #-}
  annih' :: forall a. Unit Either -> (a, Unit Either)
annih' = Void -> (a, Void)
Unit Either -> (a, Unit Either)
forall a. Void -> a
absurd
  {-# INLINE annih' #-}

-- | Cartesian unit structure on @K@ (effectful sequential product).
instance (Monad m) => Unital (,) (K m) where
  unitl :: forall a. K m (Unit (,), a) a
unitl = ((Unit (,), a) -> m a) -> K m (Unit (,), a) a
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K (((Unit (,), a) -> m a) -> K m (Unit (,), a) a)
-> ((Unit (,), a) -> m a) -> K m (Unit (,), a) a
forall a b. (a -> b) -> a -> b
$ \((), a
a) -> a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a
  {-# INLINE unitl #-}
  unitl' :: forall a. K m a (Unit (,), a)
unitl' = (a -> m (Unit (,), a)) -> K m a (Unit (,), a)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((a -> m (Unit (,), a)) -> K m a (Unit (,), a))
-> (a -> m (Unit (,), a)) -> K m a (Unit (,), a)
forall a b. (a -> b) -> a -> b
$ \a
a -> ((), a) -> m ((), a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((), a
a)
  {-# INLINE unitl' #-}
  unitr :: forall a. K m (a, Unit (,)) a
unitr = ((a, Unit (,)) -> m a) -> K m (a, Unit (,)) a
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K (((a, Unit (,)) -> m a) -> K m (a, Unit (,)) a)
-> ((a, Unit (,)) -> m a) -> K m (a, Unit (,)) a
forall a b. (a -> b) -> a -> b
$ \(a
a, ()) -> a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a
  {-# INLINE unitr #-}
  unitr' :: forall a. K m a (a, Unit (,))
unitr' = (a -> m (a, Unit (,))) -> K m a (a, Unit (,))
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((a -> m (a, Unit (,))) -> K m a (a, Unit (,)))
-> (a -> m (a, Unit (,))) -> K m a (a, Unit (,))
forall a b. (a -> b) -> a -> b
$ \a
a -> (a, ()) -> m (a, ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a, ())
  {-# INLINE unitr' #-}

-- | Cartesian tensor on @K@ (effectful sequential product).
instance (Monad m) => Tensor (,) (K m) where
  tensor :: forall a b c d. K m a b -> K m c d -> K m (a, c) (b, d)
tensor (K a -> m b
f) (K c -> m d
g) =
    ((a, c) -> m (b, d)) -> K m (a, c) (b, d)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K (((a, c) -> m (b, d)) -> K m (a, c) (b, d))
-> ((a, c) -> m (b, d)) -> K m (a, c) (b, d)
forall a b. (a -> b) -> a -> b
$ \(a
a, c
c) -> do
      b <- a -> m b
f a
a
      d <- g c
      pure (b, d)
  {-# INLINE tensor #-}

instance (Monad m) => Action (,) (K m) where
  braid :: forall a b. K m (a, b) (b, a)
braid = ((a, b) -> m (b, a)) -> K m (a, b) (b, a)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K (((a, b) -> m (b, a)) -> K m (a, b) (b, a))
-> ((a, b) -> m (b, a)) -> K m (a, b) (b, a)
forall a b. (a -> b) -> a -> b
$ \(a
a, b
b) -> (b, a) -> m (b, a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b
b, a
a)
  {-# INLINE braid #-}

-- | Distributivity of @(,)@ over 'Either' on @K m@.
instance (Monad m) => Distributive (,) Either (K m) where
  distl :: forall a b c. K m (a, Either b c) (Either (a, b) (a, c))
distl =
    ((a, Either b c) -> m (Either (a, b) (a, c)))
-> K m (a, Either b c) (Either (a, b) (a, c))
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K (((a, Either b c) -> m (Either (a, b) (a, c)))
 -> K m (a, Either b c) (Either (a, b) (a, c)))
-> ((a, Either b c) -> m (Either (a, b) (a, c)))
-> K m (a, Either b c) (Either (a, b) (a, c))
forall a b. (a -> b) -> a -> b
$
      Either (a, b) (a, c) -> m (Either (a, b) (a, c))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (a, b) (a, c) -> m (Either (a, b) (a, c)))
-> ((a, Either b c) -> Either (a, b) (a, c))
-> (a, Either b c)
-> m (Either (a, b) (a, c))
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. \case
        (a
a, Left b
b) -> (a, b) -> Either (a, b) (a, c)
forall a b. a -> Either a b
Left (a
a, b
b)
        (a
a, Right c
c) -> (a, c) -> Either (a, b) (a, c)
forall a b. b -> Either a b
Right (a
a, c
c)
  {-# INLINE distl #-}
  distl' :: forall a b c. K m (Either (a, b) (a, c)) (a, Either b c)
distl' =
    (Either (a, b) (a, c) -> m (a, Either b c))
-> K m (Either (a, b) (a, c)) (a, Either b c)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((Either (a, b) (a, c) -> m (a, Either b c))
 -> K m (Either (a, b) (a, c)) (a, Either b c))
-> (Either (a, b) (a, c) -> m (a, Either b c))
-> K m (Either (a, b) (a, c)) (a, Either b c)
forall a b. (a -> b) -> a -> b
$
      (a, Either b c) -> m (a, Either b c)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((a, Either b c) -> m (a, Either b c))
-> (Either (a, b) (a, c) -> (a, Either b c))
-> Either (a, b) (a, c)
-> m (a, Either b c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. \case
        Left (a
a, b
b) -> (a
a, b -> Either b c
forall a b. a -> Either a b
Left b
b)
        Right (a
a, c
c) -> (a
a, c -> Either b c
forall a b. b -> Either a b
Right c
c)
  {-# INLINE distl' #-}
  distr :: forall a b c. K m (Either a b, c) (Either (a, c) (b, c))
distr =
    ((Either a b, c) -> m (Either (a, c) (b, c)))
-> K m (Either a b, c) (Either (a, c) (b, c))
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K (((Either a b, c) -> m (Either (a, c) (b, c)))
 -> K m (Either a b, c) (Either (a, c) (b, c)))
-> ((Either a b, c) -> m (Either (a, c) (b, c)))
-> K m (Either a b, c) (Either (a, c) (b, c))
forall a b. (a -> b) -> a -> b
$
      Either (a, c) (b, c) -> m (Either (a, c) (b, c))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (a, c) (b, c) -> m (Either (a, c) (b, c)))
-> ((Either a b, c) -> Either (a, c) (b, c))
-> (Either a b, c)
-> m (Either (a, c) (b, c))
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. \case
        (Left a
a, c
c) -> (a, c) -> Either (a, c) (b, c)
forall a b. a -> Either a b
Left (a
a, c
c)
        (Right b
b, c
c) -> (b, c) -> Either (a, c) (b, c)
forall a b. b -> Either a b
Right (b
b, c
c)
  {-# INLINE distr #-}
  distr' :: forall a c b. K m (Either (a, c) (b, c)) (Either a b, c)
distr' =
    (Either (a, c) (b, c) -> m (Either a b, c))
-> K m (Either (a, c) (b, c)) (Either a b, c)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((Either (a, c) (b, c) -> m (Either a b, c))
 -> K m (Either (a, c) (b, c)) (Either a b, c))
-> (Either (a, c) (b, c) -> m (Either a b, c))
-> K m (Either (a, c) (b, c)) (Either a b, c)
forall a b. (a -> b) -> a -> b
$
      (Either a b, c) -> m (Either a b, c)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Either a b, c) -> m (Either a b, c))
-> (Either (a, c) (b, c) -> (Either a b, c))
-> Either (a, c) (b, c)
-> m (Either a b, c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. \case
        Left (a
a, c
c) -> (a -> Either a b
forall a b. a -> Either a b
Left a
a, c
c)
        Right (b
b, c
c) -> (b -> Either a b
forall a b. b -> Either a b
Right b
b, c
c)
  {-# INLINE distr' #-}
  annih :: forall a. K m (a, Unit Either) (Unit Either)
annih = ((a, Unit Either) -> m (Unit Either))
-> K m (a, Unit Either) (Unit Either)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K (((a, Unit Either) -> m (Unit Either))
 -> K m (a, Unit Either) (Unit Either))
-> ((a, Unit Either) -> m (Unit Either))
-> K m (a, Unit Either) (Unit Either)
forall a b. (a -> b) -> a -> b
$ Void -> m Void
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Void -> m Void) -> (Void -> Void) -> Void -> m Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. Void -> Void
forall a. Void -> a
absurd (Void -> m (Unit Either))
-> ((a, Unit Either) -> Void)
-> (a, Unit Either)
-> m (Unit Either)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. (a, Void) -> Void
(a, Unit Either) -> Void
forall a b. (a, b) -> b
snd
  {-# INLINE annih #-}
  annih' :: forall a. K m (Unit Either) (a, Unit Either)
annih' = (Unit Either -> m (a, Unit Either))
-> K m (Unit Either) (a, Unit Either)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((Unit Either -> m (a, Unit Either))
 -> K m (Unit Either) (a, Unit Either))
-> (Unit Either -> m (a, Unit Either))
-> K m (Unit Either) (a, Unit Either)
forall a b. (a -> b) -> a -> b
$ (a, Void) -> m (a, Void)
(a, Void) -> m (a, Unit Either)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((a, Void) -> m (a, Unit Either))
-> (Unit Either -> (a, Void)) -> Unit Either -> m (a, Unit Either)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. Void -> (a, Void)
Unit Either -> (a, Void)
forall a. Void -> a
absurd
  {-# INLINE annih' #-}

type instance Unit Either = Void

-- | Coproduct unit structure on functions.
--
-- Laws: 'unitl' eliminates 'Left', 'unitl'' injects 'Right'; 'unitr'
-- eliminates 'Right', 'unitr'' injects 'Left'.
instance Unital Either (->) where
  unitl :: forall a. Either (Unit Either) a -> a
unitl = (Void -> a) -> (a -> a) -> Either Void a -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Void -> a
forall a. Void -> a
absurd a -> a
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id
  {-# INLINE unitl #-}
  unitl' :: forall a. a -> Either (Unit Either) a
unitl' = a -> Either Void a
a -> Either (Unit Either) a
forall a b. b -> Either a b
Right
  {-# INLINE unitl' #-}
  unitr :: forall a. Either a (Unit Either) -> a
unitr = (a -> a) -> (Void -> a) -> Either a Void -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> a
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id Void -> a
forall a. Void -> a
absurd
  {-# INLINE unitr #-}
  unitr' :: forall a. a -> Either a (Unit Either)
unitr' = a -> Either a Void
a -> Either a (Unit Either)
forall a b. a -> Either a b
Left
  {-# INLINE unitr' #-}

-- | Coproduct tensor action on functions.
--
-- >>> tensor ((+1) :: Int -> Int) ((*2) :: Int -> Int) (Left 3 :: Either Int Int)
-- Left 4
--
-- >>> tensor ((+1) :: Int -> Int) ((*2) :: Int -> Int) (Right 3 :: Either Int Int)
-- Right 6
instance Tensor Either (->) where
  tensor :: forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
tensor = (a -> b) -> (c -> d) -> Either a c -> Either b d
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap
  {-# INLINE tensor #-}

-- | Coproduct symmetry on functions.
--
-- >>> braid (Left 3 :: Either Int Int) :: Either Int Int
-- Right 3
instance Action Either (->) where
  braid :: forall a b. Either a b -> Either b a
braid = \case
    Left a
a -> a -> Either b a
forall a b. b -> Either a b
Right a
a
    Right b
b -> b -> Either b a
forall a b. a -> Either a b
Left b
b
  {-# INLINE braid #-}

-- | Coproduct unit structure on @K@ @m@.
instance (Monad m) => Unital Either (K m) where
  unitl :: forall a. K m (Either (Unit Either) a) a
unitl = (Either (Unit Either) a -> m a) -> K m (Either (Unit Either) a) a
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((Either (Unit Either) a -> m a) -> K m (Either (Unit Either) a) a)
-> (Either (Unit Either) a -> m a)
-> K m (Either (Unit Either) a) a
forall a b. (a -> b) -> a -> b
$ (Unit Either -> m a) -> (a -> m a) -> Either (Unit Either) a -> m a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Void -> m a
Unit Either -> m a
forall a. Void -> a
absurd a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  {-# INLINE unitl #-}
  unitl' :: forall a. K m a (Either (Unit Either) a)
unitl' = (a -> m (Either (Unit Either) a)) -> K m a (Either (Unit Either) a)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((a -> m (Either (Unit Either) a))
 -> K m a (Either (Unit Either) a))
-> (a -> m (Either (Unit Either) a))
-> K m a (Either (Unit Either) a)
forall a b. (a -> b) -> a -> b
$ Either Void a -> m (Either Void a)
Either Void a -> m (Either (Unit Either) a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Void a -> m (Either (Unit Either) a))
-> (a -> Either Void a) -> a -> m (Either (Unit Either) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. a -> Either Void a
forall a b. b -> Either a b
Right
  {-# INLINE unitl' #-}
  unitr :: forall a. K m (Either a (Unit Either)) a
unitr = (Either a (Unit Either) -> m a) -> K m (Either a (Unit Either)) a
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((Either a (Unit Either) -> m a) -> K m (Either a (Unit Either)) a)
-> (Either a (Unit Either) -> m a)
-> K m (Either a (Unit Either)) a
forall a b. (a -> b) -> a -> b
$ (a -> m a) -> (Unit Either -> m a) -> Either a (Unit Either) -> m a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Void -> m a
Unit Either -> m a
forall a. Void -> a
absurd
  {-# INLINE unitr #-}
  unitr' :: forall a. K m a (Either a (Unit Either))
unitr' = (a -> m (Either a (Unit Either))) -> K m a (Either a (Unit Either))
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((a -> m (Either a (Unit Either)))
 -> K m a (Either a (Unit Either)))
-> (a -> m (Either a (Unit Either)))
-> K m a (Either a (Unit Either))
forall a b. (a -> b) -> a -> b
$ Either a Void -> m (Either a Void)
Either a Void -> m (Either a (Unit Either))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either a Void -> m (Either a (Unit Either)))
-> (a -> Either a Void) -> a -> m (Either a (Unit Either))
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. a -> Either a Void
forall a b. a -> Either a b
Left
  {-# INLINE unitr' #-}

-- | Coproduct tensor action on @K@ @m@.
--
-- >>> import Circuit.Category (K(..), runK)
-- >>> let f = K (\n -> pure (n + 1)) :: K IO Int Int
-- >>> let g = K (\n -> pure (n * 2)) :: K IO Int Int
-- >>> runK (tensor f g) (Left 3 :: Either Int Int)
-- Left 4
-- >>> runK (tensor f g) (Right 3 :: Either Int Int)
-- Right 6
instance (Monad m) => Tensor Either (K m) where
  tensor :: forall a b c d. K m a b -> K m c d -> K m (Either a c) (Either b d)
tensor (K a -> m b
f) (K c -> m d
g) =
    (Either a c -> m (Either b d)) -> K m (Either a c) (Either b d)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((Either a c -> m (Either b d)) -> K m (Either a c) (Either b d))
-> (Either a c -> m (Either b d)) -> K m (Either a c) (Either b d)
forall a b. (a -> b) -> a -> b
$ \case
      Left a
a -> b -> Either b d
forall a b. a -> Either a b
Left (b -> Either b d) -> m b -> m (Either b d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
a
      Right c
c -> d -> Either b d
forall a b. b -> Either a b
Right (d -> Either b d) -> m d -> m (Either b d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> m d
g c
c
  {-# INLINE tensor #-}

-- | Coproduct symmetry on @K@ @m@.
instance (Monad m) => Action Either (K m) where
  braid :: forall a b. K m (Either a b) (Either b a)
braid = (Either a b -> m (Either b a)) -> K m (Either a b) (Either b a)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((Either a b -> m (Either b a)) -> K m (Either a b) (Either b a))
-> (Either a b -> m (Either b a)) -> K m (Either a b) (Either b a)
forall a b. (a -> b) -> a -> b
$ Either b a -> m (Either b a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either b a -> m (Either b a))
-> (Either a b -> Either b a) -> Either a b -> m (Either b a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. Either a b -> Either b a
forall a b. Either a b -> Either 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)
braid
  {-# INLINE braid #-}

type instance Unit These = Void

-- | Inclusive unit structure on functions.
--
-- Laws: 'unitl' eliminates a vacuous 'This', 'unitl'' injects with 'That';
-- 'unitr' eliminates a vacuous 'That', 'unitr'' injects with 'This'.
instance Unital These (->) where
  unitl :: forall a. These (Unit These) a -> a
unitl (That a
a) = a
a
  unitl (This Unit These
v) = Void -> a
forall a. Void -> a
absurd Void
Unit These
v
  unitl (These Unit These
v a
_) = Void -> a
forall a. Void -> a
absurd Void
Unit These
v
  {-# INLINE unitl #-}
  unitl' :: forall a. a -> These (Unit These) a
unitl' = a -> These Void a
a -> These (Unit These) a
forall a b. b -> These a b
That
  {-# INLINE unitl' #-}
  unitr :: forall a. These a (Unit These) -> a
unitr (This a
a) = a
a
  unitr (That Unit These
v) = Void -> a
forall a. Void -> a
absurd Void
Unit These
v
  unitr (These a
_ Unit These
v) = Void -> a
forall a. Void -> a
absurd Void
Unit These
v
  {-# INLINE unitr #-}
  unitr' :: forall a. a -> These a (Unit These)
unitr' = a -> These a Void
a -> These a (Unit These)
forall a b. a -> These a b
This
  {-# INLINE unitr' #-}

-- | Inclusive tensor action on functions.
instance Tensor These (->) where
  tensor :: forall a b c d. (a -> b) -> (c -> d) -> These a c -> These b d
tensor = (a -> b) -> (c -> d) -> These a c -> These b d
forall a b c d. (a -> b) -> (c -> d) -> These a c -> These b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap
  {-# INLINE tensor #-}

-- | Inclusive symmetry on functions.
instance Action These (->) where
  braid :: forall a b. These a b -> These b a
braid (This a
a) = a -> These b a
forall a b. b -> These a b
That a
a
  braid (That b
b) = b -> These b a
forall a b. a -> These a b
This b
b
  braid (These a
a b
b) = b -> a -> These b a
forall a b. a -> b -> These a b
These b
b a
a
  {-# INLINE braid #-}

-- | Inclusive unit structure on @K@ @m@.
instance (Monad m) => Unital These (K m) where
  unitl :: forall a. K m (These (Unit These) a) a
unitl = (These (Unit These) a -> m a) -> K m (These (Unit These) a) a
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((These (Unit These) a -> m a) -> K m (These (Unit These) a) a)
-> (These (Unit These) a -> m a) -> K m (These (Unit These) a) a
forall a b. (a -> b) -> a -> b
$ \case
    That a
a -> a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a
    This Unit These
v -> Void -> m a
forall a. Void -> a
absurd Void
Unit These
v
    These Unit These
v a
_ -> Void -> m a
forall a. Void -> a
absurd Void
Unit These
v
  {-# INLINE unitl #-}
  unitl' :: forall a. K m a (These (Unit These) a)
unitl' = (a -> m (These (Unit These) a)) -> K m a (These (Unit These) a)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((a -> m (These (Unit These) a)) -> K m a (These (Unit These) a))
-> (a -> m (These (Unit These) a)) -> K m a (These (Unit These) a)
forall a b. (a -> b) -> a -> b
$ These Void a -> m (These Void a)
These Void a -> m (These (Unit These) a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (These Void a -> m (These (Unit These) a))
-> (a -> These Void a) -> a -> m (These (Unit These) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. a -> These Void a
forall a b. b -> These a b
That
  {-# INLINE unitl' #-}
  unitr :: forall a. K m (These a (Unit These)) a
unitr = (These a (Unit These) -> m a) -> K m (These a (Unit These)) a
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((These a (Unit These) -> m a) -> K m (These a (Unit These)) a)
-> (These a (Unit These) -> m a) -> K m (These a (Unit These)) a
forall a b. (a -> b) -> a -> b
$ \case
    This a
a -> a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a
    That Unit These
v -> Void -> m a
forall a. Void -> a
absurd Void
Unit These
v
    These a
_ Unit These
v -> Void -> m a
forall a. Void -> a
absurd Void
Unit These
v
  {-# INLINE unitr #-}
  unitr' :: forall a. K m a (These a (Unit These))
unitr' = (a -> m (These a (Unit These))) -> K m a (These a (Unit These))
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((a -> m (These a (Unit These))) -> K m a (These a (Unit These)))
-> (a -> m (These a (Unit These))) -> K m a (These a (Unit These))
forall a b. (a -> b) -> a -> b
$ These a Void -> m (These a Void)
These a Void -> m (These a (Unit These))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (These a Void -> m (These a (Unit These)))
-> (a -> These a Void) -> a -> m (These a (Unit These))
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. a -> These a Void
forall a b. a -> These a b
This
  {-# INLINE unitr' #-}

-- | Inclusive tensor action on @K@ @m@.
instance (Monad m) => Tensor These (K m) where
  tensor :: forall a b c d. K m a b -> K m c d -> K m (These a c) (These b d)
tensor (K a -> m b
f) (K c -> m d
g) =
    (These a c -> m (These b d)) -> K m (These a c) (These b d)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((These a c -> m (These b d)) -> K m (These a c) (These b d))
-> (These a c -> m (These b d)) -> K m (These a c) (These b d)
forall a b. (a -> b) -> a -> b
$ \case
      This a
a -> b -> These b d
forall a b. a -> These a b
This (b -> These b d) -> m b -> m (These b d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
a
      That c
c -> d -> These b d
forall a b. b -> These a b
That (d -> These b d) -> m d -> m (These b d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> m d
g c
c
      These a
a c
c -> b -> d -> These b d
forall a b. a -> b -> These a b
These (b -> d -> These b d) -> m b -> m (d -> These b d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
a m (d -> These b d) -> m d -> m (These b d)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> c -> m d
g c
c
  {-# INLINE tensor #-}

-- | Inclusive symmetry on @K@ @m@.
instance (Monad m) => Action These (K m) where
  braid :: forall a b. K m (These a b) (These b a)
braid =
    (These a b -> m (These b a)) -> K m (These a b) (These b a)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((These a b -> m (These b a)) -> K m (These a b) (These b a))
-> (These a b -> m (These b a)) -> K m (These a b) (These b a)
forall a b. (a -> b) -> a -> b
$
      These b a -> m (These b a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (These b a -> m (These b a))
-> (These a b -> These b a) -> These a b -> m (These b a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. \case
        This a
a -> a -> These b a
forall a b. b -> These a b
That a
a
        That b
b -> b -> These b a
forall a b. a -> These a b
This b
b
        These a
a b
b -> b -> a -> These b a
forall a b. a -> b -> These a b
These b
b a
a
  {-# INLINE braid #-}

-- | Lift 'Unital' through 'Trace'.
instance (Unital t arr) => Unital t (Trace t' arr) where
  unitl :: forall a. Trace t' arr (t (Unit t) a) a
unitl = arr (t (Unit t) a) a
-> Syntax (SigCompose :+: SigYank t') arr (t (Unit t) a) a
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base arr (t (Unit t) a) a
forall a. arr (t (Unit t) a) a
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr (t (Unit t) a) a
unitl
  unitl' :: forall a. Trace t' arr a (t (Unit t) a)
unitl' = arr a (t (Unit t) a)
-> Syntax (SigCompose :+: SigYank t') arr a (t (Unit t) a)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base arr a (t (Unit t) a)
forall a. arr a (t (Unit t) a)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr a (t (Unit t) a)
unitl'
  unitr :: forall a. Trace t' arr (t a (Unit t)) a
unitr = arr (t a (Unit t)) a
-> Syntax (SigCompose :+: SigYank t') arr (t a (Unit t)) a
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base arr (t a (Unit t)) a
forall a. arr (t a (Unit t)) a
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr (t a (Unit t)) a
unitr
  unitr' :: forall a. Trace t' arr a (t a (Unit t))
unitr' = arr a (t a (Unit t))
-> Syntax (SigCompose :+: SigYank t') arr a (t a (Unit t))
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base arr a (t a (Unit t))
forall a. arr a (t a (Unit t))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr a (t a (Unit t))
unitr'

-- | Lift 'Tensor'/'Action' through 'Trace'.
--
-- This is the single lawful instance: it evaluates each 'Trace' branch
-- independently with 'Circuit.Syntax.eval' and combines the results using the
-- base arrow's tensor. It is correct and black-hole-free, but does not fuse
-- feedback loops. For the fused superposition of two 'Circuit.Trace.yank's,
-- use 'superpose'.
instance (Tensor t arr, Traced t' arr) => Tensor t (Trace t' arr) where
  tensor :: forall a b c d.
Trace t' arr a b
-> Trace t' arr c d -> Trace t' arr (t a c) (t b d)
tensor Trace t' arr a b
f Trace t' arr c d
g = arr (t a c) (t b d) -> Trace t' arr (t a c) (t b d)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (arr a b -> arr c d -> arr (t a c) (t b d)
forall a b c d. arr a b -> arr c d -> arr (t a c) (t 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)
tensor (Trace t' arr a b -> arr a 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 Trace t' arr a b
f) (Trace t' arr c d -> arr c d
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 Trace t' arr c d
g))

instance (Action t arr, Traced t' arr) => Action t (Trace t' arr) where
  braid :: forall a b. Trace t' arr (t a b) (t b a)
braid = arr (t a b) (t b a) -> Trace t' arr (t a b) (t b a)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base arr (t a b) (t b a)
forall a b. arr (t a b) (t 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)
braid

-- | Fused parallel composition for 'Trace' when the feedback tensor matches.
--
-- Two 'Circuit.Trace.yank's in parallel superpose into one 'Circuit.Trace.yank' over a paired channel,
-- satisfying the superposing axiom of traced monoidal categories:
--
-- @superpose (trace f) (trace g) = trace (pre . tensor f g . post)@
--
-- where @pre@ and @post@ rearrange the paired channel via associators
-- and braiding. This preserves sharing for recursive circuits; the lawful
-- 'Tensor' instance falls back to independent evaluation.
--
-- >>> let k1 = yank (base (\(ns, _) -> (1 : ns, take 3 ns))) :: Trace (,) (->) [Int] [Int]
-- >>> let k2 = yank (base (\(ns, _) -> (2 : ns, take 3 ns)))
-- >>> eval (superpose k1 k2) ([], [])
-- ([1,1,1],[2,2,2])
--
-- The same fusion works for @K@, preserving sharing across the
-- recursive channels under @MonadFix@.
--
-- >>> let k1 = yank (base (K $ \(ns, _) -> pure (1 : ns, take 3 ns))) :: Trace (,) (K Identity) [Int] [Int]
-- >>> let k2 = yank (base (K $ \(ns, _) -> pure (2 : ns, take 3 ns)))
-- >>> runK (eval (superpose k1 k2)) ([], [])
-- Identity ([1,1,1],[2,2,2])
superpose ::
  forall t arr a b c d.
  (Tensor t arr, Traced t arr) =>
  Trace t arr a b ->
  Trace t arr c d ->
  Trace t arr (t a c) (t b d)
superpose :: forall (t :: * -> * -> *) (arr :: * -> * -> *) a b c d.
(Tensor t arr, Traced t arr) =>
Trace t arr a b -> Trace t arr c d -> Trace t arr (t a c) (t b d)
superpose Trace t arr a b
x Trace t arr c d
y =
  case (Trace t arr a b
x, Trace t arr c d
y) of
    (Lift arr a b
f, Lift arr c d
g) ->
      arr (t a c) (t b d) -> Trace t arr (t a c) (t b d)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (arr a b -> arr c d -> arr (t a c) (t b d)
forall a b c d. arr a b -> arr c d -> arr (t a c) (t 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)
tensor arr a b
f arr c d
g)
    (Op (R (Yank Syntax (SigCompose :+: SigYank t) arr (t s a) (t s b)
f)), Lift arr c d
g) ->
      Trace t arr (t s (t a c)) (t s (t b d))
-> Trace t arr (t a c) (t b d)
forall (t :: * -> * -> *) (arr :: * -> * -> *) s a b.
Trace t arr (t s a) (t s b) -> Trace t arr a b
yank (arr (t (t s b) d) (t s (t b d))
-> Trace t arr (t (t s b) d) (t s (t b d))
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base arr (t (t s b) d) (t s (t b d))
forall x y z. arr (t (t x y) z) (t x (t y z))
assoc Trace t arr (t (t s b) d) (t s (t b d))
-> Syntax
     (SigCompose :+: SigYank t) arr (t (t s a) c) (t (t s b) d)
-> Syntax
     (SigCompose :+: SigYank t) arr (t (t s a) c) (t s (t b d))
forall b c a.
Syntax (SigCompose :+: SigYank t) arr b c
-> Syntax (SigCompose :+: SigYank t) arr a b
-> Syntax (SigCompose :+: SigYank t) arr a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. arr (t (t s a) c) (t (t s b) d)
-> Syntax
     (SigCompose :+: SigYank t) arr (t (t s a) c) (t (t s b) d)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (arr (t s a) (t s b) -> arr c d -> arr (t (t s a) c) (t (t s b) d)
forall a b c d. arr a b -> arr c d -> arr (t a c) (t 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)
tensor (Syntax (SigCompose :+: SigYank t) arr (t s a) (t s b)
-> arr (t s a) (t s 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 Syntax (SigCompose :+: SigYank t) arr (t s a) (t s b)
f) arr c d
g) Syntax (SigCompose :+: SigYank t) arr (t (t s a) c) (t s (t b d))
-> Syntax
     (SigCompose :+: SigYank t) arr (t s (t a c)) (t (t s a) c)
-> Trace t arr (t s (t a c)) (t s (t b d))
forall b c a.
Syntax (SigCompose :+: SigYank t) arr b c
-> Syntax (SigCompose :+: SigYank t) arr a b
-> Syntax (SigCompose :+: SigYank t) arr a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. arr (t s (t a c)) (t (t s a) c)
-> Syntax
     (SigCompose :+: SigYank t) arr (t s (t a c)) (t (t s a) c)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base arr (t s (t a c)) (t (t s a) c)
forall x y z. arr (t x (t y z)) (t (t x y) z)
assoc')
    (Lift arr a b
f, Op (R (Yank Syntax (SigCompose :+: SigYank t) arr (t s c) (t s d)
g))) ->
      Trace t arr (t s (t a c)) (t s (t b d))
-> Trace t arr (t a c) (t b d)
forall (t :: * -> * -> *) (arr :: * -> * -> *) s a b.
Trace t arr (t s a) (t s b) -> Trace t arr a b
yank (arr (t b (t s d)) (t s (t b d))
-> Trace t arr (t b (t s d)) (t s (t b d))
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base arr (t b (t s d)) (t s (t b d))
forall x y z. arr (t x (t y z)) (t y (t x z))
shuffle Trace t arr (t b (t s d)) (t s (t b d))
-> Syntax
     (SigCompose :+: SigYank t) arr (t a (t s c)) (t b (t s d))
-> Syntax
     (SigCompose :+: SigYank t) arr (t a (t s c)) (t s (t b d))
forall b c a.
Syntax (SigCompose :+: SigYank t) arr b c
-> Syntax (SigCompose :+: SigYank t) arr a b
-> Syntax (SigCompose :+: SigYank t) arr a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. arr (t a (t s c)) (t b (t s d))
-> Syntax
     (SigCompose :+: SigYank t) arr (t a (t s c)) (t b (t s d))
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (arr a b -> arr (t s c) (t s d) -> arr (t a (t s c)) (t b (t s d))
forall a b c d. arr a b -> arr c d -> arr (t a c) (t 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)
tensor arr a b
f (Syntax (SigCompose :+: SigYank t) arr (t s c) (t s d)
-> arr (t s c) (t s d)
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 Syntax (SigCompose :+: SigYank t) arr (t s c) (t s d)
g)) Syntax (SigCompose :+: SigYank t) arr (t a (t s c)) (t s (t b d))
-> Syntax
     (SigCompose :+: SigYank t) arr (t s (t a c)) (t a (t s c))
-> Trace t arr (t s (t a c)) (t s (t b d))
forall b c a.
Syntax (SigCompose :+: SigYank t) arr b c
-> Syntax (SigCompose :+: SigYank t) arr a b
-> Syntax (SigCompose :+: SigYank t) arr a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. arr (t s (t a c)) (t a (t s c))
-> Syntax
     (SigCompose :+: SigYank t) arr (t s (t a c)) (t a (t s c))
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base arr (t s (t a c)) (t a (t s c))
forall x y z. arr (t x (t y z)) (t y (t x z))
shuffle)
    (Op (R (Yank Syntax (SigCompose :+: SigYank t) arr (t s a) (t s b)
f)), Op (R (Yank Syntax (SigCompose :+: SigYank t) arr (t s c) (t s d)
g))) ->
      Trace t arr (t (t s s) (t a c)) (t (t s s) (t b d))
-> Trace t arr (t a c) (t b d)
forall (t :: * -> * -> *) (arr :: * -> * -> *) s a b.
Trace t arr (t s a) (t s b) -> Trace t arr a b
yank (arr (t (t s b) (t s d)) (t (t s s) (t b d))
-> Trace t arr (t (t s b) (t s d)) (t (t s s) (t b d))
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base arr (t (t s b) (t s d)) (t (t s s) (t b d))
forall u v w x. arr (t (t u v) (t w x)) (t (t u w) (t v x))
post Trace t arr (t (t s b) (t s d)) (t (t s s) (t b d))
-> Syntax
     (SigCompose :+: SigYank t)
     arr
     (t (t s a) (t s c))
     (t (t s b) (t s d))
-> Syntax
     (SigCompose :+: SigYank t)
     arr
     (t (t s a) (t s c))
     (t (t s s) (t b d))
forall b c a.
Syntax (SigCompose :+: SigYank t) arr b c
-> Syntax (SigCompose :+: SigYank t) arr a b
-> Syntax (SigCompose :+: SigYank t) arr a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. arr (t (t s a) (t s c)) (t (t s b) (t s d))
-> Syntax
     (SigCompose :+: SigYank t)
     arr
     (t (t s a) (t s c))
     (t (t s b) (t s d))
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (arr (t s a) (t s b)
-> arr (t s c) (t s d)
-> arr (t (t s a) (t s c)) (t (t s b) (t s d))
forall a b c d. arr a b -> arr c d -> arr (t a c) (t 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)
tensor (Syntax (SigCompose :+: SigYank t) arr (t s a) (t s b)
-> arr (t s a) (t s 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 Syntax (SigCompose :+: SigYank t) arr (t s a) (t s b)
f) (Syntax (SigCompose :+: SigYank t) arr (t s c) (t s d)
-> arr (t s c) (t s d)
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 Syntax (SigCompose :+: SigYank t) arr (t s c) (t s d)
g)) Syntax
  (SigCompose :+: SigYank t)
  arr
  (t (t s a) (t s c))
  (t (t s s) (t b d))
-> Syntax
     (SigCompose :+: SigYank t)
     arr
     (t (t s s) (t a c))
     (t (t s a) (t s c))
-> Trace t arr (t (t s s) (t a c)) (t (t s s) (t b d))
forall b c a.
Syntax (SigCompose :+: SigYank t) arr b c
-> Syntax (SigCompose :+: SigYank t) arr a b
-> Syntax (SigCompose :+: SigYank t) arr a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. arr (t (t s s) (t a c)) (t (t s a) (t s c))
-> Syntax
     (SigCompose :+: SigYank t)
     arr
     (t (t s s) (t a c))
     (t (t s a) (t s c))
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base arr (t (t s s) (t a c)) (t (t s a) (t s c))
forall u v w x. arr (t (t u v) (t w x)) (t (t u w) (t v x))
pre)
    -- Non-normal forms fall back to the lawful independent-evaluation instance.
    (Trace t arr a b, Trace t arr c d)
_ ->
      arr (t a c) (t b d) -> Trace t arr (t a c) (t b d)
forall (arr :: * -> * -> *) a b (t :: * -> * -> *).
arr a b -> Trace t arr a b
base (arr a b -> arr c d -> arr (t a c) (t b d)
forall a b c d. arr a b -> arr c d -> arr (t a c) (t 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)
tensor (Trace t arr a b -> arr a 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 Trace t arr a b
x) (Trace t arr c d -> arr c d
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 Trace t arr c d
y))
  where
    assoc :: forall x y z. arr (t (t x y) z) (t x (t y z))
    assoc :: forall x y z. arr (t (t x y) z) (t x (t y z))
assoc = arr (t (t x y) z) (t x (t y z))
forall x y z. arr (t (t x y) z) (t x (t y z))
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))
Ch.assoc

    assoc' :: forall x y z. arr (t x (t y z)) (t (t x y) z)
    assoc' :: forall x y z. arr (t x (t y z)) (t (t x y) z)
assoc' = arr (t x (t y z)) (t (t x y) z)
forall x y z. arr (t x (t y z)) (t (t x y) z)
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)
Ch.assoc'

    shuffle :: forall x y z. arr (t x (t y z)) (t y (t x z))
    shuffle :: forall x y z. arr (t x (t y z)) (t y (t x z))
shuffle = arr (t x (t y z)) (t y (t x z))
forall x y z. arr (t x (t y z)) (t y (t x z))
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))
Ch.slide

    pre, post :: forall u v w x. arr (t (t u v) (t w x)) (t (t u w) (t v x))
    pre :: forall u v w x. arr (t (t u v) (t w x)) (t (t u w) (t v x))
pre = arr (t (t u v) (t w x)) (t u (t v (t w x)))
forall x y z. arr (t (t x y) z) (t x (t y z))
assoc arr (t (t u v) (t w x)) (t u (t v (t w x)))
-> arr (t u (t v (t w x))) (t u (t w (t v x)))
-> arr (t (t u v) (t w x)) (t u (t w (t v x)))
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr (t v (t w x)) (t w (t v x))
-> arr (t u (t v (t w x))) (t u (t w (t v x)))
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 arr (t v (t w x)) (t w (t v x))
forall x y z. arr (t x (t y z)) (t y (t x z))
shuffle arr (t (t u v) (t w x)) (t u (t w (t v x)))
-> arr (t u (t w (t v x))) (t (t u w) (t v x))
-> arr (t (t u v) (t w x)) (t (t u w) (t v x))
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr (t u (t w (t v x))) (t (t u w) (t v x))
forall x y z. arr (t x (t y z)) (t (t x y) z)
assoc'
    post :: forall u v w x. arr (t (t u v) (t w x)) (t (t u w) (t v x))
post = arr (t (t u v) (t w x)) (t u (t v (t w x)))
forall x y z. arr (t (t x y) z) (t x (t y z))
assoc arr (t (t u v) (t w x)) (t u (t v (t w x)))
-> arr (t u (t v (t w x))) (t u (t w (t v x)))
-> arr (t (t u v) (t w x)) (t u (t w (t v x)))
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr (t v (t w x)) (t w (t v x))
-> arr (t u (t v (t w x))) (t u (t w (t v x)))
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 arr (t v (t w x)) (t w (t v x))
forall x y z. arr (t x (t y z)) (t y (t x z))
shuffle arr (t (t u v) (t w x)) (t u (t w (t v x)))
-> arr (t u (t w (t v x))) (t (t u w) (t v x))
-> arr (t (t u v) (t w x)) (t (t u w) (t v x))
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr (t u (t w (t v x))) (t (t u w) (t v x))
forall x y z. arr (t x (t y z)) (t (t x y) z)
assoc'