{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Matrices over a semiring as a category with biproducts.
--
-- = Overview
--
-- Matrices over a semiring are not a /metaphor/ for category theory — they
-- /are/ the morphisms of a category with biproducts.  Objects are finite
-- index types; a morphism @i -> j@ is one scalar per input\/output pair.
-- 'Either' gives block matrices and is simultaneously product and coproduct
-- — a biproduct.  This is the matrix calculus, and it is a categorical fact,
-- not an analogy.
--
-- The encoding is initial: 'Mat' is the fully-applied leaf, 'Id' \/ 'Fun' \/
-- 'Par' \/ 'Comp' are symbolic constructors, and 'runMat' pays only boundary
-- evidence to collect results.
--
-- Evaluation is by pushing a sparse formal sum through the term.  'Fun' needs
-- no finite evidence; 'Mat' carries its own dictionary; 'Par' is structural
-- recursion; 'Comp' is composition of formal sums.  This is total and
-- terminating by construction — the free-semimodule semantics of the
-- category.
--
-- = Monoidal structure
--
-- __Tensor@Either@__: 'tensor' places two matrices on disjoint wires (block
-- diagonal).  'unitl' \/ 'unitr' witness that 'Void' (the uninhabited type)
-- is the tensor unit, reflecting the fact that a @0 × n@ or @m × 0@ matrix
-- has no entries.  Unit laws hold: @tensor (unitl . unitl') id = id@.
--
-- __Action@Either@__: 'braid' permutes index positions — the symmetry of the
-- biproduct.  The slide @slide :: Either a (Either b c) -> Either b
-- (Either a c)@ is derivable as @assoc . tensor braid id . assoc'@.
--
-- = Biproduct structure and the 2-category
--
-- The additive monoid on each hom-set gives matrices over a semiring
-- the structure of a /locally posetal 2-category/ when the semiring is
-- idempotent:
--
-- * __0-cells__: finite types (the index sets).
--
-- * __1-cells__: matrices @i -> j@, elements of the free semimodule.
--
-- * __2-cells__: for idempotent semirings ('Bool', 'Tropical'),
--   the additive monoid @+@ induces a partial order:
--
--   @
--   m ≤ n   iff   m + n = n
--   @
--
--   This is the natural 2-categorical structure: matrix inequality is a
--   2-cell, and composition is monotone in both arguments.
--
-- The biproduct structure means 'Either' is simultaneously product and
-- coproduct.  For any finite types @a, b@ there exist:
--
-- * __projections__ @p1 :: a ⊕ b -> a@, @p2 :: a ⊕ b -> b@ (implemented as
--   pattern-matching on 'Left'\/'Right');
-- * __injections__ @i1 :: a -> a ⊕ b@, @i2 :: b -> a ⊕ b@ (the 'Left' and
--   'Right' constructors).
--
-- satisfying the biproduct equations:
--
-- @
-- p1 . i1 = id,    p2 . i2 = id,
-- p1 . i2 = 0,     p2 . i1 = 0,
-- i1 . p1 + i2 . p2 = id
-- @
--
-- where @0@ is the zero matrix and @+@ is pointwise addition.  Every matrix
-- decomposes into its components via these projections and injections.
--
-- = Kleene star as closure
--
-- The Kleene star 'starM' computes the reflexive-transitive closure of a
-- square matrix in the 2-category.  For idempotent semirings, this is the
-- least fixed point of @X ↦ I + A · X@, i.e. the closure operator of the
-- locally posetal 2-category:
--
-- * @Bool@: transitive closure of a graph (reachability).
-- * @Tropical@ (min-plus): all-pairs shortest paths (Floyd-Warshall).
-- * @StarSemiring String@: regular expression for all paths.
--
-- These carriers are not merely semirings; the canonical ones are
-- /quantales/ — complete join-semilattices with monoidal multiplication
-- distributing over arbitrary joins. See "NumHask.Algebra.Quantale". In
-- that setting matrix addition is pointwise join and the Kleene star is the
-- least fixed point @I + A + A² + …@. 'starM' uses the 'StarSemiring'
-- fragment, which is exactly the iterative-join part of a quantale.
--
-- Kleene's algorithm enumerates intermediate indices: @O(|V|³)@ in the
-- number of elements of the 'Finite' type.
--
-- = Trace as Schur-complement
--
-- 'traceMat' computes the trace (feedback loop) of a block matrix:
--
-- @
--   ┌     ┐
--   │ a c │   :  a ⊕ b  →  a ⊕ c
--   │ b d │
--   └     ┘
--
--   traceMat  →  d + c · a* · b   :  b → c
-- @
--
-- This is exactly the Schur-complement formula for biproduct categories.
-- The trace satisfies the standard traced-monoidal laws (naturality,
-- sliding, vanishing, yanking) — see the docspec examples.
--
-- = Traced instance
--
-- With local 'Category' carrying @Ob (Mat s) a = Finite a@, the feedback
-- channel of 'trace' carries 'Finite' evidence. 'traceMat' is therefore a
-- lawful 'Traced' 'Either' instance (Schur-complement / star-closure).
--
-- = Relation to harpie
--
-- harpie provides statically-shaped arrays (@Harpie.Fixed.Array@) with
-- type-level dimensions.  Where 'Finite' enumerates a type's inhabitants at
-- runtime, a harpie @Array @[n] s@ knows its shape at compile time via
-- @KnownNat n@.  A matrix @i -> j@ could be a harpie array of shape @[i, j]@
-- with indices drawn from @Fin n@ (harpie's type-level finite set).  The
-- trace formula would still be the Schur-complement; the difference is that
-- the index set is a 'Nat' rather than a type-class dictionary.
--
-- Benchmarking ('Finite' enumeration vs matrix ops) shows that 'universe'
-- enumeration cost is linear in the number of inhabitants and typically
-- dominated by the @O(|V|³)@ star-closure computation for non-trivial
-- matrices.  See the enumeration spike section below for details.
module Circuit.Mat
  ( -- * Finite index types
    Finite (..),

    -- * Matrices
    Mat (..),
    runMat,

    -- * Closure
    starM,

    -- * Trace (explicit finite-channel form)
    traceMat,

    -- * Contraction
    dot,

    -- * Linear implication (explicit finite-channel form)
    evalMat,
    curryMat,
    uncurryMat,

    -- * Involution structure (Ex6: reversibility, duality, conjugation)
    Dual (..),
    transposeMat,
    dualMat,
    Conjugate (..),
    conjugateMat,

    -- * Dense field calculus (re-exported from Circuit.Mat.Field)
    MatrixM,
    cholM,
    invtriM,
    inverseM,
    MatField (..),
  )
where

import Circuit.Category (Category (..))
import Circuit.Channel (Channel (..), Strength (..))
import Circuit.Mat.Field
import Circuit.Tensor (Action (..), Tensor (..), Unital (..), Unit)
import Data.Bool (bool)
import Data.List (foldl')
import Data.Void (Void, absurd)
import NumHask.Algebra.Additive (Additive (..), Subtractive (..), sum)
import NumHask.Algebra.Multiplicative (Multiplicative (..))
import NumHask.Algebra.Ring (Distributive, InvolutiveRing (..), StarSemiring (..))
import NumHask.Data.Complex (Complex (..))
import Prelude hiding (curry, id, sum, uncurry, (*), (+), (.))

-- $setup
--
-- >>> :m -Prelude
-- >>> :set -XRebindableSyntax
-- >>> :set -XStandaloneDeriving
-- >>> import NumHask.Prelude
-- >>> import NumHask.Free.Carriers
-- >>> import Circuit.Mat
-- >>> data Node = A | B | C deriving (Eq, Ord, Enum, Bounded, Show)
-- >>> instance Finite Node where universe = [A, B, C]
-- >>> let sameMat m n = [runMat m i j | i <- universe, j <- universe] == [runMat n i j | i <- universe, j <- universe]

-- | A finite index type: enumerable and comparable.
class (Eq a) => Finite a where
  universe :: [a]

instance Finite () where
  universe :: [()]
universe = [()]

instance Finite Bool where
  universe :: [Bool]
universe = [Bool
False, Bool
True]

instance Finite Void where
  universe :: [Void]
universe = []

instance (Finite a, Finite b) => Finite (Either a b) where
  universe :: [Either a b]
universe = (a -> Either a b) -> [a] -> [Either a b]
forall a b. (a -> b) -> [a] -> [b]
map a -> Either a b
forall a b. a -> Either a b
Left [a]
forall a. Finite a => [a]
universe [Either a b] -> [Either a b] -> [Either a b]
forall a. [a] -> [a] -> [a]
++ (b -> Either a b) -> [b] -> [Either a b]
forall a b. (a -> b) -> [a] -> [b]
map b -> Either a b
forall a b. b -> Either a b
Right [b]
forall a. Finite a => [a]
universe

instance (Finite a, Finite b) => Finite (a, b) where
  universe :: [(a, b)]
universe = [(a
x, b
y) | a
x <- [a]
forall a. Finite a => [a]
universe, b
y <- [b]
forall a. Finite a => [a]
universe]

-- | 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'.
data Mat s i j where
  Mat :: (Finite i, Finite j) => (i -> j -> s) -> Mat s i j
  Id :: Mat s a a
  Fun :: (i -> j) -> Mat s i j
  Par :: Mat s a b -> Mat s c d -> Mat s (Either a c) (Either b d)
  Comp :: Mat s j k -> Mat s i j -> Mat s i k

-- | A sparse formal sum, i.e. a free semimodule element.
type Vec i s = [(i, s)]

-- | Push a formal sum through a matrix term.
--
-- Evidence flows perfectly: 'Fun' needs none; 'Mat' carries its own
-- 'Finite' dictionary; 'Par' is structural recursion; 'Comp' is
-- composition of formal sums.  The result is a formal sum over the output
-- indices; collecting equality is paid only at the boundary by 'runMat'.
push ::
  (Additive s, Multiplicative s) =>
  Vec i s ->
  Mat s i j ->
  Vec j s
push :: forall s i j.
(Additive s, Multiplicative s) =>
Vec i s -> Mat s i j -> Vec j s
push Vec i s
v Mat s i j
Id = Vec i s
[(j, s)]
v
push Vec i s
v (Fun i -> j
f) = [(i -> j
f i
i, s
x) | (i
i, s
x) <- Vec i s
v]
push Vec i s
v (Mat i -> j -> s
f) = [(j
j, s
x s -> s -> s
forall a. Multiplicative a => a -> a -> a
* i -> j -> s
f i
i j
j) | (i
i, s
x) <- Vec i s
v, j
j <- [j]
forall a. Finite a => [a]
universe]
push Vec i s
v (Par Mat s a b
m Mat s c d
n) = [(j, s)]
[(Either b d, s)]
lefts [(j, s)] -> [(j, s)] -> [(j, s)]
forall a. [a] -> [a] -> [a]
++ [(j, s)]
[(Either b d, s)]
rights
  where
    vLeft :: [(a, s)]
vLeft = [(a
a, s
x) | (Left a
a, s
x) <- Vec i s
v]
    vRight :: [(c, s)]
vRight = [(c
c, s
x) | (Right c
c, s
x) <- Vec i s
v]
    lefts :: [(Either b d, s)]
lefts = [(b -> Either b d
forall a b. a -> Either a b
Left b
b, s
x) | (b
b, s
x) <- [(a, s)] -> Mat s a b -> Vec b s
forall s i j.
(Additive s, Multiplicative s) =>
Vec i s -> Mat s i j -> Vec j s
push [(a, s)]
vLeft Mat s a b
m]
    rights :: [(Either b d, s)]
rights = [(d -> Either b d
forall a b. b -> Either a b
Right d
d, s
x) | (d
d, s
x) <- [(c, s)] -> Mat s c d -> Vec d s
forall s i j.
(Additive s, Multiplicative s) =>
Vec i s -> Mat s i j -> Vec j s
push [(c, s)]
vRight Mat s c d
n]
push Vec i s
v (Comp Mat s j j
g Mat s i j
f) = Vec j s -> Mat s j j -> [(j, s)]
forall s i j.
(Additive s, Multiplicative s) =>
Vec i s -> Mat s i j -> Vec j s
push (Vec i s -> Mat s i j -> Vec j s
forall s i j.
(Additive s, Multiplicative s) =>
Vec i s -> Mat s i j -> Vec j s
push Vec i s
v Mat s i j
f) Mat s j j
g

-- | Run a matrix at a single input\/output pair.
--
-- Equality evidence is required only at the boundary (the output index).
runMat ::
  (Additive s, Multiplicative s, Eq j) =>
  Mat s i j ->
  i ->
  j ->
  s
runMat :: forall s j i.
(Additive s, Multiplicative s, Eq j) =>
Mat s i j -> i -> j -> s
runMat Mat s i j
m i
i j
j = [s] -> s
forall a (f :: * -> *). (Additive a, Foldable f) => f a -> a
sum [s
x | (j
j', s
x) <- Vec i s -> Mat s i j -> Vec j s
forall s i j.
(Additive s, Multiplicative s) =>
Vec i s -> Mat s i j -> Vec j s
push [(i
i, s
forall a. Multiplicative a => a
one)] Mat s i j
m, j
j' j -> j -> Bool
forall a. Eq a => a -> a -> Bool
== j
j]

instance Category (Mat s) where
  id :: forall a. Mat s a a
id = Mat s a a
forall s a. Mat s a a
Id
  . :: forall b c a. Mat s b c -> Mat s a b -> Mat s a c
(.) = Mat s b c -> Mat s a b -> Mat s a c
forall s b c a. Mat s b c -> Mat s a b -> Mat s a c
Comp

-- | Associator for 'Either'.
assocEither :: Either (Either a b) c -> Either a (Either b c)
assocEither :: forall a b c. Either (Either a b) c -> Either a (Either b c)
assocEither (Left (Left a
a)) = a -> Either a (Either b c)
forall a b. a -> Either a b
Left a
a
assocEither (Left (Right b
b)) = Either b c -> Either a (Either b c)
forall a b. b -> Either a b
Right (b -> Either b c
forall a b. a -> Either a b
Left b
b)
assocEither (Right c
c) = Either b c -> Either a (Either b c)
forall a b. b -> Either a b
Right (c -> Either b c
forall a b. b -> Either a b
Right c
c)

-- | Inverse associator for 'Either'.
assocEither' :: Either a (Either b c) -> Either (Either a b) c
assocEither' :: forall a b c. Either a (Either b c) -> Either (Either a b) c
assocEither' (Left a
a) = Either a b -> Either (Either a b) c
forall a b. a -> Either a b
Left (a -> Either a b
forall a b. a -> Either a b
Left a
a)
assocEither' (Right (Left b
b)) = Either a b -> Either (Either a b) c
forall a b. a -> Either a b
Left (b -> Either a b
forall a b. b -> Either a b
Right b
b)
assocEither' (Right (Right c
c)) = c -> Either (Either a b) c
forall a b. b -> Either a b
Right c
c

