Safe Haskell	None
Language	GHC2024

Proarrow.Category.Internal

Contents

Finite categories are the ones internal to FINHASK
The converse: an internal category in FINSET is a finite category

Description

Internal categories: ik `InternalIn` k is a category internal to k, given by an object of objects C0 ik, an object of arrows C1 ik, and source/target/identity/composition structure maps.

Internal to finite sets these are the finite categories, and each direction needs a different presentation of finite sets. A FiniteCat counts its arrows only at the value level, so it is internal to FINHASK. Going back, Enumerable wants the object list as a type, which only the skeleton FINSET supplies, so INTERNAL is built from an internal category in FINSET.

Synopsis

class InternalIn (ik :: k) k1 where
- type C0 (ik :: k) :: k1
- type C1 (ik :: k) :: k1
- source :: (C1 ik :: k1) ~> (C0 ik :: k1)
- target :: (C1 ik :: k1) ~> (C0 ik :: k1)
- identity :: (C0 ik :: k1) ~> (C1 ik :: k1)
- compose :: Cosink '[C1 ik :: k1, C1 ik :: k1, C1 ik :: k1]
newtype ObIx k = ObIx Natural
data ArrIx k = ArrIx {
- arrSrc :: Natural
- arrTgt :: Natural
- arrPos :: Natural
}
data CompIx k = CompIx (ArrIx k) (ArrIx k)
obCount :: Enumerable k => Natural
withObIx :: Enumerable k => Natural -> (forall (a :: k). Ob a => Proxy a -> r) -> r
homSize :: FiniteCat k => Natural -> Natural -> Natural
type NumObs (ik :: k) = UN 'FS (C0 ik :: FINSET)
type NumArrs (ik :: k) = UN 'FS (C1 ik :: FINSET)
data INTERNAL (ik :: k) = IN (ORDINAL (NumObs ik))
data Internal (a :: INTERNAL ik) (b :: INTERNAL ik) where
- Internal :: forall {k} (ik :: k) (a :: INTERNAL ik) (b :: INTERNAL ik). (Ob a, Ob b) => Natural -> Internal a b
tableOf :: forall (a :: FINSET) (b :: FINSET). FinSet a b -> [Natural]
compTable :: forall {k} (ik :: k). InternalIn ik FINSET => [(Natural, Natural, Natural)]
obNum :: forall {k} {ik :: k} (a :: INTERNAL ik). (Enumerable (INTERNAL ik), Ob a) => Natural
internalIsFinite :: forall {k} (ik :: k) r. (InternalIn ik FINSET, SNatI (NumObs ik)) => (FiniteCat (INTERNAL ik) => r) -> r

Documentation

class InternalIn (ik :: k) k1 where Source Github #

An internal category in a category k.

Associated Types

type C0 (ik :: k) :: k1 Source Github #

type C1 (ik :: k) :: k1 Source Github #

Methods

source :: (C1 ik :: k1) ~> (C0 ik :: k1) Source Github #

target :: (C1 ik :: k1) ~> (C0 ik :: k1) Source Github #

identity :: (C0 ik :: k1) ~> (C1 ik :: k1) Source Github #

compose :: Cosink '[C1 ik :: k1, C1 ik :: k1, C1 ik :: k1] Source Github #

Instances

Instances details

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 #

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 #

Finite categories are the ones internal to `FINHASK`

newtype ObIx k Source Github #

An object of k as an inhabitant of a finite Haskell type: its index in Objects k.

Constructors

ObIx Natural

Instances

Instances details

Show (ObIx k) Source Github #
Instance details Defined in Proarrow.Category.Internal Methods showsPrec :: Int -> ObIx k -> ShowS Github # show :: ObIx k -> String Github # showList :: [ObIx k] -> ShowS Github #
Eq (ObIx k) Source Github #
Instance details Defined in Proarrow.Category.Internal Methods (==) :: ObIx k -> ObIx k -> Bool Github # (/=) :: ObIx k -> ObIx k -> Bool Github #
Ord (ObIx k) Source Github #
Instance details Defined in Proarrow.Category.Internal Methods compare :: ObIx k -> ObIx k -> Ordering Github # (<) :: ObIx k -> ObIx k -> Bool Github # (<=) :: ObIx k -> ObIx k -> Bool Github # (>) :: ObIx k -> ObIx k -> Bool Github # (>=) :: ObIx k -> ObIx k -> Bool Github # max :: ObIx k -> ObIx k -> ObIx k Github # min :: ObIx k -> ObIx k -> ObIx k Github #
Enumerable k => Finite (ObIx k) Source Github #
Instance details Defined in Proarrow.Category.Internal Methods universeF :: [ObIx k] Github # cardinality :: Tagged (ObIx k) Natural Github #
Enumerable k => Universe (ObIx k) Source Github #
Instance details Defined in Proarrow.Category.Internal Methods universe :: [ObIx k] Github #

