{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Instance.Mat where

import Data.Complex (Complex, conjugate)
import Data.Kind (Type)
import Data.Type.Nat (Nat (..), SNat (..), SNatI, snat, type Mult, type Plus)
import Data.Vec.Lazy (Vec (..), chunks, concat, concatMap, tabulate, (++))
import Prelude (($), type (~))
import Prelude qualified as P

import Data.Fin (Fin)
import Proarrow.Category.Enriched.Dagger (DaggerProfunctor (..))
import Proarrow.Category.Instance.FinSet (FINSET (..), FinSet (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Action (Costrong (..), MonoidalAction (..), Strong (..))
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard)
import Proarrow.Category.Monoidal.Distributive (Distributive (..), distLInv, distRInv)
import Proarrow.Category.Monoidal.Hypergraph (Frobenius (..), Hypergraph, spiderDefault)
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault, obj, type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Monoid (Comonoid (..), Monoid (..))
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..), HasBiproducts)
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Object.Dual
  ( CompactClosed (..)
  , ExpSA
  , StarAutonomous (..)
  , applySA
  , coactCC
  , currySA
  , expSA
  )
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Representable (Rep (..))

type n + m = Plus n m
type (*) n m = Mult n m

type data MatK (a :: Type) = M Nat
type instance UN M (M n) = n

data Mat :: CAT (MatK a) where
  Mat
    :: forall {a} m n
     . (IsNat m, IsNat n)
    => {forall {a} (m :: Nat) (n :: Nat).
Mat (M m) (M n) -> Vec n (Vec m a)
unMat :: Vec n (Vec m a)}
    -> Mat (M m :: MatK a) (M n)

app :: (P.Num a, P.Applicative (Vec m)) => Vec n (Vec m a) -> Vec m a -> Vec n a
app :: forall a (m :: Nat) (n :: Nat).
(Num a, Applicative (Vec m)) =>
Vec n (Vec m a) -> Vec m a -> Vec n a
app Vec n (Vec m a)
m Vec m a
v = (Vec m a -> a) -> Vec n (Vec m a) -> Vec n a
forall a b. (a -> b) -> Vec n a -> Vec n b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (Vec m a -> a
forall a. Num a => Vec m a -> a
forall (t :: Type -> Type) a. (Foldable t, Num a) => t a -> a
P.sum (Vec m a -> a) -> (Vec m a -> Vec m a) -> Vec m a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a -> a -> a) -> Vec m a -> Vec m a -> Vec m a
forall a b c. (a -> b -> c) -> Vec m a -> Vec m b -> Vec m c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
P.liftA2 a -> a -> a
forall a. Num a => a -> a -> a
(P.*) Vec m a
v) Vec n (Vec m a)
m

arr :: forall n m a. (P.Num a) => FinSet (FS m) (FS n) -> Mat (M n :: MatK a) (M m :: MatK a)
arr :: forall (n :: Nat) (m :: Nat) a.
Num a =>
FinSet (FS m) (FS n) -> Mat (M n) (M m)
arr (FinSet Vec n (Fin m)
v) = forall (n :: Nat) r. SNatI n => (IsNat n => r) -> r
withIsNat @n ((IsNat n => Mat (M n) (M m)) -> Mat (M n) (M m))
-> (IsNat n => Mat (M n) (M m)) -> Mat (M n) (M m)
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) r. SNatI n => (IsNat n => r) -> r
withIsNat @m ((IsNat m => Mat (M n) (M m)) -> Mat (M n) (M m))
-> (IsNat m => Mat (M n) (M m)) -> Mat (M n) (M m)
forall a b. (a -> b) -> a -> b
$ Vec m (Vec n a) -> Mat (M n) (M m)
forall {a} (m :: Nat) (n :: Nat).
(IsNat m, IsNat n) =>
Vec n (Vec m a) -> Mat (M m) (M n)
Mat ((Fin n -> Vec n a) -> Vec m (Fin n) -> Vec m (Vec n a)
forall a b. (a -> b) -> Vec m a -> Vec m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap Fin n -> Vec n a
forall a (n :: Nat). (Num a, IsNat n) => Fin n -> Vec n a
one Vec m (Fin n)
Vec n (Fin m)
v)

arr' :: forall n m a. (P.Num a) => FinSet (FS m) (FS n) -> Mat (M m :: MatK a) (M n :: MatK a)
arr' :: forall (n :: Nat) (m :: Nat) a.
Num a =>
FinSet (FS m) (FS n) -> Mat (M m) (M n)
arr' (FinSet Vec n (Fin m)
v) = forall (n :: Nat) r. SNatI n => (IsNat n => r) -> r
withIsNat @n ((IsNat n => Mat (M m) (M n)) -> Mat (M m) (M n))
-> (IsNat n => Mat (M m) (M n)) -> Mat (M m) (M n)
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) r. SNatI n => (IsNat n => r) -> r
withIsNat @m ((IsNat m => Mat (M m) (M n)) -> Mat (M m) (M n))
-> (IsNat m => Mat (M m) (M n)) -> Mat (M m) (M n)
forall a b. (a -> b) -> a -> b
$ Vec n (Vec m a) -> Mat (M m) (M n)
forall {a} (m :: Nat) (n :: Nat).
(IsNat m, IsNat n) =>
Vec n (Vec m a) -> Mat (M m) (M n)
Mat ((Fin n -> Vec n a) -> Vec m (Fin n) -> Vec n (Vec m a)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vec m a -> f (Vec m b)
P.traverse Fin n -> Vec n a
forall a (n :: Nat). (Num a, IsNat n) => Fin n -> Vec n a
one Vec m (Fin n)
Vec n (Fin m)
v)

one :: (P.Num a, IsNat n) => Fin n -> Vec n a
one :: forall a (n :: Nat). (Num a, IsNat n) => Fin n -> Vec n a
one Fin n
m = (Fin n -> a) -> Vec n a
forall (n :: Nat) a. SNatI n => (Fin n -> a) -> Vec n a
tabulate \Fin n
n -> if Fin n
n Fin n -> Fin n -> Bool
forall a. Eq a => a -> a -> Bool
P.== Fin n
m then a
1 else a
0

zero :: (P.Num a, IsNat n) => Vec n a
zero :: forall a (n :: Nat). (Num a, IsNat n) => Vec n a
zero = a -> Vec n a
forall a. a -> Vec n a
forall (f :: Type -> Type) a. Applicative f => a -> f a
P.pure a
0

withIsNat :: forall n r. (SNatI n) => ((IsNat n) => r) -> r
withIsNat :: forall (n :: Nat) r. SNatI n => (IsNat n => r) -> r
withIsNat IsNat n => r
r = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SZ -> r
IsNat n => r
r
  SS @n' -> forall (n :: Nat) r. SNatI n => (IsNat n => r) -> r
withIsNat @n' r
IsNat n => r
IsNat n1 => r
r

