{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

-- | Structural semantics for traced monoidal categories.
--
-- This module collects the structural superclass chain
-- @Channel → Strength → Traced@ and all base instances for the standard
-- base arrows @(->)@ and @K m@.  These classes
-- describe the monoidal structure, tensorial strength, and feedback-fixing
-- trace that underlie the syntax in "Circuit.Trace".
--
-- 'assoc' and 'assoc'' here reassociate /rightward/ and /leftward/
-- respectively. The monomorphic helpers in "Circuit.Tensor" have the same
-- names but the opposite directions. Also, 'slide' here is the slide
-- @t a (t b c) -> t b (t a c)@; the symmetric braiding @t a b -> t b a@
-- lives in Circuit.Tensor as braid. Where both structures exist,
-- @slide = assoc' .> tensor braid id .> assoc@.
--
-- Kind-polymorphic: @t@ and @arr@ share object kind (inferred via PolyKinds).
module Circuit.Channel
  ( Channel (..),
    Strength (..),
    Traced (..),
  )
where

import Circuit.Category (Category (..), K (..))
import Control.Monad.Fix (MonadFix, mfix)
import Data.These (These (..))
import GHC.Exts (PromptTag#, control0#, newPromptTag#, prompt#)
import GHC.IO (IO (..))
import Prelude hiding (id, (.))

-- $setup
-- >>> :set -XLambdaCase
-- >>> import Circuit.Category ((.>))
-- >>> import Circuit.Channel (Traced (..))
-- >>> import Circuit.Tensor (unitl, unitl')
-- >>> import Circuit.Category (K (..), runK)
-- >>> import Data.Void (Void)

-- * Channel

-- | A monoidal structure on the tensor @t@ internal to the category @arr@.
--
-- Provides the associator and braiding required to reassociate and braid
-- nested tensor values inside an arrow. This is the structure that traced
-- categories inherit as a superclass.
--
-- The previous quantified superclass that stated closure of an object
-- constraint under the tensor has been removed along with the @Ob@
-- apparatus; composite-object legitimacy is an audit concern.
class
  (Category arr) =>
  Channel t arr
  where
  -- | Reassociate to the right: @t (t a b) c -> t a (t b c)@.
  assoc ::
    arr (t (t a b) c) (t a (t b c))

  -- | Inverse reassociation: @t a (t b c) -> t (t a b) c@.
  assoc' ::
    arr (t a (t b c)) (t (t a b) c)

  -- | Swap the two outer positions, leaving the inner payload in place:
  -- @t a (t b c) -> t b (t a c)@.
  slide ::
    arr (t a (t b c)) (t b (t a c))

-- | Cartesian monoidal structure for @(,)@.
--
-- >>> assoc ((1, 2), 3) :: (Int, (Int, Int))
-- (1,(2,3))
--
-- >>> assoc' (1, (2, 3)) :: ((Int, Int), Int)
-- ((1,2),3)
--
-- >>> (assoc .> assoc') ((1, 2), 3) :: ((Int, Int), Int)
-- ((1,2),3)
--
-- >>> slide (1, (2, 3)) :: (Int, (Int, Int))
-- (2,(1,3))
instance Channel (,) (->) where
  assoc :: forall a b c. ((a, b), c) -> (a, (b, c))
assoc ~(~(a
a, b
b), c
c) = (a
a, (b
b, c
c))
  assoc' :: forall a b c. (a, (b, c)) -> ((a, b), c)
assoc' ~(a
a, ~(b
b, c
c)) = ((a
a, b
b), c
c)
  slide :: forall a b c. (a, (b, c)) -> (b, (a, c))
slide ~(a
a, ~(b
b, c
c)) = (b
b, (a
a, c
c))

-- | Cocartesian monoidal structure for @Either@.
--
-- >>> assoc (Left (Left 1) :: Either (Either Int Bool) Char) :: Either Int (Either Bool Char)
-- Left 1
--
-- >>> assoc' (Left 1 :: Either Int (Either Bool Char)) :: Either (Either Int Bool) Char
-- Left (Left 1)
--
-- >>> slide (Left 1 :: Either Int (Either Bool Char)) :: Either Bool (Either Int Char)
-- Right (Left 1)
instance Channel Either (->) where
  assoc :: forall a b c. Either (Either a b) c -> Either a (Either b c)
assoc (Left (Left a
a)) = a -> Either a (Either b c)
forall a b. a -> Either a b
Left a
a
  assoc (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)
  assoc (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)
  assoc' :: forall a b c. Either a (Either b c) -> Either (Either a b) c
assoc' (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)
  assoc' (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)
  assoc' (Right (Right c
c)) = c -> Either (Either a b) c
forall a b. b -> Either a b
Right c
c
  slide :: forall a b c. Either a (Either b c) -> Either b (Either a c)
slide (Left a
a) = Either a c -> Either b (Either a c)
forall a b. b -> Either a b
Right (a -> Either a c
forall a b. a -> Either a b
Left a
a)
  slide (Right (Left b
b)) = b -> Either b (Either a c)
forall a b. a -> Either a b
Left b
b
  slide (Right (Right c
c)) = Either a c -> Either b (Either a c)
forall a b. b -> Either a b
Right (c -> Either a c
forall a b. b -> Either a b
Right c
c)

-- | Inclusive monoidal structure for @These@.
--
-- @These@ sits above both @(,)@ and 'Either': 'This' is the residual-only
-- branch, 'That' is the payload-only branch, and 'These' carries both.
instance Channel These (->) where
  assoc :: forall a b c. These (These a b) c -> These a (These b c)
assoc (This (This a
a)) = a -> These a (These b c)
forall a b. a -> These a b
This a
a
  assoc (This (That b
b)) = These b c -> These a (These b c)
forall a b. b -> These a b
That (b -> These b c
forall a b. a -> These a b
This b
b)
  assoc (This (These a
a b
b)) = a -> These b c -> These a (These b c)
forall a b. a -> b -> These a b
These a
a (b -> These b c
forall a b. a -> These a b
This b
b)
  assoc (That c
c) = These b c -> These a (These b c)
forall a b. b -> These a b
That (c -> These b c
forall a b. b -> These a b
That c
c)
  assoc (These (This a
a) c
c) = a -> These b c -> These a (These b c)
forall a b. a -> b -> These a b
These a
a (c -> These b c
forall a b. b -> These a b
That c
c)
  assoc (These (That b
b) c
c) = These b c -> These a (These b c)
forall a b. b -> These a b
That (b -> c -> These b c
forall a b. a -> b -> These a b
These b
b c
c)
  assoc (These (These a
a b
b) c
c) = a -> These b c -> These a (These b c)
forall a b. a -> b -> These a b
These a
a (b -> c -> These b c
forall a b. a -> b -> These a b
These b
b c
c)
  assoc' :: forall a b c. These a (These b c) -> These (These a b) c
assoc' (This a
a) = These a b -> These (These a b) c
forall a b. a -> These a b
This (a -> These a b
forall a b. a -> These a b
This a
a)
  assoc' (That (This b
