A finite index type: enumerable and comparable.

Matrix over a semiring s, indexed by i (rows) and j (columns).

• Mat is the concrete, fully-applied leaf; it carries Finite dictionaries so that push can enumerate indices when needed.
• Id, Fun, Par, and Comp are symbolic; they are evaluated by push.

Note: Par does not require Finite — it is a structural constructor whose Finite evidence is supplied by the subterms or by Mat leaves. The Tensor instance uses Par for tensor.

Run a matrix at a single input/output pair.

Equality evidence is required only at the boundary (the output index).

Reflexive-transitive closure of a square matrix.

Implements Kleene's algorithm: for each intermediate index k, update all entries m(i,j) := m(i,j) + m(i,k) * star(m(k,k)) * m(k,j). The closure is the original matrix with the loop applied, plus the identity at the end, so starM m = I + m + m² + ... for arbitrary star semirings.

For idempotent semirings, this is the closure operator of the locally posetal 2-category: starM computes the least fixed point of X ↦ I + A · X.

>>> let g = Mat (\i j -> case (i, j) of (A, B) -> True; (B, C) -> True; _ -> False) :: Mat Bool Node Node
>>> runMat (starM g) A C
True

>>> let w = Mat (\i j -> case (i, j) of (A, B) -> MinPlus 1; (B, C) -> MinPlus 2; (A, C) -> MinPlus 10; _ -> zero) :: Mat (MinPlus Double) Node Node
>>> getMinPlus (runMat (starM w) A C)
3.0

Trace over an explicit finite feedback channel a.

For a block matrix [[a, a->c], [b->a, b->c]], the trace is the Schur-complement:

traceMat  [[a, c], [b, d]]  =  d + c · a* · b

This is the standard trace for biproduct categories, satisfying the traced-monoidal laws.

Naturality

Post-composing the data output with g before tracing equals tracing then post-composing with g. The blocks are coupled so the loop is live.

>>> let fFun (Left ()) (Left ()) = False; fFun (Left ()) (Right B) = True; fFun (Right A) (Left ()) = True; fFun _ _ = False
>>> let f = Mat fFun :: Mat Bool (Either () Node) (Either () Node)
>>> let g = Mat (\i j -> case (i, j) of (B, C) -> True; _ -> False) :: Mat Bool Node Node
>>> sameMat (traceMat (Comp (Par Id g) f)) (Comp g (traceMat f))
True

Sliding

Moving g through the feedback wire. Feedback channel is Bool, g is the swap permutation, and the blocks are coupled so the loop is live.

>>> let gSwap = Mat (\i j -> i /= j) :: Mat Bool Bool Bool
>>> let fSlideFun (Left False) (Left True) = True; fSlideFun (Left True) (Right B) = True; fSlideFun (Right A) (Left False) = True; fSlideFun (Right B) (Right C) = True; fSlideFun _ _ = False
>>> let fSlide = Mat fSlideFun :: Mat Bool (Either Bool Node) (Either Bool Node)
>>> sameMat (traceMat (Comp (Par gSwap Id) fSlide)) (traceMat (Comp fSlide (Par gSwap Id)))
True

Vanishing

Tracing over the unit channel () collapses to the Schur-complement formula mbc + mac * star maa * mba.

>>> let blockFun (Left ()) (Left ()) = False; blockFun (Left ()) (Right B) = True; blockFun (Right A) (Left ()) = True; blockFun _ _ = False
>>> let block = Mat blockFun :: Mat Bool (Either () Node) (Either () Node)
>>> let expected = Mat (\i j -> case (i, j) of (A, B) -> True; _ -> False) :: Mat Bool Node Node
>>> sameMat (traceMat block) expected
True

Regression: nested Comp terminates

The old reduceComp fallthrough looped on m . m . m.

>>> let m = Mat (\i j -> case (i, j) of (A, A) -> True; (A, B) -> True; (B, B) -> True; _ -> False) :: Mat Bool Node Node
>>> runMat (Comp m (Comp m m)) A B
True
>>> runMat (Comp m (Comp m m)) B A
False

Categorical dot product of two vectors over the same finite index set.

Both vectors are given as functions from the index set to the semiring. The construction uses only Par, the coproduct swap, and traceMat — no row/column naming, no dimension indices.

The feedback channel in the trace is the shared index set a; because the block on that channel is zero, star reduces to one and the Schur complement becomes the sum of products.

Compact-closed implication on index pairs: A ⊸ B is the space of matrix entries (a, b). curry/uncurry reshape; eval contracts the repeated index (transpose + product).

These are named constrained combinators rather than Lolli class methods because the unconstrained tower no longer carries object evidence.

Object-level duality marker. Dual i is the dual index set of i; it carries the same inhabitants but is a distinct type, so duality is visible at the object level.

Reversibility: matrix transpose.

This is the dagger/reversibility involution. It is contravariant and identity-on-objects: a morphism i -> j becomes j -> i, but the object labels themselves do not change.

Duality: the dual of a linear map f :: i -> j is f* :: j* -> i*.

This is not identity-on-objects: it tags both source and target with Dual. Over a field it is the transpose carried by the dual basis.

Scalar involution. For Complex this is adj / complex conjugation.

Conjugation: the composite of duality and reversibility, expressed with the standard identification of a finite-dimensional space with its dual.

It is a covariant endofunctor on objects and, over Complex, is entrywise complex conjugation. It is distinct from both transposeMat (identity-on-objects contravariant) and dualMat (not identity-on-objects).

A square matrix of statically-known size.

Cholesky decomposition using the Cholesky-Crout algorithm.

>>> e = F.array @[3,3] @Double [4,12,-16,12,37,-43,-16,-43,98]
>>> pretty (cholM e)
[[2.0,0.0,0.0],
 [6.0,1.0,0.0],
 [-8.0,5.0,3.0]]
>>> F.mult (cholM e) (F.transpose (cholM e)) == e
True

Inversion of a triangular matrix.

>>> t = F.array @[3,3] @Double [1,0,1,0,1,2,0,0,1]
>>> pretty (invtriM t)
[[1.0,0.0,-1.0],
 [0.0,1.0,-2.0],
 [0.0,0.0,1.0]]
>>> F.ident @[3,3] == F.mult t (invtriM t)
True

Inverse of a square matrix via Cholesky decomposition.

>>> e = F.array @[3,3] @Double [4,12,-16,12,37,-43,-16,-43,98]
>>> pretty (inverseM e)
[[49.36111111111111,-13.555555555555554,2.1111111111111107],
 [-13.555555555555554,3.7777777777777772,-0.5555555555555555],
 [2.1111111111111107,-0.5555555555555555,0.1111111111111111]]

Newtype wrapper that gives square matrices a multiplicative (and, over a field, divisible) structure.

The unit is the identity matrix; multiplication is the usual matrix product. Division uses Cholesky-based inversion.