class (SNatI n, P.Applicative (Vec n), n + Z ~ n, n * Z ~ Z, n * S Z ~ n) => IsNat (n :: Nat) where
  matId :: (P.Num a) => Vec n (Vec n a)
  withPlusNat :: (IsNat m) => ((IsNat (n + m)) => r) -> r
  withMultNat :: (IsNat m) => ((IsNat (n * m)) => r) -> r
  withPlusSucc :: (IsNat m) => ((n + (S m) ~ S (n + m)) => r) -> r
  withMultSucc :: (IsNat m) => ((n * (S m) ~ n + (n * m)) => r) -> r
  withPlusSym :: (IsNat m) => (((n + m) ~ (m + n)) => r) -> r
  withMultSym :: (IsNat m) => (((n * m) ~ (m * n)) => r) -> r
  withAssocPlus :: (IsNat m, IsNat o) => (((n + m) + o ~ n + (m + o)) => r) -> r
  withAssocMult :: (IsNat m, IsNat o) => (((n * m) * o ~ n * (m * o)) => r) -> r
  withDist :: (IsNat m, IsNat o) => (((n + m) * o ~ (n * o) + (m * o)) => r) -> r
instance IsNat Z where
  matId :: forall a. Num a => Vec 'Z (Vec 'Z a)
