{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Instance.Mat where

import Data.Complex (Complex, conjugate)
import Data.Kind (Type)
import Prelude (($), type (~))
import Prelude qualified as P

import Proarrow.Category.Dagger (DaggerProfunctor (..))
import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , SymMonoidal (..)
  , TracedMonoidalProfunctor (..)
  )
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault, obj)
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Object.Dual (CompactClosed (..), StarAutonomous (..), compactClosedTrace)
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))

type data Nat = Z | S Nat

type family (+) (a :: Nat) (b :: Nat) :: Nat where
  Z + b = b
  S a + b = S (a + b)
type family (*) (a :: Nat) (b :: Nat) :: Nat where
  Z * b = Z
  S a * b = b + (a * b)

data Vec :: Nat -> Type -> Type where
  Nil :: Vec Z a
  Cons :: a -> Vec n a -> Vec (S n) a

instance P.Functor (Vec n) where
  fmap :: forall a b. (a -> b) -> Vec n a -> Vec n b
fmap a -> b
_ Vec n a
Nil = Vec n b
Vec Z b
forall a. Vec Z a
Nil
  fmap a -> b
f (Cons a
x Vec n a
xs) = b -> Vec n b -> Vec (S n) b
forall a (m :: Nat). a -> Vec m a -> Vec (S m) a
Cons (a -> b
f a
x) ((a -> b) -> Vec n a -> Vec n b
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 -> b
f Vec n a
xs)
instance P.Foldable (Vec n) where
  foldMap :: forall m a. Monoid m => (a -> m) -> Vec n a -> m
foldMap a -> m
_ Vec n a
Nil = m
forall a. Monoid a => a
P.mempty
  foldMap a -> m
f (Cons a
x Vec n a
xs) = a -> m
f a
x m -> m -> m
forall a. Semigroup a => a -> a -> a
P.<> (a -> m) -> Vec n a -> m
forall m a. Monoid m => (a -> m) -> Vec n a -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
P.foldMap a -> m
f Vec n a
xs
instance P.Traversable (Vec n) where
  traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vec n a -> f (Vec n b)
traverse a -> f b
_ Vec n a
Nil = Vec n b -> f (Vec n b)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
P.pure Vec n b
Vec Z b
forall a. Vec Z a
Nil
  traverse a -> f b
