Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.FinSet

Description

The skeleton of the category of finite sets: objects are natural numbers (FS n) and a morphism FS n ~> FS m is a function stored as its table, a length-n vector of indices below m. Distributive and cartesian closed (exponentials via the Exp type family), with all structure computed concretely.

Synopsis

data FINSET = FS Nat
data FinSet (a :: FINSET) (b :: FINSET) where
- FinSet :: forall (n :: Nat) (m :: Nat). (SNatI n, SNatI m) => {..} -> FinSet ('FS n) ('FS m)
mult :: forall (n :: Nat) (m :: Nat). (SNatI n, SNatI m) => Fin n -> Fin m -> Fin (Mult n m)
unmult :: forall (n :: Nat) (m :: Nat). (SNatI n, SNatI m) => Fin (Mult n m) -> (Fin n, Fin m)
type family Exp (a :: Nat) (b :: Nat) :: Nat where ...
exp :: forall (n :: Nat) (m :: Nat). (SNatI n, SNatI m) => Vec n (Fin m) -> Fin (Exp m n)
unExp :: forall (n :: Nat) (m :: Nat). (SNatI n, SNatI m) => Fin (Exp m n) -> Vec n (Fin m)
findIso :: forall (n :: Nat). SNatI n => [(Fin n, Fin n)] -> Maybe (Iso' ('FS n) ('FS n))
findBijection :: forall (n :: Nat). SNatI n => [(Fin n, Fin n)] -> Maybe (Vec n (Fin n))
findIndex :: forall a (n :: Nat). (a -> Bool) -> Vec n a -> Fin n

Documentation

data FINSET Source Github #

Constructors

FS Nat

Instances

Instances details

Monoidal FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type Unit
Instance details Defined in Proarrow.Category.Instance.FinSet type Unit = 'FS Nat1
type (a :: FINSET) ** (b :: FINSET)
Instance details Defined in Proarrow.Category.Instance.FinSet type (a :: FINSET) ** (b :: FINSET) = a && b

Methods

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

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

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

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

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

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

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

SymMonoidal FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

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

Closed FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type ('FS a :: FINSET) ~~> ('FS b :: FINSET)
Instance details Defined in Proarrow.Category.Instance.FinSet type ('FS a :: FINSET) ~~> ('FS b :: FINSET) = 'FS (Exp b a)

Methods

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

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

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

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

CopyDiscard FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

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

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

Distributive FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

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

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

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

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

ElementaryTopos FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

HasEpiMonoFactorization FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

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

HasSubobjectClassifier FINSET Source Github #

>>> import Proarrow.Colimit.Pushout (isEpi)
>>> import Data.Fin
>>> import Data.Type.Nat
>>> let f :: FinSet (FS Nat3) (FS Nat3) = FinSet $ fin2 ::: fin0 ::: fin1 ::: VNil
>>> (pushout f f \(FinSet g1) (FinSet g2) -> P.show (g1, g2)) :: P.String
"(0 ::: 1 ::: 2 ::: VNil,0 ::: 1 ::: 2 ::: VNil)"
>>> isEpi f
True
>>> import Proarrow.Limit.Pullback (isMono)
>>> (pullback f f \(FinSet l) (FinSet r) -> P.show (l, r)) :: P.String
"(0 ::: 1 ::: 2 ::: VNil,0 ::: 1 ::: 2 ::: VNil)"
>>> isMono f
True
>>> import Proarrow.Category.Topos (classifyImage, classifyKernelPair, and, or, implies, false)
>>> (classifyImage f, classifyKernelPair f)
(FinSet {unFinSet = 1 ::: 1 ::: 1 ::: VNil},FinSet {unFinSet = 1 ::: 0 ::: 0 ::: 0 ::: 1 ::: 0 ::: 0 ::: 0 ::: 1 ::: VNil})
>>> [and, or, implies] :: [FinSet (FS Nat4) (FS Nat2)]
[FinSet {unFinSet = 0 ::: 0 ::: 0 ::: 1 ::: VNil},FinSet {unFinSet = 0 ::: 1 ::: 1 ::: 1 ::: VNil},FinSet {unFinSet = 1 ::: 1 ::: 0 ::: 1 ::: VNil}]
>>> false :: FinSet (FS Nat1) (FS Nat2)
FinSet {unFinSet = 0 ::: VNil}

Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type Omega
Instance details Defined in Proarrow.Category.Instance.FinSet type Omega = 'FS Nat2

Methods

true :: (TerminalObject :: FINSET) ~> (Omega :: FINSET) Source Github #

classifyGraph :: forall (a :: FINSET) (b :: FINSET). (a ~> b) -> (a && b) ~> (Omega :: FINSET) Source Github #

HasBinaryCoproducts FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type ('FS a :: FINSET) \|\| ('FS b :: FINSET)
Instance details Defined in Proarrow.Category.Instance.FinSet type ('FS a :: FINSET) \|\| ('FS b :: FINSET) = 'FS (Plus a b)

Methods

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

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

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

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

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

HasCoequalizers FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

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

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

HasInitialObject FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.FinSet type InitialObject = 'FS Nat0

Methods

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

HasPushouts FINSET Source Github #

>>> import Data.Fin
>>> import Data.Type.Nat
>>> let l :: FinSet (FS Nat4) (FS Nat3) = FinSet $ fin0 ::: fin0 ::: fin1 ::: fin2 ::: VNil
>>> let r :: FinSet (FS Nat4) (FS Nat5) = FinSet $ fin0 ::: fin2 ::: fin4 ::: fin4 ::: VNil
>>> (pushout l r \(FinSet l') (FinSet r') -> P.show (l', r')) :: P.String
"(1 ::: 3 ::: 3 ::: VNil,1 ::: 0 ::: 1 ::: 2 ::: 3 ::: VNil)"

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

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

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

CategoryOf FINSET Source Github #

The skeleton of the category of finite sets: objects are natural numbers and an arrow FS n ~> FS m is a function given by its table.

Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.FinSet type (~>) = FinSet
type Ob (a :: FINSET)
Instance details Defined in Proarrow.Category.Instance.FinSet type Ob (a :: FINSET) = (Is 'FS a, SNatI (UN 'FS a))