-- | Symmetric swap for 'Either'.
swapEither :: Either a b -> Either b a
swapEither :: forall a b. Either a b -> Either b a
swapEither (Left a
a) = a -> Either b a
forall a b. b -> Either a b
Right a
a
swapEither (Right b
b) = b -> Either b a
forall a b. a -> Either a b
Left b
b

-- | Nested-slide braid for 'Either'.
--
-- This is the coproduct slide, derivable as @assoc . tensor braid id . assoc'@.
slideEither :: Either a (Either b c) -> Either b (Either a c)
slideEither :: forall a b c. Either a (Either b c) -> Either b (Either a c)
slideEither (Left a
a) = Either a c -> Either b (Either a c)
forall a b. b -> Either a b
Right (a -> Either a c
forall a b. a -> Either a b
Left a
a)
slideEither (Right (Left b
b)) = b -> Either b (Either a c)
forall a b. a -> Either a b
Left b
b
slideEither (Right (Right c
c)) = Either a c -> Either b (Either a c)
forall a b. b -> Either a b
Right (c -> Either a c
forall a b. b -> Either a b
Right c
c)

-- | Coproduct tensor action on 'Mat'.
--
-- 'tensor' places two matrices on disjoint 'Either' wires (block diagonal).
-- Unit laws use 'Void' as the tensor unit — a matrix indexed by 'Void'
-- has no entries, so the unitor is the identity on the payload.
--
-- >>> let a = Mat (\i j -> if i == j then (1 :: Int) else 0) :: Mat Int Node Node
-- >>> let b = Mat (\i j -> (2 :: Int)) :: Mat Int Node Node
-- >>> runMat (tensor a b) (Left A) (Left A)
-- 1
-- >>> runMat (tensor a b) (Right A) (Right A)
-- 2
instance Unital Either (Mat s) where
  unitl :: forall a. Mat s (Either (Unit Either) a) a