data ArrIx k Source Github #

An arrow of k as an inhabitant of a finite Haskell type: the indices of its source and target objects, and its own position in that hom-set.

Constructors

ArrIx
Fields arrSrc :: Natural arrTgt :: Natural arrPos :: Natural

Instances

Instances details

Show (ArrIx k) Source Github #
Instance details Defined in Proarrow.Category.Internal Methods showsPrec :: Int -> ArrIx k -> ShowS Github # show :: ArrIx k -> String Github # showList :: [ArrIx k] -> ShowS Github #
Eq (ArrIx k) Source Github #
Instance details Defined in Proarrow.Category.Internal Methods (==) :: ArrIx k -> ArrIx k -> Bool Github # (/=) :: ArrIx k -> ArrIx k -> Bool Github #
Ord (ArrIx k) Source Github #
Instance details Defined in Proarrow.Category.Internal Methods compare :: ArrIx k -> ArrIx k -> Ordering Github # (<) :: ArrIx k -> ArrIx k -> Bool Github # (<=) :: ArrIx k -> ArrIx k -> Bool Github # (>) :: ArrIx k -> ArrIx k -> Bool Github # (>=) :: ArrIx k -> ArrIx k -> Bool Github # max :: ArrIx k -> ArrIx k -> ArrIx k Github # min :: ArrIx k -> ArrIx k -> ArrIx k Github #
FiniteCat k => Finite (ArrIx k) Source Github #
Instance details Defined in Proarrow.Category.Internal Methods universeF :: [ArrIx k] Github # cardinality :: Tagged (ArrIx k) Natural Github #
FiniteCat k => Universe (ArrIx k) Source Github #
Instance details Defined in Proarrow.Category.Internal Methods universe :: [ArrIx k] Github #

data CompIx k Source Github #

A composable pair, and the apex of compose: the pullback of source along target. The arrows are given outer first, so that the legs of compose come out in the order that instance wants them: the first leg composed after the second.

Constructors

CompIx (ArrIx k) (ArrIx k)

Instances

Instances details

Show (CompIx k) Source Github #
Instance details Defined in Proarrow.Category.Internal Methods showsPrec :: Int -> CompIx k -> ShowS Github # show :: CompIx k -> String Github # showList :: [CompIx k] -> ShowS Github #
Eq (CompIx k) Source Github #
Instance details Defined in Proarrow.Category.Internal Methods (==) :: CompIx k -> CompIx k -> Bool Github # (/=) :: CompIx k -> CompIx k -> Bool Github #
Ord (CompIx k) Source Github #
Instance details Defined in Proarrow.Category.Internal Methods compare :: CompIx k -> CompIx k -> Ordering Github # (<) :: CompIx k -> CompIx k -> Bool Github # (<=) :: CompIx k -> CompIx k -> Bool Github # (>) :: CompIx k -> CompIx k -> Bool Github # (>=) :: CompIx k -> CompIx k -> Bool Github # max :: CompIx k -> CompIx k -> CompIx k Github # min :: CompIx k -> CompIx k -> CompIx k Github #
FiniteCat k => Finite (CompIx k) Source Github #
Instance details Defined in Proarrow.Category.Internal Methods universeF :: [CompIx k] Github # cardinality :: Tagged (CompIx k) Natural Github #
FiniteCat k => Universe (CompIx k) Source Github #
Instance details Defined in Proarrow.Category.Internal Methods universe :: [CompIx k] Github #

obCount :: Enumerable k => Natural Source Github #

How many objects k has, by walking its object list.

withObIx :: Enumerable k => Natural -> (forall (a :: k). Ob a => Proxy a -> r) -> r Source Github #

Recover the object sitting at an index, together with the Ob evidence that lets the Finitary methods be called at it. The index must be below obCount; every index the enumerations below produce is.

homSize :: FiniteCat k => Natural -> Natural -> Natural Source Github #

The size of a hom-set, named by the indices of its endpoints.

The converse: an internal category in `FINSET` is a finite category

type NumObs (ik :: k) = UN 'FS (C0 ik :: FINSET) Source Github #

How many objects and how many arrows an internal category in FINSET has. These are types. That is what FINSET has over FINHASK, and the converse needs it, because Enumerable asks for its object list at the type level.

type NumArrs (ik :: k) = UN 'FS (C1 ik :: FINSET) Source Github #

data INTERNAL (ik :: k) Source Github #

The category an internal category in FINSET presents, as a kind: its objects are the elements of C0 ik, numbered by ORDINAL.

Constructors

IN (ORDINAL (NumObs ik))

Instances

Instances details