HasBinaryProducts FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type ('FS a :: FINSET) && ('FS b :: FINSET)
Instance details Defined in Proarrow.Category.Instance.FinSet type ('FS a :: FINSET) && ('FS b :: FINSET) = 'FS (Mult a b)

Methods

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

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

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

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

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

HasEqualizers FINSET Source Github #

>>> import Data.Fin
>>> import Data.Type.Nat
>>> import Data.Vec.Lazy
>>> let f :: FinSet (FS Nat4) (FS Nat3) = FinSet $ fin0 ::: fin1 ::: fin1 ::: fin0 ::: VNil
>>> let g :: FinSet (FS Nat4) (FS Nat3) = FinSet $ fin2 ::: fin0 ::: fin1 ::: fin0 ::: VNil
>>> let h :: FinSet (FS Nat3) (FS Nat4) = FinSet $ fin3 ::: fin2 ::: fin3 ::: VNil
>>> (equalize f g \incl -> let p = factorEqualizer incl h in P.show (incl, p, incl . p)) :: P.String
"(FinSet {unFinSet = 2 ::: 3 ::: VNil},FinSet {unFinSet = 1 ::: 0 ::: 1 ::: VNil},FinSet {unFinSet = 3 ::: 2 ::: 3 ::: VNil})"

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

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

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

HasPullbacks FINSET Source Github #