unitl = (Either Void a -> a) -> Mat s (Either Void a) a
forall i j s. (i -> j) -> Mat s i j
Fun ((Void -> a) -> (a -> a) -> Either Void a -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Void -> a
forall a. Void -> a
absurd a -> a
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id)
  unitl' :: forall a. Mat s a (Either (Unit Either) a)
unitl' = (a -> Either Void a) -> Mat s a (Either Void a)
forall i j s. (i -> j) -> Mat s i j
Fun a -> Either Void a
forall a b. b -> Either a b
Right
  unitr :: forall a. Mat s (Either a (Unit Either)) a
unitr = (Either a Void -> a) -> Mat s (Either a Void) a
forall i j s. (i -> j) -> Mat s i j
Fun ((a -> a) -> (Void -> a) -> Either a Void -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> a
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id Void -> a
forall a. Void -> a
absurd)
  unitr' :: forall a. Mat s a (Either a (Unit Either))
unitr' = (a -> Either a Void) -> Mat s a (Either a Void)
forall i j s. (i -> j) -> Mat s i j
Fun a -> Either a Void
forall a b. a -> Either a b
Left

instance Tensor Either (Mat s) where
  tensor :: forall a b c d.
Mat s a b -> Mat s c d -> Mat s (Either a c) (Either b d)
tensor = Mat s a b -> Mat s c d -> Mat s (Either a c) (Either b d)
forall s a b c d.
Mat s a b -> Mat s c d -> Mat s (Either a c) (Either b d)
Par

