Documentation

Cocartesian channel plumbing for 'Diff.

Cartesian channel plumbing for 'Diff.

Cocartesian tensorial strength for 'Diff.

Cartesian tensorial strength for 'Diff.

Trace for 'Diff with the Either tensor.

The Either trace is a while-loop: 'Left a' means "iterate again", 'Right c' means "return". Forward pass runs until the body produces a Right, recording each body's pullback. Backward pass replays those pullbacks in reverse order, propagating the output cotangent back through the iteration chain.

The number of iterations is treated as locally constant by the derivative: small perturbations of the input do not change the branch sequence. This is the standard reverse-mode treatment of data-dependent control flow.

Proof obligation (joins the linearity obligation on the other traces): a cotangent on a sum is represented as the same sum, and its tag must match the primal trajectory — the cotangent space at a point of Either a c is the cotangent space of the branch the point is in. Every honest pullback maps an output-tagged cotangent to an input-tagged one; the replay errors loudly on any mismatch rather than misreading a dishonest primitive.

Trace for 'Diff with the (,) tensor.

The forward pass ties the standard lazy knot:

let (a, c) = body (a, b) in c

The backward pass ties the same shape of knot, transposed. Given dc on the output, the full backward pair (da, db) satisfies a self-referential equation solved by a single lazy binding:

let bd = backward (fst bd, dc) in snd bd

The knot flows through the pair rather than through the channel cotangent alone — backward is called once, the pair is destructured once, and the shape mirrors the forward knot identically.

pullback closes over backward, which closes over the forward pass's intermediates. The closure is the tape: no explicit Wengert list is built because GHC's heap holds the graph. For linear backward maps this is a Neumann series computed lazily; for general maps it is the implicit function theorem as a lazy knot.

Monoidal product for Diff: independent wires, no additive constraint.

>>> let f = Diff (\x -> (x + 1, \d -> d)) :: Diff' Int Int
>>> let g = Diff (\x -> (x * 2, \d -> 2 * d)) :: Diff' Int Int
>>> let (y, pb) = runDiff (tensor f g) (3, 4)
>>> y
(4,8)
>>> pb (1, 1)
(1,2)

Category for Diff.

'Circuit.Diff still provides Category; circuits needs the local Category with associated Ob (default ()) so Monoidal Traced free Trace folds typecheck after kind-gen.

Copy in D: the pullback is plus (fan-in on the backward pass).

>>> import Circuit.Tensor (Action(..))
>>> import Circuit.Bimonoid (Copy(..), Merge(..))
>>> let (_, pb) = runDiff (copy :: Diff' Int (Int, Int)) 5
>>> pb (1, 2)
3

Add in D: the pullback is copy (fan-out on the backward pass).

>>> let (_, pb) = runDiff (plus :: Diff' (Int, Int) Int) (3, 4)
>>> pb 1
(1,1)

Mechanical Num mirror so that base-polymorphic code can also use 'Diff as its carrier. Non-smooth methods (abs, signum) raise an error; the useful cases (literals, +, *, -) work out of the box.

Additive structure: sum rule.

zero is the constant zero function; (+) adds outputs and fans-in cotangents.

Subtractive structure: negation pushes through the pullback.

Exponential field: exp, log, and the derived power/root family.

Trigonometric field: the elementary transcendental family.

Divisive structure: reciprocal rule.

Division inherits the product rule via the default / = * . recip.

Multiplicative structure: product rule.

one is the constant one function.