b)) = These a b -> These (These a b) c
forall a b. a -> These a b
This (b -> These a b
forall a b. b -> These a b
That b
b)
  assoc' (That (That c
c)) = c -> These (These a b) c
forall a b. b -> These a b
That c
c
  assoc' (That (These b
b c
c)) = These a b -> c -> These (These a b) c
forall a b. a -> b -> These a b
These (b -> These a b
forall a b. b -> These a b
That b
b) c
c
  assoc' (These a
a (This b
b)) = These a b -> These (These a b) c
forall a b. a -> These a b
This (a -> b -> These a b
forall a b. a -> b -> These a b
These a
a b
b)
  assoc' (These a
a (That c
c)) = These a b -> c -> These (These a b) c
forall a b. a -> b -> These a b
These (a -> These a b
forall a b. a -> These a b
This a
a) c
c
  assoc' (These a
a (These b
b c
c)) = These a b -> c -> These (These a b) c
forall a b. a -> b -> These a b
These (a -> b -> These a b
forall a b. a -> b -> These a b
These a
a b
b) c
c
  slide :: forall a b c. These a (These b c) -> These b (These a c)
slide (This a
a) = These a c -> These b (These a c)
forall a b. b -> These a b
That (a -> These a c
forall a b. a -> These a b
This a
a)
  slide (That (This b
b)) = b -> These b (These a c)
forall a b. a -> These a b
This b
b
  slide (That (That c
c)) = These a c -> These b (These a c)
forall a b. b -> These a b
That (c -> These a c
forall a b. b -> These a b
That c
c)
  slide (That (These b
b c
c)) = b -> These a c -> These b (These a c)
forall a b. a -> b -> These a b
These b
b (c -> These a c
forall a b. b -> These a b
That c
c)
  slide (These a
a (This b
b)) = b -> These a c -> These b (These a c)
forall a b. a -> b -> These a b
These b
b (a -> These a c
forall a b. a -> These a b
This a
a)
  slide (These a
a (That c
c)) = These a c -> These b (These a c)
forall a b. b -> These a b
That (a -> c -> These a c
forall a b. a -> b -> These a b
These a
a c
c)
  slide (These a
a (These b
b c
c)) = b -> These a c -> These b (These a c)
forall a b. a -> b -> These a b
These b
b (a -> c -> These a c
forall a b. a -> b -> These a b
These a
a c
c)

-- * Strength

-- | Tensorial strength for a tensor @t@ inside a category @arr@.
--
-- 'strength' tensors a plain morphism with the ambient channel. It is
-- /not/ a syntactic inverse of 'trace'; it is the strength
-- ("tensorial strength") of the tensor @t@ acting on morphisms.
class (Channel t arr) => Strength t arr where
  strength ::
    arr b c ->
    arr (t a b) (t a c)