>>> import Data.Fin
>>> import Data.Type.Nat
>>> import Data.Vec.Lazy
>>> let f :: FinSet (FS Nat6) (FS Nat3) = FinSet $ fin0 ::: fin1 ::: fin0 ::: fin0 ::: fin2 ::: fin1 ::: VNil
>>> let g :: FinSet (FS Nat4) (FS Nat3) = FinSet $ fin2 ::: fin0 ::: fin1 ::: fin0 ::: VNil
>>> (pullback f g \(FinSet l) (FinSet r) -> P.show (l, r)) :: P.String
"(0 ::: 0 ::: 1 ::: 2 ::: 2 ::: 3 ::: 3 ::: 4 ::: 5 ::: VNil,1 ::: 3 ::: 2 ::: 1 ::: 3 ::: 1 ::: 3 ::: 0 ::: 2 ::: VNil)"

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

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

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

HasTerminalObject FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.FinSet type TerminalObject = 'FS Nat1

Methods

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

Promonad FinSet Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

id :: forall (a :: FINSET). Ob a => FinSet a a Source Github #

(.) :: forall (b :: FINSET) (c :: FINSET) (a :: FINSET). FinSet b c -> FinSet a b -> FinSet a c Source Github #

InternalIn BOOL FINSET Source Github #

>>> import Data.Fin
>>> import Data.Type.Nat
>>> import Data.Vec.Lazy
>>> import Proarrow.Limit.Pullback
>>> import Prelude qualified as P
>>> (pullback (source @BOOL @FINSET) (target @BOOL @FINSET) \(FinSet l) (FinSet r) -> P.show (l, r)) :: P.String
"(0 ::: 1 ::: 2 ::: 2 ::: VNil,0 ::: 0 ::: 1 ::: 2 ::: VNil)"

Instance details

Defined in Proarrow.Category.Internal

Associated Types

type C0 BOOL
Instance details Defined in Proarrow.Category.Internal type C0 BOOL = 'FS Nat2
type C1 BOOL
Instance details Defined in Proarrow.Category.Internal type C1 BOOL = 'FS Nat3

Methods

source :: (C1 BOOL :: FINSET) ~> (C0 BOOL :: FINSET) Source Github #

target :: (C1 BOOL :: FINSET) ~> (C0 BOOL :: FINSET) Source Github #

identity :: (C0 BOOL :: FINSET) ~> (C1 BOOL :: FINSET) Source Github #

compose :: Cosink '[C1 BOOL :: FINSET, C1 BOOL :: FINSET, C1 BOOL :: FINSET] Source Github #

MonoidalProfunctor FinSet Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

one :: FinSet (Unit :: FINSET) (Unit :: FINSET) Source Github #

(**) :: forall (x1 :: FINSET) (x2 :: FINSET) (y1 :: FINSET) (y2 :: FINSET). FinSet x1 x2 -> FinSet y1 y2 -> FinSet (x1 ** y1) (x2 ** y2) Source Github #

Profunctor FinSet Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

dimap :: forall (c :: FINSET) (a :: FINSET) (b :: FINSET) (d :: FINSET). (c ~> a) -> (b ~> d) -> FinSet a b -> FinSet c d Source Github #

lmap :: forall (c :: FINSET) (a :: FINSET) (b :: FINSET). (c ~> a) -> FinSet a b -> FinSet c b Source Github #

rmap :: forall (b :: FINSET) (d :: FINSET) (a :: FINSET). (b ~> d) -> FinSet a b -> FinSet a d Source Github #

(\\) :: forall (a :: FINSET) (b :: FINSET) r. ((Ob a, Ob b) => r) -> FinSet a b -> r Source Github #

FunctorForRep Fun Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinRel

Associated Types