(InternalIn ik FINSET, SNatI (NumObs ik)) => Enumerable (INTERNAL ik) Source Github #

Instance details

Defined in Proarrow.Category.Internal

Methods

withIndex :: forall (a :: INTERNAL ik) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: INTERNAL ik) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb (INTERNAL ik) (At (INTERNAL ik) i) Source Github #

(InternalIn ik FINSET, SNatI (NumObs ik)) => Finite (INTERNAL ik) Source Github #

Instance details

Defined in Proarrow.Category.Internal

Associated Types

type Objects (INTERNAL ik)
Instance details Defined in Proarrow.Category.Internal type Objects (INTERNAL ik) = MapWrap ('IN :: ORDINAL (NumObs ik) -> INTERNAL ik) (Objects (ORDINAL (NumObs ik)))

Methods

finite :: IndexedList (Objects (INTERNAL ik)) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects (INTERNAL ik)) i ~ At (INTERNAL ik) i => r) -> r Source Github #

InternalIn ik FINSET => Indexed (INTERNAL ik) Source Github #

Instance details

Defined in Proarrow.Category.Internal

(InternalIn ik FINSET, SNatI (NumObs ik)) => CategoryOf (INTERNAL ik) Source Github #

Instance details

Defined in Proarrow.Category.Internal

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Internal type (~>) = Internal :: INTERNAL ik -> INTERNAL ik -> Type

