{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-- | A span-shaped Mealy machine: a morphism across a tensored channel.
--
-- @
--   Body t ch arr a b  =  arr (t ch a) (t ch b)
-- @
--
-- Both the channel and the payload enter together, and both exit together.
-- 'Circuit.System.System' specializes this shape to a Moore machine over a
-- polynomial interface; 'Circuit.Process.Process' is the pointed monomial
-- special case of that.
--
-- == Anatomy
--
-- * __@t@ — tensor__: the bifunctor that pairs a channel with a payload.
--   Common choices are @(,)@ for simultaneous sharing, 'Either' for sequential
--   iteration, and 'Data.These.These' for scheduled interleaving.
--
-- * __@ch@ — channel__: the value threaded alongside the payload.  It may be
--   state, residual, a stream, or a feedback wire.
--
-- * __@arr@ — arrow / morphism__: the base category.  Usually @(->)@ or a
--   Kleisli arrow @K m@.
--
-- This arrangement is the common shape underlying loops, processes, systems,
-- and channel ends: a morphism whose input and output both carry an ambient
-- channel.  'Body' makes that shape explicit before any tracing, scheduling,
-- or pole-splitting is added.
module Circuit.Body
  ( -- * Knot-body category
    Body (..),
    SomeBody (..),
    runSomeBody,
    runFlowchart,

    -- * Carrier-tensoring composition
    cascadeBody,
    cascadeSome,
  )
where

import Circuit.Category (Category (..), K (..), Pointed (..), (.>))
import Circuit.Channel (Channel (..), Strength (..))
import Circuit.Poles (HasDual (..), In (..), Out (..), Poles (..))
import Circuit.Tensor (Tensor (..), TensorSeed (..), Unit)
import Data.Void (Void, absurd)
import Prelude hiding (id, (.))

-- | A morphism across a tensored channel.
--
-- @Body t ch arr a b@ is a morphism @arr (t ch a) (t ch b)@.  The channel
-- @ch@ is threaded alongside the payload by the tensor @t@; it may be state,
-- residual, a stream, or any other value the base arrow @arr@ carries along
-- with the input and output.  Composition threads the same channel through
-- both morphisms.
newtype Body t ch arr a b = Body {forall {k} {k} {k} (t :: k -> k -> k) (ch :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
Body t ch arr a b -> arr (t ch a) (t ch b)
morphism :: arr (t ch a) (t ch b)}

instance (Category arr) => Category (Body t ch arr) where
  id :: forall a. Body t ch arr a a
  id :: forall (a :: k). Body t ch arr a a
id = arr (t ch a) (t ch a) -> Body t ch arr a a
forall {k} {k} {k} (t :: k -> k -> k) (ch :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body arr (t ch a) (t ch a)
forall (a :: k). arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id
  {-# INLINE id #-}

  (.) :: forall a b c. Body t ch arr b c -> Body t ch arr a b -> Body t ch arr a c
  Body arr (t ch b) (t ch c)
g . :: forall (a :: k) (b :: k) (c :: k).
Body t ch arr b c -> Body t ch arr a b -> Body t ch arr a c
. Body arr (t ch a) (t ch b)
f = arr (t ch a) (t ch c) -> Body t ch arr a c
forall {k} {k} {k} (t :: k -> k -> k) (ch :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body (arr (t ch b) (t ch c)
g arr (t ch b) (t ch c)
-> arr (t ch a) (t ch b) -> arr (t ch a) (t ch c)
forall (b :: k) (c :: k) (a :: k). arr b c -> arr a b -> 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 ch a) (t ch b)
f)
  {-# INLINE (.) #-}

-- | A 'Body' with its channel type hidden.
data SomeBody t arr a b where
  SomeBody :: ch -> Body t ch arr a b -> SomeBody t arr a b

-- | Run an existentially-packed cartesian body over a list of inputs.
--
-- This is the @(,)@ / list specialisation of 'SomeBody'.
runSomeBody :: SomeBody (,) (->) a b -> [a] -> [b]
runSomeBody :: forall a b. SomeBody (,) (->) a b -> [a] -> [b]
runSomeBody (SomeBody ch
ch0 (Body (ch, a) -> (ch, b)
f)) [a]
xs =
  let (ch
_, [b]
bs) = ((ch, [b]) -> a -> (ch, [b])) -> (ch, [b]) -> [a] -> (ch, [b])
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\(ch
ch, [b]
acc) a
a -> let (ch
ch', b
b) = (ch, a) -> (ch, b)
f (ch
ch, a
a) in (ch
ch', b
b b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [b]
acc)) (ch
ch0, []) [a]
xs
   in [b] -> [b]
forall a. [a] -> [a]
reverse [b]
bs

-- | Run an 'Either' body as a partial function @a -> b@ with a fuel bound.
-- Execution starts with the external input @a@; if the body emits a label
-- @ch@ the runner feeds @Left ch@ back in, decrementing the fuel.
--
-- Returns the result (if any) and the number of steps taken.  A flowchart has
-- no stored state — the input is the entire initial configuration — so there
-- is no seed parameter.  This is the coproduct analogue of 'runSomeBody':
-- where @(,)@ bodies run as stream functions, 'Either' bodies run as halting
-- computations.
runFlowchart :: Body Either ch (->) a b -> Int -> a -> (Maybe b, Int)
runFlowchart :: forall ch a b.
Body Either ch (->) a b -> Int -> a -> (Maybe b, Int)
runFlowchart (Body Either ch a -> Either ch b
f) Int
fuel0 a
a0 = Int -> Int -> Either ch a -> (Maybe b, Int)
go Int
fuel0 Int
0 (a -> Either ch a
forall a b. b -> Either a b
Right a
a0)
  where
    go :: Int -> Int -> Either ch a -> (Maybe b, Int)
go Int
0 Int
steps Either ch a
_ = (Maybe b
forall a. Maybe a
Nothing, Int
steps)
    go Int
n Int
steps (Left ch
ch) =
      case Either ch a -> Either ch b
f (ch -> Either ch a
forall a b. a -> Either a b
Left ch
ch) of
        Left ch
ch' -> Int -> Int -> Either ch a -> (Maybe b, Int)
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int
steps Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (ch -> Either ch a
forall a b. a -> Either a b
Left ch
ch')
        Right b
b -> (b -> Maybe b
forall a. a -> Maybe a
Just b
b, Int
steps Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
    go Int
n Int
steps (Right a
a) =
      case Either ch a -> Either ch b
f (a -> Either ch a
forall a b. b -> Either a b
Right a
a) of
        Left ch
ch' -> Int -> Int -> Either ch a -> (Maybe b, Int)
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int
steps Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (ch -> Either ch a
forall a b. a -> Either a b
Left ch
ch')
        Right b
b -> (b -> Maybe b
forall a. a -> Maybe a
Just b
b, Int
steps Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

-- * HasDual instances for Body

-- | Unit poles for @Body (,) s (->)@ at the unit object @()@.
--
-- The companion discards its input and returns @()@; the conjoint delegates
-- to the companion. Yanking recovers the identity on @()@.
instance HasDual () (Body (,) s (->)) where
  open :: Poles (Body (,) s (->)) () ()
open =
    let outU :: Out (Body (,) ch (->)) ()
outU = (forall x. In (Body (,) ch (->)) x -> Body (,) ch (->) x ())
-> Out (Body (,) ch (->)) ()
forall {k} {k1} (arr :: k -> k1 -> *) (a :: k1).
(forall (x :: k). In arr x -> arr x a) -> Out arr a
Out ((forall x. In (Body (,) ch (->)) x -> Body (,) ch (->) x ())
 -> Out (Body (,) ch (->)) ())
-> (forall x. In (Body (,) ch (->)) x -> Body (,) ch (->) x ())
-> Out (Body (,) ch (->)) ()
forall a b. (a -> b) -> a -> b
$ \In (Body (,) ch (->)) x
_ -> ((ch, x) -> (ch, ())) -> Body (,) ch (->) x ()
forall {k} {k} {k} (t :: k -> k -> k) (ch :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body (((ch, x) -> (ch, ())) -> Body (,) ch (->) x ())
-> ((ch, x) -> (ch, ())) -> Body (,) ch (->) x ()
forall a b. (a -> b) -> a -> b
$ \(ch
s, x
_) -> (ch
s, ())
        inU :: In arr a
inU = (forall (x :: k1). Out arr x -> arr a x) -> In arr a
forall {k} {k1} (arr :: k -> k1 -> *) (a :: k).
(forall (x :: k1). Out arr x -> arr a x) -> In arr a
In ((forall (x :: k1). Out arr x -> arr a x) -> In arr a)
-> (forall (x :: k1). Out arr x -> arr a x) -> In arr a
forall a b. (a -> b) -> a -> b
$ \Out arr x
o -> Out arr x -> forall (x :: k). In arr x -> arr x x
forall {k1} {k2} (arr :: k1 -> k2 -> *) (a :: k2).
Out arr a -> forall (x :: k1). In arr x -> arr x a
emit Out arr x
o In arr a
inU
     in In (Body (,) s (->)) ()
-> Out (Body (,) s (->)) () -> Poles (Body (,) s (->)) () ()
forall {k} {k1} (arr :: k -> k1 -> *) (a :: k) (b :: k1).
In arr a -> Out arr b -> Poles arr a b
Poles In (Body (,) s (->)) ()
forall {k} {k1} {arr :: k -> k1 -> *} {a :: k}. In arr a
inU Out (Body (,) s (->)) ()
forall {ch}. Out (Body (,) ch (->)) ()
outU

-- | Unit poles for @Body (,) s (K m)@.
--
-- Same shape as the @(->)@ instance, but the companion returns @()@ in the
-- monad and threads the ambient state through unchanged.
instance (Monad m) => HasDual () (Body (,) s (K m)) where
  open :: Poles (Body (,) s (K m)) () ()
open =
    let outU :: Out (Body (,) a (K m)) ()
outU = (forall x. In (Body (,) a (K m)) x -> Body (,) a (K m) x ())
-> Out (Body (,) a (K m)) ()
forall {k} {k1} (arr :: k -> k1 -> *) (a :: k1).
(forall (x :: k). In arr x -> arr x a) -> Out arr a
Out ((forall x. In (Body (,) a (K m)) x -> Body (,) a (K m) x ())
 -> Out (Body (,) a (K m)) ())
-> (forall x. In (Body (,) a (K m)) x -> Body (,) a (K m) x ())
-> Out (Body (,) a (K m)) ()
forall a b. (a -> b) -> a -> b
$ \In (Body (,) a (K m)) x
_ -> K m (a, x) (a, ()) -> Body (,) a (K m) x ()
forall {k} {k} {k} (t :: k -> k -> k) (ch :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body (K m (a, x) (a, ()) -> Body (,) a (K m) x ())
-> K m (a, x) (a, ()) -> Body (,) a (K m) x ()
forall a b. (a -> b) -> a -> b
$ ((a, x) -> m (a, ())) -> K m (a, x) (a, ())
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K (((a, x) -> m (a, ())) -> K m (a, x) (a, ()))
-> ((a, x) -> m (a, ())) -> K m (a, x) (a, ())
forall a b. (a -> b) -> a -> b
$ \(a
s, x
_) -> (a, ()) -> m (a, ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
s, ())
        inU :: In arr a
inU = (forall (x :: k1). Out arr x -> arr a x) -> In arr a
forall {k} {k1} (arr :: k -> k1 -> *) (a :: k).
(forall (x :: k1). Out arr x -> arr a x) -> In arr a
In ((forall (x :: k1). Out arr x -> arr a x) -> In arr a)
-> (forall (x :: k1). Out arr x -> arr a x) -> In arr a
forall a b. (a -> b) -> a -> b
$ \Out arr x
o -> Out arr x -> forall (x :: k). In arr x -> arr x x
forall {k1} {k2} (arr :: k1 -> k2 -> *) (a :: k2).
Out arr a -> forall (x :: k1). In arr x -> arr x a
emit Out arr x
o In arr a
inU
     in In (Body (,) s (K m)) ()
-> Out (Body (,) s (K m)) () -> Poles (Body (,) s (K m)) () ()
forall {k} {k1} (arr :: k -> k1 -> *) (a :: k) (b :: k1).
In arr a -> Out arr b -> Poles arr a b
Poles In (Body (,) s (K m)) ()
forall {k} {k1} {arr :: k -> k1 -> *} {a :: k}. In arr a
inU Out (Body (,) s (K m)) ()
forall {a}. Out (Body (,) a (K m)) ()
outU

-- | Unit poles for @Body Either s (->)@ at the unit object @Void@.
--
-- The coproduct case needs a distinguished element of the carrier @s@: on a
-- @Right x@ input the companion must return @Left s@ for some @s@, and there
-- is no ambient state to use.  'Pointed' captures exactly that, which is
-- weaker than 'Monoid'.  This is the structural pointedness requirement that
-- makes @Either@ differ from @(,)@.
instance (Pointed s) => HasDual Void (Body Either s (->)) where
  open :: Poles (Body Either s (->)) Void Void
open =
    let outU :: Out (Body Either s (->)) a
outU = (forall x. In (Body Either s (->)) x -> Body Either s (->) x a)
-> Out (Body Either s (->)) a
forall {k} {k1} (arr :: k -> k1 -> *) (a :: k1).
(forall (x :: k). In arr x -> arr x a) -> Out arr a
Out ((forall x. In (Body Either s (->)) x -> Body Either s (->) x a)
 -> Out (Body Either s (->)) a)
-> (forall x. In (Body Either s (->)) x -> Body Either s (->) x a)
-> Out (Body Either s (->)) a
forall a b. (a -> b) -> a -> b
$ \In (Body Either s (->)) x
_ -> (Either s x -> Either s a) -> Body Either s (->) x a
forall {k} {k} {k} (t :: k -> k -> k) (ch :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body ((Either s x -> Either s a) -> Body Either s (->) x a)
-> (Either s x -> Either s a) -> Body Either s (->) x a
forall a b. (a -> b) -> a -> b
$ \case
          Left s
s -> s -> Either s a
forall a b. a -> Either a b
Left s
s
          Right x
_ -> s -> Either s a
forall a b. a -> Either a b
Left s
forall a. Pointed a => a
point
        inU :: In (Body Either ch (->)) Void
inU = (forall x.
 Out (Body Either ch (->)) x -> Body Either ch (->) Void x)
-> In (Body Either ch (->)) Void
forall {k} {k1} (arr :: k -> k1 -> *) (a :: k).
(forall (x :: k1). Out arr x -> arr a x) -> In arr a
In ((forall x.
  Out (Body Either ch (->)) x -> Body Either ch (->) Void x)
 -> In (Body Either ch (->)) Void)
-> (forall x.
    Out (Body Either ch (->)) x -> Body Either ch (->) Void x)
-> In (Body Either ch (->)) Void
forall a b. (a -> b) -> a -> b
$ \Out (Body Either ch (->)) x
_ -> (Either ch Void -> Either ch x) -> Body Either ch (->) Void x
forall {k} {k} {k} (t :: k -> k -> k) (ch :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body ((Either ch Void -> Either ch x) -> Body Either ch (->) Void x)
-> (Either ch Void -> Either ch x) -> Body Either ch (->) Void x
forall a b. (a -> b) -> a -> b
$ \case
          Left ch
s -> ch -> Either ch x
forall a b. a -> Either a b
Left ch
s
          Right Void
v -> Void -> Either ch x
forall a. Void -> a
absurd Void
v
     in In (Body Either s (->)) Void
-> Out (Body Either s (->)) Void
-> Poles (Body Either s (->)) Void Void
forall {k} {k1} (arr :: k -> k1 -> *) (a :: k) (b :: k1).
In arr a -> Out arr b -> Poles arr a b
Poles In (Body Either s (->)) Void
forall {ch}. In (Body Either ch (->)) Void
inU Out (Body Either s (->)) Void
forall {a}. Out (Body Either s (->)) a
outU

-- | Unit poles for @Body Either s (K m)@ at @Void@.
instance (Monad m, Pointed s) => HasDual Void (Body Either s (K m)) where
  open :: Poles (Body Either s (K m)) Void Void
open =
    let outU :: Out (Body Either s (K m)) a
outU = (forall x. In (Body Either s (K m)) x -> Body Either s (K m) x a)
-> Out (Body Either s (K m)) a
forall {k} {k1} (arr :: k -> k1 -> *) (a :: k1).
(forall (x :: k). In arr x -> arr x a) -> Out arr a
Out ((forall x. In (Body Either s (K m)) x -> Body Either s (K m) x a)
 -> Out (Body Either s (K m)) a)
-> (forall x.
    In (Body Either s (K m)) x -> Body Either s (K m) x a)
-> Out (Body Either s (K m)) a
forall a b. (a -> b) -> a -> b
$ \In (Body Either s (K m)) x
_ -> K m (Either s x) (Either s a) -> Body Either s (K m) x a
forall {k} {k} {k} (t :: k -> k -> k) (ch :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body (K m (Either s x) (Either s a) -> Body Either s (K m) x a)
-> K m (Either s x) (Either s a) -> Body Either s (K m) x a
forall a b. (a -> b) -> a -> b
$ (Either s x -> m (Either s a)) -> K m (Either s x) (Either s a)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((Either s x -> m (Either s a)) -> K m (Either s x) (Either s a))
-> (Either s x -> m (Either s a)) -> K m (Either s x) (Either s a)
forall a b. (a -> b) -> a -> b
$ \case
          Left s
s -> Either s a -> m (Either s a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (s -> Either s a
forall a b. a -> Either a b
Left s
s)
          Right x
_ -> Either s a -> m (Either s a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (s -> Either s a
forall a b. a -> Either a b
Left s
forall a. Pointed a => a
point)
        inU :: In (Body Either a (K m)) Void
inU = (forall x.
 Out (Body Either a (K m)) x -> Body Either a (K m) Void x)
-> In (Body Either a (K m)) Void
forall {k} {k1} (arr :: k -> k1 -> *) (a :: k).
(forall (x :: k1). Out arr x -> arr a x) -> In arr a
In ((forall x.
  Out (Body Either a (K m)) x -> Body Either a (K m) Void x)
 -> In (Body Either a (K m)) Void)
-> (forall x.
    Out (Body Either a (K m)) x -> Body Either a (K m) Void x)
-> In (Body Either a (K m)) Void
forall a b. (a -> b) -> a -> b
$ \Out (Body Either a (K m)) x
_ -> K m (Either a Void) (Either a x) -> Body Either a (K m) Void x
forall {k} {k} {k} (t :: k -> k -> k) (ch :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body (K m (Either a Void) (Either a x) -> Body Either a (K m) Void x)
-> K m (Either a Void) (Either a x) -> Body Either a (K m) Void x
forall a b. (a -> b) -> a -> b
$ (Either a Void -> m (Either a x))
-> K m (Either a Void) (Either a x)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((Either a Void -> m (Either a x))
 -> K m (Either a Void) (Either a x))
-> (Either a Void -> m (Either a x))
-> K m (Either a Void) (Either a x)
forall a b. (a -> b) -> a -> b
$ \case
          Left a
s -> Either a x -> m (Either a x)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Either a x
forall a b. a -> Either a b
Left a
s)
          Right Void
v -> Void -> m (Either a x)
forall a. Void -> a
absurd Void
v
     in In (Body Either s (K m)) Void
-> Out (Body Either s (K m)) Void
-> Poles (Body Either s (K m)) Void Void
forall {k} {k1} (arr :: k -> k1 -> *) (a :: k) (b :: k1).
In arr a -> Out arr b -> Poles arr a b
Poles In (Body Either s (K m)) Void
forall {a}. In (Body Either a (K m)) Void
inU Out (Body Either s (K m)) Void
forall {a}. Out (Body Either s (K m)) a
outU

-- * Carrier-tensoring composition

-- | Compose two bodies at carriers @ch@ and @ch'@ into a body at carrier
-- @t ch ch'@.  This is the body-level building block of horizontal 2-cell
-- algebra and of the 'Category' instance for 'SomeBody'.
--
-- The composite is
--
-- @
--   assoc .> slide .> strength f .> slide .> strength g .> assoc'
-- @
cascadeBody ::
  (Strength t arr) =>
  Body t ch' arr b c ->
  Body t ch arr a b ->
  Body t (t ch ch') arr a c
cascadeBody :: forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch' :: k)
       (b :: k) (c :: k) (ch :: k) (a :: k).
Strength t arr =>
Body t ch' arr b c
-> Body t ch arr a b -> Body t (t ch ch') arr a c
cascadeBody Body t ch' arr b c
g Body t ch arr a b
f =
  arr (t (t ch ch') a) (t (t ch ch') c) -> Body t (t ch ch') arr a c
forall {k} {k} {k} (t :: k -> k -> k) (ch :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body
    ( arr (t (t ch ch') a) (t ch (t ch' a))
forall (a :: k) (b :: k) (c :: k). 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
        arr (t (t ch ch') a) (t ch (t ch' a))
-> arr (t ch (t ch' a)) (t ch' (t ch a))
-> arr (t (t ch ch') a) (t ch' (t ch a))
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr (t ch (t ch' a)) (t ch' (t ch a))
forall (a :: k) (b :: k) (c :: k). 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
        arr (t (t ch ch') a) (t ch' (t ch a))
-> arr (t ch' (t ch a)) (t ch' (t ch b))
-> arr (t (t ch ch') a) (t ch' (t ch b))
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr (t ch a) (t ch b) -> arr (t ch' (t ch a)) (t ch' (t ch b))
forall (b :: k) (c :: k) (a :: k). 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 (Body t ch arr a b -> arr (t ch a) (t ch b)
forall {k} {k} {k} (t :: k -> k -> k) (ch :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
Body t ch arr a b -> arr (t ch a) (t ch b)
morphism Body t ch arr a b
f)
        arr (t (t ch ch') a) (t ch' (t ch b))
-> arr (t ch' (t ch b)) (t ch (t ch' b))
-> arr (t (t ch ch') a) (t ch (t ch' b))
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr (t ch' (t ch b)) (t ch (t ch' b))
forall (a :: k) (b :: k) (c :: k). 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
        arr (t (t ch ch') a) (t ch (t ch' b))
-> arr (t ch (t ch' b)) (t ch (t ch' c))
-> arr (t (t ch ch') a) (t ch (t ch' c))
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr (t ch' b) (t ch' c) -> arr (t ch (t ch' b)) (t ch (t ch' c))
forall (b :: k) (c :: k) (a :: k). 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 (Body t ch' arr b c -> arr (t ch' b) (t ch' c)
forall {k} {k} {k} (t :: k -> k -> k) (ch :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
Body t ch arr a b -> arr (t ch a) (t ch b)
morphism Body t ch' arr b c
g)
        arr (t (t ch ch') a) (t ch (t ch' c))
-> arr (t ch (t ch' c)) (t (t ch ch') c)
-> arr (t (t ch ch') a) (t (t ch ch') c)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr (t ch (t ch' c)) (t (t ch ch') c)
forall (a :: k) (b :: k) (c :: k). 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'
    )

-- | Pointed carrier-tensoring composition for @t = (,)@ and @arr = (->)@.
--
-- Seeds pair under the tensor, and the composite can be run with
-- 'runSomeBody'.  This is the pointed counterpart to the unpointed
-- 'cascadeBody'.
cascadeSome ::
  SomeBody (,) (->) b c ->
  SomeBody (,) (->) a b ->
  SomeBody (,) (->) a c
cascadeSome :: forall b c a.
SomeBody (,) (->) b c
-> SomeBody (,) (->) a b -> SomeBody (,) (->) a c
cascadeSome (SomeBody ch
s2 Body (,) ch (->) b c
g) (SomeBody ch
s1 Body (,) ch (->) a b
f) =
  (ch, ch) -> Body (,) (ch, ch) (->) a c -> SomeBody (,) (->) a c
forall {k} {k} ch (t :: * -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k).
ch -> Body t ch arr a b -> SomeBody t arr a b
SomeBody (ch
s1, ch
s2) (Body (,) ch (->) b c
-> Body (,) ch (->) a b -> Body (,) (ch, ch) (->) a c
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch' :: k)
       (b :: k) (c :: k) (ch :: k) (a :: k).
Strength t arr =>
Body t ch' arr b c
-> Body t ch arr a b -> Body t (t ch ch') arr a c
cascadeBody Body (,) ch (->) b c
g Body (,) ch (->) a b
f)

-- | 'Category' instance for 'SomeBody'.
--
-- The carrier of the composite is the tensor of the two carriers, and the
-- stored seed is combined with 'seedPair'.  Identity needs a seed at the
-- tensor unit, hence the 'Pointed (Unit t)' requirement.  Tensors whose unit
-- is uninhabited (e.g. 'Either' with @Unit Either = Void@) therefore do not
-- admit an identity; tensors without a canonical value-level pairing (also
-- 'Either', 'Data.These.These') do not admit composition.
instance
  (Strength t arr, Pointed (Unit t), TensorSeed t) =>
  Category (SomeBody t arr)
  where
  id :: forall a. SomeBody t arr a a
  id :: forall a. SomeBody t arr a a
id = Unit t -> Body t (Unit t) arr a a -> SomeBody t arr a a
forall {k} {k} ch (t :: * -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k).
ch -> Body t ch arr a b -> SomeBody t arr a b
SomeBody (Unit t
forall a. Pointed a => a
point :: Unit t) (arr (t (Unit t) a) (t (Unit t) a) -> Body t (Unit t) arr a a
forall {k} {k} {k} (t :: k -> k -> k) (ch :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body arr (t (Unit t) a) (t (Unit t) a)
forall a. arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id)
  {-# INLINE id #-}

  (.) :: forall a b c. SomeBody t arr b c -> SomeBody t arr a b -> SomeBody t arr a c
  SomeBody ch
s2 Body t ch arr b c
g . :: forall a b c.
SomeBody t arr b c -> SomeBody t arr a b -> SomeBody t arr a c
. SomeBody ch
s1 Body t ch arr a b
f = t ch ch -> Body t (t ch ch) arr a c -> SomeBody t arr a c
forall {k} {k} ch (t :: * -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k).
ch -> Body t ch arr a b -> SomeBody t arr a b
SomeBody (ch -> ch -> t ch ch
forall a b. a -> b -> t a b
forall (t :: * -> * -> *) a b. TensorSeed t => a -> b -> t a b
seedPair ch
s1 ch
s2) (Body t ch arr b c -> Body t ch arr a b -> Body t (t ch ch) arr a c
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch' :: k)
       (b :: k) (c :: k) (ch :: k) (a :: k).
Strength t arr =>
Body t ch' arr b c
-> Body t ch arr a b -> Body t (t ch ch') arr a c
cascadeBody Body t ch arr b c
g Body t ch arr a b
f)
  {-# INLINE (.) #-}