Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Mat

Description

The category of matrices over a numeric type a: objects are natural numbers (dimensions, M n of kind MatK a) and a morphism is an n-by-m matrix, composed by matrix multiplication. A dagger (conjugate-transpose) category with biproducts, whose Kronecker-product tensor makes it compact closed. It is the library's linear-algebra playground. The compact structure's dual is the plain transpose, distinct from dagger once the entries are complex.

Synopsis

type (+) (n :: Nat) (m :: Nat) = Plus n m
type (*) (n :: Nat) (m :: Nat) = Mult n m
data MatK a = M Nat
data Mat (b :: MatK a) (c :: MatK a) where
- Mat :: forall {a} (m :: Nat) (n :: Nat). (IsNat m, IsNat n) => {..} -> Mat ('M m :: MatK a) ('M n :: MatK a)
app :: forall a (m :: Nat) (n :: Nat). (Num a, Applicative (Vec m)) => Vec n (Vec m a) -> Vec m a -> Vec n a
arr :: forall (n :: Nat) (m :: Nat) a. 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 m :: MatK a) ('M n :: MatK a)
oneV :: forall a (n :: Nat). (Num a, IsNat n) => Fin n -> Vec n a
zero :: forall a (n :: Nat). (Num a, IsNat n) => Vec n a
withIsNat :: forall (n :: Nat) r. SNatI n => (IsNat n => r) -> r
class (SNatI n, Applicative (Vec n), (n + 'Z) ~ n, (n * 'Z) ~ 'Z, (n * 'S 'Z) ~ n) => IsNat (n :: Nat) where
- matId :: Num a => Vec n (Vec n a)
- withPlusNat :: forall (m :: Nat) r. IsNat m => (IsNat (n + m) => r) -> r
- withMultNat :: forall (m :: Nat) r. IsNat m => (IsNat (n * m) => r) -> r
- withPlusSucc :: forall (m :: Nat) r. IsNat m => ((n + 'S m) ~ 'S (n + m) => r) -> r
- withMultSucc :: forall (m :: Nat) r. IsNat m => ((n * 'S m) ~ (n + (n * m)) => r) -> r
- withPlusSym :: forall (m :: Nat) r. IsNat m => ((n + m) ~ (m + n) => r) -> r
- withMultSym :: forall (m :: Nat) r. IsNat m => ((n * m) ~ (m * n) => r) -> r
- withAssocPlus :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => (((n + m) + o) ~ (n + (m + o)) => r) -> r
- withAssocMult :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => (((n * m) * o) ~ (n * (m * o)) => r) -> r
- withDist :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => (((n + m) * o) ~ ((n * o) + (m * o)) => r) -> r
transpose :: forall a (n :: MatK a) (m :: MatK a). Mat n m -> Mat m n
at :: forall (m :: Nat) a. Vec m a -> Int -> a
rref :: forall a (m :: Nat). (Fractional a, Eq a) => Int -> [Vec m a] -> ([Int], [Vec m a])
data family Conjugate :: MatK (Complex a) +-> MatK (Complex a)
data family App :: MatK a +-> Type

Documentation

type (+) (n :: Nat) (m :: Nat) = Plus n m Source Github #

type (*) (n :: Nat) (m :: Nat) = Mult n m Source Github #

data MatK a Source Github #

Constructors

M Nat

Instances

Instances details

Num a => Monoidal (MatK a) Source Github #

Products of the dimensions of the matrices as the tensor. This is the Kronecker product of matrices.

Instance details

Defined in Proarrow.Category.Instance.Mat

Associated Types

type Unit
Instance details Defined in Proarrow.Category.Instance.Mat type Unit = 'M ('S 'Z) :: MatK a

Methods

withOb2 :: forall (a0 :: MatK a) (b :: MatK a) r. (Ob a0, Ob b) => (Ob (a0 ** b) => r) -> r Source Github #

leftUnitor :: forall (a0 :: MatK a). Ob a0 => ((Unit :: MatK a) ** a0) ~> a0 Source Github #

leftUnitorInv :: forall (a0 :: MatK a). Ob a0 => a0 ~> ((Unit :: MatK a) ** a0) Source Github #

rightUnitor :: forall (a0 :: MatK a). Ob a0 => (a0 ** (Unit :: MatK a)) ~> a0 Source Github #

rightUnitorInv :: forall (a0 :: MatK a). Ob a0 => a0 ~> (a0 ** (Unit :: MatK a)) Source Github #

associator :: forall (a0 :: MatK a) (b :: MatK a) (c :: MatK a). (Ob a0, Ob b, Ob c) => ((a0 ** b) ** c) ~> (a0 ** (b ** c)) Source Github #

associatorInv :: forall (a0 :: MatK a) (b :: MatK a) (c :: MatK a). (Ob a0, Ob b, Ob c) => (a0 ** (b ** c)) ~> ((a0 ** b) ** c) Source Github #

Num a => SymMonoidal (MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

swap :: forall (a0 :: MatK a) (b :: MatK a). (Ob a0, Ob b) => (a0 ** b) ~> (b ** a0) Source Github #

Num a => Closed (MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

withObExp :: forall (a0 :: MatK a) (b :: MatK a) r. (Ob a0, Ob b) => (Ob (a0 ~~> b) => r) -> r Source Github #

curry :: forall (a0 :: MatK a) (b :: MatK a) (c :: MatK a). (Ob a0, Ob b) => ((a0 ** b) ~> c) -> a0 ~> (b ~~> c) Source Github #

apply :: forall (a0 :: MatK a) (b :: MatK a). (Ob a0, Ob b) => ((a0 ~~> b) ** a0) ~> b Source Github #

(^^^) :: forall (a0 :: MatK a) (b :: MatK a) (x :: MatK a) (y :: MatK a). (b ~> y) -> (x ~> a0) -> (a0 ~~> b) ~> (x ~~> y) Source Github #

Num a => CompactClosed (MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

distribDual :: forall (a0 :: MatK a) (b :: MatK a). (Ob a0, Ob b) => Dual (a0 ** b) ~> (Dual a0 ** Dual b) Source Github #

dualUnit :: Dual (Unit :: MatK a) ~> (Unit :: MatK a) Source Github #

dualityUnit :: forall (a0 :: MatK a). Ob a0 => (Unit :: MatK a) ~> (a0 ** Dual a0) Source Github #

dualityCounit :: forall (a0 :: MatK a). Ob a0 => (Dual a0 ** a0) ~> (Unit :: MatK a) Source Github #

Num a => CopyDiscard (MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

copy :: forall (a0 :: MatK a). Ob a0 => a0 ~> (a0 ** a0) Source Github #

discard :: forall (a0 :: MatK a). Ob a0 => a0 ~> (Unit :: MatK a) Source Github #

Num a => Distributive (MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

distL :: forall (a0 :: MatK a) (b :: MatK a) (c :: MatK a). (Ob a0, Ob b, Ob c) => (a0 ** (b || c)) ~> ((a0 ** b) || (a0 ** c)) Source Github #

distR :: forall (a0 :: MatK a) (b :: MatK a) (c :: MatK a). (Ob a0, Ob b, Ob c) => ((a0 || b) ** c) ~> ((a0 ** c) || (b ** c)) Source Github #

absorbL :: forall (a0 :: MatK a). Ob a0 => (a0 ** (InitialObject :: MatK a)) ~> (InitialObject :: MatK a) Source Github #

absorbR :: forall (a0 :: MatK a). Ob a0 => ((InitialObject :: MatK a) ** a0) ~> (InitialObject :: MatK a) Source Github #

Num a => Hypergraph (MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Num a => StarAutonomous (MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

withObDual :: forall (a0 :: MatK a) r. Ob a0 => (Ob (Dual a0) => r) -> r Source Github #

dual :: forall (a0 :: MatK a) (b :: MatK a). (a0 ~> b) -> Dual b ~> Dual a0 Source Github #

dualInv :: forall (a0 :: MatK a) (b :: MatK a). (Ob a0, Ob b) => (Dual a0 ~> Dual b) -> b ~> a0 Source Github #

linDist :: forall (a0 :: MatK a) (b :: MatK a) (c :: MatK a). (Ob a0, Ob b, Ob c) => ((a0 ** b) ~> Dual c) -> a0 ~> Dual (b ** c) Source Github #

linDistInv :: forall (a0 :: MatK a) (b :: MatK a) (c :: MatK a). (Ob a0, Ob b, Ob c) => (a0 ~> Dual (b ** c)) -> (a0 ** b) ~> Dual c Source Github #

doubleNeg :: forall (a0 :: MatK a). Ob a0 => Dual (Dual a0) ~> a0 Source Github #

doubleNegInv :: forall (a0 :: MatK a). Ob a0 => a0 ~> Dual (Dual a0) Source Github #

(Fractional a, Eq a) => HasEpiMonoFactorization (MatK a) Source Github #

Epi-mono factorization is computed via defaultFactorize: f factors as the coequalizer of its cokernel pair (the epi onto its image) followed by the equalizer factorization of f through that epi (the mono inclusion of the image).

>>> import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
>>> let h = Mat @(S (S Z)) @(S (S Z)) ((1 ::: 2 ::: VNil) ::: (2 ::: 4 ::: VNil) ::: VNil) :: Mat (M (S (S Z))) (M (S (S Z)) :: MatK P.Double)
>>> (case factorize h of e :.: m -> case (e, m) of (Mat ev, Mat mv) -> P.show (ev, mv, unMat (m . e))) :: P.String
"((2.0 ::: 4.0 ::: VNil) ::: VNil,(0.5 ::: VNil) ::: (1.0 ::: VNil) ::: VNil,(1.0 ::: 2.0 ::: VNil) ::: (2.0 ::: 4.0 ::: VNil) ::: VNil)"

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

factorize :: forall (a0 :: MatK a) (b :: MatK a). (a0 ~> b) -> (Hom (MatK a) :.: Hom (MatK a)) a0 b Source Github #

Num a => HasBinaryCoproducts (MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

withObCoprod :: forall (a0 :: MatK a) (b :: MatK a) r. (Ob a0, Ob b) => (Ob (a0 || b) => r) -> r Source Github #

lft :: forall (a0 :: MatK a) (b :: MatK a). (Ob a0, Ob b) => a0 ~> (a0 || b) Source Github #

rgt :: forall (a0 :: MatK a) (b :: MatK a). (Ob a0, Ob b) => b ~> (a0 || b) Source Github #

(|||) :: forall (x :: MatK a) (a0 :: MatK a) (y :: MatK a). (x ~> a0) -> (y ~> a0) -> (x || y) ~> a0 Source Github #

(+++) :: forall (a0 :: MatK a) (b :: MatK a) (x :: MatK a) (y :: MatK a). (a0 ~> x) -> (b ~> y) -> (a0 || b) ~> (x || y) Source Github #

Num a => HasBiproducts (MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

sum :: forall (a0 :: MatK a) (b :: MatK a). (a0 ~> b) -> (a0 ~> b) -> a0 ~> b Source Github #

(Fractional a, Eq a) => HasCoequalizers (MatK a) Source Github #

The coequalizer of f, g :: M m ~> M n is the cokernel of f - g. Since dagger is a contravariant involution on Mat, it is the equalizer of dagger f, dagger g transported back.

>>> let f = Mat @(S Z) @(S (S Z)) ((2 ::: VNil) ::: (0 ::: VNil) ::: VNil) :: Mat (M (S Z)) (M (S (S Z)) :: MatK P.Double)
>>> let g = Mat @(S Z) @(S (S Z)) ((0 ::: VNil) ::: (3 ::: VNil) ::: VNil) :: Mat (M (S Z)) (M (S (S Z)) :: MatK P.Double)
>>> let w = Mat @(S (S Z)) @(S Z) ((3 ::: 2 ::: VNil) ::: VNil) :: Mat (M (S (S Z))) (M (S Z) :: MatK P.Double)
>>> (coequalize f g \q@(Mat qv) -> case factorCoequalizer q w of s@(Mat sv) -> P.show (qv, sv, unMat (s . q))) :: P.String
"((1.5 ::: 1.0 ::: VNil) ::: VNil,(2.0 ::: VNil) ::: VNil,(3.0 ::: 2.0 ::: VNil) ::: VNil)"

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

coequalize :: forall (a0 :: MatK a) (b :: MatK a) r. (a0 ~> b) -> (a0 ~> b) -> (forall (c :: MatK a). (b ~> c) -> r) -> r Source Github #

factorCoequalizer :: forall (c :: MatK a) (x :: MatK a) (c' :: MatK a). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #

Num a => HasInitialObject (MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.Mat type InitialObject = 'M 'Z :: MatK a

Methods

initiate :: forall (a0 :: MatK a). Ob a0 => (InitialObject :: MatK a) ~> a0 Source Github #

(Fractional a, Eq a) => HasPushouts (MatK a) Source Github #

Pushouts are computed via pushoutDefault, as the coequalizer of lft . f and rgt . g on the coproduct a || b, the standard linear-algebra construction of a cofiber product of vector spaces.

>>> let f = Mat @(S Z) @(S Z) ((2 ::: VNil) ::: VNil) :: Mat (M (S Z)) (M (S Z) :: MatK P.Double)
>>> let g = Mat @(S Z) @(S Z) ((3 ::: VNil) ::: VNil) :: Mat (M (S Z)) (M (S Z) :: MatK P.Double)
>>> (pushout f g \p q -> case (p, q) of (Mat pv, Mat qv) -> P.show (pv, qv)) :: P.String
"((1.5 ::: VNil) ::: VNil,(1.0 ::: VNil) ::: VNil)"

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

pushout :: forall (o :: MatK a) (a0 :: MatK a) (b :: MatK a) r. (o ~> a0) -> (o ~> b) -> (forall (p :: MatK a). (a0 ~> p) -> (b ~> p) -> r) -> r Source Github #

factorPushout :: forall (a0 :: MatK a) (b :: MatK a) (p :: MatK a) (q :: MatK a). (a0 ~> p) -> (b ~> p) -> (a0 ~> q) -> (b ~> q) -> p ~> q Source Github #

Num a => CategoryOf (MatK a) Source Github #

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 details

Defined in Proarrow.Category.Instance.Mat

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.Mat type (~>) = Mat :: MatK a -> MatK a -> Type

Num a => HasBinaryProducts (MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

withObProd :: forall (a0 :: MatK a) (b :: MatK a) r. (Ob a0, Ob b) => (Ob (a0 && b) => r) -> r Source Github #

fst :: forall (a0 :: MatK a) (b :: MatK a). (Ob a0, Ob b) => (a0 && b) ~> a0 Source Github #

snd :: forall (a0 :: MatK a) (b :: MatK a). (Ob a0, Ob b) => (a0 && b) ~> b Source Github #

(&&&) :: forall (a0 :: MatK a) (x :: MatK a) (y :: MatK a). (a0 ~> x) -> (a0 ~> y) -> a0 ~> (x && y) Source Github #

(***) :: forall (a0 :: MatK a) (b :: MatK a) (x :: MatK a) (y :: MatK a). (a0 ~> x) -> (b ~> y) -> (a0 && b) ~> (x && y) Source Github #

(Fractional a, Eq a) => HasEqualizers (MatK a) Source Github #

The equalizer of two linear maps f, g :: M m ~> M n is the kernel of f - g: the subspace of M m on which they agree. Computed by row-reducing f - g to reduced row echelon form; the free (non-pivot) columns of the result index a basis of the kernel.

>>> import Data.Vec.Lazy (Vec(..))
>>> let f = Mat @(S (S Z)) @(S Z) ((1 ::: 2 ::: VNil) ::: VNil) :: Mat (M (S (S Z))) (M (S Z) :: MatK P.Double)
>>> let g = Mat @(S (S Z)) @(S Z) ((3 ::: 0 ::: VNil) ::: VNil) :: Mat (M (S (S Z))) (M (S Z) :: MatK P.Double)
>>> let h = Mat @(S Z) @(S (S Z)) ((1 ::: VNil) ::: (1 ::: VNil) ::: VNil) :: Mat (M (S Z)) (M (S (S Z)) :: MatK P.Double)
>>> (equalize f g \incl@(Mat inclv) -> case factorEqualizer incl h of p@(Mat pv) -> P.show (inclv, pv, unMat (incl . p))) :: P.String
"((1.0 ::: VNil) ::: (1.0 ::: VNil) ::: VNil,(1.0 ::: VNil) ::: VNil,(1.0 ::: VNil) ::: (1.0 ::: VNil) ::: VNil)"

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

equalize :: forall (a0 :: MatK a) (b :: MatK a) r. (a0 ~> b) -> (a0 ~> b) -> (forall (e :: MatK a). (e ~> a0) -> r) -> r Source Github #

factorEqualizer :: forall (e :: MatK a) (x :: MatK a) (e' :: MatK a). (e ~> x) -> (e' ~> x) -> e' ~> e Source Github #

(Fractional a, Eq a) => HasPullbacks (MatK a) Source Github #

Pullbacks are computed via pullbackDefault, as the equalizer of f . fst and g . snd on the product a && b, the standard linear-algebra construction of a fiber product of vector spaces.

>>> let f = Mat @(S Z) @(S Z) ((2 ::: VNil) ::: VNil) :: Mat (M (S Z)) (M (S Z) :: MatK P.Double)
>>> let g = Mat @(S Z) @(S Z) ((3 ::: VNil) ::: VNil) :: Mat (M (S Z)) (M (S Z) :: MatK P.Double)
>>> (pullback f g \p q -> case (p, q) of (Mat pv, Mat qv) -> P.show (pv, qv)) :: P.String
"((1.5 ::: VNil) ::: VNil,(1.0 ::: VNil) ::: VNil)"

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

pullback :: forall (o :: MatK a) (a0 :: MatK a) (b :: MatK a) r. (a0 ~> o) -> (b ~> o) -> (forall (p :: MatK a). (p ~> a0) -> (p ~> b) -> r) -> r Source Github #

factorPullback :: forall (a0 :: MatK a) (b :: MatK a) (p :: MatK a) (q :: MatK a). (p ~> a0) -> (p ~> b) -> (q ~> a0) -> (q ~> b) -> q ~> p Source Github #

Num a => HasTerminalObject (MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Mat type TerminalObject = 'M 'Z :: MatK a

Methods

terminate :: forall (a0 :: MatK a). Ob a0 => a0 ~> (TerminalObject :: MatK a) Source Github #

Num a => FunctorForRep (App :: MatK a +-> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

fmap :: forall (a0 :: MatK a) (b :: MatK a). (a0 ~> b) -> ((App :: MatK a +-> Type) @ a0) ~> ((App :: MatK a +-> Type) @ b) Source Github #

Num a => MonoidalProfunctor (Rep (App :: MatK a +-> Type) :: Type -> MatK a -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

one :: Rep (App :: MatK a +-> Type) (Unit :: Type) (Unit :: MatK a) Source Github #

(**) :: forall x1 (x2 :: MatK a) y1 (y2 :: MatK a). Rep (App :: MatK a +-> Type) x1 x2 -> Rep (App :: MatK a +-> Type) y1 y2 -> Rep (App :: MatK a +-> Type) (x1 ** y1) (x2 ** y2) Source Github #

RealFloat a => DaggerProfunctor (Mat :: MatK (Complex a) -> MatK (Complex a) -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

dagger :: forall (a0 :: MatK (Complex a)) (b :: MatK (Complex a)). Mat a0 b -> Mat b a0 Source Github #

Num a => DaggerProfunctor (Mat :: MatK a -> MatK a -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

dagger :: forall (a0 :: MatK a) (b :: MatK a). Mat a0 b -> Mat b a0 Source Github #

Num a => Promonad (Mat :: MatK a -> MatK a -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

id :: forall (a0 :: MatK a). Ob a0 => Mat a0 a0 Source Github #

(.) :: forall (b :: MatK a) (c :: MatK a) (a0 :: MatK a). Mat b c -> Mat a0 b -> Mat a0 c Source Github #

(Num a, MonoidalAction t) => Costrong (t :: (MatK a, MatK a) +-> MatK a) (Mat :: MatK a -> MatK a -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

coact :: forall (a0 :: MatK a) (x :: MatK a) (y :: MatK a). (Ob a0, Ob x, Ob y) => Mat (Act t a0 x) (Act t a0 y) -> Mat x y Source Github #

Num a => MonoidalProfunctor (Mat :: MatK a -> MatK a -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

one :: Mat (Unit :: MatK a) (Unit :: MatK a) Source Github #

(**) :: forall (x1 :: MatK a) (x2 :: MatK a) (y1 :: MatK a) (y2 :: MatK a). Mat x1 x2 -> Mat y1 y2 -> Mat (x1 ** y1) (x2 ** y2) Source Github #

Num a => Profunctor (Mat :: MatK a -> MatK a -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

dimap :: forall (c :: MatK a) (a0 :: MatK a) (b :: MatK a) (d :: MatK a). (c ~> a0) -> (b ~> d) -> Mat a0 b -> Mat c d Source Github #

lmap :: forall (c :: MatK a) (a0 :: MatK a) (b :: MatK a). (c ~> a0) -> Mat a0 b -> Mat c b Source Github #

rmap :: forall (b :: MatK a) (d :: MatK a) (a0 :: MatK a). (b ~> d) -> Mat a0 b -> Mat a0 d Source Github #

(\\) :: forall (a0 :: MatK a) (b :: MatK a) r. ((Ob a0, Ob b) => r) -> Mat a0 b -> r Source Github #

RealFloat a => FunctorForRep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

fmap :: forall (a0 :: MatK (Complex a)) (b :: MatK (Complex a)). (a0 ~> b) -> ((Conjugate :: MatK (Complex a) +-> MatK (Complex a)) @ a0) ~> ((Conjugate :: MatK (Complex a) +-> MatK (Complex a)) @ b) Source Github #

RealFloat a => MonoidalProfunctor (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) :: MatK (Complex a) -> MatK (Complex a) -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

one :: Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) (Unit :: MatK (Complex a)) (Unit :: MatK (Complex a)) Source Github #

(**) :: forall (x1 :: MatK (Complex a)) (x2 :: MatK (Complex a)) (y1 :: MatK (Complex a)) (y2 :: MatK (Complex a)). Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) x1 x2 -> Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) y1 y2 -> Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) (x1 ** y1) (x2 ** y2) Source Github #

RealFloat a => Corepresentable (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) :: MatK (Complex a) -> MatK (Complex a) -> Type) Source Github #

Conjugation is a self-adjoint functor

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

coindex :: forall (a0 :: MatK (Complex a)) (b :: MatK (Complex a)). Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) a0 b -> (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) %% a0) ~> b Source Github #

cotabulate :: forall (a0 :: MatK (Complex a)) (b :: MatK (Complex a)). Ob a0 => ((Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) %% a0) ~> b) -> Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) a0 b Source Github #

corepMap :: forall (a0 :: MatK (Complex a)) (b :: MatK (Complex a)). (a0 ~> b) -> (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) %% a0) ~> (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) %% b) Source Github #

corepUniv :: forall (a0 :: MatK (Complex a)). Ob a0 => Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) a0 (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) %% a0) Source Github #

(Num a, IsNat n) => Frobenius ('M n :: MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

(Num a, IsNat n) => CocommutativeComonoid ('M n :: MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

(Num a, IsNat n) => CommutativeMonoid ('M n :: MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

(Num a, IsNat n) => Comonoid ('M n :: MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

counit :: ('M n :: MatK a) ~> (Unit :: MatK a) Source Github #

comult :: ('M n :: MatK a) ~> (('M n :: MatK a) ** ('M n :: MatK a)) Source Github #

(Num a, IsNat n) => Monoid ('M n :: MatK a) Source Github #

Monoids are associative, unital algebras.

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

mempty :: (Unit :: MatK a) ~> ('M n :: MatK a) Source Github #

mappend :: (('M n :: MatK a) ** ('M n :: MatK a)) ~> ('M n :: MatK a) Source Github #

RealFloat a => Involution (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) :: MatK (Complex a) -> MatK (Complex a) -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

involuted :: forall (a0 :: MatK (Complex a)) (a' :: MatK (Complex a)). (Ob a0, Ob a') => PIso a0 a' (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) % (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) % a0)) (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) % (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) % a')) Source Github #

type Unit Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

type Unit = 'M ('S 'Z) :: MatK a

type InitialObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

type InitialObject = 'M 'Z :: MatK a

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

type (~>) = Mat :: MatK a -> MatK a -> Type

type TerminalObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

type TerminalObject = 'M 'Z :: MatK a

type Dual (n :: MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

type Dual (n :: MatK a) = n

type Ob (n :: MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

type Ob (n :: MatK a) = (Is ('M :: Nat -> MatK a) n, IsNat (UN ('M :: Nat -> MatK a) n))

type (x :: MatK a) ~~> (y :: MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

type (x :: MatK a) ~~> (y :: MatK a) = ExpSA x y

type (App :: MatK a +-> Type) @ ('M n :: MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

type (App :: MatK a +-> Type) @ ('M n :: MatK a) = Vec n a

type (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) @ (n :: MatK (Complex a)) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

type (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) @ (n :: MatK (Complex a)) = n

type (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) :: MatK (Complex a) -> MatK (Complex a) -> Type) %% (n :: MatK (Complex a)) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

type (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) :: MatK (Complex a) -> MatK (Complex a) -> Type) %% (n :: MatK (Complex a)) = n

type ('M x :: MatK a) ** ('M y :: MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

type ('M x :: MatK a) ** ('M y :: MatK a) = 'M (y * x) :: MatK a

type ('M x :: MatK a) || ('M y :: MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

type ('M x :: MatK a) || ('M y :: MatK a) = 'M (x + y) :: MatK a

type ('M x :: MatK a) && ('M y :: MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

type ('M x :: MatK a) && ('M y :: MatK a) = 'M (x + y) :: MatK a

data Mat (b :: MatK a) (c :: MatK a) where Source Github #

Constructors

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

Instances

Instances details

RealFloat a => DaggerProfunctor (Mat :: MatK (Complex a) -> MatK (Complex a) -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Mat Methods dagger :: forall (a0 :: MatK (Complex a)) (b :: MatK (Complex a)). Mat a0 b -> Mat b a0 Source Github #
Num a => DaggerProfunctor (Mat :: MatK a -> MatK a -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Mat Methods dagger :: forall (a0 :: MatK a) (b :: MatK a). Mat a0 b -> Mat b a0 Source Github #
Num a => Promonad (Mat :: MatK a -> MatK a -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Mat Methods id :: forall (a0 :: MatK a). Ob a0 => Mat a0 a0 Source Github # (.) :: forall (b :: MatK a) (c :: MatK a) (a0 :: MatK a). Mat b c -> Mat a0 b -> Mat a0 c Source Github #
(Num a, MonoidalAction t) => Costrong (t :: (MatK a, MatK a) +-> MatK a) (Mat :: MatK a -> MatK a -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Mat Methods coact :: forall (a0 :: MatK a) (x :: MatK a) (y :: MatK a). (Ob a0, Ob x, Ob y) => Mat (Act t a0 x) (Act t a0 y) -> Mat x y Source Github #
Num a => MonoidalProfunctor (Mat :: MatK a -> MatK a -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Mat Methods one :: Mat (Unit :: MatK a) (Unit :: MatK a) Source Github # () :: forall (x1 :: MatK a) (x2 :: MatK a) (y1 :: MatK a) (y2 :: MatK a). Mat x1 x2 -> Mat y1 y2 -> Mat (x1 y1) (x2 ** y2) Source Github #
Num a => Profunctor (Mat :: MatK a -> MatK a -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Mat Methods dimap :: forall (c :: MatK a) (a0 :: MatK a) (b :: MatK a) (d :: MatK a). (c ~> a0) -> (b ~> d) -> Mat a0 b -> Mat c d Source Github # lmap :: forall (c :: MatK a) (a0 :: MatK a) (b :: MatK a). (c ~> a0) -> Mat a0 b -> Mat c b Source Github # rmap :: forall (b :: MatK a) (d :: MatK a) (a0 :: MatK a). (b ~> d) -> Mat a0 b -> Mat a0 d Source Github # (\\) :: forall (a0 :: MatK a) (b :: MatK a) r. ((Ob a0, Ob b) => r) -> Mat a0 b -> r Source Github #

app :: forall a (m :: Nat) (n :: Nat). (Num a, Applicative (Vec m)) => Vec n (Vec m a) -> Vec m a -> Vec n a Source Github #

arr :: forall (n :: Nat) (m :: Nat) a. Num a => FinSet ('FS m) ('FS n) -> Mat ('M n :: MatK a) ('M m :: MatK a) Source Github #

arr' :: forall (n :: Nat) (m :: Nat) a. Num a => FinSet ('FS m) ('FS n) -> Mat ('M m :: MatK a) ('M n :: MatK a) Source Github #

oneV :: forall a (n :: Nat). (Num a, IsNat n) => Fin n -> Vec n a Source Github #

zero :: forall a (n :: Nat). (Num a, IsNat n) => Vec n a Source Github #

withIsNat :: forall (n :: Nat) r. SNatI n => (IsNat n => r) -> r Source Github #

class (SNatI n, Applicative (Vec n), (n + 'Z) ~ n, (n * 'Z) ~ 'Z, (n * 'S 'Z) ~ n) => IsNat (n :: Nat) where Source Github #

Methods

matId :: Num a => Vec n (Vec n a) Source Github #

withPlusNat :: forall (m :: Nat) r. IsNat m => (IsNat (n + m) => r) -> r Source Github #

withMultNat :: forall (m :: Nat) r. IsNat m => (IsNat (n * m) => r) -> r Source Github #

withPlusSucc :: forall (m :: Nat) r. IsNat m => ((n + 'S m) ~ 'S (n + m) => r) -> r Source Github #

withMultSucc :: forall (m :: Nat) r. IsNat m => ((n * 'S m) ~ (n + (n * m)) => r) -> r Source Github #

withPlusSym :: forall (m :: Nat) r. IsNat m => ((n + m) ~ (m + n) => r) -> r Source Github #

withMultSym :: forall (m :: Nat) r. IsNat m => ((n * m) ~ (m * n) => r) -> r Source Github #

withAssocPlus :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => (((n + m) + o) ~ (n + (m + o)) => r) -> r Source Github #

withAssocMult :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => (((n * m) * o) ~ (n * (m * o)) => r) -> r Source Github #

withDist :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => (((n + m) * o) ~ ((n * o) + (m * o)) => r) -> r Source Github #

Instances

Instances details

IsNat 'Z Source Github #
Instance details Defined in Proarrow.Category.Instance.Mat Methods matId :: Num a => Vec 'Z (Vec 'Z a) Source Github # withPlusNat :: forall (m :: Nat) r. IsNat m => (IsNat ('Z + m) => r) -> r Source Github # withMultNat :: forall (m :: Nat) r. IsNat m => (IsNat ('Z * m) => r) -> r Source Github # withPlusSucc :: forall (m :: Nat) r. IsNat m => (('Z + 'S m) ~ 'S ('Z + m) => r) -> r Source Github # withMultSucc :: forall (m :: Nat) r. IsNat m => (('Z * 'S m) ~ ('Z + ('Z * m)) => r) -> r Source Github # withPlusSym :: forall (m :: Nat) r. IsNat m => (('Z + m) ~ (m + 'Z) => r) -> r Source Github # withMultSym :: forall (m :: Nat) r. IsNat m => (('Z * m) ~ (m * 'Z) => r) -> r Source Github # withAssocPlus :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => ((('Z + m) + o) ~ ('Z + (m + o)) => r) -> r Source Github # withAssocMult :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => ((('Z * m) * o) ~ ('Z * (m * o)) => r) -> r Source Github # withDist :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => ((('Z + m) * o) ~ (('Z * o) + (m * o)) => r) -> r Source Github #
IsNat n => IsNat ('S n) Source Github #
Instance details Defined in Proarrow.Category.Instance.Mat Methods matId :: Num a => Vec ('S n) (Vec ('S n) a) Source Github # withPlusNat :: forall (m :: Nat) r. IsNat m => (IsNat ('S n + m) => r) -> r Source Github # withMultNat :: forall (m :: Nat) r. IsNat m => (IsNat ('S n * m) => r) -> r Source Github # withPlusSucc :: forall (m :: Nat) r. IsNat m => (('S n + 'S m) ~ 'S ('S n + m) => r) -> r Source Github # withMultSucc :: forall (m :: Nat) r. IsNat m => (('S n * 'S m) ~ ('S n + ('S n * m)) => r) -> r Source Github # withPlusSym :: forall (m :: Nat) r. IsNat m => (('S n + m) ~ (m + 'S n) => r) -> r Source Github # withMultSym :: forall (m :: Nat) r. IsNat m => (('S n * m) ~ (m * 'S n) => r) -> r Source Github # withAssocPlus :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => ((('S n + m) + o) ~ ('S n + (m + o)) => r) -> r Source Github # withAssocMult :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => ((('S n * m) * o) ~ ('S n * (m * o)) => r) -> r Source Github # withDist :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => ((('S n + m) * o) ~ (('S n * o) + (m * o)) => r) -> r Source Github #

transpose :: forall a (n :: MatK a) (m :: MatK a). Mat n m -> Mat m n Source Github #

Plain transpose, with no conjugation.

Three operations on a matrix are easy to confuse, and at MatK (Complex a) they differ: this one, the entrywise Conjugate functor, and dagger, which is their composite (the conjugate-transpose). Composition and the compact-closed structure are bilinear and must not conjugate, so they are written in terms of transpose rather than dagger. At a real element type dagger is transpose, so the distinction is easy to lose.

at :: forall (m :: Nat) a. Vec m a -> Int -> a Source Github #

Reads the entry of a row at a runtime column index.

rref :: forall a (m :: Nat). (Fractional a, Eq a) => Int -> [Vec m a] -> ([Int], [Vec m a]) Source Github #

Row-reduces the given matrix, given as a list of rows of the given width, to reduced row echelon form, returning the ascending pivot column indices together with the reduced rows.

data family Conjugate :: MatK (Complex a) +-> MatK (Complex a) Source Github #

Instances

Instances details

RealFloat a => FunctorForRep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) Source Github #
Instance details Defined in Proarrow.Category.Instance.Mat Methods fmap :: forall (a0 :: MatK (Complex a)) (b :: MatK (Complex a)). (a0 ~> b) -> ((Conjugate :: MatK (Complex a) +-> MatK (Complex a)) @ a0) ~> ((Conjugate :: MatK (Complex a) +-> MatK (Complex a)) @ b) Source Github #
RealFloat a => MonoidalProfunctor (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) :: MatK (Complex a) -> MatK (Complex a) -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Mat Methods one :: Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) (Unit :: MatK (Complex a)) (Unit :: MatK (Complex a)) Source Github # () :: forall (x1 :: MatK (Complex a)) (x2 :: MatK (Complex a)) (y1 :: MatK (Complex a)) (y2 :: MatK (Complex a)). Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) x1 x2 -> Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) y1 y2 -> Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) (x1 y1) (x2 ** y2) Source Github #
RealFloat a => Corepresentable (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) :: MatK (Complex a) -> MatK (Complex a) -> Type) Source Github #	Conjugation is a self-adjoint functor
Instance details Defined in Proarrow.Category.Instance.Mat Methods coindex :: forall (a0 :: MatK (Complex a)) (b :: MatK (Complex a)). Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) a0 b -> (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) %% a0) ~> b Source Github # cotabulate :: forall (a0 :: MatK (Complex a)) (b :: MatK (Complex a)). Ob a0 => ((Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) %% a0) ~> b) -> Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) a0 b Source Github # corepMap :: forall (a0 :: MatK (Complex a)) (b :: MatK (Complex a)). (a0 ~> b) -> (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) %% a0) ~> (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) %% b) Source Github # corepUniv :: forall (a0 :: MatK (Complex a)). Ob a0 => Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) a0 (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) %% a0) Source Github #
RealFloat a => Involution (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) :: MatK (Complex a) -> MatK (Complex a) -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Mat Methods involuted :: forall (a0 :: MatK (Complex a)) (a' :: MatK (Complex a)). (Ob a0, Ob a') => PIso a0 a' (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) % (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) % a0)) (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) % (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) % a')) Source Github #
type (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) @ (n :: MatK (Complex a)) Source Github #
Instance details Defined in Proarrow.Category.Instance.Mat type (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) @ (n :: MatK (Complex a)) = n
type (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) :: MatK (Complex a) -> MatK (Complex a) -> Type) %% (n :: MatK (Complex a)) Source Github #
Instance details Defined in Proarrow.Category.Instance.Mat type (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) :: MatK (Complex a) -> MatK (Complex a) -> Type) %% (n :: MatK (Complex a)) = n

data family App :: MatK a +-> Type Source Github #

Instances

Instances details

Num a => FunctorForRep (App :: MatK a +-> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Mat Methods fmap :: forall (a0 :: MatK a) (b :: MatK a). (a0 ~> b) -> ((App :: MatK a +-> Type) @ a0) ~> ((App :: MatK a +-> Type) @ b) Source Github #
Num a => MonoidalProfunctor (Rep (App :: MatK a +-> Type) :: Type -> MatK a -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Mat Methods one :: Rep (App :: MatK a +-> Type) (Unit :: Type) (Unit :: MatK a) Source Github # () :: forall x1 (x2 :: MatK a) y1 (y2 :: MatK a). Rep (App :: MatK a +-> Type) x1 x2 -> Rep (App :: MatK a +-> Type) y1 y2 -> Rep (App :: MatK a +-> Type) (x1 y1) (x2 ** y2) Source Github #
type (App :: MatK a +-> Type) @ ('M n :: MatK a) Source Github #
Instance details Defined in Proarrow.Category.Instance.Mat type (App :: MatK a +-> Type) @ ('M n :: MatK a) = Vec n a