-- | Cartesian tensorial strength for @(,)@.
--
-- The implementation uses explicit projections so that the result pair
-- constructor exists before the feedback channel is forced; this keeps
-- fused 'Circuit.Trace.yank' bodies productive even when the body has a strict
-- top-level pattern on the recursive channel.
--
-- >>> strength (+1) (error "forced" :: (Int, Int)) `seq` ()
-- ()
instance Strength (,) (->) where
  strength :: forall b c a. (b -> c) -> (a, b) -> (a, c)
strength b -> c
f (a, b)
p = ((a, b) -> a
forall a b. (a, b) -> a
fst (a, b)
p, b -> c
f ((a, b) -> b
forall a b. (a, b) -> b
snd (a, b)
p))

-- | Either tensorial strength for @Either@.
--
-- 'strength' is the functorial action under 'Either'.
instance Strength Either (->) where
  strength :: forall b c a. (b -> c) -> Either a b -> Either a c
strength = (b -> c) -> Either a b -> Either a c
forall a b. (a -> b) -> Either a a -> Either a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap

-- | Inclusive tensorial strength for @These@.
--
-- 'strength' applies the payload morphism to the 'That' branch and the
-- 'These' branch, leaving the 'This' residual branch untouched.
instance Strength These (->) where
  strength :: forall b c a. (b -> c) -> These a b -> These a c
strength b -> c
_ (This a
a) = a -> These a c
forall a b. a -> These a b
This a
a
  strength b -> c
f (That b
b) = c -> These a c
forall a b. b -> These a b
That (b -> c
f b
b)
  strength b -> c
f (These a
a b
b) = a -> c -> These a c
forall a b. a -> b -> These a b
These a
a (b -> c
f b
b)

-- * Traced

-- | A trace over a morphism @arr@ and tensor @t@.
--
-- @trace@ closes the feedback loop, eliminating the tensor channel.
-- It extends the 'Strength' structure with the feedback-fixing operation.
--
-- Object constraints on the feedback channel (@a@) used to let constrained
-- categories instance this class lawfully; those constraints are now
-- explicit at the instance site rather than inherited from a constraint
-- family.
--
-- Law note: the traced-category Sliding axiom is restricted in the
-- premonoidal setting. Benton & Hyland, "Traced Premonoidal Categories"
-- (2003, Def 3.2) replace unrestricted Sliding with /Central Sliding/:
-- a morphism @g@ may slide past the trace only when @g@ is central.
-- Dually, /Centre Preservation/ says @trace f@ is central whenever @f@ is.
-- This class does not enforce the side-conditions at the type level; lawful
-- instances must guarantee them by construction. See the @circuits-axioma@
-- sliding oracles for witnesses that the side-condition is not vacuous.
class (Strength t arr) => Traced t arr where
  trace ::
    arr (t a b) (t a c) ->
    arr b c

-- * Cartesian tensor — lazy knot

