Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Mat

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 => 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 #

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

distR0 :: 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 => 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 => 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 #

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 #

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 #

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

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

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 #

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 => 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 #

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

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

par :: 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 => MonoidalAction (MatK a) (MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

withObAct :: forall (a0 :: MatK a) (x :: MatK a) r. (Ob a0, Ob x) => (Ob (Act a0 x) => r) -> r Source Github #

unitor :: forall (x :: MatK a). Ob x => Act (Unit :: MatK a) x ~> x Source Github #

unitorInv :: forall (x :: MatK a). Ob x => x ~> Act (Unit :: MatK a) x Source Github #

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

multiplicatorInv :: forall (a0 :: MatK a) (b :: MatK a) (x :: MatK a). (Ob a0, Ob b, Ob x) => Act a0 (Act b x) ~> Act (a0 ** b) x 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 => MonoidalProfunctor (Mat :: MatK a -> MatK a -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

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

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) 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 #

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

Num a => Costrong (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 a0 x) (Act a0 y) -> Mat x y Source Github #

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

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

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

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

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

spider :: forall (n0 :: Nat) (m :: Nat). (SNatI n0, SNatI m) => NFold n0 ('M n :: MatK a) ~> NFold m ('M n :: MatK a) Source Github #

(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 #

type UN ('M :: Nat -> MatK a) ('M n :: MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

type UN ('M :: Nat -> MatK a) ('M n :: MatK a) = n

type Unit Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

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

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

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

type InitialObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

type InitialObject = 'M 'Z :: MatK a

type TerminalObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

type TerminalObject = 'M 'Z :: MatK a

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 Dual (n :: MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

type Dual (n :: 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 Act (p :: MatK a) (x :: MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

type Act (p :: MatK a) (x :: MatK a) = p ** x

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 => MonoidalProfunctor (Mat :: MatK a -> MatK a -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Mat Methods par0 :: Mat (Unit :: MatK a) (Unit :: MatK a) Source Github # 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) 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 # (\\) :: forall (a0 :: MatK a) (b :: MatK a) r. ((Ob a0, Ob b) => r) -> Mat a0 b -> r Source Github #
Num a => Costrong (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 a0 x) (Act a0 y) -> Mat x y Source Github #
Num a => Strong (MatK a) (Mat :: MatK a -> MatK a -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Mat Methods act :: forall (a0 :: MatK a) (b :: MatK a) (x :: MatK a) (y :: MatK a). (a0 ~> b) -> Mat x y -> Mat (Act a0 x) (Act b y) 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 #

one :: 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 #

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 par0 :: Rep (App :: MatK a +-> Type) (Unit :: Type) (Unit :: MatK a) Source Github # par :: 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