matId = Vec 'Z (Vec 'Z a)
forall a. Vec 'Z a
VNil
  withPlusNat :: forall (m :: Nat) r. IsNat m => (IsNat ('Z + m) => r) -> r
withPlusNat IsNat ('Z + m) => r
r = r
IsNat ('Z + m) => r
r
  withMultNat :: forall (m :: Nat) r. IsNat m => (IsNat ('Z * m) => r) -> r
withMultNat IsNat ('Z * m) => r
r = r
IsNat ('Z * m) => r
r
  withPlusSucc :: forall (m :: Nat) r.
IsNat m =>
((('Z + 'S m) ~ 'S ('Z + m)) => r) -> r
withPlusSucc (('Z + 'S m) ~ 'S ('Z + m)) => r
r = r
(('Z + 'S m) ~ 'S ('Z + m)) => r
r
  withMultSucc :: forall (m :: Nat) r.
IsNat m =>
((('Z * 'S m) ~ ('Z + ('Z * m))) => r) -> r
withMultSucc (('Z * 'S m) ~ ('Z + ('Z * m))) => r
r = r
(('Z * 'S m) ~ ('Z + ('Z * m))) => r
r
  withPlusSym :: forall (m :: Nat) r. IsNat m => ((('Z + m) ~ (m + 'Z)) => r) -> r
withPlusSym (('Z + m) ~ (m + 'Z)) => r
r = r
(('Z + m) ~ (m + 'Z)) => r
r
  withMultSym :: forall (m :: Nat) r. IsNat m => ((('Z * m) ~ (m * 'Z)) => r) -> r
withMultSym (('Z * m) ~ (m * 'Z)) => r
r = r
(('Z * m) ~ (m * 'Z)) => r
r
  withAssocPlus :: forall (m :: Nat) (o :: Nat) r.
(IsNat m, IsNat o) =>
(((('Z + m) + o) ~ ('Z + (m + o))) => r) -> r
withAssocPlus ((('Z + m) + o) ~ ('Z + (m + o))) => r
r = r
((('Z + m) + o) ~ ('Z + (m + o))) => r
r
  withAssocMult :: forall (m :: Nat) (o :: Nat) r.
(IsNat m, IsNat o) =>
(((('Z * m) * o) ~ ('Z * (m * o))) => r) -> r
withAssocMult ((('Z * m) * o) ~ ('Z * (m * o))) => r
r = r
((('Z * m) * o) ~ ('Z * (m * o))) => r
r
  withDist :: forall (m :: Nat) (o :: Nat) r.
(IsNat m, IsNat o) =>
(((('Z + m) * o) ~ (('Z * o) + (m * o))) => r) -> r
withDist ((('Z + m) * o) ~ (('Z * o) + (m * o))) => r
r = r
((('Z + m) * o) ~ (('Z * o) + (m * o))) => r
r
instance (IsNat n) => IsNat (S n) where
  matId :: forall a. Num a => Vec ('S n) (Vec ('S n) a)
matId = (a
1 a -> Vec n a -> Vec ('S n) a
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec n a
forall a (n :: Nat). (Num a, IsNat n) => Vec n a
zero) Vec ('S n) a -> Vec n (Vec ('S n) a) -> Vec ('S n) (Vec ('S n) a)
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: ((Vec n a -> Vec ('S n) a)
-> Vec n (Vec n a) -> Vec n (Vec ('S n) a)
forall a b. (a -> b) -> Vec n a -> Vec n b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (a
0 a -> Vec n a -> Vec ('S n) a
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
:::) Vec n (Vec n a)
forall a. Num a => Vec n (Vec n a)
forall (n :: Nat) a. (IsNat n, Num a) => Vec n (Vec n a)
matId)
  withPlusNat :: forall (m :: Nat) r. IsNat m => (IsNat ('S n + m) => r) -> r
withPlusNat @m IsNat ('S n + m) => r
r = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n + m) => r) -> r
withPlusNat @n @m r
IsNat (n + m) => r
IsNat ('S n + m) => r
r
  withMultNat :: forall (m :: Nat) r. IsNat m => (IsNat ('S n * m) => r) -> r
withMultNat @m IsNat ('S n * m) => r
r = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n * m) => r) -> r
withMultNat @n @m (forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n + m) => r) -> r
withPlusNat @m @(n * m) r
IsNat ('S n * m) => r
IsNat (m + (n * m)) => r
r)
  withPlusSucc :: forall (m :: Nat) r.
IsNat m =>
((('S n + 'S m) ~ 'S ('S n + m)) => r) -> r
withPlusSucc @m (('S n + 'S m) ~ 'S ('S n + m)) => r
r = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(((n + 'S m) ~ 'S (n + m)) => r) -> r
withPlusSucc @n @m r
((n + 'S m) ~ 'S (n + m)) => r
(('S n + 'S m) ~ 'S ('S n + m)) => r
r
  withMultSucc :: forall (m :: Nat) r.
IsNat m =>
((('S n * 'S m) ~ ('S n + ('S n * m))) => r) -> r
withMultSucc @m (('S n * 'S m) ~ ('S n + ('S n * m))) => r
r =
    forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n * m) => r) -> r
withMultNat @n @m ((IsNat (n * m) => r) -> r) -> (IsNat (n * m) => r) -> r
forall a b. (a -> b) -> a -> b
$
      forall (n :: Nat) (m :: Nat) (o :: Nat) r.
(IsNat n, IsNat m, IsNat o) =>
((((n + m) + o) ~ (n + (m + o))) => r) -> r
withAssocPlus @n @m @(n * m) (((((n + m) + (n * m)) ~ (n + (m + (n * m)))) => r) -> r)
-> ((((n + m) + (n * m)) ~ (n + (m + (n * m)))) => r) -> r
forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(((n + m) ~ (m + n)) => r) -> r
withPlusSym @n @m ((((n + m) ~ (m + n)) => r) -> r)
-> (((n + m) ~ (m + n)) => r) -> r
forall a b. (a -> b) -> a -> b
$
          forall (n :: Nat) (m :: Nat) (o :: Nat) r.
(IsNat n, IsNat m, IsNat o) =>
((((n + m) + o) ~ (n + (m + o))) => r) -> r
withAssocPlus @m @n @(n * m) (((Plus (m + n) (n * m) ~ (m + (n + (n * m)))) => r) -> r)
-> ((Plus (m + n) (n * m) ~ (m + (n + (n * m)))) => r) -> r
forall a b. (a -> b) -> a -> b
$
            forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(((n * 'S m) ~ (n + (n * m))) => r) -> r
withMultSucc @n @m r
((n * 'S m) ~ (n + (n * m))) => r
(('S n * 'S m) ~ ('S n + ('S n * m))) => r
r
  withPlusSym :: forall (m :: Nat) r.
IsNat m =>
((('S n + m) ~ (m + 'S n)) => r) -> r
withPlusSym @m (('S n + m) ~ (m + 'S n)) => r
r = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(((n + 'S m) ~ 'S (n + m)) => r) -> r
withPlusSucc @m @n ((((m + 'S n) ~ 'S (m + n)) => r) -> r)
-> (((m + 'S n) ~ 'S (m + n)) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(((n + m) ~ (m + n)) => r) -> r
withPlusSym @n @m r
((n + m) ~ (m + n)) => r
(('S n + m) ~ (m + 'S n)) => r
r
  withMultSym :: forall (m :: Nat) r.
IsNat m =>
((('S n * m) ~ (m * 'S n)) => r) -> r
withMultSym @m (('S n * m) ~ (m * 'S n)) => r
r = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(((n * 'S m) ~ (n + (n * m))) => r) -> r
withMultSucc @m @n ((((m * 'S n) ~ (m + (m * n))) => r) -> r)
-> (((m * 'S n) ~ (m + (m * n))) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(((n * m) ~ (m * n)) => r) -> r
withMultSym @n @m r
((n * m) ~ (m * n)) => r
(('S n * m) ~ (m * 'S n)) => r
r
  withAssocPlus :: forall (m :: Nat) (o :: Nat) r.
(IsNat m, IsNat o) =>
(((('S n + m) + o) ~ ('S n + (m + o))) => r) -> r
withAssocPlus @m @o ((('S n + m) + o) ~ ('S n + (m + o))) => r
r = forall (n :: Nat) (m :: Nat) (o :: Nat) r.
(IsNat n, IsNat m, IsNat o) =>
((((n + m) + o) ~ (n + (m + o))) => r) -> r
withAssocPlus @n @m @o r
(((n + m) + o) ~ (n + (m + o))) => r
((('S n + m) + o) ~ ('S n + (m + o))) => r
r
  withAssocMult :: forall (m :: Nat) (o :: Nat) r.
(IsNat m, IsNat o) =>
(((('S n * m) * o) ~ ('S n * (m * o))) => r) -> r
withAssocMult @m @o ((('S n * m) * o) ~ ('S n * (m * o))) => r
r = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n * m) => r) -> r
withMultNat @n @m ((IsNat (n * m) => r) -> r) -> (IsNat (n * m) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (m :: Nat) (o :: Nat) r.
(IsNat n, IsNat m, IsNat o) =>
((((n * m) * o) ~ (n * (m * o))) => r) -> r
withAssocMult @n @m @o (forall (n :: Nat) (m :: Nat) (o :: Nat) r.
(IsNat n, IsNat m, IsNat o) =>
((((n + m) * o) ~ ((n * o) + (m * o))) => r) -> r
withDist @m @(n * m) @o r
((('S n * m) * o) ~ ('S n * (m * o))) => r
(((m + (n * m)) * o) ~ ((m * o) + ((n * m) * o))) => r
r)
  withDist :: forall (m :: Nat) (o :: Nat) r.
(IsNat m, IsNat o) =>
(((('S n + m) * o) ~ (('S n * o) + (m * o))) => r) -> r
withDist @m @o ((('S n + m) * o) ~ (('S n * o) + (m * o))) => r
r = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n * m) => r) -> r
withMultNat @n @o ((IsNat (n * o) => r) -> r) -> (IsNat (n * o) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n * m) => r) -> r
withMultNat @m @o ((IsNat (m * o) => r) -> r) -> (IsNat (m * o) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (m :: Nat) (o :: Nat) r.
(IsNat n, IsNat m, IsNat o) =>
((((n + m) + o) ~ (n + (m + o))) => r) -> r
withAssocPlus @o @(n * o) @(m * o) (((((o + (n * o)) + (m * o)) ~ (o + ((n * o) + (m * o)))) => r)
 -> r)
-> ((((o + (n * o)) + (m * o)) ~ (o + ((n * o) + (m * o)))) => r)
-> r
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (m :: Nat) (o :: Nat) r.
(IsNat n, IsNat m, IsNat o) =>
((((n + m) * o) ~ ((n * o) + (m * o))) => r) -> r
withDist @n @m @o r
(((n + m) * o) ~ ((n * o) + (m * o))) => r
((('S n + m) * o) ~ (('S n * o) + (m * o))) => r
r

instance {-# OVERLAPPABLE #-} (P.Num a) => DaggerProfunctor (Mat :: CAT (MatK a)) where
  dagger :: forall (a :: MatK a) (b :: MatK a). Mat a b -> Mat b a
dagger (Mat Vec n (Vec m a)
m) = Vec m (Vec n a) -> Mat (M n) (M m)
forall {a} (m :: Nat) (n :: Nat).
(IsNat m, IsNat n) =>
Vec n (Vec m a) -> Mat (M m) (M n)
Mat (Vec n (Vec m a) -> Vec m (Vec n a)
forall (t :: Type -> Type) (f :: Type -> Type) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: Type -> Type) a.
Applicative f =>
Vec n (f a) -> f (Vec n a)
P.sequenceA Vec n (Vec m a)
m)

instance {-# OVERLAPS #-} (P.RealFloat a) => DaggerProfunctor (Mat :: CAT (MatK (Complex a))) where
  dagger :: forall (a :: MatK (Complex a)) (b :: MatK (Complex a)).
Mat a b -> Mat b a
dagger (Mat Vec n (Vec m (Complex a))
m) = Vec m (Vec n (Complex a)) -> Mat (M n) (M m)
forall {a} (m :: Nat) (n :: Nat).
(IsNat m, IsNat n) =>
Vec n (Vec m a) -> Mat (M m) (M n)
Mat ((Vec m (Complex a) -> Vec m (Complex a))
-> Vec n (Vec m (Complex a)) -> Vec m (Vec n (Complex a))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vec n a -> f (Vec n b)
P.traverse ((Complex a -> Complex a) -> Vec m (Complex a) -> Vec m (Complex a)
forall a b. (a -> b) -> Vec m a -> Vec m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap Complex a -> Complex a
forall a. Num a => Complex a -> Complex a
conjugate) Vec n (Vec m (Complex a))
m)

instance (P.Num a) => Profunctor (Mat :: CAT (MatK a)) where
  dimap :: forall (c :: MatK a) (a :: MatK a) (b :: MatK a) (d :: MatK a).
(c ~> a) -> (b ~> d) -> Mat a b -> Mat c d
dimap = (c ~> a) -> (b ~> d) -> Mat a b -> Mat c d
Mat c a -> Mat b d -> Mat a b -> Mat c d
forall {k} (p :: k +-> k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: MatK a) (b :: MatK a) r.
((Ob a, Ob b) => r) -> Mat a b -> r
\\ Mat{} = r
(Ob a, Ob b) => r
r
instance (P.Num a) => Promonad (Mat :: CAT (MatK a)) where
  id :: forall (a :: MatK a). Ob a => Mat a a
id = Vec (UN M a) (Vec (UN M a) a) -> Mat (M (UN M a)) (M (UN M a))
forall {a} (m :: Nat) (n :: Nat).
(IsNat m, IsNat n) =>
Vec n (Vec m a) -> Mat (M m) (M n)
Mat Vec (UN M a) (Vec (UN M a) a)
forall a. Num a => Vec (UN M a) (Vec (UN M a) a)
forall (n :: Nat) a. (IsNat n, Num a) => Vec n (Vec n a)
matId
  Mat Vec n (Vec m a)
m . :: forall (b :: MatK a) (c :: MatK a) (a :: MatK a).
Mat b c -> Mat a b -> Mat a c
. Mat a b
n = case Mat a b -> Mat b a
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
forall (a :: MatK a) (b :: MatK a). Mat a b -> Mat b a
dagger Mat a b
n of Mat Vec n (Vec m a)
nT -> Vec n (Vec n a) -> Mat (M n) (M n)
forall {a} (m :: Nat) (n :: Nat).
(IsNat m, IsNat n) =>
Vec n (Vec m a) -> Mat (M m) (M n)
Mat ((Vec m a -> Vec n a) -> Vec n (Vec m a) -> Vec n (Vec n a)
forall a b. (a -> b) -> Vec n a -> Vec n b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (Vec n (Vec m a) -> Vec m a -> Vec n a
forall a (m :: Nat) (n :: Nat).
(Num a, Applicative (Vec m)) =>
Vec n (Vec m a) -> Vec m a -> Vec n a
app Vec n (Vec m a)
nT) Vec n (Vec m a)
Vec n (Vec m a)
m)

-- | The category of matrices with entries in a type @a@, where the objects are natural numbers and the arrows @n ~> m@ are matrices of dimension @n@ by @m@.
instance (P.Num a) => CategoryOf (MatK a) where
  type (~>) = Mat
  type Ob n = (Is M n, IsNat (UN M n))

instance (P.Num a) => HasInitialObject (MatK a) where
  type InitialObject = M Z
  initiate :: forall (a :: MatK a). Ob a => InitialObject ~> a
initiate = Vec (UN M a) (Vec 'Z a) -> Mat (M 'Z) (M (UN M a))
forall {a} (m :: Nat) (n :: Nat).
(IsNat m, IsNat n) =>
Vec n (Vec m a) -> Mat (M m) (M n)
Mat (Vec 'Z a -> Vec (UN M a) (Vec 'Z a)
forall a. a -> Vec (UN M a) a
forall (f :: Type -> Type) a. Applicative f => a -> f a
P.pure Vec 'Z a
forall a. Vec 'Z a
VNil)
instance (P.Num a) => HasTerminalObject (MatK a) where
  type TerminalObject = M Z
  terminate :: forall (a :: MatK a). Ob a => a ~> TerminalObject
terminate = Vec 'Z (Vec (UN M a) a) -> Mat (M (UN M a)) (M 'Z)
forall {a} (m :: Nat) (n :: Nat).
(IsNat m, IsNat n) =>
Vec n (Vec m a) -> Mat (M m) (M n)
Mat Vec 'Z (Vec (UN M a) a)
forall a. Vec 'Z a
VNil

instance (P.Num a) => HasBinaryCoproducts (MatK a) where
  type M x || M y = M (x + y)
  withObCoprod :: forall (a :: MatK a) (b :: MatK a) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @(M x) @(M y) Ob (a || b) => r
r = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n + m) => r) -> r
withPlusNat @x @y r
Ob (a || b) => r
IsNat (UN M a + UN M b) => r
r
  lft :: forall (a :: MatK a) (b :: MatK a). (Ob a, Ob b) => a ~> (a || b)
lft @(M m) @(M n) = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n + m) => r) -> r
withPlusNat @m @n (Vec (UN M a + UN M b) (Vec (UN M a) a)
-> Mat (M (UN M a)) (M (UN M a + UN M b))
forall {a} (m :: Nat) (n :: Nat).
(IsNat m, IsNat n) =>
Vec n (Vec m a) -> Mat (M m) (M n)
Mat (forall (n :: Nat) a. (IsNat n, Num a) => Vec n (Vec n a)
matId @m Vec (UN M a) (Vec (UN M a) a)
-> Vec (UN M b) (Vec (UN M a) a)
-> Vec (UN M a + UN M b) (Vec (UN M a) a)
forall (n :: Nat) a (m :: Nat).
Vec n a -> Vec m a -> Vec (Plus n m) a
++ (Vec (UN M a) a
forall a (n :: Nat). (Num a, IsNat n) => Vec n a
zero Vec (UN M a) a
-> Vec (UN M b) (Vec (UN M b) a) -> Vec (UN M b) (Vec (UN M a) a)
forall a b. a -> Vec (UN M b) b -> Vec (UN M b) a
forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
P.<$ forall (n :: Nat) a. (IsNat n, Num a) => Vec n (Vec n a)
matId @n @a)))
  rgt :: forall (a :: MatK a) (b :: MatK a). (Ob a, Ob b) => b ~> (a || b)
rgt @(M m) @(M n) = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n + m) => r) -> r
withPlusNat @m @n (Vec (UN M a + UN M b) (Vec (UN M b) a)
-> Mat (M (UN M b)) (M (UN M a + UN M b))
forall {a} (m :: Nat) (n :: Nat).
(IsNat m, IsNat n) =>
Vec n (Vec m a) -> Mat (M m) (M n)
Mat ((Vec (UN M b) a
forall a (n :: Nat). (Num a, IsNat n) => Vec n a
zero Vec (UN M b) a
-> Vec (UN M a) (Vec (UN M a) a) -> Vec (UN M a) (Vec (UN M b) a)
forall a b. a -> Vec (UN M a) b -> Vec (UN M a) a
forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
P.<$ forall (n :: Nat) a. (IsNat n, Num a) => Vec n (Vec n a)
matId @m @a) Vec (UN M a) (Vec (UN M b) a)
-> Vec (UN M b) (Vec (UN M b) a)
-> Vec (UN M a + UN M b) (Vec (UN M b) a)
forall (n :: Nat) a (m :: Nat).
Vec n a -> Vec m a -> Vec (Plus n m) a
++ forall (n :: Nat) a. (IsNat n, Num a) => Vec n (Vec n a)
matId @n))
  Mat @m Vec n (Vec m a)
a ||| :: forall (x :: MatK a) (a :: MatK a) (y :: MatK a).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Mat @n Vec n (Vec m a)
b = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n + m) => r) -> r
withPlusNat @m @n (Vec n (Vec (m + m) a) -> Mat (M (m + m)) (M n)
forall {a} (m :: Nat) (n :: Nat).
(IsNat m, IsNat n) =>
Vec n (Vec m a) -> Mat (M m) (M n)
Mat ((Vec m a -> Vec m a -> Vec (m + m) a)
-> Vec n (Vec m a) -> Vec n (Vec m a) -> Vec n (Vec (m + m) a)
forall a b c. (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
P.liftA2 Vec m a -> Vec m a -> Vec (m + m) a
forall (n :: Nat) a (m :: Nat).
Vec n a -> Vec m a -> Vec (Plus n m) a
(++) Vec n (Vec m a)
a Vec n (Vec m a)
Vec n (Vec m a)
b))
instance (P.Num a) => HasBinaryProducts (MatK a) where
  type M x && M y = M (x + y)
  withObProd :: forall (a :: MatK a) (b :: MatK a) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @(M x) @(M y) Ob (a && b) => r
r = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n + m) => r) -> r
withPlusNat @x @y r
Ob (a && b) => r
IsNat (UN M a + UN M b) => r
r
  fst :: forall (a :: MatK a) (b :: MatK a). (Ob a, Ob b) => (a && b) ~> a
fst @(M m) @(M n) = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n + m) => r) -> r
withPlusNat @m @n (Vec (UN M a) (Vec (UN M a + UN M b) a)
-> Mat (M (UN M a + UN M b)) (M (UN M a))
forall {a} (m :: Nat) (n :: Nat).
(IsNat m, IsNat n) =>
Vec n (Vec m a) -> Mat (M m) (M n)
Mat ((Vec (UN M a) a -> Vec (UN M a + UN M b) a)
-> Vec (UN M a) (Vec (UN M a) a)
-> Vec (UN M a) (Vec (UN M a + UN M b) a)
forall a b. (a -> b) -> Vec (UN M a) a -> Vec (UN M a) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (Vec (UN M a) a -> Vec (UN M b) a -> Vec (UN M a + UN M b) a
forall (n :: Nat) a (m :: Nat).
Vec n a -> Vec m a -> Vec (Plus n m) a
++ (a
0 a -> Vec (UN M b) (Vec (UN M b) a) -> Vec (UN M b) a
forall a b. a -> Vec (UN M b) b -> Vec (UN M b) a
forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
P.<$ forall (n :: Nat) a. (IsNat n, Num a) => Vec n (Vec n a)
matId @n @a)) (forall (n :: Nat) a. (IsNat n, Num a) => Vec n (Vec n a)
matId @m)))
  snd :: forall (a :: MatK a) (b :: MatK a). (Ob a, Ob b) => (a && b) ~> b
snd @(M m) @(M n) = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n + m) => r) -> r
withPlusNat @m @n (Vec (UN M b) (Vec (UN M a + UN M b) a)
-> Mat (M (UN M a + UN M b)) (M (UN M b))
forall {a} (m :: Nat) (n :: Nat).
(IsNat m, IsNat n) =>
Vec n (Vec m a) -> Mat (M m) (M n)
Mat ((Vec (UN M b) a -> Vec (UN M a + UN M b) a)
-> Vec (UN M b) (Vec (UN M b) a)
-> Vec (UN M b) (Vec (UN M a + UN M b) a)
forall a b. (a -> b) -> Vec (UN M b) a -> Vec (UN M b) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap ((a
0 a -> Vec (UN M a) (Vec (UN M a) a) -> Vec (UN M a) a
forall a b. a -> Vec (UN M a) b -> Vec (UN M a) a
forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
P.<$ forall (n :: Nat) a. (IsNat n, Num a) => Vec n (Vec n a)
matId @m @a) Vec (UN M a) a -> Vec (UN M b) a -> Vec (UN M a + UN M b) a
forall (n :: Nat) a (m :: Nat).
Vec n a -> Vec m a -> Vec (Plus n m) a
++) (forall (n :: Nat) a. (IsNat n, Num a) => Vec n (Vec n a)
matId @n)))
  Mat @_ @m Vec n (Vec m a)
a &&& :: forall (a :: MatK a) (x :: MatK a) (y :: MatK a).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Mat @_ @n Vec n (Vec m a)
b = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n + m) => r) -> r
withPlusNat @m @n (Vec (n + n) (Vec m a) -> Mat (M m) (M (n + n))
forall {a} (m :: Nat) (n :: Nat).
(IsNat m, IsNat n) =>
Vec n (Vec m a) -> Mat (M m) (M n)
Mat (Vec n (Vec m a)
a Vec n (Vec m a) -> Vec n (Vec m a) -> Vec (n + n) (Vec m a)
forall (n :: Nat) a (m :: Nat).
Vec n a -> Vec m a -> Vec (Plus n m) a
++ Vec n (Vec m a)
Vec n (Vec m a)
b))
instance (P.Num a) => HasBiproducts (MatK a)

instance (P.Num a) => MonoidalProfunctor (Mat :: CAT (MatK a)) where
  par0 :: Mat Unit Unit
par0 = Mat Unit Unit
Mat (M ('S 'Z)) (M ('S 'Z))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: MatK a). Ob a => Mat a a
id
  Mat @fx @fy Vec n (Vec m a)
f par :: forall (x1 :: MatK a) (x2 :: MatK a) (y1 :: MatK a) (y2 :: MatK a).
Mat x1 x2 -> Mat y1 y2 -> Mat (x1 ** y1) (x2 ** y2)
`par` Mat @gx @gy Vec n (Vec m a)
g =
    forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n * m) => r) -> r
withMultNat @gx @fx ((IsNat (m * m) => Mat (x1 ** y1) (x2 ** y2))
 -> Mat (x1 ** y1) (x2 ** y2))
-> (IsNat (m * m) => Mat (x1 ** y1) (x2 ** y2))
-> Mat (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$
      forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n * m) => r) -> r
withMultNat @gy @fy ((IsNat (n * n) => Mat (x1 ** y1) (x2 ** y2))
 -> Mat (x1 ** y1) (x2 ** y2))
-> (IsNat (n * n) => Mat (x1 ** y1) (x2 ** y2))
-> Mat (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$
        Vec (n * n) (Vec (m * m) a) -> Mat (M (m * m)) (M (n * n))
forall {a} (m :: Nat) (n :: Nat).
(IsNat m, IsNat n) =>
Vec n (Vec m a) -> Mat (M m) (M n)
Mat (Vec (n * n) (Vec (m * m) a) -> Mat (M (m * m)) (M (n * n)))
-> Vec (n * n) (Vec (m * m) a) -> Mat (M (m * m)) (M (n * n))
forall a b. (a -> b) -> a -> b
$
          (Vec m a -> Vec n (Vec (m * m) a))
-> Vec n (Vec m a) -> Vec (n * n) (Vec (m * m) a)
forall a (m :: Nat) b (n :: Nat).
(a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
concatMap (\Vec m a
grow -> (Vec m a -> Vec (m * m) a)
-> Vec n (Vec m a) -> Vec n (Vec (m * m) a)
forall a b. (a -> b) -> Vec n a -> Vec n b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (\Vec m a
frow -> (a -> Vec m a) -> Vec m a -> Vec (m * m) a
forall a (m :: Nat) b (n :: Nat).
(a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
concatMap (\a
a -> (a -> a) -> Vec m a -> Vec m a
forall a b. (a -> b) -> Vec m a -> Vec m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (a
a a -> a -> a
forall a. Num a => a -> a -> a
P.*) Vec m a
frow) Vec m a
grow) Vec n (Vec m a)
f) Vec n (Vec m a)
g

-- | Products of the dimensions of the matrices as the tensor. This is the Kronecker product of matrices.
instance (P.Num a) => Monoidal (MatK a) where
  type Unit = M (S Z)
  type M x ** M y = M (y * x)
  withOb2 :: forall (a :: MatK a) (b :: MatK a) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @(M x) @(M y) Ob (a ** b) => r
r = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n * m) => r) -> r
withMultNat @y @x r
Ob (a ** b) => r
IsNat (UN M b * UN M a) => r
r
  leftUnitor :: forall (a :: MatK a). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
Mat (M (UN M a)) (M (UN M a))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: MatK a). Ob a => Mat a a
id
  leftUnitorInv :: forall (a :: MatK a). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
Mat (M (UN M a)) (M (UN M a))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: MatK a). Ob a => Mat a a
id
  rightUnitor :: forall (a :: MatK a). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
Mat (M (UN M a)) (M (UN M a))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: MatK a). Ob a => Mat a a
id
  rightUnitorInv :: forall (a :: MatK a). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
Mat (M (UN M a)) (M (UN M a))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: MatK a). Ob a => Mat a a
id
  associator :: forall (a :: MatK a) (b :: MatK a) (c :: MatK a).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(M b) @(M c) @(M d) = forall (n :: Nat) (m :: Nat) (o :: Nat) r.
(IsNat n, IsNat m, IsNat o) =>
((((n * m) * o) ~ (n * (m * o))) => r) -> r
withAssocMult @d @c @b (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: MatK a). (CategoryOf (MatK a), Ob a) => Obj a
obj @(M b) Mat (M (UN M a)) (M (UN M a))
-> Mat (M (UN M b) ** M (UN M c)) (M (UN M b) ** M (UN M c))
-> Mat
     (M (UN M a) ** (M (UN M b) ** M (UN M c)))
     (M (UN M a) ** (M (UN M b) ** M (UN M c)))
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: MatK a) (x2 :: MatK a) (y1 :: MatK a) (y2 :: MatK a).
Mat x1 x2 -> Mat y1 y2 -> Mat (x1 ** y1) (x2 ** y2)
`par` (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: MatK a). (CategoryOf (MatK a), Ob a) => Obj a
obj @(M c) Mat (M (UN M b)) (M (UN M b))
-> Mat (M (UN M c)) (M (UN M c))
-> Mat (M (UN M b) ** M (UN M c)) (M (UN M b) ** M (UN M c))
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: MatK a) (x2 :: MatK a) (y1 :: MatK a) (y2 :: MatK a).
Mat x1 x2 -> Mat y1 y2 -> Mat (x1 ** y1) (x2 ** y2)
`par` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: MatK a). (CategoryOf (MatK a), Ob a) => Obj a
obj @(M d)))
  associatorInv :: forall (a :: MatK a) (b :: MatK a) (c :: MatK a).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(M b) @(M c) @(M d) = forall (n :: Nat) (m :: Nat) (o :: Nat) r.
(IsNat n, IsNat m, IsNat o) =>
((((n * m) * o) ~ (n * (m * o))) => r) -> r
withAssocMult @d @c @b (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: MatK a). (CategoryOf (MatK a), Ob a) => Obj a
obj @(M b) Mat (M (UN M a)) (M (UN M a))
-> Mat (M (UN M b) ** M (UN M c)) (M (UN M b) ** M (UN M c))
-> Mat
     (M (UN M a) ** (M (UN M b) ** M (UN M c)))
     (M (UN M a) ** (M (UN M b) ** M (UN M c)))
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: MatK a) (x2 :: MatK a) (y1 :: MatK a) (y2 :: MatK a).
Mat x1 x2 -> Mat y1 y2 -> Mat (x1 ** y1) (x2 ** y2)
`par` (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: MatK a). (CategoryOf (MatK a), Ob a) => Obj a
obj @(M c) Mat (M (UN M b)) (M (UN M b))
-> Mat (M (UN M c)) (M (UN M c))
-> Mat (M (UN M b) ** M (UN M c)) (M (UN M b) ** M (UN M c))
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: MatK a) (x2 :: MatK a) (y1 :: MatK a) (y2 :: MatK a).
Mat x1 x2 -> Mat y1 y2 -> Mat (x1 ** y1) (x2 ** y2)
`par` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: MatK a). (CategoryOf (MatK a), Ob a) => Obj a
obj @(M d)))