(InternalIn ik FINSET, SNatI (NumObs ik)) => Promonad (Internal :: INTERNAL ik -> INTERNAL ik -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Internal

Methods

id :: forall (a :: INTERNAL ik). Ob a => Internal a a Source Github #

(.) :: forall (b :: INTERNAL ik) (c :: INTERNAL ik) (a :: INTERNAL ik). Internal b c -> Internal a b -> Internal a c Source Github #

(InternalIn ik FINSET, SNatI (NumObs ik)) => Finitary (Internal :: INTERNAL ik -> INTERNAL ik -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Internal

Methods

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

toIndex :: forall (a :: INTERNAL ik) (b :: INTERNAL ik). (Ob a, Ob b) => Internal a b -> Natural Source Github #

fromIndex :: forall (a :: INTERNAL ik) (b :: INTERNAL ik). (Ob a, Ob b) => Natural -> Internal a b Source Github #

elements :: forall (a :: INTERNAL ik) (b :: INTERNAL ik). (Ob a, Ob b) => [Internal a b] Source Github #

(InternalIn ik FINSET, SNatI (NumObs ik)) => Profunctor (Internal :: INTERNAL ik -> INTERNAL ik -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Internal

Methods

dimap :: forall (c :: INTERNAL ik) (a :: INTERNAL ik) (b :: INTERNAL ik) (d :: INTERNAL ik). (c ~> a) -> (b ~> d) -> Internal a b -> Internal c d Source Github #

lmap :: forall (c :: INTERNAL ik) (a :: INTERNAL ik) (b :: INTERNAL ik). (c ~> a) -> Internal a b -> Internal c b Source Github #

rmap :: forall (b :: INTERNAL ik) (d :: INTERNAL ik) (a :: INTERNAL ik). (b ~> d) -> Internal a b -> Internal a d Source Github #

(\\) :: forall (a :: INTERNAL ik) (b :: INTERNAL ik) r. ((Ob a, Ob b) => r) -> Internal a b -> r Source Github #

type Objects (INTERNAL ik) Source Github #

Instance details

Defined in Proarrow.Category.Internal

type Objects (INTERNAL ik) = MapWrap ('IN :: ORDINAL (NumObs ik) -> INTERNAL ik) (Objects (ORDINAL (NumObs ik)))

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Internal

type (~>) = Internal :: INTERNAL ik -> INTERNAL ik -> Type

type At (INTERNAL ik) i Source Github #

Instance details

Defined in Proarrow.Category.Internal

type At (INTERNAL ik) i = FmapWrap ('IN :: ORDINAL (NumObs ik) -> INTERNAL ik) (At (ORDINAL (NumObs ik)) i)

type Index (a :: INTERNAL ik) Source Github #

Instance details

Defined in Proarrow.Category.Internal

type Index (a :: INTERNAL ik) = Index (UN ('IN :: ORDINAL (NumObs ik) -> INTERNAL ik) a)

type Ob (a :: INTERNAL ik) Source Github #

Instance details

Defined in Proarrow.Category.Internal

type Ob (a :: INTERNAL ik) = (Is ('IN :: ORDINAL (NumObs ik) -> INTERNAL ik) a, IsOrdinal (UN ('IN :: ORDINAL (NumObs ik) -> INTERNAL ik) a))

data Internal (a :: INTERNAL ik) (b :: INTERNAL ik) where Source Github #

An arrow of the presented category: an element of C1 ik. That its source and target are the objects claimed is a runtime invariant, as the table invariants of FinSet are.

Constructors

Internal :: forall {k} (ik :: k) (a :: INTERNAL ik) (b :: INTERNAL ik). (Ob a, Ob b) => Natural -> Internal a b

Instances

Instances details

(InternalIn ik FINSET, SNatI (NumObs ik)) => Promonad (Internal :: INTERNAL ik -> INTERNAL ik -> Type) Source Github #
Instance details Defined in Proarrow.Category.Internal Methods id :: forall (a :: INTERNAL ik). Ob a => Internal a a Source Github # (.) :: forall (b :: INTERNAL ik) (c :: INTERNAL ik) (a :: INTERNAL ik). Internal b c -> Internal a b -> Internal a c Source Github #
(InternalIn ik FINSET, SNatI (NumObs ik)) => Finitary (Internal :: INTERNAL ik -> INTERNAL ik -> Type) Source Github #
Instance details Defined in Proarrow.Category.Internal Methods size :: forall (a :: INTERNAL ik) (b :: INTERNAL ik). (Ob a, Ob b) => Natural Source Github # toIndex :: forall (a :: INTERNAL ik) (b :: INTERNAL ik). (Ob a, Ob b) => Internal a b -> Natural Source Github # fromIndex :: forall (a :: INTERNAL ik) (b :: INTERNAL ik). (Ob a, Ob b) => Natural -> Internal a b Source Github # elements :: forall (a :: INTERNAL ik) (b :: INTERNAL ik). (Ob a, Ob b) => [Internal a b] Source Github #
(InternalIn ik FINSET, SNatI (NumObs ik)) => Profunctor (Internal :: INTERNAL ik -> INTERNAL ik -> Type) Source Github #
Instance details Defined in Proarrow.Category.Internal Methods dimap :: forall (c :: INTERNAL ik) (a :: INTERNAL ik) (b :: INTERNAL ik) (d :: INTERNAL ik). (c ~> a) -> (b ~> d) -> Internal a b -> Internal c d Source Github # lmap :: forall (c :: INTERNAL ik) (a :: INTERNAL ik) (b :: INTERNAL ik). (c ~> a) -> Internal a b -> Internal c b Source Github # rmap :: forall (b :: INTERNAL ik) (d :: INTERNAL ik) (a :: INTERNAL ik). (b ~> d) -> Internal a b -> Internal a d Source Github # (\\) :: forall (a :: INTERNAL ik) (b :: INTERNAL ik) r. ((Ob a, Ob b) => r) -> Internal a b -> r Source Github #

tableOf :: forall (a :: FINSET) (b :: FINSET). FinSet a b -> [Natural] Source Github #

A structure map as a list of indices into its codomain.

compTable :: forall {k} (ik :: k). InternalIn ik FINSET => [(Natural, Natural, Natural)] Source Github #

The composition table: for each composable pair, the outer arrow, the inner arrow, and their composite, as indices into C1 ik.

obNum :: forall {k} {ik :: k} (a :: INTERNAL ik). (Enumerable (INTERNAL ik), Ob a) => Natural Source Github #

Which element of C0 ik an object names.

internalIsFinite :: forall {k} (ik :: k) r. (InternalIn ik FINSET, SNatI (NumObs ik)) => (FiniteCat (INTERNAL ik) => r) -> r Source Github #

The converse, as a statement: an internal category in FINSET presents a FiniteCat.

At BOOL the presented category has the hom-sets of BOOL back: one arrow each way except from TRU to FLS, where there is none.

>>> import Proarrow.Category.Instance.Ordinal (ORDINAL (..))
>>> :{
[ size @(Hom (INTERNAL BOOL)) @(IN OZ) @(IN OZ)
, size @(Hom (INTERNAL BOOL)) @(IN OZ) @(IN (OS OZ))
, size @(Hom (INTERNAL BOOL)) @(IN (OS OZ)) @(IN OZ)
, size @(Hom (INTERNAL BOOL)) @(IN (OS OZ)) @(IN (OS OZ))
] :: [Natural]
:}
[1,1,0,1]

>>> let f = fromIndex @(Hom (INTERNAL BOOL)) @(IN OZ) @(IN (OS OZ)) 0
>>> toIndex @(Hom (INTERNAL BOOL)) @(IN OZ) @(IN (OS OZ)) (id @_ @(IN (OS OZ)) . f)
0

Documentation

Instances

Finite categories are the ones internal to FINHASK

Instances

Instances

Instances

The converse: an internal category in FINSET is a finite category

Instances

Instances

Finite categories are the ones internal to `FINHASK`

The converse: an internal category in `FINSET` is a finite category