-- | Coproduct symmetry on 'Mat'.
--
-- 'braid' permutes index positions on the 'Either' sum.
--
-- >>> runMat (braid :: Mat Int (Either Node Node) (Either Node Node)) (Left A) (Right A)
-- 1
-- >>> runMat braid (Right A) (Left A)
-- 1
instance Action Either (Mat s) where
  braid :: forall a b. Mat s (Either a b) (Either b a)
braid = (Either a b -> Either b a) -> Mat s (Either a b) (Either b a)
forall i j s. (i -> j) -> Mat s i j
Fun Either a b -> Either b a
forall a b. Either a b -> Either b a
swapEither

-- | 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.
evalMat ::
  (Additive s, Multiplicative s, Eq a, Eq b, Finite a, Finite b) =>
  Mat s (a, (a, b)) b
evalMat :: forall s a b.
(Additive s, Multiplicative s, Eq a, Eq b, Finite a, Finite b) =>
Mat s (a, (a, b)) b
evalMat = ((a, (a, b)) -> b -> s) -> Mat s (a, (a, b)) b
forall i j s. (Finite i, Finite j) => (i -> j -> s) -> Mat s i j
Mat (((a, (a, b)) -> b -> s) -> Mat s (a, (a, b)) b)
-> ((a, (a, b)) -> b -> s) -> Mat s (a, (a, b)) b
forall a b. (a -> b) -> a -> b
$ \(a
x, (a
x', b
y)) b
y' -> s -> s -> Bool -> s
forall a. a -> a -> Bool -> a
bool s
forall a. Additive a => a
zero s
forall a. Multiplicative a => a
one (a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x' Bool -> Bool -> Bool
&& b
y b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
y')

curryMat ::
  (Additive s, Multiplicative s, Eq c, Finite a, Finite b, Finite c) =>
  Mat s (a, b) c ->
  Mat s a (b, c)
curryMat :: forall s c a b.
(Additive s, Multiplicative s, Eq c, Finite a, Finite b,
 Finite c) =>
Mat s (a, b) c -> Mat s a (b, c)
curryMat Mat s (a, b) c
f = (a -> (b, c) -> s) -> Mat s a (b, c)
forall i j s. (Finite i, Finite j) => (i -> j -> s) -> Mat s i j
Mat ((a -> (b, c) -> s) -> Mat s a (b, c))
-> (a -> (b, c) -> s) -> Mat s a (b, c)
forall a b. (a -> b) -> a -> b
$ \a
x (b
y, c
z) -> Mat s (a, b) c -> (a, b) -> c -> s
forall s j i.
(Additive s, Multiplicative s, Eq j) =>
Mat s i j -> i -> j -> s
runMat Mat s (a, b) c
f (a
x, b
y) c
z

uncurryMat ::
  (Additive s, Multiplicative s, Eq b, Finite a, Finite b, Finite c) =>
  Mat s a (b, c) ->
  Mat s (a, b) c
uncurryMat :: forall s b a c.
(Additive s, Multiplicative s, Eq b, Finite a, Finite b,
 Finite c) =>
Mat s a (b, c) -> Mat s (a, b) c
uncurryMat Mat s a (b, c)
g = ((a, b) -> c -> s) -> Mat s (a, b) c
forall i j s. (Finite i, Finite j) => (i -> j -> s) -> Mat s i j
Mat (((a, b) -> c -> s) -> Mat s (a, b) c)
-> ((a, b) -> c -> s) -> Mat s (a, b) c
forall a b. (a -> b) -> a -> b
$ \(a
x, b
y) c
z -> Mat s a (b, c) -> a -> (b, c) -> s
forall s j i.
(Additive s, Multiplicative s, Eq j) =>
Mat s i j -> i -> j -> s
runMat Mat s a (b, c)
g a
x (b
y, c
z)

-- | Arrow-level monoidal structure for 'Either' inside 'Mat'.
instance (Additive s, Multiplicative s) => Channel Either (Mat s) where
  assoc :: forall a b c. Mat s (Either (Either a b) c) (Either a (Either b c))
assoc = (Either (Either a b) c -> Either a (Either b c))
-> Mat s (Either (Either a b) c) (Either a (Either b c))
forall i j s. (i -> j) -> Mat s i j
Fun Either (Either a b) c -> Either a (Either b c)
forall a b c. Either (Either a b) c -> Either a (Either b c)
assocEither
  assoc' :: forall a b c. Mat s (Either a (Either b c)) (Either (Either a b) c)
assoc' = (Either a (Either b c) -> Either (Either a b) c)
-> Mat s (Either a (Either b c)) (Either (Either a b) c)
forall i j s. (i -> j) -> Mat s i j
Fun Either a (Either b c) -> Either (Either a b) c
forall a b c. Either a (Either b c) -> Either (Either a b) c
assocEither'
  slide :: forall a b c. Mat s (Either a (Either b c)) (Either b (Either a c))
slide = (Either a (Either b c) -> Either b (Either a c))
-> Mat s (Either a (Either b c)) (Either b (Either a c))
forall i j s. (i -> j) -> Mat s i j
Fun Either a (Either b c) -> Either b (Either a c)
forall a b c. Either a (Either b c) -> Either b (Either a c)
slideEither

-- | Tensorial strength for the 'Either' tensor on 'Mat'.
instance (Additive s, Multiplicative s) => Strength Either (Mat s) where
  strength :: forall b c a. Mat s b c -> Mat s (Either a b) (Either a c)
strength = Mat s a a -> Mat s b c -> Mat s (Either a b) (Either a c)
forall s a b c d.
Mat s a b -> Mat s c d -> Mat s (Either a c) (Either b d)
Par Mat s a a
forall s a. Mat s a a
Id

-- | 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
starM :: (StarSemiring s, Additive s, Multiplicative s, Finite a) => Mat s a a -> Mat s a a
starM :: forall s a.
(StarSemiring s, Additive s, Multiplicative s, Finite a) =>
Mat s a a -> Mat s a a
starM Mat s a a
m = (a -> a -> s) -> Mat s a a
forall i j s. (Finite i, Finite j) => (i -> j -> s) -> Mat s i j
Mat (\a
i a
j -> a -> a -> s
closed a
i a
j s -> s -> s
forall a. Additive a => a -> a -> a
+ case a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
j of Bool
True -> s
forall a. Multiplicative a => a
one; Bool
False -> s
forall a. Additive a => a
zero)
  where
    f :: a -> a -> s
f = Mat s a a -> a -> a -> s
forall s j i.
(Additive s, Multiplicative s, Eq j) =>
Mat s i j -> i -> j -> s
runMat Mat s a a
m
    step :: (t -> t -> a) -> t -> t -> t -> a
step t -> t -> a
stepm t
k t
i t
j = t -> t -> a
stepm t
i t
j a -> a -> a
forall a. Additive a => a -> a -> a
+ (t -> t -> a
stepm t
i t
k a -> a -> a
forall a. Multiplicative a => a -> a -> a
* a -> a
forall a. StarSemiring a => a -> a
star (t -> t -> a
stepm t
k t
k) a -> a -> a
forall a. Multiplicative a => a -> a -> a
* t -> t -> a
stepm t
k t
j)
    closed :: a -> a -> s
closed = ((a -> a -> s) -> a -> a -> a -> s)
-> (a -> a -> s) -> [a] -> a -> a -> s
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (a -> a -> s) -> a -> a -> a -> s
forall {a} {t}. StarSemiring a => (t -> t -> a) -> t -> t -> t -> a
step a -> a -> s
f [a]
forall a. Finite a => [a]
universe

-- | Explicit finite-channel composition for use inside 'traceMat'.
ecomp ::
  (Additive s, Multiplicative s, Finite i, Finite j, Finite k) =>
  Mat s j k ->
  Mat s i j ->
  Mat s i k
ecomp :: forall s i j k.
(Additive s, Multiplicative s, Finite i, Finite j, Finite k) =>
Mat s j k -> Mat s i j -> Mat s i k
ecomp Mat s j k
g Mat s i j
f = (i -> k -> s) -> Mat s i k
forall i j s. (Finite i, Finite j) => (i -> j -> s) -> Mat s i j
Mat (\i
i k
k -> [s] -> s
forall a (f :: * -> *). (Additive a, Foldable f) => f a -> a
sum [Mat s i j -> i -> j -> s
forall s j i.
(Additive s, Multiplicative s, Eq j) =>
Mat s i j -> i -> j -> s
runMat Mat s i j
f i
i j
j s -> s -> s
forall a. Multiplicative a => a -> a -> a
* Mat s j k -> j -> k -> s
forall s j i.
(Additive s, Multiplicative s, Eq j) =>
Mat s i j -> i -> j -> s
runMat Mat s j k
g j
j k
k | j
j <- [j]
forall a. Finite a => [a]
universe])

-- | 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
traceMat ::
  (StarSemiring s, Additive s, Multiplicative s, Finite a, Finite b, Finite c) =>
  Mat s (Either a b) (Either a c) ->
  Mat s b c
traceMat :: forall s a b c.
(StarSemiring s, Additive s, Multiplicative s, Finite a, Finite b,
 Finite c) =>
Mat s (Either a b) (Either a c) -> Mat s b c
traceMat Mat s (Either a b) (Either a c)
m = Mat s b c
mbc Mat s b c -> Mat s b c -> Mat s b c
forall {i} {j} {s}.
(Finite i, Finite j, Additive s, Multiplicative s) =>
Mat s i j -> Mat s i j -> Mat s i j
`addMat` Mat s a c -> Mat s b a -> Mat s b c
forall s i j k.
(Additive s, Multiplicative s, Finite i, Finite j, Finite k) =>
Mat s j k -> Mat s i j -> Mat s i k
ecomp (Mat s a c -> Mat s a a -> Mat s a c
forall s i j k.
(Additive s, Multiplicative s, Finite i, Finite j, Finite k) =>
Mat s j k -> Mat s i j -> Mat s i k
ecomp Mat s a c
mac (Mat s a a -> Mat s a a
forall s a.
(StarSemiring s, Additive s, Multiplicative s, Finite a) =>
Mat s a a -> Mat s a a
starM Mat s a a
maa)) Mat s b a
mba
  where
    maa :: Mat s a a
maa = (a -> a -> s) -> Mat s a a
forall i j s. (Finite i, Finite j) => (i -> j -> s) -> Mat s i j
Mat (\a
i a
j -> Mat s (Either a b) (Either a c) -> Either a b -> Either a c -> s
forall s j i.
(Additive s, Multiplicative s, Eq j) =>
Mat s i j -> i -> j -> s
runMat Mat s (Either a b) (Either a c)
m (a -> Either a b
forall a b. a -> Either a b
Left a
i) (a -> Either a c
forall a b. a -> Either a b
Left a
j))
    mac :: Mat s a c
mac = (a -> c -> s) -> Mat s a c
forall i j s. (Finite i, Finite j) => (i -> j -> s) -> Mat s i j
Mat (\a
i c
j -> Mat s (Either a b) (Either a c) -> Either a b -> Either a c -> s
forall s j i.
(Additive s, Multiplicative s, Eq j) =>
Mat s i j -> i -> j -> s
runMat Mat s (Either a b) (Either a c)
m (a -> Either a b
forall a b. a -> Either a b
Left a
i) (c -> Either a c
forall a b. b -> Either a b
Right c
j))
    mba :: Mat s b a
mba = (b -> a -> s) -> Mat s b a
forall i j s. (Finite i, Finite j) => (i -> j -> s) -> Mat s i j
Mat (\b
i a
j -> Mat s (Either a b) (Either a c) -> Either a b -> Either a c -> s
forall s j i.
(Additive s, Multiplicative s, Eq j) =>
Mat s i j -> i -> j -> s
runMat Mat s (Either a b) (Either a c)
m (b -> Either a b
forall a b. b -> Either a b
Right b
i) (a -> Either a c
forall a b. a -> Either a b
Left a
j))
    mbc :: Mat s b c
mbc = (b -> c -> s) -> Mat s b c
forall i j s. (Finite i, Finite j) => (i -> j -> s) -> Mat s i j
Mat (\b
i c
j -> Mat s (Either a b) (Either a c) -> Either a b -> Either a c -> s
forall s j i.
(Additive s, Multiplicative s, Eq j) =>
Mat s i j -> i -> j -> s
runMat Mat s (Either a b) (Either a c)
m (b -> Either a b
forall a b. b -> Either a b
Right b
i) (c -> Either a c
forall a b. b -> Either a b
Right c
j))
    addMat :: Mat s i j -> Mat s i j -> Mat s i j
addMat Mat s i j
x Mat s i j
y = (i -> j -> s) -> Mat s i j
forall i j s. (Finite i, Finite j) => (i -> j -> s) -> Mat s i j
Mat (\i
i j
j -> Mat s i j -> i -> j -> s
forall s j i.
(Additive s, Multiplicative s, Eq j) =>
Mat s i j -> i -> j -> s
runMat Mat s i j
x i
i j
j s -> s -> s
forall a. Additive a => a -> a -> a
+ Mat s i j -> i -> j -> s
forall s j i.
(Additive s, Multiplicative s, Eq j) =>
Mat s i j -> i -> j -> s
runMat Mat s i j
y i
i j
j)

-- | 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.
dot ::
  (StarSemiring s, Additive s, Multiplicative s, Eq a, Finite a) =>
  (a -> s) ->
  (a -> s) ->
  s
dot :: forall s a.
(StarSemiring s, Additive s, Multiplicative s, Eq a, Finite a) =>
(a -> s) -> (a -> s) -> s
dot a -> s
f a -> s
g = Mat s () () -> () -> () -> s
forall s j i.
(Additive s, Multiplicative s, Eq j) =>
Mat s i j -> i -> j -> s
runMat (Mat s (Either a ()) (Either a ()) -> Mat s () ()
forall s a b c.
(StarSemiring s, Additive s, Multiplicative s, Finite a, Finite b,
 Finite c) =>
Mat s (Either a b) (Either a c) -> Mat s b c
traceMat (Mat s (Either () a) (Either a ())
-> Mat s (Either a ()) (Either () a)
-> Mat s (Either a ()) (Either a ())
forall s b c a. Mat s b c -> Mat s a b -> Mat s a c
Comp (Mat s () a -> Mat s a () -> Mat s (Either () a) (Either a ())
forall s a b c d.
Mat s a b -> Mat s c d -> Mat s (Either a c) (Either b d)
Par Mat s () a
col Mat s a ()
row) ((Either a () -> Either () a) -> Mat s (Either a ()) (Either () a)
forall i j s. (i -> j) -> Mat s i j
Fun Either a () -> Either () a
forall a b. Either a b -> Either b a
swapEither))) () ()
  where
    col :: Mat s () a
col = (() -> a -> s) -> Mat s () a
forall i j s. (Finite i, Finite j) => (i -> j -> s) -> Mat s i j
Mat (\() a
j -> a -> s
f a
j)
    row :: Mat s a ()
row = (a -> () -> s) -> Mat s a ()
forall i j s. (Finite i, Finite j) => (i -> j -> s) -> Mat s i j
Mat (\a
i () -> a -> s
g a
i)

-- ===========================================================================
-- Involution structure: reversibility, duality, conjugation (Ex6)
-- ===========================================================================

-- | 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.
newtype Dual a = Dual a
  deriving (Dual a -> Dual a -> Bool
(Dual a -> Dual a -> Bool)
-> (Dual a -> Dual a -> Bool) -> Eq (Dual a)
forall a. Eq a => Dual a -> Dual a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Dual a -> Dual a -> Bool
== :: Dual a -> Dual a -> Bool
$c/= :: forall a. Eq a => Dual a -> Dual a -> Bool
/= :: Dual a -> Dual a -> Bool
Eq, Eq (Dual a)
Eq (Dual a) =>
(Dual a -> Dual a -> Ordering)
-> (Dual a -> Dual a -> Bool)
-> (Dual a -> Dual a -> Bool)
-> (Dual a -> Dual a -> Bool)
-> (Dual a -> Dual a -> Bool)
-> (Dual a -> Dual a -> Dual a)
-> (Dual a -> Dual a -> Dual a)
-> Ord (Dual a)
Dual a -> Dual a -> Bool
Dual a -> Dual a -> Ordering
Dual a -> Dual a -> Dual a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Dual a)
forall a. Ord a => Dual a -> Dual a -> Bool
forall a. Ord a => Dual a -> Dual a -> Ordering
forall a. Ord a => Dual a -> Dual a -> Dual a
$ccompare :: forall a. Ord a => Dual a -> Dual a -> Ordering
compare :: Dual a -> Dual a -> Ordering
$c< :: forall a. Ord a => Dual a -> Dual a -> Bool
< :: Dual a -> Dual a -> Bool
$c<= :: forall a. Ord a => Dual a -> Dual a -> Bool
<= :: Dual a -> Dual a -> Bool
$c> :: forall a. Ord a => Dual a -> Dual a -> Bool
> :: Dual a -> Dual a -> Bool
$c>= :: forall a. Ord a => Dual a -> Dual a -> Bool
>= :: Dual a -> Dual a -> Bool
$cmax :: forall a. Ord a => Dual a -> Dual a -> Dual a
max :: Dual a -> Dual a -> Dual a
$cmin :: forall a. Ord a => Dual a -> Dual a -> Dual a
min :: Dual a -> Dual a -> Dual a
Ord, Int -> Dual a -> ShowS
[Dual a] -> ShowS
Dual a -> String
(Int -> Dual a -> ShowS)
-> (Dual a -> String) -> ([Dual a] -> ShowS) -> Show (Dual a)
forall a. Show a => Int -> Dual a -> ShowS
forall a. Show a => [Dual a] -> ShowS
forall a. Show a => Dual a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Dual a -> ShowS
showsPrec :: Int -> Dual a -> ShowS
$cshow :: forall a. Show a => Dual a -> String
show :: Dual a -> String
$cshowList :: forall a. Show a => [Dual a] -> ShowS
showList :: [Dual a] -> ShowS
Show)