instance (P.Num a) => SymMonoidal (MatK a) where
  swap :: forall (a :: MatK a) (b :: MatK a).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @(M x) @(M y) = FinSet (FS (Mult (UN M a) (UN M b))) (FS (Mult (UN M b) (UN M a)))
-> Mat (M (Mult (UN M b) (UN M a))) (M (Mult (UN M a) (UN M b)))
forall (n :: Nat) (m :: Nat) a.
Num a =>
FinSet (FS m) (FS n) -> Mat (M n) (M m)
arr (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @(FS x) @(FS y))

instance (P.Num a) => Distributive (MatK a) where
  distL :: forall (a :: MatK a) (b :: MatK a) (c :: MatK a).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @(M a') @(M b) @(M c) = FinSet
  (FS (Plus (Mult (UN M b) (UN M a)) (Mult (UN M c) (UN M a))))
  (FS (Mult (Plus (UN M b) (UN M c)) (UN M a)))
-> Mat
     (M (Mult (Plus (UN M b) (UN M c)) (UN M a)))
     (M (Plus (Mult (UN M b) (UN M a)) (Mult (UN M c) (UN M a))))
forall (n :: Nat) (m :: Nat) a.
Num a =>
FinSet (FS m) (FS n) -> Mat (M n) (M m)
arr (forall {k} (a :: k) (b :: k) (c :: k).
(Monoidal k, HasCoproducts k, Ob a, Ob b, Ob c) =>
((a ** c) || (b ** c)) ~> ((a || b) ** c)
forall (a :: FINSET) (b :: FINSET) (c :: FINSET).
(Monoidal FINSET, HasCoproducts FINSET, Ob a, Ob b, Ob c) =>
((a ** c) || (b ** c)) ~> ((a || b) ** c)
distRInv @(FS b) @(FS c) @(FS a'))
  distR :: forall (a :: MatK a) (b :: MatK a) (c :: MatK a).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @(M a') @(M b) @(M c) = FinSet
  (FS (Plus (Mult (UN M c) (UN M a)) (Mult (UN M c) (UN M b))))
  (FS (Mult (UN M c) (Plus (UN M a) (UN M b))))
-> Mat
     (M (Mult (UN M c) (Plus (UN M a) (UN M b))))
     (M (Plus (Mult (UN M c) (UN M a)) (Mult (UN M c) (UN M b))))
forall (n :: Nat) (m :: Nat) a.
Num a =>
FinSet (FS m) (FS n) -> Mat (M n) (M m)
arr (forall {k} (a :: k) (b :: k) (c :: k).
(Monoidal k, HasCoproducts k, Ob a, Ob b, Ob c) =>
((a ** b) || (a ** c)) ~> (a ** (b || c))
forall (a :: FINSET) (b :: FINSET) (c :: FINSET).
(Monoidal FINSET, HasCoproducts FINSET, Ob a, Ob b, Ob c) =>
((a ** b) || (a ** c)) ~> (a ** (b || c))
distLInv @(FS c) @(FS a') @(FS b))
  distL0 :: forall (a :: MatK a). Ob a => (a ** InitialObject) ~> InitialObject
distL0 = (a ** InitialObject) ~> InitialObject
Mat (M 'Z) (M 'Z)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: MatK a). Ob a => Mat a a
id
  distR0 :: forall (a :: MatK a). Ob a => (InitialObject ** a) ~> InitialObject
distR0 = (InitialObject ** a) ~> InitialObject
Mat (M 'Z) (M 'Z)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: MatK a). Ob a => Mat a a
id

instance (P.Num a) => Closed (MatK a) where
  type x ~~> y = ExpSA x y
  withObExp :: forall (a :: MatK a) (b :: MatK a) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @(M x) @(M y) Ob (a ~~> b) => r
r = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n * m) => r) -> r
withMultNat @y @x r
Ob (a ~~> b) => r
IsNat (UN M b * UN M a) => r
r
  curry :: forall (a :: MatK a) (b :: MatK a) (c :: MatK a).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @x @y = forall {k} (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpSA b c
forall (a :: MatK a) (b :: MatK a) (c :: MatK a).
(StarAutonomous (MatK a), Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpSA b c
currySA @x @y
  apply :: forall (a :: MatK a) (b :: MatK a).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @y @z = forall {k} (b :: k) (c :: k).
(StarAutonomous k, Ob b, Ob c) =>
(ExpSA b c ** b) ~> c
forall (b :: MatK a) (c :: MatK a).
(StarAutonomous (MatK a), Ob b, Ob c) =>
(ExpSA b c ** b) ~> c
applySA @y @z
  ^^^ :: forall (a :: MatK a) (b :: MatK a) (x :: MatK a) (y :: MatK a).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
(^^^) = (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
(b ~> y) -> (x ~> a) -> ExpSA a b ~> ExpSA x y
forall {k} (a :: k) (b :: k) (x :: k) (y :: k).
StarAutonomous k =>
(b ~> y) -> (x ~> a) -> ExpSA a b ~> ExpSA x y
expSA

instance (P.Num a) => StarAutonomous (MatK a) where
  type Dual n = n
  dual :: forall (a :: MatK a) (b :: MatK a). (a ~> b) -> Dual b ~> Dual a
dual = (a ~> b) -> Dual b ~> Dual a
Mat a b -> Mat b a
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
forall (a :: MatK a) (b :: MatK a). Mat a b -> Mat b a
dagger
  dualInv :: forall (a :: MatK a) (b :: MatK a).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv = (Dual a ~> Dual b) -> b ~> a
Mat (M (UN M a)) (M (UN M b)) -> Mat (M (UN M b)) (M (UN M a))
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
forall (a :: MatK a) (b :: MatK a). Mat a b -> Mat b a
dagger
  linDist :: forall (a :: MatK a) (b :: MatK a) (c :: MatK a).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @(M x) @(M y) @(M z) (Mat Vec n (Vec m a)
m) = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n * m) => r) -> r
withMultNat @z @y ((IsNat (UN M c * UN M b) => a ~> Dual (b ** c))
 -> a ~> Dual (b ** c))
-> (IsNat (UN M c * UN M b) => a ~> Dual (b ** c))
-> a ~> Dual (b ** c)
forall a b. (a -> b) -> a -> b
$ Vec (UN M c * UN M b) (Vec (UN M a) a)
-> Mat (M (UN M a)) (M (UN M c * UN M b))
forall {a} (m :: Nat) (n :: Nat).
(IsNat m, IsNat n) =>
Vec n (Vec m a) -> Mat (M m) (M n)
Mat (Vec n (Vec (UN M b) (Vec (UN M a) a))
-> Vec (Mult n (UN M b)) (Vec (UN M a) a)
forall (n :: Nat) (m :: Nat) a. Vec n (Vec m a) -> Vec (Mult n m) a
concat ((Vec m a -> Vec (UN M b) (Vec (UN M a) a))
-> Vec n (Vec m a) -> Vec n (Vec (UN M b) (Vec (UN M a) a))
forall a b. (a -> b) -> Vec n a -> Vec n b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (forall (n :: Nat) (m :: Nat) a.
(SNatI n, SNatI m) =>
Vec (Mult n m) a -> Vec n (Vec m a)
chunks @y @x) Vec n (Vec m a)
m))
  linDistInv :: forall (a :: MatK a) (b :: MatK a) (c :: MatK a).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @(M x) @(M y) @(M z) (Mat Vec n (Vec m a)
m) = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n * m) => r) -> r
withMultNat @y @x ((IsNat (UN M b * UN M a) => (a ** b) ~> Dual c)
 -> (a ** b) ~> Dual c)
-> (IsNat (UN M b * UN M a) => (a ** b) ~> Dual c)
-> (a ** b) ~> Dual c
forall a b. (a -> b) -> a -> b
$ Vec (UN M c) (Vec (UN M b * UN M a) a)
-> Mat (M (UN M b * UN M a)) (M (UN M c))
forall {a} (m :: Nat) (n :: Nat).
(IsNat m, IsNat n) =>
Vec n (Vec m a) -> Mat (M m) (M n)
Mat ((Vec (UN M b) (Vec m a) -> Vec (UN M b * UN M a) a)
-> Vec (UN M c) (Vec (UN M b) (Vec m a))
-> Vec (UN M c) (Vec (UN M b * UN M a) a)
forall a b. (a -> b) -> Vec (UN M c) a -> Vec (UN M c) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap Vec (UN M b) (Vec m a) -> Vec (Mult (UN M b) m) a
Vec (UN M b) (Vec m a) -> Vec (UN M b * UN M a) a
forall (n :: Nat) (m :: Nat) a. Vec n (Vec m a) -> Vec (Mult n m) a
concat (forall (n :: Nat) (m :: Nat) a.
(SNatI n, SNatI m) =>
Vec (Mult n m) a -> Vec n (Vec m a)
chunks @z @y Vec n (Vec m a)
Vec (Mult (UN M c) (UN M b)) (Vec m a)
m))

instance (P.Num a) => CompactClosed (MatK a) where
  distribDual :: forall (a :: MatK a) (b :: MatK a).
(Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual @m @n = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n * m) => r) -> r
withMultNat @(UN M m) @(UN M n) ((IsNat (UN M a * UN M b) => Dual (a ** b) ~> (Dual a ** Dual b))
 -> Dual (a ** b) ~> (Dual a ** Dual b))
