Documentation

The Category instance is the generic free-category instance: id is a lifted identity and composition is a SigCompose node.

Unconstrained function category.

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, These) do not admit composition.

Category instance for Circ.

The laws hold only up to invertible Sq: on-the-nose associativity and unitality are impossible as Haskell values because the carriers of the two sides differ. Observational witnesses live in Axioma.Circ.

Distributivity of (,) over Either on K m.

Cocartesian monoidal structure for K m with Either.

Inclusive monoidal structure for K m with These.

Cartesian monoidal structure for K m with (,).

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.

Inclusive tensorial strength for K m with These.

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]

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

Coproduct as multiplicative disjunction on K arrows.

Dualising object () for K m.

Same shape as the (->) instance, but the constant companion returns () in the monad.

Dualising object Bool for K m.

Same shape as the (->) instance, but the constant companion returns False in the monad.

Coproduct symmetry on K m.

Inclusive symmetry on K m.

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

Inclusive tensor action on K m.

Cartesian tensor on K (effectful sequential product).

Coproduct unit structure on K m.

Inclusive unit structure on K m.

Cartesian unit structure on K (effectful sequential product).

Unit poles for Body Either s (K m) at Void.

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.

Cartesian shared fusion on K arrows.

Kleisli arrows embed pure functions by returning the result in the monad.

Kleisli arrows embed pure functions by returning the result in the monad.

Functions embed as themselves.

The singleton type is canonically pointed.

Maybe is canonically pointed at Nothing.

Lists are canonically pointed at the empty list.