-- | The cartesian trace ties a lazy knot: the feedback value @a@ and
-- output @c@ are produced simultaneously in a single recursive binding.
--
-- Only works in a lazy setting — the feedback value is a self-referential
-- thunk.  In a strict language this binding is circular and divergent.
-- Haskell's lazy evaluation makes cyclic sharing possible without an
-- explicit fixpoint operator.
--
-- >>> :{
-- let powers (ns, ()) =
--       (1 : map (*2) ns, take 5 ns)
-- :}
--
-- >>> trace powers () :: [Integer]
-- [1,2,4,8,16]
--
-- >>> trace (\(acc, x) -> (acc, x + 1)) 5
-- 6
--
-- Vanishing (a): tracing over the unit does nothing.
--
-- The unit is @()@ for the @(,)@ tensor. The unitor laws say that
-- threading a plain payload through the unit channel is the same as
-- applying the payload morphism directly.
--
-- >>> let f = (+1) :: Int -> Int
-- >>> trace (unitl' . f . unitl :: ((), Int) -> ((), Int)) 5
-- 6
--
-- >>> trace ((unitl' . (+ 3) . unitl) :: ((), Int) -> ((), Int)) 0
-- 3
--
-- Yanking: tracing a braid is the identity.
--
-- >>> let braid (x, y) = (y, x)
-- >>> trace braid 42
-- 42
--
-- >>> trace ((\(a, b) -> (b, a)) :: (Int, Int) -> (Int, Int)) 42
-- 42
--
-- Tightening: payload morphisms pass freely through the trace.
--
-- >>> let f (x, a) = (x, a)
-- >>> trace ((\(x, a) -> (x, a + 1)) . f . (\(x, a) -> (x, a * 2))) 5
-- 11
--
-- Sliding: a morphism on the channel slides from one side to the other.
--
-- >>> let braid (x, y) = (y, x)
-- >>> trace ((\(a, b) -> (b, a + 1)) . (\(a, b) -> (b, a)) :: (Int, Int) -> (Int, Int)) 5
-- 6
--
-- >>> trace ((\(a, b) -> (b + 1, a)) :: (Int, Int) -> (Int, Int)) 5
-- 6
--
-- Strength: an independent payload wire is invisible to the trace.
--
-- >>> let f (x, c) = (x, c + 1)
-- >>> let g (x, (a, c)) = (x', (a * 2, d)) where (x', d) = f (x, c)
-- >>> trace g (3, 5)
-- (6,6)
--
-- >>> trace ((\(x, (p, q)) -> (x, (p + 7, q + 1))) :: (Int, (Int, Int)) -> (Int, (Int, Int))) (0, 5)
-- (7,6)
instance Traced (,) (->) where
  trace :: forall a b c. ((a, b) -> (a, c)) -> b -> c
trace (a, b) -> (a, c)
f b
b = let ~(a
a, c
c) = (a, b) -> (a, c)
f (a
a, b
b) in c
c

-- * Either tensor — iteration

-- | The Either trace iterates: 'Left' feeds back (continue), 'Right'
-- terminates (exit). A compact, under-appreciated pattern for loops in Haskell.
--
-- >>> :{
-- let fac (n, acc) | n <= 1    = Right acc
--                  | otherwise = Left (n - 1, n * acc)
-- :}
--
-- >>> trace (either fac fac) (5, 1 :: Int)
-- 120
--
-- >>> :{
-- let countdown = \case
--       Left n | n > 0 -> Left (n - 1)
--              | otherwise -> Right n
--       Right n | n > 0 -> Left (n - 1)
--               | otherwise -> Right n
-- :}
--
-- >>> trace countdown (3 :: Int)
-- 0
--
-- Vanishing (a): tracing over the unit does nothing.
--
-- The unit is 'Data.Void.Void' for the 'Either' tensor. The unitor
-- laws say that threading a plain payload through the unit channel is the
-- same as applying the payload morphism directly.
--
-- >>> let f = (+1) :: Int -> Int
-- >>> trace (unitl' . f . unitl :: Either Void Int -> Either Void Int) 5
-- 6
--
-- >>> trace ((unitl' . (+ 3) . unitl) :: Either Void Int -> Either Void Int) 0
-- 3
--
-- Yanking: tracing a braid is the identity.
--
-- >>> :{
-- let swapEither (Left x)  = Right x
--     swapEither (Right x) = Left x
-- :}
--
-- >>> trace swapEither 42
-- 42
--
-- >>> trace ((\e -> case e of Left a -> Right a; Right a -> Left a) :: Either Int Int -> Either Int Int) 42
-- 42
--
-- Tightening: payload morphisms pass freely through the trace.
--
-- >>> let f = fmap ((+1) :: Int -> Int) . fmap ((*2) :: Int -> Int)
-- >>> trace (f :: Either Void Int -> Either Void Int) 5
-- 11
--
-- >>> trace (fmap ((+1) :: Int -> Int) . fmap ((*2) :: Int -> Int) :: Either Void Int -> Either Void Int) 5
-- 11
instance Traced Either (->) where
  trace :: forall a b c. (Either a b -> Either a c) -> b -> c
trace Either a b -> Either a c
f b
b = Either a b -> c
go (b -> Either a b
forall a b. b -> Either a b
Right b
b)
    where
      go :: Either a b -> c
go Either a b
x = case Either a b -> Either a c
f Either a b
x of
        Right c
c -> c
c
        Left a
a -> Either a b -> c
go (a -> Either a b
forall a b. a -> Either a b
Left a
a)

-- * K m — monoidal structure

-- | Cartesian monoidal structure for @K m@ with @(,)@.
instance (Monad m) => Channel (,) (K m) where
  assoc :: forall a b c. K m ((a, b), c) (a, (b, c))
assoc = (((a, b), c) -> m (a, (b, c))) -> K m ((a, b), c) (a, (b, c))
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((((a, b), c) -> m (a, (b, c))) -> K m ((a, b), c) (a, (b, c)))
-> (((a, b), c) -> m (a, (b, c))) -> K m ((a, b), c) (a, (b, c))
forall a b. (a -> b) -> a -> b
$ \ ~(~(a
a, b
b), c
c) -> (a, (b, c)) -> m (a, (b, c))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a, (b
b, c
c))
  assoc' :: forall a b c. K m (a, (b, c)) ((a, b), c)
assoc' = ((a, (b, c)) -> m ((a, b), c)) -> K m (a, (b, c)) ((a, b), c)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K (((a, (b, c)) -> m ((a, b), c)) -> K m (a, (b, c)) ((a, b), c))
-> ((a, (b, c)) -> m ((a, b), c)) -> K m (a, (b, c)) ((a, b), c)
forall a b. (a -> b) -> a -> b
$ \ ~(a
a, ~(b
b, c
c)) -> ((a, b), c) -> m ((a, b), c)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((a
a, b
b), c
c)
  slide :: forall a b c. K m (a, (b, c)) (b, (a, c))
slide = ((a, (b, c)) -> m (b, (a, c))) -> K m (a, (b, c)) (b, (a, c))
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K (((a, (b, c)) -> m (b, (a, c))) -> K m (a, (b, c)) (b, (a, c)))
-> ((a, (b, c)) -> m (b, (a, c))) -> K m (a, (b, c)) (b, (a, c))
forall a b. (a -> b) -> a -> b
$ \ ~(a
a, ~(b
b, c
c)) -> (b, (a, c)) -> m (b, (a, c))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b
b, (a
a, c
c))

-- | Cocartesian monoidal structure for @K m@ with 'Either'.
instance (Monad m) => Channel Either (K m) where
  assoc :: forall a b c. K m (Either (Either a b) c) (Either a (Either b c))
assoc = (Either (Either a b) c -> m (Either a (Either b c)))
-> K m (Either (Either a b) c) (Either a (Either b c))
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((Either (Either a b) c -> m (Either a (Either b c)))
 -> K m (Either (Either a b) c) (Either a (Either b c)))
-> (Either (Either a b) c -> m (Either a (Either b c)))
-> K m (Either (Either a b) c) (Either a (Either b c))
forall a b. (a -> b) -> a -> b
$ \case
    Left (Left a
a) -> Either a (Either b c) -> m (Either a (Either b c))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Either a (Either b c)
forall a b. a -> Either a b
Left a
a)
    Left (Right b
b) -> Either a (Either b c) -> m (Either a (Either b c))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (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))
    Right c
c -> Either a (Either b c) -> m (Either a (Either b c))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (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))
  assoc' :: forall a b c. K m (Either a (Either b c)) (Either (Either a b) c)
assoc' = (Either a (Either b c) -> m (Either (Either a b) c))
-> K m (Either a (Either b c)) (Either (Either a b) c)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((Either a (Either b c) -> m (Either (Either a b) c))
 -> K m (Either a (Either b c)) (Either (Either a b) c))
-> (Either a (Either b c) -> m (Either (Either a b) c))
-> K m (Either a (Either b c)) (Either (Either a b) c)
forall a b. (a -> b) -> a -> b
$ \case
    Left a
a -> Either (Either a b) c -> m (Either (Either a b) c)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (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))
    Right (Left b
b) -> Either (Either a b) c -> m (Either (Either a b) c)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (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))
    Right (Right c
c) -> Either (Either a b) c -> m (Either (Either a b) c)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (c -> Either (Either a b) c
forall a b. b -> Either a b
Right c
c)
  slide :: forall a b c. K m (Either a (Either b c)) (Either b (Either a c))