-> (IsNat (UN M a * UN M b) => Dual (a ** b) ~> (Dual a ** Dual b))
-> Dual (a ** b) ~> (Dual a ** Dual b)
forall a b. (a -> b) -> a -> b
$ Mat (M (UN M a)) (M (UN M a)) -> Mat (M (UN M a)) (M (UN M a))
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
forall (a :: MatK a) (b :: MatK a). Mat a b -> Mat b a
dagger (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: MatK a). (CategoryOf (MatK a), Ob a) => Obj a
obj @m) Mat (M (UN M a)) (M (UN M a))
-> Mat (M (UN M b)) (M (UN M b))
-> Mat (M (UN M a) ** M (UN M b)) (M (UN M a) ** M (UN M b))
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: MatK a) (x2 :: MatK a) (y1 :: MatK a) (y2 :: MatK a).
Mat x1 x2 -> Mat y1 y2 -> Mat (x1 ** y1) (x2 ** y2)
`par` Mat (M (UN M b)) (M (UN M b)) -> Mat (M (UN M b)) (M (UN M b))
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
forall (a :: MatK a) (b :: MatK a). Mat a b -> Mat b a
dagger (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: MatK a). (CategoryOf (MatK a), Ob a) => Obj a
obj @n)
  dualUnit :: Dual Unit ~> Unit