type Fun @ ('FS a :: FINSET)
Instance details Defined in Proarrow.Category.Instance.FinRel type Fun @ ('FS a :: FINSET) = 'FR a

Methods

fmap :: forall (a :: FINSET) (b :: FINSET). (a ~> b) -> (Fun @ a) ~> (Fun @ b) Source Github #

MonoidalProfunctor (Rep Fun) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinRel

Methods

one :: Rep Fun (Unit :: FINREL) (Unit :: FINSET) Source Github #

(**) :: forall (x1 :: FINREL) (x2 :: FINSET) (y1 :: FINREL) (y2 :: FINSET). Rep Fun x1 x2 -> Rep Fun y1 y2 -> Rep Fun (x1 ** y1) (x2 ** y2) Source Github #

SNatI a => CocommutativeComonoid ('FS a :: FINSET) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

SNatI a => Comonoid ('FS a :: FINSET) Source Github #

>>> import Data.Type.Nat
>>> comult @(FS Nat4)
FinSet {unFinSet = 0 ::: 5 ::: 10 ::: 15 ::: VNil}

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

counit :: 'FS a ~> (Unit :: FINSET) Source Github #

comult :: 'FS a ~> ('FS a ** 'FS a) Source Github #

Monoid ('FS Nat1) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

mempty :: (Unit :: FINSET) ~> 'FS Nat1 Source Github #

mappend :: ('FS Nat1 ** 'FS Nat1) ~> 'FS Nat1 Source Github #

MonoidalProfunctor (Coprod (Rep Fun)) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinRel

Methods

one :: Coprod (Rep Fun) (Unit :: COPROD FINREL) (Unit :: COPROD FINSET) Source Github #

(**) :: forall (x1 :: COPROD FINREL) (x2 :: COPROD FINSET) (y1 :: COPROD FINREL) (y2 :: COPROD FINSET). Coprod (Rep Fun) x1 x2 -> Coprod (Rep Fun) y1 y2 -> Coprod (Rep Fun) (x1 ** y1) (x2 ** y2) Source Github #

type Unit Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

type Unit = 'FS Nat1

type Omega Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

type Omega = 'FS Nat2

type InitialObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

type InitialObject = 'FS Nat0

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

type (~>) = FinSet

type TerminalObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

type TerminalObject = 'FS Nat1

type Ob (a :: FINSET) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

type Ob (a :: FINSET) = (Is 'FS a, SNatI (UN 'FS a))

type C0 BOOL Source Github #

Instance details

Defined in Proarrow.Category.Internal

type C0 BOOL = 'FS Nat2

type C1 BOOL Source Github #

Instance details

Defined in Proarrow.Category.Internal

type C1 BOOL = 'FS Nat3

type (a :: FINSET) ** (b :: FINSET) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

type (a :: FINSET) ** (b :: FINSET) = a && b

type Fun @ ('FS a :: FINSET) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinRel

type Fun @ ('FS a :: FINSET) = 'FR a

type ('FS a :: FINSET) ~~> ('FS b :: FINSET) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

type ('FS a :: FINSET) ~~> ('FS b :: FINSET) = 'FS (Exp b a)

type ('FS a :: FINSET) || ('FS b :: FINSET) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

type ('FS a :: FINSET) || ('FS b :: FINSET) = 'FS (Plus a b)

type ('FS a :: FINSET) && ('FS b :: FINSET) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

type ('FS a :: FINSET) && ('FS b :: FINSET) = 'FS (Mult a b)

data FinSet (a :: FINSET) (b :: FINSET) where Source Github #

Constructors

FinSet
Fields :: forall (n :: Nat) (m :: Nat). (SNatI n, SNatI m) => { unFinSet :: Vec n (Fin m) } -> FinSet ('FS n) ('FS m)

Instances

Instances details

Promonad FinSet Source Github #
Instance details Defined in Proarrow.Category.Instance.FinSet Methods id :: forall (a :: FINSET). Ob a => FinSet a a Source Github # (.) :: forall (b :: FINSET) (c :: FINSET) (a :: FINSET). FinSet b c -> FinSet a b -> FinSet a c Source Github #
MonoidalProfunctor FinSet Source Github #
Instance details Defined in Proarrow.Category.Instance.FinSet Methods one :: FinSet (Unit :: FINSET) (Unit :: FINSET) Source Github # () :: forall (x1 :: FINSET) (x2 :: FINSET) (y1 :: FINSET) (y2 :: FINSET). FinSet x1 x2 -> FinSet y1 y2 -> FinSet (x1 y1) (x2 ** y2) Source Github #
Profunctor FinSet Source Github #
Instance details Defined in Proarrow.Category.Instance.FinSet Methods dimap :: forall (c :: FINSET) (a :: FINSET) (b :: FINSET) (d :: FINSET). (c ~> a) -> (b ~> d) -> FinSet a b -> FinSet c d Source Github # lmap :: forall (c :: FINSET) (a :: FINSET) (b :: FINSET). (c ~> a) -> FinSet a b -> FinSet c b Source Github # rmap :: forall (b :: FINSET) (d :: FINSET) (a :: FINSET). (b ~> d) -> FinSet a b -> FinSet a d Source Github # (\\) :: forall (a :: FINSET) (b :: FINSET) r. ((Ob a, Ob b) => r) -> FinSet a b -> r Source Github #
Show (FinSet a b) Source Github #
Instance details Defined in Proarrow.Category.Instance.FinSet Methods showsPrec :: Int -> FinSet a b -> ShowS Github # show :: FinSet a b -> String Github # showList :: [FinSet a b] -> ShowS Github #
Eq (FinSet a b) Source Github #
Instance details Defined in Proarrow.Category.Instance.FinSet Methods (==) :: FinSet a b -> FinSet a b -> Bool Github # (/=) :: FinSet a b -> FinSet a b -> Bool Github #

mult :: forall (n :: Nat) (m :: Nat). (SNatI n, SNatI m) => Fin n -> Fin m -> Fin (Mult n m) Source Github #

>>> import Data.Type.Nat
>>> import Data.Fin
>>> mult @Nat5 @Nat4 fin4 fin2 -- 4*4+2
18
>>> mult @Nat4 @Nat5 fin2 fin4 -- 5*2+4
14

unmult :: forall (n :: Nat) (m :: Nat). (SNatI n, SNatI m) => Fin (Mult n m) -> (Fin n, Fin m) Source Github #

type family Exp (a :: Nat) (b :: Nat) :: Nat where ... Source Github #

Equations

Exp a 'Z = 'S 'Z
Exp a ('S n) = Mult a (Exp a n)

exp :: forall (n :: Nat) (m :: Nat). (SNatI n, SNatI m) => Vec n (Fin m) -> Fin (Exp m n) Source Github #

>>> import Data.Type.Nat
>>> import Data.Fin
>>> exp @_ @Nat2 (fin1 ::: fin0 ::: fin1 ::: fin1 ::: VNil)
11

unExp :: forall (n :: Nat) (m :: Nat). (SNatI n, SNatI m) => Fin (Exp m n) -> Vec n (Fin m) Source Github #

>>> import Data.Type.Nat
>>> import Data.Fin
>>> unExp @Nat3 @Nat2 fin6
1 ::: 1 ::: 0 ::: VNil

findIso :: forall (n :: Nat). SNatI n => [(Fin n, Fin n)] -> Maybe (Iso' ('FS n) ('FS n)) Source Github #

Finds an isomorphism between 'FS n' and itself that's consistent with the given (source, target) pairs, if one exists.

findBijection :: forall (n :: Nat). SNatI n => [(Fin n, Fin n)] -> Maybe (Vec n (Fin n)) Source Github #

Extends the given (source, target) pairs to a full bijection on Fin n, if they're consistent with being a partial injection (checked in both directions as they're added, so two different sources claiming the same target is rejected just as readily as one source getting conflicting targets). Unconstrained sources are matched up with whatever targets are left over, in order.

findIndex :: forall a (n :: Nat). (a -> Bool) -> Vec n a -> Fin n Source Github #