slide = (Either a (Either b c) -> m (Either b (Either a c)))
-> K m (Either a (Either b c)) (Either b (Either a c))
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((Either a (Either b c) -> m (Either b (Either a c)))
 -> K m (Either a (Either b c)) (Either b (Either a c)))
-> (Either a (Either b c) -> m (Either b (Either a c)))
-> K m (Either a (Either b c)) (Either b (Either a c))
forall a b. (a -> b) -> a -> b
$ \case
    Left a
a -> Either b (Either a c) -> m (Either b (Either a c))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either a c -> Either b (Either a c)
forall a b. b -> Either a b
Right (a -> Either a c
forall a b. a -> Either a b
Left a
a))
    Right (Left b
b) -> Either b (Either a c) -> m (Either b (Either a c))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b -> Either b (Either a c)
forall a b. a -> Either a b
Left b
b)
    Right (Right c
c) -> Either b (Either a c) -> m (Either b (Either a c))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either a c -> Either b (Either a c)
forall a b. b -> Either a b
Right (c -> Either a c
forall a b. b -> Either a b
Right c
c))

-- | Inclusive monoidal structure for @K m@ with 'These'.
instance (Monad m) => Channel These (K m) where
  assoc :: forall a b c. K m (These (These a b) c) (These a (These b c))
assoc =
    (These (These a b) c -> m (These a (These b c)))
-> K m (These (These a b) c) (These a (These b c))
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((These (These a b) c -> m (These a (These b c)))
 -> K m (These (These a b) c) (These a (These b c)))
-> (These (These a b) c -> m (These a (These b c)))
-> K m (These (These a b) c) (These a (These b c))
forall a b. (a -> b) -> a -> b
$
      These a (These b c) -> m (These a (These b c))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (These a (These b c) -> m (These a (These b c)))
