A reverse-mode differentiable function tagged by a phantom type p.

The phantom tag prevents perturbation confusion: values of type Diff p a b can only be composed with other Diff p values. Nested AD introduces a fresh tag for each level.

runDiff f a returns a pair (b, pullback) where b = f a and pullback maps a cotangent db on the output to a cotangent da on the input.

The untagged differentiable arrow. Existing code can continue to use this; it is simply Diff ().

Iterated trace for strict carriers.

The lazy trace diverges on strict cotangent types (Double, etc.) when the feedback channel has nonzero self-coupling (∂a_out/∂a_in ≠ 0). traceNFrom replaces the lazy knot with truncated fixed-point iteration.

• Forward — iterate from caller-supplied seed x0, N steps. There is no canonical seed for the forward pass (the fixpoint is arbitrary nonlinear), so the caller provides one.
• Backward — iterate from zero, N steps, extract snd once. The backward equation is guaranteed affine (calculus promises linearity in cotangents), so zero is the principled seed. The Neumann summation happens inside the iteration — no double-counting, and plus retreats to where the theory says it lives: inside prims and Copy.

Lives beside the lawful-but-lazy instance, not replacing it.

Trace with a closed-form backward pass via the Kleene star.

The integer n in traceNFrom truncates a series on both passes. But only the forward fixpoint is genuinely nonlinear; the backward channel equation is affine — calculus promises linearity in cotangents:

da = A·da + C·dc        solution:  da = star A · C·dc

with star a = one + a·star a — the Neumann series as algebra, 1/(1−a) over a field. Because the pullback is linear, the blocks A and C·dc are extractable by probing:

backward (dj, dc) = (A·dj + C·dc, B·dj + D·dc)
A    = fst (backward (one,  0))   -- channel self-coupling
C·dc = fst (backward (zero, dc))

and the trace's pullback is the Schur complement D·dc + B·star A·C·dc, recovered with one more probe at the backward fixpoint:

db = snd (backward (star A · C·dc, dc))

(Check: A·(star A·C·dc) + C·dc = (A·star A + one)·C·dc = star A·C·dc — the star law discharges the fixpoint.)

So: forward still iterates from the caller's seed (no closed form exists for an arbitrary nonlinear fixpoint), but the backward pass is exact in three calls to backward — no Neumann index at all. The star probe is computed once per forward point and shared across all cotangents.

The closed form is the truncated iteration's limit; pure-Prelude witness at a = 0.3, c = 2:

>>> let daIter = iterate (\d -> 0.3 * d + 2.0 * 1.0) 0 !! 200
>>> abs (daIter - 1.0 / (1.0 - 0.3) * 2.0) < 1e-12
True

Caveat: numhask declares StarSemiring but ships no instances; the only carriers in the tower are FieldStar (star a = recip (1−a)), Warshall, and MinPlus. For bare Double channels and for vector channels solved by starMatrix, see Circuit.Diff.Star — the Schur-complement bridge proper.

Proof obligation: the probes assume the pullback is linear. Every honestly-constructed 'Diff primitive satisfies this (a pullback is a linear map); a primitive whose backward closure is affine-with-offset is a bug that this function will silently misread.

Trace via the Kleene star — the execution formula, lazy form.

For a knot body with channel self-coupling block A and cross-blocks B, C, D, the trace is the Schur complement:

traceStar f = D + B · star A · C

The lazy trace instance for 'Diff computes exactly this via a lazy fixpoint rather than closed form, so this alias is definable without using star at all. Note that numhask ships no StarSemiring instances, so for concrete carriers prefer traceStarFrom (scalar channel, closed-form backward) or Circuit.Diff.Star.traceStarMatrix (vector channel, solved by starMatrix — the bridge made literal).

2x² + 3x + 5 built from tensor, dup, and plus on the Diff arrow. No Net needed — the instances are the denotations the rows will realise to.

The gradient is 4x + 3, so at x = 1: value 10, gradient 7.

>>> let (y, pb) = runDiff quadD 1.0
>>> y
10.0
>>> pb 1.0
7.0