proarrow
Safe HaskellNone
LanguageGHC2024

Proarrow.Category.Instance.FinHask

Documentation

newtype Fin (n :: Nat) Source Github #

Constructors

Fin 

Fields

Instances

Instances details
Num (Fin n) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

(+) :: Fin n -> Fin n -> Fin n Github #

(-) :: Fin n -> Fin n -> Fin n Github #

(*) :: Fin n -> Fin n -> Fin n Github #

negate :: Fin n -> Fin n Github #

abs :: Fin n -> Fin n Github #

signum :: Fin n -> Fin n Github #

fromInteger :: Integer -> Fin n Github #

Show (Fin n) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

showsPrec :: Int -> Fin n -> ShowS Github #

show :: Fin n -> String Github #

showList :: [Fin n] -> ShowS Github #

Eq (Fin n) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

(==) :: Fin n -> Fin n -> Bool Github #

(/=) :: Fin n -> Fin n -> Bool Github #

Ord (Fin n) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

compare :: Fin n -> Fin n -> Ordering Github #

(<) :: Fin n -> Fin n -> Bool Github #

(<=) :: Fin n -> Fin n -> Bool Github #

(>) :: Fin n -> Fin n -> Bool Github #

(>=) :: Fin n -> Fin n -> Bool Github #

max :: Fin n -> Fin n -> Fin n Github #

min :: Fin n -> Fin n -> Fin n Github #

KnownNat n => Finite (Fin n) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

KnownNat n => Universe (Fin n) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

universe :: [Fin n] Source Github #

data FINHASK Source Github #

Constructors

FH Type 

Instances

Instances details
Monoidal FINHASK Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Associated Types

type Unit 
Instance details

Defined in Proarrow.Category.Instance.FinHask

type (a :: FINHASK) ** (b :: FINHASK) 
Instance details

Defined in Proarrow.Category.Instance.FinHask

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

Methods

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

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

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

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

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

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

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

SymMonoidal FINHASK Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

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

Closed FINHASK Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Associated Types

type (a :: FINHASK) ~~> (b :: FINHASK) 
Instance details

Defined in Proarrow.Category.Instance.FinHask

type (a :: FINHASK) ~~> (b :: FINHASK) = 'FH (FinHask a b)

Methods

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

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

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

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

CopyDiscard FINHASK Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

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

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

Distributive FINHASK Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

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

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

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

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

ElementaryTopos FINHASK Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

HasEpiMonoFactorization FINHASK Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

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

HasSubobjectClassifier FINHASK Source Github #
>>> import Proarrow.Colimit.Pushout (isEpi)
>>> let f :: FinHask (FH (Fin 3)) (FH (Fin 3)) = fromList [(0,2), (1,0), (2,1)]
>>> (pushout f f \(FinHask g1) (FinHask g2) -> P.show (g1, g2)) :: P.String
"(fromList [(0,0),(1,1),(2,2)],fromList [(0,0),(1,1),(2,2)])"
>>> isEpi (f :: FinHask (FH (Fin 3)) (FH (Fin 3)))
True
>>> import Proarrow.Limit.Pullback (isMono)
>>> (pullback f f \(FinHask l) (FinHask r) -> P.show (l, r)) :: P.String
"(fromList [(0,0),(1,1),(2,2)],fromList [(0,0),(1,1),(2,2)])"
>>> isMono f
True
>>> import Proarrow.Category.Topos (classifyImage, classifyKernelPair, and, or, implies, false)
>>> (case factorize f of p :.: q -> P.show (p, q) \\ p \\ q) :: P.String
"(fromList [(0,0),(1,1),(2,2)],fromList [(0,2),(1,0),(2,1)])"
>>> (classifyImage f, classifyKernelPair f)
(fromList [(0,True),(1,True),(2,True)],fromList [((0,0),True),((0,1),False),((0,2),False),((1,0),False),((1,1),True),((1,2),False),((2,0),False),((2,1),False),((2,2),True)])
>>> [and, or, implies] :: [FinHask (FH (Bool, Bool)) (FH Bool)]
[fromList [((False,False),False),((False,True),False),((True,False),False),((True,True),True)],fromList [((False,False),False),((False,True),True),((True,False),True),((True,True),True)],fromList [((False,False),True),((False,True),True),((True,False),False),((True,True),True)]]
>>> false :: FinHask (FH ()) (FH Bool)
fromList [((),False)]
Instance details

Defined in Proarrow.Category.Instance.FinHask

Associated Types

type Omega 
Instance details

Defined in Proarrow.Category.Instance.FinHask

type Omega = 'FH Bool

Methods

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

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

HasBinaryCoproducts FINHASK Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Associated Types

