Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.FinHask

Description

The category of finite Haskell types: objects are types with Universe/Finite instances (wrapped in FH), and a morphism is a function stored extensionally as a finite lookup table (Map), so morphisms can be enumerated, shown and compared. A finite, fully inspectable stand-in for Proarrow.Category.Instance.Hask.

Synopsis

newtype Fin (n :: Nat) = Fin {
- unFin :: Int
}
data FINHASK = FH Type
data FinHask (a :: FINHASK) (b :: FINHASK) where
- FinHask :: forall a1 b1. (Ob ('FH a1), Ob ('FH b1)) => {..} -> FinHask ('FH a1) ('FH b1)
(!) :: forall (a :: FINHASK) (b :: FINHASK). Ord (UN 'FH a) => FinHask a b -> UN 'FH a -> UN 'FH b
arr :: (Ob ('FH a), Ob ('FH b)) => (a -> b) -> FinHask ('FH a) ('FH b)
reifyList :: [a] -> (forall l. Ob ('FH l) => Map l a -> r) -> r
fromList :: (Ob ('FH a), Ob ('FH b)) => [(a, b)] -> FinHask ('FH a) ('FH b)
toList :: (Ob ('FH a), Ob ('FH b)) => FinHask ('FH a) ('FH b) -> [(a, b)]
position :: (Finite x, Eq x) => x -> Natural
card :: Finite x => Natural
unionFind :: Ord a => [(a, a)] -> a -> a

Documentation

newtype Fin (n :: Nat) Source Github #

Constructors

Fin
Fields unFin :: Int

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 Methods universeF :: [Fin n] Github # cardinality :: Tagged (Fin n) Natural Github #
KnownNat n => Universe (Fin n) Source Github #
Instance details Defined in Proarrow.Category.Instance.FinHask Methods universe :: [Fin n] 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 Unit = TerminalObject :: 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 type InitialObject = 'FH Void

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 #

The category of finite Haskell types, with morphisms stored extensionally as finite lookup tables.

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 #

Copowered FINHASK FINHASK Source Github #

Kept with the class, for the same reason as Powered FINHASK FINHASK.

Instance details

Defined in Proarrow.Colimit.Copower

Associated Types

type (n :: FINHASK) *. (a :: FINHASK)
Instance details Defined in Proarrow.Colimit.Copower type (n :: FINHASK) . (a :: FINHASK) = n * a

Methods

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

copower :: forall (a :: FINHASK) (b :: FINHASK) (n :: FINHASK). (Ob a, Ob b) => (n ~> HomObj FINHASK a b) -> (n *. a) ~> b Source Github #

uncopower :: forall (a :: FINHASK) (n :: FINHASK) (b :: FINHASK). (Ob a, Ob n) => ((n *. a) ~> b) -> n ~> HomObj FINHASK a b 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 #

Powered FINHASK FINHASK Source Github #

Kept with the class: FINHASK is above Proarrow.Category.Enriched, which this module needs.

Instance details

Defined in Proarrow.Limit.Power

Associated Types

type (a :: FINHASK) ^ (n :: FINHASK)
Instance details Defined in Proarrow.Limit.Power type (a :: FINHASK) ^ (n :: FINHASK) = n ~~> a

Methods

withObPower :: forall (a :: FINHASK) (n :: FINHASK) r. (Ob a, Ob n) => (Ob (a ^ n) => r) -> r Source Github #

power :: forall (a :: FINHASK) (b :: FINHASK) (n :: FINHASK). (Ob a, Ob b) => (n ~> HomObj FINHASK a b) -> a ~> (b ^ n) Source Github #

unpower :: forall (b :: FINHASK) (n :: FINHASK) (a :: FINHASK). (Ob b, Ob n) => (a ~> (b ^ n)) -> n ~> HomObj FINHASK a b Source Github #

Finitary FinHask Source Github #

The hom-sets of FINHASK are finite, so its hom-profunctor is finitary. It is numbered in the order of the universe the Finite instance above enumerates, but arithmetically instead of by searching it. A morphism is a table of values indexed by universeF @a. Reading that table as a numeral in base |b|, most significant digit first, gives universe's own order, since universe is traverse (a -> (a,) <$> universe) universe and for lists <*> varies its right operand fastest. So it is the last element of a that varies fastest.

Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

size :: forall (a :: FINHASK) (b :: FINHASK). (Ob a, Ob b) => Natural Source Github #

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

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

elements :: forall (a :: FINHASK) (b :: FINHASK). (Ob a, Ob b) => [FinHask a b] Source Github #

FiniteCat k => InternalIn (k :: Kind) FINHASK Source Github #

Every finite category is a category internal to FINHASK: objects and arrows are carried by their indices, and the structure maps are the lookup tables that read those indices back.

At BOOL every table agrees with the hand-written FINSET presentation above, with the arrows coming out in the order Fls, F2T, Tru.

>>> import Data.List (elemIndex)
>>> import Proarrow.Category.Instance.FinHask (toList)
>>> let ix a = P.maybe (-1) P.id (elemIndex a (U.universeF :: [ArrIx BOOL])) :: P.Int
>>> P.map P.snd (toList (source @BOOL @FINHASK))
[0,0,1]
>>> P.map P.snd (toList (target @BOOL @FINHASK))
[0,1,1]
>>> P.map (ix P.. P.snd) (toList (identity @BOOL @FINHASK))
[0,2]
>>> :{
(case compose @BOOL @FINHASK of
   Cone (Leg l1 (Leg l2 (Leg l3 Apex))) ->
     let g l = P.map (ix P.. P.snd) (toList l) in (g l1, g l2, g l3))
  :: ([P.Int], [P.Int], [P.Int])
:}
([0,1,2,2],[0,0,1,2],[0,1,1,2])

Instance details

Defined in Proarrow.Category.Internal

Associated Types

type C0 (k :: Kind)
Instance details Defined in Proarrow.Category.Internal type C0 (k :: Kind) = 'FH (ObIx k)
type C1 (k :: Kind)
Instance details Defined in Proarrow.Category.Internal type C1 (k :: Kind) = 'FH (ArrIx k)

Methods

source :: (C1 k :: FINHASK) ~> (C0 k :: FINHASK) Source Github #

target :: (C1 k :: FINHASK) ~> (C0 k :: FINHASK) Source Github #

identity :: (C0 k :: FINHASK) ~> (C1 k :: FINHASK) Source Github #

compose :: Cosink '[C1 k :: FINHASK, C1 k :: FINHASK, C1 k :: FINHASK] 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 #

(Finitary p, LocallyFinite j, LocallyFinite k) => EnrichedProfunctor FINHASK (p :: j +-> k) Source Github #

A finitary profunctor is a profunctor enriched in finite sets. The hom-object is the hom-set itself, which Elt makes an object of FINHASK out of nothing but the numbering, and the whiskerings are the two dimaps.

Instance details

Defined in Proarrow.Category.Enriched

Methods

withProObj :: forall (a :: k) (b :: j) r. (Ob a, Ob b) => (Ob (ProObj FINHASK p a b) => r) -> r Source Github #

underlying :: forall (a :: k) (b :: j). p a b -> (Unit :: FINHASK) ~> ProObj FINHASK p a b Source Github #

enriched :: forall (a :: k) (b :: j). (Ob a, Ob b) => ((Unit :: FINHASK) ~> ProObj FINHASK p a b) -> p a b Source Github #

rmap :: forall (a :: k) (b :: j) (c :: j). (Ob a, Ob b, Ob c) => (HomObj FINHASK b c ** ProObj FINHASK p a b) ~> ProObj FINHASK p a c Source Github #

lmap :: forall (a :: k) (b :: j) (c :: k). (Ob a, Ob b, Ob c) => (HomObj FINHASK c a ** ProObj FINHASK p a b) ~> ProObj FINHASK p c b Source Github #

Ob ('FH a) => CocommutativeComonoid ('FH a :: FINHASK) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinHask

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 #

HasBinaryCoproducts (SORTED s) Source Github #

The ports of both, those of the second numbered after those of the first.

Instance details

Defined in Proarrow.Category.Instance.OpenHypergraph

Methods

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

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

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

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

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

HasInitialObject (SORTED s) Source Github #

No ports.

Instance details

Defined in Proarrow.Category.Instance.OpenHypergraph

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.OpenHypergraph type InitialObject = 'SUB ('FH (Port ('[] :: [s]))) :: SUBCAT (Sorted s)

Methods

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

HasPushouts (SORTED s) Source Github #

The pushout of FINHASK, whose apex is then renumbered as the ports of the sorts of its elements, each of which comes from one of the two sides.

Instance details

Defined in Proarrow.Category.Instance.OpenHypergraph

Methods

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

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

Alternative (Boxes l :: SORTED s -> Type) Source Github #

No boxes, and the boxes of both sides, the nodes of the second numbered after those of the first.

Instance details

Defined in Proarrow.Category.Instance.OpenHypergraph

Methods

empty :: forall (a :: SORTED s). Ob a => (Unit :: Type) ~> Boxes l a Source Github #

alt :: forall (a :: SORTED s) (b :: SORTED s) (c :: SORTED s). (Ob a, Ob b) => ((a || b) ~> c) -> (Boxes l a ** Boxes l b) ~> Boxes l c Source Github #

Functor (Boxes l :: SORTED s -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.OpenHypergraph

Methods

map :: forall (a :: SORTED s) (b :: SORTED s). (a ~> b) -> Boxes l a ~> Boxes l b Source Github #

type Unit Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinHask

type Unit = TerminalObject :: 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 InitialObject = 'FH Void

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 C0 (k :: Kind) Source Github #

Instance details

Defined in Proarrow.Category.Internal

type C0 (k :: Kind) = 'FH (ObIx k)

type C1 (k :: Kind) Source Github #

Instance details

Defined in Proarrow.Category.Internal

type C1 (k :: Kind) = 'FH (ArrIx k)

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 (n :: FINHASK) *. (a :: FINHASK) Source Github #

Instance details

Defined in Proarrow.Colimit.Copower

type (n :: FINHASK) *. (a :: FINHASK) = n ** a

type (a :: FINHASK) ^ (n :: FINHASK) Source Github #

Instance details

Defined in Proarrow.Limit.Power

type (a :: FINHASK) ^ (n :: FINHASK) = n ~~> a

type ProObj FINHASK (p :: j +-> k) (a :: k) (b :: j) Source Github #

Instance details

Defined in Proarrow.Category.Enriched

type ProObj FINHASK (p :: j +-> k) (a :: k) (b :: j) = 'FH (Elt p 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)

type InitialObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.OpenHypergraph

type InitialObject = 'SUB ('FH (Port ('[] :: [s]))) :: SUBCAT (Sorted s)

type (a :: SORTED s) || (b :: SORTED s) Source Github #

Instance details

Defined in Proarrow.Category.Instance.OpenHypergraph

type (a :: SORTED s) || (b :: SORTED s) = 'SUB ('FH (Port ((PortSorts (UN ('SUB :: FINHASK -> SUBCAT (Sorted s)) a) :: [s]) ++ (PortSorts (UN ('SUB :: FINHASK -> SUBCAT (Sorted s)) b) :: [s])))) :: SUBCAT (Sorted s)

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

Constructors

FinHask
Fields :: forall a1 b1. (Ob ('FH a1), Ob ('FH b1)) => { unFinHask :: Map a1 b1 } -> FinHask ('FH a1) ('FH b1)

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 #
Finitary FinHask Source Github #	The hom-sets of `FINHASK` are finite, so its hom-profunctor is finitary. It is numbered in the order of the `universe` the `Finite` instance above enumerates, but arithmetically instead of by searching it. A morphism is a table of values indexed by `universeF @a`. Reading that table as a numeral in base `\|b\|`, most significant digit first, gives `universe`'s own order, since `universe` is `traverse (a -> (a,) <$> universe) universe` and for lists `<>` varies its right operand fastest. So it is the last* element of `a` that varies fastest.
Instance details Defined in Proarrow.Category.Instance.FinHask Methods size :: forall (a :: FINHASK) (b :: FINHASK). (Ob a, Ob b) => Natural Source Github # toIndex :: forall (a :: FINHASK) (b :: FINHASK). (Ob a, Ob b) => FinHask a b -> Natural Source Github # fromIndex :: forall (a :: FINHASK) (b :: FINHASK). (Ob a, Ob b) => Natural -> FinHask a b Source Github # elements :: forall (a :: FINHASK) (b :: FINHASK). (Ob a, Ob b) => [FinHask a b] 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 Methods universeF :: [FinHask a b] Github # cardinality :: Tagged (FinHask a b) Natural Github #
(Ob a, Ob b) => Universe (FinHask a b) Source Github #
Instance details Defined in Proarrow.Category.Instance.FinHask Methods universe :: [FinHask a b] 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 #

position :: (Finite x, Eq x) => x -> Natural Source Github #

Where a value sits in its own type's universe.

card :: Finite x => Natural Source Github #

How many inhabitants a type has.

unionFind :: Ord a => [(a, a)] -> a -> a Source Github #

The representative of each element after joining the given pairs: union-find, on a map of parent pointers.