dualUnit = Dual Unit ~> Unit
Mat (M ('S 'Z)) (M ('S 'Z))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: MatK a). Ob a => Mat a a
id

instance (P.Num a) => MonoidalAction (MatK a) (MatK a) where
  type Act p x = p ** x
  withObAct :: forall (a :: MatK a) (x :: MatK a) r.
(Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @b @c Ob (Act a x) => r
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @b @c r
Ob (a ** x) => r
Ob (Act a x) => r
r
  unitor :: forall (x :: MatK a). Ob x => Act Unit x ~> x
unitor = (Unit ** M (UN M x)) ~> M (UN M x)
Act Unit x ~> x
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
forall (a :: MatK a). Ob a => (Unit ** a) ~> a
leftUnitor
  unitorInv :: forall (x :: MatK a). Ob x => x ~> Act Unit x
unitorInv = x ~> Act Unit x
M (UN M x) ~> (Unit ** M (UN M x))
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
forall (a :: MatK a). Ob a => a ~> (Unit ** a)
leftUnitorInv
  multiplicator :: forall (a :: MatK a) (b :: MatK a) (x :: MatK a).
(Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicator @b @c @d = forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @b @c @d
  multiplicatorInv :: forall (a :: MatK a) (b :: MatK a) (x :: MatK a).
(Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicatorInv @b @c @d = forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @_ @b @c @d

instance (P.Num a) => Strong (MatK a) (Mat :: CAT (MatK a)) where
  act :: forall (a :: MatK a) (b :: MatK a) (x :: MatK a) (y :: MatK a).
(a ~> b) -> Mat x y -> Mat (Act a x) (Act b y)
act = (a ~> b) -> Mat x y -> Mat (Act a x) (Act b y)
Mat a b -> Mat x y -> Mat (a ** x) (b ** y)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: MatK a) (x2 :: MatK a) (y1 :: MatK a) (y2 :: MatK a).
Mat x1 x2 -> Mat y1 y2 -> Mat (x1 ** y1) (x2 ** y2)
par

instance (P.Num a) => Costrong (MatK a) (Mat :: CAT (MatK a)) where
  coact :: forall (a :: MatK a) (x :: MatK a) (y :: MatK a).
(Ob a, Ob x, Ob y) =>
Mat (Act a x) (Act a y) -> Mat x y
coact @x = forall {m} {k} (u :: m) (x :: k) (y :: k).
(CompactClosed m, MonoidalAction m k, Ob x, Ob y, Ob u) =>
(Act u x ~> Act u y) -> x ~> y
forall (u :: MatK a) (x :: MatK a) (y :: MatK a).
(CompactClosed (MatK a), MonoidalAction (MatK a) (MatK a), Ob x,
 Ob y, Ob u) =>
(Act u x ~> Act u y) -> x ~> y
coactCC @x

-- | Monoids are associative, unital algebras.
instance (P.Num a, IsNat n) => Monoid (M n :: MatK a) where
  mempty :: Unit ~> M n
mempty = FinSet (FS n) (FS ('S 'Z)) -> Mat (M ('S 'Z)) (M n)
forall (n :: Nat) (m :: Nat) a.
Num a =>
FinSet (FS m) (FS n) -> Mat (M n) (M m)
arr FS n ~> Unit
FinSet (FS n) (FS ('S 'Z))
forall {k} (c :: k). Comonoid c => c ~> Unit
counit
  mappend :: (M n ** M n) ~> M n
mappend = FinSet (FS n) (FS (Mult n n)) -> Mat (M (Mult n n)) (M n)
forall (n :: Nat) (m :: Nat) a.
Num a =>
FinSet (FS m) (FS n) -> Mat (M n) (M m)
arr FS n ~> (FS n ** FS n)
FinSet (FS n) (FS (Mult n n))
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult

instance (P.Num a, IsNat n) => Comonoid (M n :: MatK a) where
  counit :: M n ~> Unit
counit = FinSet (FS n) (FS ('S 'Z)) -> Mat (M n) (M ('S 'Z))
forall (n :: Nat) (m :: Nat) a.
Num a =>
FinSet (FS m) (FS n) -> Mat (M m) (M n)
arr' FS n ~> Unit
FinSet (FS n) (FS ('S 'Z))
forall {k} (c :: k). Comonoid c => c ~> Unit
counit
  comult :: M n ~> (M n ** M n)
comult = FinSet (FS n) (FS (Mult n n)) -> Mat (M n) (M (Mult n n))
forall (n :: Nat) (m :: Nat) a.
Num a =>
FinSet (FS m) (FS n) -> Mat (M m) (M n)
arr' FS n ~> (FS n ** FS n)
FinSet (FS n) (FS (Mult n n))
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult
instance (P.Num a, IsNat n) => Frobenius (M n :: MatK a) where
  spider :: forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
NFold n (M n) ~> NFold m (M n)
spider @x @y = forall {k} (n :: Nat) (m :: Nat) (a :: k).
(Monoid a, Comonoid a, SNatI n, SNatI m) =>
NFold n a ~> NFold m a
forall (n :: Nat) (m :: Nat) (a :: MatK a).
(Monoid a, Comonoid a, SNatI n, SNatI m) =>
NFold n a ~> NFold m a
spiderDefault @x @y @(M n)
instance (P.Num a) => Hypergraph (MatK a)
instance (P.Num a) => CopyDiscard (MatK a)

data family App :: MatK a +-> Type
instance (P.Num a) => FunctorForRep (App :: MatK a +-> Type) where
  type App @a @ M n = Vec n a
  fmap :: forall (a :: MatK a) (b :: MatK a).
(a ~> b) -> (App @ a) ~> (App @ b)
fmap (Mat Vec n (Vec m a)
m) = Vec n (Vec m a) -> Vec m a -> Vec n a
forall a (m :: Nat) (n :: Nat).
(Num a, Applicative (Vec m)) =>
Vec n (Vec m a) -> Vec m a -> Vec n a
app Vec n (Vec m a)
m
instance (P.Num a) => MonoidalProfunctor (Rep App :: MatK a +-> Type) where
  par0 :: Rep App Unit Unit
par0 = (() ~> (App @ M ('S 'Z))) -> Rep App () (M ('S 'Z))
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep \() -> a
1 a -> Vec 'Z a -> Vec ('S 'Z) a
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec 'Z a
forall a. Vec 'Z a
VNil
  Rep @_ @_ @b x1 ~> (App @ x2)
f par :: forall x1 (x2 :: MatK a) y1 (y2 :: MatK a).
Rep App x1 x2 -> Rep App y1 y2 -> Rep App (x1 ** y1) (x2 ** y2)
`par` Rep @_ @_ @c y1 ~> (App @ y2)
g = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @b @c ((Ob (x2 ** y2) => Rep App (x1 ** y1) (x2 ** y2))
 -> Rep App (x1 ** y1) (x2 ** y2))
-> (Ob (x2 ** y2) => Rep App (x1 ** y1) (x2 ** y2))
-> Rep App (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$ ((x1, y1) ~> (App @ M (Mult (UN M y2) (UN M x2))))
-> Rep App (x1, y1) (M (Mult (UN M y2) (UN M x2)))
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (\(x1
x, y1
y) -> (a -> Vec (UN M x2) a)
-> Vec (UN M y2) a -> Vec (Mult (UN M y2) (UN M x2)) a
forall a (m :: Nat) b (n :: Nat).
(a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
concatMap (\a
a -> (a
a a -> a -> a
forall a. Num a => a -> a -> a
P.*) (a -> a) -> Vec (UN M x2) a -> Vec (UN M x2) a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.<$> x1 ~> (App @ x2)
x1 -> Vec (UN M x2) a
f x1
x) (y1 ~> (App @ y2)
y1 -> Vec (UN M y2) a
g y1
y))