-> (These (These a b) c -> These a (These b c))
-> These (These a b) c
-> m (These a (These 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
        This (This a
a) -> a -> These a (These b c)
forall a b. a -> These a b
This a
a
        This (That b
b) -> These b c -> These a (These b c)
forall a b. b -> These a b
That (b -> These b c
forall a b. a -> These a b
This b
b)
        This (These a
a b
b) -> a -> These b c -> These a (These b c)
forall a b. a -> b -> These a b
These a
a (b -> These b c
forall a b. a -> These a b
This b
b)
        That c
c -> These b c -> These a (These b c)
forall a b. b -> These a b
That (c -> These b c
forall a b. b -> These a b
That c
c)
        These (This a
a) c
c -> a -> These b c -> These a (These b c)
forall a b. a -> b -> These a b
These a
a (c -> These b c
forall a b. b -> These a b
That c
c)
        These (That b
b) c
c -> These b c -> These a (These b c)
forall a b. b -> These a b
That (b -> c -> These b c
forall a b. a -> b -> These a b
These b
b c
c)
        These (These a
a b
b) c
c -> a -> These b c -> These a (These b c)
forall a b. a -> b -> These a b
These a
a (b -> c -> These b c
forall a b. a -> b -> These a b
These b
b c
c)
  assoc' :: forall a b c. K m (These a (These b c)) (These (These a b) c)
assoc' =
    (These a (These b c) -> m (These (These a b) c))
-> K m (These a (These b c)) (These (These a b) c)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((These a (These b c) -> m (These (These a b) c))
 -> K m (These a (These b c)) (These (These a b) c))
-> (These a (These b c) -> m (These (These a b) c))
-> K m (These a (These b c)) (These (These a b) c)
forall a b. (a -> b) -> a -> b
$
      These (These a b) c -> m (These (These a b) c)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (These (These a b) c -> m (These (These a b) c))
-> (These a (These b c) -> These (These a b) c)
-> These a (These b c)
-> m (These (These 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
        This a
a -> These a b -> These (These a b) c
forall a b. a -> These a b
This (a -> These a b
forall a b. a -> These a b
This a
a)
        That (This b
b) -> These a b -> These (These a b) c
forall a b. a -> These a b
This (b -> These a b
forall a b. b -> These a b
That b
b)
        That (That c
c) -> c -> These (These a b) c
forall a b. b -> These a b
That c
c
        That (These b
b c
c) -> These a b -> c -> These (These a b) c
forall a b. a -> b -> These a b
These (b -> These a b
forall a b. b -> These a b
That b
b) c
c
        These a
a (This b
b) -> These a b -> These (These a b) c
forall a b. a -> These a b
This (a -> b -> These a b
forall a b. a -> b -> These a b
These a
a b
b)
        These a
a (That c
c) -> These a b -> c -> These (These a b) c
forall a b. a -> b -> These a b
These (a -> These a b
forall a b. a -> These a b
This a
a) c
c
        These a
a (These b
b c
c) -> These a b -> c -> These (These a b) c
forall a b. a -> b -> These a b
These (a -> b -> These a b
forall a b. a -> b -> These a b
These a
a b
b) c
c
  slide :: forall a b c. K m (These a (These b c)) (These b (These a c))
slide =
    (These a (These b c) -> m (These b (These a c)))
-> K m (These a (These b c)) (These b (These a c))
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((These a (These b c) -> m (These b (These a c)))
 -> K m (These a (These b c)) (These b (These a c)))
-> (These a (These b c) -> m (These b (These a c)))
-> K m (These a (These b c)) (These b (These a c))
forall a b. (a -> b) -> a -> b
$
      These b (These a c) -> m (These b (These a c))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (These b (These a c) -> m (These b (These a c)))
-> (These a (These b c) -> These b (These a c))
-> These a (These b c)
-> m (These b (These 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
        This a
a -> These a c -> These b (These a c)
forall a b. b -> These a b
That (a -> These a c
forall a b. a -> These a b
This a
a)
        That (This b
b) -> b -> These b (These a c)
forall a b. a -> These a b
This b
b
        That (That c
c) -> These a c -> These b (These a c)
forall a b. b -> These a b
That (c -> These a c
forall a b. b -> These a b
That c
c)
        That (These b
b c
c) -> b -> These a c -> These b (These a c)
forall a b. a -> b -> These a b
These b
b (c -> These a c
forall a b. b -> These a b
That c
c)
        These a
a (This b
b) -> b -> These a c -> These b (These a c)
forall a b. a -> b -> These a b
These b
b (a -> These a c
forall a b. a -> These a b
This a
a)
        These a
a (That c
c) -> These a c -> These b (These a c)
forall a b. b -> These a b
That (a -> c -> These a c
forall a b. a -> b -> These a b
These a
a c
c)
        These a
a (These b
b c
c) -> b -> These a c -> These b (These a c)
forall a b. a -> b -> These a b
These b
b (a -> c -> These a c
forall a b. a -> b -> These a b
These a
a c
c)

-- * K m (,) — lazy knot via MonadFix

-- | Traced for @K m@ with the cartesian tensor, requiring @MonadFix m@.
--
-- The lazy knot is tied via 'mfix'. The feedback channel is lazy in the
-- recursive binding — the body must not force the feedback value before
-- producing it, or 'mfix' will diverge (just as the pure @(,)@ trace
-- black-holes on strict fields).
--
-- >>> :{
-- let fibs = K $ \(fibs, ()) ->
--       pure (0 : 1 : zipWith (+) fibs (drop 1 fibs), take 3 fibs)
-- :}
--
-- >>> runK (trace fibs) ()
-- [0,1,1]
instance (Monad m) => Strength (,) (K m) where
  strength :: forall b c a. K m b c -> K m (a, b) (a, c)
strength (K b -> m c
f) =
    ((a, b) -> m (a, c)) -> K m (a, b) (a, c)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K
      ( \(a, b)
p -> do
          c <- b -> m c
f ((a, b) -> b
forall a b. (a, b) -> b
snd (a, b)
p)
          pure (fst p, c)
      )

instance (MonadFix m) => Traced (,) (K m) where
  trace :: forall a b c. K m (a, b) (a, c) -> K m b c
trace (K (a, b) -> m (a, c)
f) =
    (b -> m c) -> K m b c
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K
      ( \b
b -> do
          (_, c) <- ((a, c) -> m (a, c)) -> m (a, c)
forall a. (a -> m a) -> m a
forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
mfix (((a, c) -> m (a, c)) -> m (a, c))
-> ((a, c) -> m (a, c)) -> m (a, c)
forall a b. (a -> b) -> a -> b
$ \ ~(a
s, c
_) -> (a, b) -> m (a, c)
f (a
s, b
b)
          pure c
      )

-- * K m Either — iteration for any Monad

-- | Traced for @K m@ with the 'Either' tensor, for any @Monad m@.
--
-- Iterates by feeding 'Left' back into the step function until a 'Right'
-- is produced. Uses plain recursion — builds stack proportional to
-- iteration count.
--
-- >>> :{
-- let countTo target = K $ \case
--       Left n | n < target -> pure (Left (n + 1))
--              | otherwise  -> pure (Right n)
--       Right ()            -> pure (Left 0)
-- :}
--
-- >>> runK (trace (countTo (3 :: Int))) ()
-- 3
--
-- This instance is @OVERLAPPABLE@: the IO-specific instance below takes
-- priority for @IO@, providing constant-stack iteration via delimited
-- continuations.
instance (Monad m) => Strength Either (K m) where
  strength :: forall b c a. K m b c -> K m (Either a b) (Either a c)
strength (K b -> m c
f) =
    (Either a b -> m (Either a c)) -> K m (Either a b) (Either a c)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((Either a b -> m (Either a c)) -> K m (Either a b) (Either a c))
-> (Either a b -> m (Either a c)) -> K m (Either a b) (Either a c)
forall a b. (a -> b) -> a -> b
$ \case
      Left a
a -> Either a c -> m (Either a c)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Either a c
forall a b. a -> Either a b
Left a
a)
      Right b
b -> c -> Either a c
forall a b. b -> Either a b
Right (c -> Either a c) -> m c -> m (Either a c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> m c
f b
b

-- | Inclusive tensorial strength for @K m@ with 'These'.
instance (Monad m) => Strength These (K m) where
  strength :: forall b c a. K m b c -> K m (These a b) (These a c)
strength (K b -> m c
f) =
    (These a b -> m (These a c)) -> K m (These a b) (These a c)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((These a b -> m (These a c)) -> K m (These a b) (These a c))
-> (These a b -> m (These a c)) -> K m (These a b) (These a c)
forall a b. (a -> b) -> a -> b
$ \case
      This a
a -> These a c -> m (These a c)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> These a c
forall a b. a -> These a b
This a
a)
      That b
b -> c -> These a c
forall a b. b -> These a b
That (c -> These a c) -> m c -> m (These a c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> m c
f b
b
      These a
a b
b -> a -> c -> These a c
forall a b. a -> b -> These a b
These a
a (c -> These a c) -> m c -> m (These a c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> m c
f b
b

instance {-# OVERLAPPABLE #-} (Monad m) => Traced Either (K m) where
  trace :: forall a b c. K m (Either a b) (Either a c) -> K m b c
trace (K Either a b -> m (Either a c)
f) =
    (b -> m c) -> K m b c
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((b -> m c) -> K m b c) -> (b -> m c) -> K m b c
forall a b. (a -> b) -> a -> b
$ \b
b -> Either a b -> m c
go (b -> Either a b
forall a b. b -> Either a b
Right b
b)
    where
      go :: Either a b -> m c
go Either a b
x =
        Either a b -> m (Either a c)
f Either a b
x m (Either a c) -> (Either a c -> m c) -> m c
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Right c
c -> c -> m c
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure c
c
          Left a
a -> Either a b -> m c
go (a -> Either a b
forall a b. a -> Either a b
Left a
a)

-- * K IO Either — delimited continuations (constant stack)

-- | GHC delimited-continuation primops.
data PromptTag a = PromptTag (PromptTag# a)

-- | Create a new prompt tag for delimited continuations.
newPromptTag :: IO (PromptTag a)
newPromptTag :: forall a. IO (PromptTag a)
newPromptTag =
  (State# RealWorld -> (# State# RealWorld, PromptTag a #))
-> IO (PromptTag a)
forall a. (State# RealWorld -> (# State# RealWorld, a #)) -> IO a
IO
    ( \State# RealWorld
s ->
        case State# RealWorld -> (# State# RealWorld, PromptTag# a #)
forall a. State# RealWorld -> (# State# RealWorld, PromptTag# a #)
newPromptTag# State# RealWorld
s of
          (# State# RealWorld
s', PromptTag# a
t #) -> (# State# RealWorld
s', PromptTag# a -> PromptTag a
forall a. PromptTag# a -> PromptTag a
PromptTag PromptTag# a
t #)
    )

-- | Run an IO computation under a prompt boundary.
prompt :: PromptTag a -> IO a -> IO a
prompt :: forall a. PromptTag a -> IO a -> IO a
prompt (PromptTag PromptTag# a
t) (IO State# RealWorld -> (# State# RealWorld, a #)
m) = (State# RealWorld -> (# State# RealWorld, a #)) -> IO a
forall a. (State# RealWorld -> (# State# RealWorld, a #)) -> IO a
IO (PromptTag# a
-> (State# RealWorld -> (# State# RealWorld, a #))
-> State# RealWorld
-> (# State# RealWorld, a #)
forall a.
PromptTag# a
-> (State# RealWorld -> (# State# RealWorld, a #))
-> State# RealWorld
-> (# State# RealWorld, a #)
prompt# PromptTag# a
t State# RealWorld -> (# State# RealWorld, a #)
m)

-- | Captures the continuation up to the nearest prompt with the matching tag.
control0 :: forall a b. PromptTag a -> ((IO b -> IO a) -> IO a) -> IO b
control0 :: forall a b. PromptTag a -> ((IO b -> IO a) -> IO a) -> IO b
control0 (PromptTag PromptTag# a
t) (IO b -> IO a) -> IO a
f = (State# RealWorld -> (# State# RealWorld, b #)) -> IO b
forall a. (State# RealWorld -> (# State# RealWorld, a #)) -> IO a
IO (PromptTag# a
-> (((State# RealWorld -> (# State# RealWorld, b #))
     -> State# RealWorld -> (# State# RealWorld, a #))
    -> State# RealWorld -> (# State# RealWorld, a #))
-> State# RealWorld
-> (# State# RealWorld, b #)
forall a b.
PromptTag# a
-> (((State# RealWorld -> (# State# RealWorld, b #))
     -> State# RealWorld -> (# State# RealWorld, a #))
    -> State# RealWorld -> (# State# RealWorld, a #))
-> State# RealWorld
-> (# State# RealWorld, b #)
control0# PromptTag# a
t ((State# RealWorld -> (# State# RealWorld, b #))
 -> State# RealWorld -> (# State# RealWorld, a #))
-> State# RealWorld -> (# State# RealWorld, a #)
arg)
  where
    arg :: ((State# RealWorld -> (# State# RealWorld, b #))
 -> State# RealWorld -> (# State# RealWorld, a #))
-> State# RealWorld -> (# State# RealWorld, a #)
arg (State# RealWorld -> (# State# RealWorld, b #))
-> State# RealWorld -> (# State# RealWorld, a #)
f# State# RealWorld
s = case (IO b -> IO a) -> IO a
f (\(IO State# RealWorld -> (# State# RealWorld, b #)
x) -> (State# RealWorld -> (# State# RealWorld, a #)) -> IO a
forall a. (State# RealWorld -> (# State# RealWorld, a #)) -> IO a
IO ((State# RealWorld -> (# State# RealWorld, b #))
-> State# RealWorld -> (# State# RealWorld, a #)
f# State# RealWorld -> (# State# RealWorld, b #)
x)) of IO State# RealWorld -> (# State# RealWorld, a #)
m -> State# RealWorld -> (# State# RealWorld, a #)
m State# RealWorld
s

-- | Traced for @K IO@ with 'Either' tensor.
--
-- Each iteration re-establishes the prompt boundary. When @control0@
-- fires on @Left a@, it captures the continuation, wraps it around
-- the next loop step, and jumps back to the prompt — constant stack.
--
-- >>> :{
-- let exit42 = K $ \case
--       Right () -> pure (Right (42 :: Int))
-- :}
--
-- >>> runK (trace exit42) ()
-- 42
instance {-# OVERLAPPING #-} Traced Either (K IO) where
  trace :: forall a b c. K IO (Either a b) (Either a c) -> K IO b c
trace (K Either a b -> IO (Either a c)
body) =
    (b -> IO c) -> K IO b c
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K
      ( \b
initial -> do
          tag <- IO (PromptTag c)
forall a. IO (PromptTag a)
newPromptTag
          let go Either a b
x =
                PromptTag c -> IO c -> IO c
forall a. PromptTag a -> IO a -> IO a
prompt PromptTag c
tag (IO c -> IO c) -> IO c -> IO c
forall a b. (a -> b) -> a -> b
$
                  Either a b -> IO (Either a c)
body Either a b
x
                    IO (Either a c) -> (Either a c -> IO c) -> IO c
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ( \case
                            Right c
c -> c -> IO c
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure c
c
                            Left a
a -> PromptTag c -> ((IO c -> IO c) -> IO c) -> IO c
forall a b. PromptTag a -> ((IO b -> IO a) -> IO a) -> IO b
control0 PromptTag c
tag (\IO c -> IO c
k -> IO c -> IO c
k (Either a b -> IO c
go (a -> Either a b
forall a b. a -> Either a b
Left a
a)))
                        )
          go (Right initial)
      )