type ('FH a :: FINHASK) || ('FH b :: FINHASK) 
Instance details

Defined in Proarrow.Category.Instance.FinHask

type ('FH a :: FINHASK) || ('FH b :: FINHASK) = 'FH (Either a b)

Methods

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

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

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

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

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

HasCoequalizers FINHASK Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

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

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

HasInitialObject FINHASK Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Associated Types

type InitialObject 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

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

HasPushouts FINHASK Source Github #

Exercise 6.22 of Seven Sketches >>> let l :: FinHask (FH (Fin 4)) (FH (Fin 3)) = fromList [(0,0), (1,0), (2,1), (3,2)] >>> let r :: FinHask (FH (Fin 4)) (FH (Fin 5)) = fromList [(0,0), (1,2), (2,4), (3,4)] >>> (pushout l r l' r' -> P.show (l', r')) :: P.String "(fromList [(0,1),(1,3),(2,3)],fromList [(0,1),(1,0),(2,1),(3,2),(4,3)])"

Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

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

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

CategoryOf FINHASK Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Associated Types

type (~>) 
Instance details

Defined in Proarrow.Category.Instance.FinHask

type (~>) = FinHask
type Ob (a :: FINHASK) 
Instance details

Defined in Proarrow.Category.Instance.FinHask

type Ob (a :: FINHASK) = (Is 'FH a, Finite (UN 'FH a), Ord (UN 'FH a), Show (UN 'FH a))
HasBinaryProducts FINHASK Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Associated Types

type ('FH a :: FINHASK) && ('FH b :: FINHASK) 
Instance details

Defined in Proarrow.Category.Instance.FinHask

type ('FH a :: FINHASK) && ('FH b :: FINHASK) = 'FH (a, b)

Methods

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

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

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

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

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

HasEqualizers FINHASK Source Github #
>>> let f :: FinHask (FH (Fin 4)) (FH (Fin 3)) = fromList [(0,0), (1,1), (2,1), (3,0)]
>>> let g :: FinHask (FH (Fin 4)) (FH (Fin 3)) = fromList [(0,2), (1,0), (2,1), (3,0)]
>>> let h :: FinHask (FH (Fin 3)) (FH (Fin 4)) = fromList [(0,3), (1,2), (2,3)]
>>> (equalize f g \incl -> let p = factorEqualizer incl h in P.show (incl, p, incl . p)) :: P.String
"(fromList [(0,2),(1,3)],fromList [(0,1),(1,0),(2,1)],fromList [(0,3),(1,2),(2,3)])"
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

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

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

HasPullbacks FINHASK Source Github #

Example 3.84 of Seven Sketches (A: 0=red, 1=blue, 2=black) >>> data Color = Red | Blue | Black deriving (P.Eq, P.Ord, P.Show, P.Enum, P.Bounded, Universe, Finite) >>> let f :: FinHask (FH (Fin 6)) (FH Color) = fromList [(0,Red), (1,Blue), (2,Red), (3,Red), (4,Black), (5,Blue)] >>> let g :: FinHask (FH (Fin 4)) (FH Color) = fromList [(0,Black), (1,Red), (2,Blue), (3,Red)] >>> (pullback f g (FinHask l) (FinHask r) -> P.show (P.zip (M.elems l) (M.elems r))) :: P.String "[(0,1),(0,3),(1,2),(2,1),(2,3),(3,1),(3,3),(4,0),(5,2)]"

Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

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

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

HasTerminalObject FINHASK Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Associated Types

type TerminalObject 
Instance details

Defined in Proarrow.Category.Instance.FinHask

type TerminalObject = 'FH ()

Methods

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

HasPushoutComplements FINHASK Source Github # 
Instance details

Defined in Proarrow.Tools.DPO

Methods

pushoutComplement :: forall (a :: FINHASK) (l :: FINHASK) (g :: FINHASK) ans. (a ~> l) -> (l ~> g) -> (forall (d :: FINHASK). (a ~> d) -> (d ~> g) -> ans) -> ans -> ans Source Github #

Promonad FinHask Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

id :: forall (a :: FINHASK). Ob a => FinHask a a Source Github #

(.) :: forall (b :: FINHASK) (c :: FINHASK) (a :: FINHASK). FinHask b c -> FinHask a b -> FinHask a c Source Github #

MonoidalProfunctor FinHask Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

one :: FinHask (Unit :: FINHASK) (Unit :: FINHASK) Source Github #

(**) :: forall (x1 :: FINHASK) (x2 :: FINHASK) (y1 :: FINHASK) (y2 :: FINHASK). FinHask x1 x2 -> FinHask y1 y2 -> FinHask (x1 ** y1) (x2 ** y2) Source Github #

Profunctor FinHask Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

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