instance (Finite a) => Finite (Dual a) where
  universe :: [Dual a]
universe = (a -> Dual a) -> [a] -> [Dual a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Dual a
forall a. a -> Dual a
Dual [a]
forall a. Finite a => [a]
universe

-- | Freeze a symbolic matrix term to its underlying function.  Evaluation
-- requires finite index sets at the boundary.
freezeMat ::
  (Additive s, Multiplicative s, Finite i, Finite j, Eq j) =>
  Mat s i j ->
  (i -> j -> s)
freezeMat :: forall s i j.
(Additive s, Multiplicative s, Finite i, Finite j, Eq j) =>
Mat s i j -> i -> j -> s
freezeMat Mat s i j
m = Mat s i j -> i -> j -> s
forall s j i.
(Additive s, Multiplicative s, Eq j) =>
Mat s i j -> i -> j -> s
runMat Mat s i j
m

-- | 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.
transposeMat ::
  (Additive s, Multiplicative s, Finite i, Finite j, Eq i, Eq j) =>
  Mat s i j ->
  Mat s j i
transposeMat :: forall s i j.
(Additive s, Multiplicative s, Finite i, Finite j, Eq i, Eq j) =>
Mat s i j -> Mat s j i
transposeMat Mat s i j
m = (j -> i -> s) -> Mat s j i
forall i j s. (Finite i, Finite j) => (i -> j -> s) -> Mat s i j
Mat (\j
j i
i -> Mat s i j -> i -> j -> s
forall s i j.
(Additive s, Multiplicative s, Finite i, Finite j, Eq j) =>
Mat s i j -> i -> j -> s
freezeMat Mat s i j
m i
i j
j)

-- | 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.
dualMat ::
  (Additive s, Multiplicative s, Finite i, Finite j, Eq i, Eq j) =>
  Mat s i j ->
  Mat s (Dual j) (Dual i)
dualMat :: forall s i j.
(Additive s, Multiplicative s, Finite i, Finite j, Eq i, Eq j) =>
Mat s i j -> Mat s (Dual j) (Dual i)
dualMat Mat s i j
m = (Dual j -> Dual i -> s) -> Mat s (Dual j) (Dual i)
forall i j s. (Finite i, Finite j) => (i -> j -> s) -> Mat s i j
Mat (\(Dual j
j) (Dual i
i) -> Mat s i j -> i -> j -> s
forall s i j.
(Additive s, Multiplicative s, Finite i, Finite j, Eq j) =>
Mat s i j -> i -> j -> s
freezeMat Mat s i j
m i
i j
j)

-- | Scalar involution.  For 'Complex' this is 'adj' / complex conjugation.
class Conjugate s where
  conjugateS :: s -> s

instance Conjugate Double where
  conjugateS :: Double -> Double
conjugateS = Double -> Double
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id

instance (Distributive s, Subtractive s) => Conjugate (Complex s) where
  conjugateS :: Complex s -> Complex s
conjugateS = Complex s -> Complex s
forall a. InvolutiveRing a => a -> a
adj

-- | 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).
conjugateMat ::
  (Conjugate s, Additive s, Multiplicative s, Finite i, Finite j, Eq j) =>
  Mat s i j ->
  Mat s i j
conjugateMat :: forall s i j.
(Conjugate s, Additive s, Multiplicative s, Finite i, Finite j,
 Eq j) =>
Mat s i j -> Mat s i j
conjugateMat Mat s i j
m = (i -> j -> s) -> Mat s i j
forall i j s. (Finite i, Finite j) => (i -> j -> s) -> Mat s i j
Mat (\i
i j
j -> s -> s
forall s. Conjugate s => s -> s
conjugateS (Mat s i j -> i -> j -> s
forall s i j.
(Additive s, Multiplicative s, Finite i, Finite j, Eq j) =>
Mat s i j -> i -> j -> s
freezeMat Mat s i j
m i
i j
j))