Documentation

Cartesian channel plumbing for pullbacks.

Cocartesian monoidal structure for K m with Either.

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)

Inclusive monoidal structure for K m with These.

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.

Cartesian monoidal structure for K m with (,).

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))

Lift the Channel structure through Free.

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.

Either tensorial strength for Either.

strength is the functorial action under Either.

Inclusive tensorial strength for K m with These.

Inclusive tensorial strength for These.

strength applies the payload morphism to the That branch and the These branch, leaving the This residual branch untouched.

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]

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 yank bodies productive even when the body has a strict top-level pattern on the recursive channel.

>>> strength (+1) (error "forced" :: (Int, Int)) `seq` ()
()

Lift the Strength class through Free.

A morphism is frozen before tensoring with the feedback channel.

The cartesian trace for pullbacks.

The body is a linear map f :: (x, c) -> (x, b). The traced pullback c -> b solves the affine feedback equation in cotangent space:

(dx, db) = f (dx, dc)

solved by the same lazy knot that a differentiable arrow uses. For strict carriers with nonzero channel self-coupling this diverges, exactly as the lazy differentiable trace does. Unlike the differentiable case, though, the equation here is always affine — Pullback arrows are linear by construction — so a knot over a star-semiring carrier can be eliminated outright rather than iterated.

>>> let body = Pullback (\(dx', dc) -> (2.0 * dc, dx')) :: Pullback (Double, Double) (Double, Double)
>>> runPullback (trace body) 1.0
2.0

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

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 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

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)

Lift the Traced class through Free.

A loop body in Free arr is frozen before calling the base trace.