lmap :: forall (c :: FINHASK) (a :: FINHASK) (b :: FINHASK). (c ~> a) -> FinHask a b -> FinHask c b Source Github #

rmap :: forall (b :: FINHASK) (d :: FINHASK) (a :: FINHASK). (b ~> d) -> FinHask a b -> FinHask a d Source Github #

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

Ob ('FH a) => Comonoid ('FH a :: FINHASK) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

counit :: 'FH a ~> (Unit :: FINHASK) Source Github #

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

Monoid ('FH ()) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

mempty :: (Unit :: FINHASK) ~> 'FH () Source Github #

mappend :: ('FH () ** 'FH ()) ~> 'FH () Source Github #

type Unit Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

type Omega Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

type Omega = 'FH Bool
type InitialObject Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

type (~>) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

type (~>) = FinHask
type TerminalObject Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

type TerminalObject = 'FH ()
type Ob (a :: FINHASK) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

type Ob (a :: FINHASK) = (Is 'FH a, Finite (UN 'FH a), Ord (UN 'FH a), Show (UN 'FH a))
type (a :: FINHASK) ** (b :: FINHASK) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

type (a :: FINHASK) ** (b :: FINHASK) = a && b
type (a :: FINHASK) ~~> (b :: FINHASK) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

type (a :: FINHASK) ~~> (b :: FINHASK) = 'FH (FinHask a b)
type ('FH a :: FINHASK) || ('FH b :: FINHASK) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

type ('FH a :: FINHASK) || ('FH b :: FINHASK) = 'FH (Either a b)
type ('FH a :: FINHASK) && ('FH b :: FINHASK) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

type ('FH a :: FINHASK) && ('FH b :: FINHASK) = 'FH (a, b)

data FinHask (a :: FINHASK) (b :: FINHASK) where Source Github #

Constructors

FinHask 

Fields

Instances

Instances details
Promonad FinHask Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

id :: forall (a :: FINHASK). Ob a => FinHask a a Source Github #

(.) :: forall (b :: FINHASK) (c :: FINHASK) (a :: FINHASK). FinHask b c -> FinHask a b -> FinHask a c Source Github #

MonoidalProfunctor FinHask Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

one :: FinHask (Unit :: FINHASK) (Unit :: FINHASK) Source Github #

(**) :: forall (x1 :: FINHASK) (x2 :: FINHASK) (y1 :: FINHASK) (y2 :: FINHASK). FinHask x1 x2 -> FinHask y1 y2 -> FinHask (x1 ** y1) (x2 ** y2) Source Github #

Profunctor FinHask Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

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

lmap :: forall (c :: FINHASK) (a :: FINHASK) (b :: FINHASK). (c ~> a) -> FinHask a b -> FinHask c b Source Github #

rmap :: forall (b :: FINHASK) (d :: FINHASK) (a :: FINHASK). (b ~> d) -> FinHask a b -> FinHask a d Source Github #

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

Show (FinHask a b) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

showsPrec :: Int -> FinHask a b -> ShowS Github #

show :: FinHask a b -> String Github #

showList :: [FinHask a b] -> ShowS Github #

Eq (FinHask a b) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

(==) :: FinHask a b -> FinHask a b -> Bool Github #

(/=) :: FinHask a b -> FinHask a b -> Bool Github #

Ord (FinHask a b) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

compare :: FinHask a b -> FinHask a b -> Ordering Github #

(<) :: FinHask a b -> FinHask a b -> Bool Github #

(<=) :: FinHask a b -> FinHask a b -> Bool Github #

(>) :: FinHask a b -> FinHask a b -> Bool Github #

(>=) :: FinHask a b -> FinHask a b -> Bool Github #

max :: FinHask a b -> FinHask a b -> FinHask a b Github #

min :: FinHask a b -> FinHask a b -> FinHask a b Github #

(Ob a, Ob b) => Finite (FinHask a b) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

(Ob a, Ob b) => Universe (FinHask a b) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

universe :: [FinHask a b] Source Github #

(!) :: forall (a :: FINHASK) (b :: FINHASK). Ord (UN 'FH a) => FinHask a b -> UN 'FH a -> UN 'FH b Source Github #

arr :: (Ob ('FH a), Ob ('FH b)) => (a -> b) -> FinHask ('FH a) ('FH b) Source Github #

reifyList :: [a] -> (forall l. Ob ('FH l) => Map l a -> r) -> r Source Github #

fromList :: (Ob ('FH a), Ob ('FH b)) => [(a, b)] -> FinHask ('FH a) ('FH b) Source Github #

toList :: (Ob ('FH a), Ob ('FH b)) => FinHask ('FH a) ('FH b) -> [(a, b)] Source Github #