Pullback-instance of the comonoid structure.

Copy's pullback is addition; discard's pullback is the zero cotangent. These are not used by the transposition step of reverse-mode AD (which encodes structural rows as Lifts to avoid channel-type constraints), but they make Pullback a full bimonoid carrier.

>>> runPullback (copy :: Pullback Int (Int, Int)) 3
(3,3)
>>> runPullback (discard :: Pullback Int ()) 5
()

NOTE: neither method here uses an Additive (->) a constraint — copying and discarding are linear as they stand. If the class head permits, drop the constraint; keeping a stray Additive reads as "addition happens in this instance", which is the confusion the paragraph above tries to dispel.

Pullback-instance of the additive/monoid structure.

Addition's pullback is copying; zero's pullback is discarding.

>>> runPullback (plus :: Pullback (Int, Int) Int) (1, 2)
3
>>> runPullback (zero :: Pullback () Int) ()
0

Cartesian channel plumbing for pullbacks.

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

Parallel composition pairs pullbacks independently; braid swaps the two cotangents.

>>> let f = Pullback (+1) :: Pullback Int Int
>>> let g = Pullback (*2) :: Pullback Int Int
>>> runPullback (tensor f g) (3, 4)
(4,8)