f (Cons a
x Vec n a
xs) = b -> Vec n b -> Vec n b
b -> Vec n b -> Vec (S n) b
forall a (m :: Nat). a -> Vec m a -> Vec (S m) a
Cons (b -> Vec n b -> Vec n b) -> f b -> f (Vec n b -> Vec n b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.<$> a -> f b
f a
x f (Vec n b -> Vec n b) -> f (Vec n b) -> f (Vec n b)
forall a b. f (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
P.<*> (a -> f b) -> Vec n a -> f (Vec n b)
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 a -> f b
f Vec n a
xs

instance P.Applicative (Vec Z) where
  pure :: forall a. a -> Vec Z a
pure a
_ = Vec Z a
forall a. Vec Z a
Nil
  Vec Z (a -> b)
Nil <*> :: forall a b. Vec Z (a -> b) -> Vec Z a -> Vec Z b
<*> Vec Z a
Nil = Vec Z b
forall a. Vec Z a
Nil
instance (P.Applicative (Vec n)) => P.Applicative (Vec (S n)) where
  pure :: forall a. a -> Vec (S n) a
pure a
x = a -> Vec n a -> Vec (S n) a
forall a (m :: Nat). a -> Vec m a -> Vec (S m) a
Cons a
x (a -> Vec n a
forall a. a -> Vec n a
forall (f :: Type -> Type) a. Applicative f => a -> f a
P.pure a
x)
  Cons a -> b
f Vec n (a -> b)
fs <*> :: forall a b. Vec (S n) (a -> b) -> Vec (S n) a -> Vec (S n) b
<*> Cons a
x Vec n a
xs = b -> Vec n b -> Vec (S n) b
forall a (m :: Nat). a -> Vec m a -> Vec (S m) a
Cons (a -> b
f a
x) (Vec n (a -> b)
Vec n (a -> b)
fs Vec n (a -> b) -> Vec n a -> Vec n b
forall a b. Vec n (a -> b) -> Vec n a -> Vec n b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
P.<*> Vec n a
Vec n a
xs)

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'} m n
     . (Ob m', Ob n', m' ~ (M m :: MatK a), n' ~ M n)
    => Vec n (Vec m a)
    -> Mat m' n'

apply :: (P.Num a, P.Applicative (Vec m)) => Vec n (Vec m a) -> Vec m a -> Vec n a
apply :: forall a (m :: Nat) (n :: Nat).
(Num a, Applicative (Vec m)) =>
Vec n (Vec m a) -> Vec m a -> Vec n a
apply 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 ((a -> a -> a) -> a -> Vec m a -> a
forall a b. (a -> b -> b) -> b -> Vec m a -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
P.foldr a -> a -> a
forall a. Num a => a -> a -> a
(P.+) a
0 (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 :: PRO 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

class (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)
  zero :: (P.Num a) => Vec n a
  append :: Vec n a -> Vec m a -> Vec (n + m) a
  split :: Vec (n + m) a -> (Vec n a, Vec m a)
  concatMap :: (IsNat m) => (a -> Vec m b) -> Vec n a -> Vec (n * m) b
  unConcatMap :: (IsNat m) => (Vec m b -> a) -> Vec (n * m) b -> 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
Nil
  zero :: forall a. Num a => Vec Z a
zero = Vec Z a
forall a. Vec Z a
Nil
  append :: forall a (m :: Nat). Vec Z a -> Vec m a -> Vec (Z + m) a
append Vec Z a
Nil Vec m a
ys = Vec m a
Vec (Z + m) a
ys
  split :: forall (m :: Nat) a. Vec (Z + m) a -> (Vec Z a, Vec m a)
split Vec (Z + m) a
ys = (Vec Z a
forall a. Vec Z a
Nil, Vec m a
Vec (Z + m) a
ys)
  concatMap :: forall (m :: Nat) a b.
IsNat m =>
(a -> Vec m b) -> Vec Z a -> Vec (Z * m) b
concatMap a -> Vec m b
_ Vec Z a
Nil = Vec (Z * m) b
Vec Z b
forall a. Vec Z a
Nil
  unConcatMap :: forall (m :: Nat) b a.
IsNat m =>
(Vec m b -> a) -> Vec (Z * m) b -> Vec Z a
unConcatMap Vec m b -> a
_ Vec (Z * m) b
Nil = Vec Z a
forall a. Vec Z a
Nil
  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 = Vec (S n) a -> Vec n (Vec (S n) a) -> Vec (S n) (Vec (S n) a)
forall a (m :: Nat). a -> Vec m a -> Vec (S m) a
Cons (a -> Vec n a -> Vec (S n) a
forall a (m :: Nat). a -> Vec m a -> Vec (S m) a
Cons a
1 Vec n a
forall a. Num a => Vec n a
forall (n :: Nat) a. (IsNat n, Num a) => Vec n a
zero) ((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 -> Vec n a -> Vec (S n) a
forall a (m :: Nat). a -> Vec m a -> Vec (S m) a
Cons a
0) 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)
  zero :: forall a. Num a => Vec (S n) a
zero = a -> Vec n a -> Vec (S n) a
forall a (m :: Nat). a -> Vec m a -> Vec (S m) a
Cons a
0 Vec n a
forall a. Num a => Vec n a
forall (n :: Nat) a. (IsNat n, Num a) => Vec n a
zero
  append :: forall a (m :: Nat). Vec (S n) a -> Vec m a -> Vec (S n + m) a
append (Cons a
x Vec n a
xs) Vec m a
ys = a -> Vec (n + m) a -> Vec (S (n + m)) a
forall a (m :: Nat). a -> Vec m a -> Vec (S m) a
Cons a
x (Vec n a -> Vec m a -> Vec (n + m) a
forall a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a
forall (n :: Nat) a (m :: Nat).
IsNat n =>
Vec n a -> Vec m a -> Vec (n + m) a
append Vec n a
xs Vec m a
ys)
  split :: forall (m :: Nat) a. Vec (S n + m) a -> (Vec (S n) a, Vec m a)
split (Cons a
x Vec n a
xs) = case Vec (n + m) a -> (Vec n a, Vec m a)
forall (n :: Nat) (m :: Nat) a.
IsNat n =>
Vec (n + m) a -> (Vec n a, Vec m a)
forall (m :: Nat) a. Vec (n + m) a -> (Vec n a, Vec m a)
split Vec n a
Vec (n + m) a
xs of (Vec n a
ys, Vec m a
zs) -> (a -> Vec n a -> Vec (S n) a
forall a (m :: Nat). a -> Vec m a -> Vec (S m) a
Cons a
x Vec n a
ys, Vec m a
zs)
  concatMap :: forall (m :: Nat) a b.
IsNat m =>
(a -> Vec m b) -> Vec (S n) a -> Vec (S n * m) b
concatMap a -> Vec m b
f (Cons a
x Vec n a
xs) = a -> Vec m b
f a
x Vec m b -> Vec (n * m) b -> Vec (m + (n * m)) b
forall a (m :: Nat). Vec m a -> Vec m a -> Vec (m + m) a
forall (n :: Nat) a (m :: Nat).
IsNat n =>
Vec n a -> Vec m a -> Vec (n + m) a
`append` (a -> Vec m b) -> Vec n a -> Vec (n * m) b
forall (n :: Nat) (m :: Nat) a b.
(IsNat n, IsNat m) =>
(a -> Vec m b) -> Vec n a -> Vec (n * m) b
forall (m :: Nat) a b.
IsNat m =>
(a -> Vec m b) -> Vec n a -> Vec (n * m) b
concatMap a -> Vec m b
f Vec n a
xs
  unConcatMap :: forall (m :: Nat) b a.
IsNat m =>
(Vec m b -> a) -> Vec (S n * m) b -> Vec (S n) a
unConcatMap Vec m b -> a
f Vec (S n * m) b
mnm = case Vec (m + (n * m)) b -> (Vec m b, Vec (n * m) b)
forall (n :: Nat) (m :: Nat) a.
IsNat n =>
Vec (n + m) a -> (Vec n a, Vec m a)
forall (m :: Nat) a. Vec (m + m) a -> (Vec m a, Vec m a)
split Vec (S n * m) b
Vec (m + (n * m)) b
mnm of (Vec m b
m, Vec (n * m) b
nm) -> Vec m b -> a
f Vec m b
m a -> Vec n a -> Vec (S n) a
forall a (m :: Nat). a -> Vec m a -> Vec (S m) a
`Cons` (Vec m b -> a) -> Vec (n * m) b -> Vec n a
forall (n :: Nat) (m :: Nat) b a.
(IsNat n, IsNat m) =>
(Vec m b -> a) -> Vec (n * m) b -> Vec n a
forall (m :: Nat) b a.
IsNat m =>
(Vec m b -> a) -> Vec (n * m) b -> Vec n a
unConcatMap Vec m b -> a
f Vec (n * m) b
nm
  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) (((((m + n) + (n * m)) ~ (m + (n + (n * m)))) => r) -> r)
-> ((((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

withNat :: Vec n a -> ((IsNat n) => r) -> r
withNat :: forall (n :: Nat) a r. Vec n a -> (IsNat n => r) -> r
withNat Vec n a
Nil IsNat n => r
r = r
IsNat n => r
r
withNat (Cons a
_ Vec n a
xs) IsNat n => r
r = Vec n a -> (IsNat n => r) -> r
forall (n :: Nat) a r. Vec n a -> (IsNat n => r) -> r
withNat Vec n a
xs r
IsNat n => r
IsNat n => r
r

mat :: (Ob (M m)) => Vec n (Vec m a) -> Mat (M m :: MatK a) (M n)
mat :: forall {a} (m :: Nat) (n :: Nat) a.
Ob (M m) =>
Vec n (Vec m a) -> Mat (M m) (M n)
mat Vec n (Vec m a)
m = Vec n (Vec m a) -> (IsNat n => Mat (M m) (M n)) -> Mat (M m) (M n)
forall (n :: Nat) a r. Vec n a -> (IsNat n => r) -> r
withNat Vec n (Vec m a)
m (Vec n (Vec m a) -> Mat (M m) (M n)
forall {a} {m' :: MatK a} {n' :: MatK a} (m :: Nat) (n :: Nat).
(Ob m', Ob n', m' ~ M m, n' ~ M n) =>
Vec n (Vec m a) -> Mat m' n'
Mat Vec n (Vec m a)
m)

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 b a
forall {a} {m' :: MatK a} {n' :: MatK a} (m :: Nat) (n :: Nat).
(Ob m', Ob n', m' ~ M m, n' ~ M n) =>
Vec n (Vec m a) -> Mat 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 b a
forall {a} {m' :: MatK a} {n' :: MatK a} (m :: Nat) (n :: Nat).
(Ob m', Ob n', m' ~ M m, n' ~ M n) =>
Vec n (Vec m a) -> Mat m' n'
Mat ((Vec n (Complex a) -> Vec n (Complex a))
-> Vec m (Vec n (Complex a)) -> Vec m (Vec n (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) -> Vec n (Complex a) -> Vec n (Complex 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 Complex a -> Complex a
forall a. Num a => Complex a -> Complex a
conjugate) (Vec n (Vec m (Complex a)) -> Vec m (Vec n (Complex 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 (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 :: PRO 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 a a
forall {a} {m' :: MatK a} {n' :: MatK a} (m :: Nat) (n :: Nat).
(Ob m', Ob n', m' ~ M m, n' ~ M n) =>
Vec n (Vec m a) -> Mat 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 {j} (p :: PRO j j) (a :: j) (b :: j).
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 a c
forall {a} {m' :: MatK a} {n' :: MatK a} (m :: Nat) (n :: Nat).
(Ob m', Ob n', m' ~ M m, n' ~ M n) =>
Vec n (Vec m a) -> Mat 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
apply Vec n (Vec m a)
nT) Vec n (Vec m a)
Vec n (Vec m a)
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' :: MatK a} {n' :: MatK a} (m :: Nat) (n :: Nat).
(Ob m', Ob n', m' ~ M m, n' ~ M n) =>
Vec n (Vec m a) -> Mat 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
Nil)
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' :: MatK a} {n' :: MatK a} (m :: Nat) (n :: Nat).
(Ob m', Ob n', m' ~ M m, n' ~ M n) =>
Vec n (Vec m a) -> Mat m' n'
Mat Vec Z (Vec (UN M a) a)
forall a. Vec Z a
Nil

instance (P.Num a) => HasBinaryCoproducts (MatK a) where
  type M x || M y = M (x + y)
  lft :: forall (a :: MatK a) (b :: MatK a). (Ob a, Ob b) => a ~> (a || b)
lft @m @n = (M (UN M a) ~> M (UN M a))
-> Obj (M (UN M b)) -> M (UN M a) ~> (M (UN M a) || M (UN M b))
forall k (a :: k) (a' :: k) (b :: k).
HasBinaryCoproducts k =>
(a ~> a') -> Obj b -> a ~> (a' || b)
forall (a :: MatK a) (a' :: MatK a) (b :: MatK a).
(a ~> a') -> Obj b -> a ~> (a' || b)
lft' (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: MatK a). (CategoryOf (MatK a), Ob a) => Obj a
obj @m) (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: MatK a). (CategoryOf (MatK a), Ob a) => Obj a
obj @n)
  lft' :: forall (a :: MatK a) (a' :: MatK a) (b :: MatK a).
(a ~> a') -> Obj b -> a ~> (a' || b)
lft' (Mat Vec n (Vec m a)
m) (Mat Vec n (Vec m a)
n) = Vec (n + n) (Vec m a) -> Mat (M m) (M (n + n))
forall {a} (m :: Nat) (n :: Nat) a.
Ob (M m) =>
Vec n (Vec m a) -> Mat (M m) (M n)
mat (Vec n (Vec m a) -> Vec n (Vec m a) -> Vec (n + n) (Vec m a)
forall a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a
forall (n :: Nat) a (m :: Nat).
IsNat n =>
Vec n a -> Vec m a -> Vec (n + m) a
append Vec n (Vec m a)
m (Vec m a
forall a. Num a => Vec m a
forall (n :: Nat) a. (IsNat n, Num a) => Vec n a
zero Vec m a -> Vec n (Vec m a) -> Vec n (Vec m a)
forall a b. a -> Vec n b -> Vec n a
forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
P.<$ Vec n (Vec m a)
n))
  rgt :: forall (a :: MatK a) (b :: MatK a). (Ob a, Ob b) => b ~> (a || b)
rgt @m @n = Obj (M (UN M a))
-> (M (UN M b) ~> M (UN M b))
-> M (UN M b) ~> (M (UN M a) || M (UN M b))
forall k (a :: k) (b :: k) (b' :: k).
HasBinaryCoproducts k =>
Obj a -> (b ~> b') -> b ~> (a || b')
forall (a :: MatK a) (b :: MatK a) (b' :: MatK a).
Obj a -> (b ~> b') -> b ~> (a || b')
rgt' (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: MatK a). (CategoryOf (MatK a), Ob a) => Obj a
obj @m) (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: MatK a). (CategoryOf (MatK a), Ob a) => Obj a
obj @n)
  rgt' :: forall (a :: MatK a) (b :: MatK a) (b' :: MatK a).
Obj a -> (b ~> b') -> b ~> (a || b')
rgt' (Mat Vec n (Vec m a)
m) (Mat Vec n (Vec m a)
n) = Vec (n + n) (Vec m a) -> Mat (M m) (M (n + n))
forall {a} (m :: Nat) (n :: Nat) a.
Ob (M m) =>
Vec n (Vec m a) -> Mat (M m) (M n)
mat (Vec n (Vec m a) -> Vec n (Vec m a) -> Vec (n + n) (Vec m a)
forall a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a
forall (n :: Nat) a (m :: Nat).
IsNat n =>
Vec n a -> Vec m a -> Vec (n + m) a
append (Vec m a
forall a. Num a => Vec m a
forall (n :: Nat) a. (IsNat n, Num a) => Vec n a
zero Vec m a -> Vec n (Vec m a) -> Vec n (Vec m a)
forall a b. a -> Vec n b -> Vec n a
forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
P.<$ Vec n (Vec m a)
m) Vec n (Vec m a)
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' :: MatK a} {n' :: MatK a} (m :: Nat) (n :: Nat).
(Ob m', Ob n', m' ~ M m, n' ~ M n) =>
Vec n (Vec m a) -> Mat 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 a (m :: Nat). Vec m a -> Vec m a -> Vec (m + m) a
forall (n :: Nat) a (m :: Nat).
IsNat n =>
Vec n a -> Vec m a -> Vec (n + m) a
append 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)
  fst :: forall (a :: MatK a) (b :: MatK a). (Ob a, Ob b) => (a && b) ~> a
fst @m @n = (M (UN M a) ~> M (UN M a))
-> Obj (M (UN M b)) -> (M (UN M a) && M (UN M b)) ~> M (UN M a)
forall k (a :: k) (a' :: k) (b :: k).
HasBinaryProducts k =>
(a ~> a') -> Obj b -> (a && b) ~> a'
forall (a :: MatK a) (a' :: MatK a) (b :: MatK a).
(a ~> a') -> Obj b -> (a && b) ~> a'
fst' (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: MatK a). (CategoryOf (MatK a), Ob a) => Obj a
obj @m) (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: MatK a). (CategoryOf (MatK a), Ob a) => Obj a
obj @n)
  fst' :: forall (a :: MatK a) (a' :: MatK a) (b :: MatK a).
(a ~> a') -> Obj b -> (a && b) ~> a'
fst' (Mat @m Vec n (Vec m a)
m) (Mat @n Vec n (Vec m a)
n) = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n + m) => r) -> r
withPlusNat @m @n (Vec n (Vec (m + n) a) -> Mat (M (m + n)) (M n)
forall {a} {m' :: MatK a} {n' :: MatK a} (m :: Nat) (n :: Nat).
(Ob m', Ob n', m' ~ M m, n' ~ M n) =>
Vec n (Vec m a) -> Mat m' n'
Mat ((Vec m a -> Vec (m + n) a)
-> Vec n (Vec m a) -> Vec n (Vec (m + 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 -> Vec n a -> Vec (m + n) a
forall a (m :: Nat). Vec m a -> Vec m a -> Vec (m + m) a
forall (n :: Nat) a (m :: Nat).
IsNat n =>
Vec n a -> Vec m a -> Vec (n + m) a
`append` (a
0 a -> Vec n (Vec m a) -> Vec n a
forall a b. a -> Vec n b -> Vec n a
forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
P.<$ Vec n (Vec m a)
n)) Vec n (Vec m a)
m))
  snd :: forall (a :: MatK a) (b :: MatK a). (Ob a, Ob b) => (a && b) ~> b
snd @m @n = Obj (M (UN M a))
-> (M (UN M b) ~> M (UN M b))
-> (M (UN M a) && M (UN M b)) ~> M (UN M b)
forall k (a :: k) (b :: k) (b' :: k).
HasBinaryProducts k =>
Obj a -> (b ~> b') -> (a && b) ~> b'
forall (a :: MatK a) (b :: MatK a) (b' :: MatK a).
Obj a -> (b ~> b') -> (a && b) ~> b'
snd' (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: MatK a). (CategoryOf (MatK a), Ob a) => Obj a
obj @m) (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: MatK a). (CategoryOf (MatK a), Ob a) => Obj a
obj @n)
  snd' :: forall (a :: MatK a) (b :: MatK a) (b' :: MatK a).
Obj a -> (b ~> b') -> (a && b) ~> b'
snd' (Mat @m Vec n (Vec m a)
m) (Mat @n Vec n (Vec m a)
n) = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n + m) => r) -> r
withPlusNat @m @n (Vec n (Vec (n + m) a) -> Mat (M (n + m)) (M n)
forall {a} {m' :: MatK a} {n' :: MatK a} (m :: Nat) (n :: Nat).
(Ob m', Ob n', m' ~ M m, n' ~ M n) =>
Vec n (Vec m a) -> Mat m' n'
Mat ((Vec m a -> Vec (n + m) a)
-> Vec n (Vec m a) -> Vec n (Vec (n + 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 n a -> Vec m a -> Vec (n + m) a
forall a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a
forall (n :: Nat) a (m :: Nat).
IsNat n =>
Vec n a -> Vec m a -> Vec (n + m) a
append (a
0 a -> Vec n (Vec m a) -> Vec n a
forall a b. a -> Vec n b -> Vec n a
forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
P.<$ Vec n (Vec m a)
m)) Vec n (Vec m a)
n))
  Mat Vec n (Vec m a)
a &&& :: forall (a :: MatK a) (x :: MatK a) (y :: MatK a).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Mat Vec n (Vec m a)
b = Vec (n + n) (Vec m a) -> Mat (M m) (M (n + n))
forall {a} (m :: Nat) (n :: Nat) a.
Ob (M m) =>
Vec n (Vec m a) -> Mat (M m) (M n)
mat (Vec n (Vec m a) -> Vec n (Vec m a) -> Vec (n + n) (Vec m a)
forall a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a
forall (n :: Nat) a (m :: Nat).
IsNat n =>
Vec n a -> Vec m a -> Vec (n + m) a
append Vec n (Vec m a)
a Vec n (Vec m a)
Vec n (Vec m a)
b)

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 :: PRO 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 (x1 ** y1) (x2 ** y2)
forall {a} {m' :: MatK a} {n' :: MatK a} (m :: Nat) (n :: Nat).
(Ob m', Ob n', m' ~ M m, n' ~ M n) =>
Vec n (Vec m a) -> Mat m' n'
Mat (Vec (n * n) (Vec (m * m) a) -> Mat (x1 ** y1) (x2 ** y2))
-> Vec (n * n) (Vec (m * m) a) -> Mat (x1 ** y1) (x2 ** y2)
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 (n :: Nat) (m :: Nat) a b.
(IsNat n, IsNat m) =>
(a -> Vec m b) -> Vec n a -> Vec (n * m) b
forall (m :: Nat) a b.
IsNat m =>
(a -> Vec m b) -> Vec n a -> Vec (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 (n :: Nat) (m :: Nat) a b.
(IsNat n, IsNat m) =>
(a -> Vec m b) -> Vec n a -> Vec (n * m) b
forall (m :: Nat) a b.
IsNat m =>
(a -> Vec m b) -> Vec m a -> Vec (m * 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

instance (P.Num a) => Monoidal (MatK a) where
  type Unit = M (S Z)
  type M x ** M y = M (y * x)
  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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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
  Mat @gx @gy Vec n (Vec m a)
g swap' :: forall (a :: MatK a) (a' :: MatK a) (b :: MatK a) (b' :: MatK a).
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
`swap'` Mat @fx @fy Vec n (Vec m a)
f =
    forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n * m) => r) -> r
withMultNat @fx @gx ((IsNat (m * m) => (a ** b) ~> (b' ** a'))
 -> (a ** b) ~> (b' ** a'))
-> (IsNat (m * m) => (a ** b) ~> (b' ** a'))
-> (a ** b) ~> (b' ** a')
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) => (a ** b) ~> (b' ** a'))
 -> (a ** b) ~> (b' ** a'))
-> (IsNat (n * n) => (a ** b) ~> (b' ** a'))
-> (a ** b) ~> (b' ** a')
forall a b. (a -> b) -> a -> b
$
        forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(((n * m) ~ (m * n)) => r) -> r
withMultSym @fx @gx ((((m * m) ~ (m * m)) => (a ** b) ~> (b' ** a'))
 -> (a ** b) ~> (b' ** a'))
-> (((m * m) ~ (m * m)) => (a ** b) ~> (b' ** a'))
-> (a ** b) ~> (b' ** a')
forall a b. (a -> b) -> a -> b
$
          Vec (n * n) (Vec (m * m) a) -> Mat (M (m * m)) (M (n * n))
forall {a} {m' :: MatK a} {n' :: MatK a} (m :: Nat) (n :: Nat).
(Ob m', Ob n', m' ~ M m, n' ~ M n) =>
Vec n (Vec m a) -> Mat 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 (n :: Nat) (m :: Nat) a b.
(IsNat n, IsNat m) =>
(a -> Vec m b) -> Vec n a -> Vec (n * m) b
forall (m :: Nat) a b.
IsNat m =>
(a -> Vec m b) -> Vec n a -> Vec (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 (n :: Nat) (m :: Nat) a b.
(IsNat n, IsNat m) =>
(a -> Vec m b) -> Vec n a -> Vec (n * m) b
forall (m :: Nat) a b.
IsNat m =>
(a -> Vec m b) -> Vec m a -> Vec (m * 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

instance (P.Num a) => Closed (MatK a) where
  type M x ~~> M y = M (y * x)
  curry' :: forall (a :: MatK a) (b :: MatK a) (c :: MatK a).
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry' (Mat @x Vec n (Vec m a)
_) (Mat @y Vec n (Vec m a)
_) (Mat @_ @z 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 (n * m) => a ~> (b ~~> c)) -> a ~> (b ~~> c))
-> (IsNat (n * m) => a ~> (b ~~> c)) -> a ~> (b ~~> c)
forall a b. (a -> b) -> a -> b
$ Vec (n * n) (Vec n a) -> Mat (M n) (M (n * n))
forall {a} {m' :: MatK a} {n' :: MatK a} (m :: Nat) (n :: Nat).
(Ob m', Ob n', m' ~ M m, n' ~ M n) =>
Vec n (Vec m a) -> Mat m' n'
Mat ((Vec m (Vec n a) -> Vec n (Vec n a))
-> Vec n (Vec m (Vec n a)) -> Vec (n * n) (Vec n a)
forall (n :: Nat) (m :: Nat) a b.
(IsNat n, IsNat m) =>
(a -> Vec m b) -> Vec n a -> Vec (n * m) b
forall (m :: Nat) a b.
IsNat m =>
(a -> Vec m b) -> Vec n a -> Vec (n * m) b
concatMap Vec m (Vec n a) -> Vec n (Vec n a)
Vec n (Vec n a) -> Vec n (Vec n a)
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id ((Vec m a -> Vec m (Vec n a))
-> Vec n (Vec m a) -> Vec n (Vec m (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 (forall (n :: Nat) (m :: Nat) b a.
(IsNat n, IsNat m) =>
(Vec m b -> a) -> Vec (n * m) b -> Vec n a
unConcatMap @y @x Vec m a -> Vec n a
Vec n a -> Vec n a
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id) Vec n (Vec m a)
m))
  uncurry' :: forall (b :: MatK a) (c :: MatK a) (a :: MatK a).
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry' (Mat @y Vec n (Vec m a)
_) (Mat @z Vec n (Vec m a)
_) (Mat @x 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 (m * m) => (a ** b) ~> c) -> (a ** b) ~> c)
-> (IsNat (m * m) => (a ** b) ~> c) -> (a ** b) ~> c
forall a b. (a -> b) -> a -> b
$ Vec m (Vec (n * m) a) -> Mat (M (n * m)) (M n)
forall {a} {m' :: MatK a} {n' :: MatK a} (m :: Nat) (n :: Nat).
(Ob m', Ob n', m' ~ M m, n' ~ M n) =>
Vec n (Vec m a) -> Mat m' n'
Mat ((Vec n (Vec m a) -> Vec (n * m) a)
-> Vec m (Vec n (Vec m a)) -> Vec m (Vec (n * 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 ((Vec m a -> Vec m a) -> Vec n (Vec m a) -> Vec (n * m) a
forall (n :: Nat) (m :: Nat) a b.
(IsNat n, IsNat m) =>
(a -> Vec m b) -> Vec n a -> Vec (n * m) b
forall (m :: Nat) a b.
IsNat m =>
(a -> Vec m b) -> Vec n a -> Vec (n * m) b
concatMap Vec m a -> Vec m a
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id) (forall (n :: Nat) (m :: Nat) b a.
(IsNat n, IsNat m) =>
(Vec m b -> a) -> Vec (n * m) b -> Vec n a
unConcatMap @z @y Vec m (Vec m a) -> Vec n (Vec m a)
Vec n (Vec m a) -> Vec n (Vec m a)
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id Vec n (Vec m a)
Vec (m * m) (Vec m a)
m))
  f :: b ~> y
f@Mat{} ^^^ :: forall (b :: MatK a) (y :: MatK a) (x :: MatK a) (a :: MatK a).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ g :: x ~> a
g@Mat{} = case Mat (M m) (M n) -> Mat (M n) (M m)
forall {j} (p :: PRO j j) (a :: j) (b :: j).
DaggerProfunctor p =>
p a b -> p b a
forall (a :: MatK a) (b :: MatK a). Mat a b -> Mat b a
dagger x ~> a
Mat (M m) (M n)
g Mat (M n) (M m) -> Mat (M m) (M n) -> Mat (M n ** M m) (M m ** M n)
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` b ~> y
Mat (M m) (M n)
f of Mat Vec n (Vec m a)
h -> Vec n (Vec m a) -> Mat (M m) (M n)
forall {a} {m' :: MatK a} {n' :: MatK a} (m :: Nat) (n :: Nat).
(Ob m', Ob n', m' ~ M m, n' ~ M n) =>
Vec n (Vec m a) -> Mat m' n'
Mat Vec n (Vec m a)
h

instance (P.Num a) => StarAutonomous (MatK a) where
  type Bottom = M (S Z)
  bottomObj :: Obj Bottom
bottomObj = Obj Bottom
Mat (M (S Z)) (M (S Z))
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: MatK a). Ob a => Mat a a
id
  doubleNeg :: forall (a :: MatK a).
(StarAutonomous (MatK a), Ob a) =>
Dual (Dual a) ~> a
doubleNeg = ((a ~~> Bottom) ~~> Bottom) ~> a
Mat (M (UN M a)) (M (UN M a))
forall {k} (p :: PRO 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) => 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 = (M (UN M a) ~> M (UN M a))
-> (M (UN M b) ~> M (UN M b))
-> Dual (M (UN M a) ** M (UN M b))
   ~> (Dual (M (UN M a)) ** Dual (M (UN M b)))
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
CompactClosed k =>
(a ~> a') -> (b ~> b') -> Dual (a' ** b') ~> (Dual a ** Dual b)
forall (a :: MatK a) (a' :: MatK a) (b :: MatK a) (b' :: MatK a).
(a ~> a') -> (b ~> b') -> Dual (a' ** b') ~> (Dual a ** Dual b)
distribDual' (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: MatK a). (CategoryOf (MatK a), Ob a) => Obj a
obj @m) (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: MatK a). (CategoryOf (MatK a), Ob a) => Obj a
obj @n)
  distribDual' :: forall (a :: MatK a) (a' :: MatK a) (b :: MatK a) (b' :: MatK a).
(a ~> a') -> (b ~> b') -> Dual (a' ** b') ~> (Dual a ** Dual b)
distribDual' a :: a ~> a'
a@(Mat @_ @n Vec n (Vec m a)
_) b :: b ~> b'
b@(Mat @_ @n1 Vec n (Vec m a)
_) = forall (n :: Nat) (m :: Nat) r.
(IsNat n, IsNat m) =>
(IsNat (n * m) => r) -> r
withMultNat @n1 @n ((IsNat (n * n) => Dual (a' ** b') ~> (Dual a ** Dual b))
 -> Dual (a' ** b') ~> (Dual a ** Dual b))
-> (IsNat (n * n) => Dual (a' ** b') ~> (Dual a ** Dual b))
-> Dual (a' ** b') ~> (Dual a ** Dual b)
forall a b. (a -> b) -> a -> b
$ Mat (M m) (M n) -> Mat (M n) (M m)
forall {j} (p :: PRO j j) (a :: j) (b :: j).
DaggerProfunctor p =>
p a b -> p b a
forall (a :: MatK a) (b :: MatK a). Mat a b -> Mat b a
dagger a ~> a'
Mat (M m) (M n)
a Mat (M n) (M m) -> Mat (M n) (M m) -> Mat (M n ** M n) (M m ** M m)
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 m) (M n) -> Mat (M n) (M m)
forall {j} (p :: PRO j j) (a :: j) (b :: j).
DaggerProfunctor p =>
p a b -> p b a
forall (a :: MatK a) (b :: MatK a). Mat a b -> Mat b a
dagger b ~> b'
Mat (M m) (M n)
b

instance (P.Num a) => TracedMonoidalProfunctor (Mat :: CAT (MatK a)) where
  trace :: forall (u :: MatK a) (x :: MatK a) (y :: MatK a).
(Ob x, Ob y, Ob u) =>
Mat (x ** u) (y ** u) -> Mat x y
trace @x = forall {k} (u :: k) (x :: k) (y :: k).
(CompactClosed k, Ob x, Ob y, Ob u) =>
((x ** u) ~> (y ** u)) -> x ~> y
forall (u :: MatK a) (x :: MatK a) (y :: MatK a).
(CompactClosed (MatK a), Ob x, Ob y, Ob u) =>
((x ** u) ~> (y ** u)) -> x ~> y
compactClosedTrace @x