Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Instance.Mat

Documentation

data Nat Source Comments #

Constructors

Z
S Nat

Instances

Instances details

type UN ('M :: Nat -> MatK a) ('M n :: MatK a) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat type UN ('M :: Nat -> MatK a) ('M n :: MatK a) = n

type family (a :: Nat) + (b :: Nat) :: Nat where ... Source Comments #

Equations

'Z + b = b
('S a) + b = 'S (a + b)

type family (a :: Nat) * (b :: Nat) :: Nat where ... Source Comments #

Equations

'Z * b = 'Z
('S a) * b = b + (a * b)

data Vec (a :: Nat) b where Source Comments #

Constructors

Nil :: forall b. Vec 'Z b
Cons :: forall b (n :: Nat). b -> Vec n b -> Vec ('S n) b

Instances

Instances details

Applicative (Vec n) => Applicative (Vec ('S n)) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods pure :: a -> Vec ('S n) a Comments # (<>) :: Vec ('S n) (a -> b) -> Vec ('S n) a -> Vec ('S n) b Comments # liftA2 :: (a -> b -> c) -> Vec ('S n) a -> Vec ('S n) b -> Vec ('S n) c Comments # (>) :: Vec ('S n) a -> Vec ('S n) b -> Vec ('S n) b Comments # (<*) :: Vec ('S n) a -> Vec ('S n) b -> Vec ('S n) a Comments #
Applicative (Vec 'Z) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods pure :: a -> Vec 'Z a Comments # (<>) :: Vec 'Z (a -> b) -> Vec 'Z a -> Vec 'Z b Comments # liftA2 :: (a -> b -> c) -> Vec 'Z a -> Vec 'Z b -> Vec 'Z c Comments # (>) :: Vec 'Z a -> Vec 'Z b -> Vec 'Z b Comments # (<*) :: Vec 'Z a -> Vec 'Z b -> Vec 'Z a Comments #
Functor (Vec n) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods fmap :: (a -> b) -> Vec n a -> Vec n b Comments # (<$) :: a -> Vec n b -> Vec n a Comments #
Foldable (Vec n) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods fold :: Monoid m => Vec n m -> m Comments # foldMap :: Monoid m => (a -> m) -> Vec n a -> m Comments # foldMap' :: Monoid m => (a -> m) -> Vec n a -> m Comments # foldr :: (a -> b -> b) -> b -> Vec n a -> b Comments # foldr' :: (a -> b -> b) -> b -> Vec n a -> b Comments # foldl :: (b -> a -> b) -> b -> Vec n a -> b Comments # foldl' :: (b -> a -> b) -> b -> Vec n a -> b Comments # foldr1 :: (a -> a -> a) -> Vec n a -> a Comments # foldl1 :: (a -> a -> a) -> Vec n a -> a Comments # toList :: Vec n a -> [a] Comments # null :: Vec n a -> Bool Comments # length :: Vec n a -> Int Comments # elem :: Eq a => a -> Vec n a -> Bool Comments # maximum :: Ord a => Vec n a -> a Comments # minimum :: Ord a => Vec n a -> a Comments # sum :: Num a => Vec n a -> a Comments # product :: Num a => Vec n a -> a Comments #
Traversable (Vec n) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods traverse :: Applicative f => (a -> f b) -> Vec n a -> f (Vec n b) Comments # sequenceA :: Applicative f => Vec n (f a) -> f (Vec n a) Comments # mapM :: Monad m => (a -> m b) -> Vec n a -> m (Vec n b) Comments # sequence :: Monad m => Vec n (m a) -> m (Vec n a) Comments #

data MatK a Source Comments #

Constructors

M Nat

Instances

Instances details

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

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

Num a => MonoidalAction (MatK a) (MatK a) Source Comments #

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

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

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

multiplicator :: 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 Comments #

multiplicatorInv :: 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 Comments #

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

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

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

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

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

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

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

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

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

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

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

Num a => Costrong (MatK a) (Mat :: MatK a -> MatK a -> Type) Source Comments #

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

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

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

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

Instance details

Defined in Proarrow.Category.Instance.Mat

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

type Unit Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

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

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

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

type InitialObject Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

type InitialObject = 'M 'Z :: MatK a

type TerminalObject Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

type TerminalObject = 'M 'Z :: MatK a

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

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

Instance details

Defined in Proarrow.Category.Instance.Mat

type Dual (n :: MatK a) = n

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

Instance details

Defined in Proarrow.Category.Instance.Mat

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

type Act (p :: MatK a) (x :: MatK a) Source Comments #

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

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

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

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

Constructors

Mat :: forall {a} {b :: MatK a} {c :: MatK a} (m :: Nat) (n :: Nat). (Ob b, Ob c, b ~ ('M m :: MatK a), c ~ ('M n :: MatK a)) => Vec n (Vec m a) -> Mat b c

Instances

Instances details

RealFloat a => DaggerProfunctor (Mat :: MatK (Complex a) -> MatK (Complex a) -> Type) Source Comments #
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 Comments #
Num a => DaggerProfunctor (Mat :: MatK a -> MatK a -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods dagger :: forall (a0 :: MatK a) (b :: MatK a). Mat a0 b -> Mat b a0 Source Comments #
Num a => Promonad (Mat :: MatK a -> MatK a -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods id :: forall (a0 :: MatK a). Ob a0 => Mat a0 a0 Source Comments # (.) :: forall (b :: MatK a) (c :: MatK a) (a0 :: MatK a). Mat b c -> Mat a0 b -> Mat a0 c Source Comments #
Num a => MonoidalProfunctor (Mat :: MatK a -> MatK a -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods par0 :: Mat (Unit :: MatK a) (Unit :: MatK a) Source Comments # 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 Comments #
Num a => Profunctor (Mat :: MatK a -> MatK a -> Type) Source Comments #
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 Comments # (\\) :: forall (a0 :: MatK a) (b :: MatK a) r. ((Ob a0, Ob b) => r) -> Mat a0 b -> r Source Comments #
Num a => Costrong (MatK a) (Mat :: MatK a -> MatK a -> Type) Source Comments #
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 Comments #
Num a => Strong (MatK a) (Mat :: MatK a -> MatK a -> Type) Source Comments #
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 Comments #

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

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

Methods

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

zero :: Num a => Vec n a Source Comments #

append :: forall a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a Source Comments #

split :: forall (m :: Nat) a. Vec (n + m) a -> (Vec n a, Vec m a) Source Comments #

concatMap :: forall (m :: Nat) a b. IsNat m => (a -> Vec m b) -> Vec n a -> Vec (n * m) b Source Comments #

unConcatMap :: forall (m :: Nat) b a. IsNat m => (Vec m b -> a) -> Vec (n * m) b -> Vec n a Source Comments #

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

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

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

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

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

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

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

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

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

Instances

Instances details

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

withNat :: forall (n :: Nat) a r. Vec n a -> (IsNat n => r) -> r Source Comments #

mat :: forall {a1} (m :: Nat) (n :: Nat) a2. Ob ('M m :: MatK a1) => Vec n (Vec m a2) -> Mat ('M m :: MatK a2) ('M n :: MatK a2) Source Comments #