proarrow-0: Category theory with a central role for profunctors
Safe HaskellNone
LanguageHaskell2010

Proarrow.Category.Equipment.Stateful

Documentation

newtype STT m k (i :: ()) (j :: ()) Source Comments #

Constructors

ST (k +-> k) 

Instances

Instances details
MonoidalAction m k => Bicategory (STT m k :: () -> () -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

Methods

o :: forall {i :: ()} (j :: ()) (k0 :: ()) (a :: STT m k j k0) (b :: STT m k j k0) (c :: STT m k i j) (d :: STT m k i j). (a ~> b) -> (c ~> d) -> O a c ~> O b d Source Comments #

withOb2 :: forall {i :: ()} {j :: ()} {k0 :: ()} (a :: STT m k j k0) (b :: STT m k i j) r. (Ob a, Ob b, Ob0 (STT m k) i, Ob0 (STT m k) j, Ob0 (STT m k) k0) => (Ob (O a b) => r) -> r Source Comments #

(\\\) :: forall (i :: ()) (j :: ()) (ps :: STT m k i j) (qs :: STT m k i j) r. ((Ob0 (STT m k) i, Ob0 (STT m k) j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r Source Comments #

leftUnitor :: forall {i :: ()} {j :: ()} (a :: STT m k i j). (Ob0 (STT m k) i, Ob0 (STT m k) j, Ob a) => O (I :: STT m k j j) a ~> a Source Comments #

leftUnitorInv :: forall {i :: ()} {j :: ()} (a :: STT m k i j). (Ob0 (STT m k) i, Ob0 (STT m k) j, Ob a) => a ~> O (I :: STT m k j j) a Source Comments #

rightUnitor :: forall {i :: ()} {j :: ()} (a :: STT m k i j). (Ob0 (STT m k) i, Ob0 (STT m k) j, Ob a) => O a (I :: STT m k i i) ~> a Source Comments #

rightUnitorInv :: forall {i :: ()} {j :: ()} (a :: STT m k i j). (Ob0 (STT m k) i, Ob0 (STT m k) j, Ob a) => a ~> O a (I :: STT m k i i) Source Comments #

associator :: forall {h :: ()} {i :: ()} {j :: ()} {k0 :: ()} (a :: STT m k j k0) (b :: STT m k i j) (c :: STT m k h i). (Ob0 (STT m k) h, Ob0 (STT m k) i, Ob0 (STT m k) j, Ob0 (STT m k) k0, Ob a, Ob b, Ob c) => O (O a b) c ~> O a (O b c) Source Comments #

associatorInv :: forall {h :: ()} {i :: ()} {j :: ()} {k0 :: ()} (a :: STT m k j k0) (b :: STT m k i j) (c :: STT m k h i). (Ob0 (STT m k) h, Ob0 (STT m k) i, Ob0 (STT m k) j, Ob0 (STT m k) k0, Ob a, Ob b, Ob c) => O a (O b c) ~> O (O a b) c Source Comments #

(MonoidalAction m k, SymMonoidal m, Adjunction ('PK l) ('PK r), Ob l, Ob r, Strong m r, Strong m l) => Adjunction ('ST l :: STT m k i j) ('ST r :: STT m k j i) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

Methods

unit :: (I :: STT m k i i) ~> O ('ST r :: STT m k j i) ('ST l :: STT m k i j) Source Comments #

counit :: O ('ST l :: STT m k i j) ('ST r :: STT m k j i) ~> (I :: STT m k j j) Source Comments #

(MonoidalAction m k, SymMonoidal m, Ob (Unit :: m)) => Equipment (STT m k :: () -> () -> Type) (MonK m :: () -> () -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

Methods

mapConjoint :: forall {j :: ()} {k0 :: ()} (f :: MonK m j k0) (g :: MonK m j k0). (f ~> g) -> Conjoint (STT m k) g ~> Conjoint (STT m k) f Source Comments #

withObConjoint :: forall {j :: ()} {k0 :: ()} (f :: MonK m j k0) r. Ob f => (Ob (Conjoint (STT m k) f) => r) -> r Source Comments #

conjToId :: forall (k0 :: ()). Ob0 (MonK m) k0 => Conjoint (STT m k) (I :: MonK m k k) ~> (I :: STT m k k k) Source Comments #

conjFromId :: forall (k0 :: ()). Ob0 (MonK m) k0 => (I :: STT m k k k) ~> Conjoint (STT m k) (I :: MonK m k k) Source Comments #

conjToCompose :: forall {k1 :: ()} {j :: ()} {k2 :: ()} (f :: MonK m j k2) (g :: MonK m k1 j). Obj f -> Obj g -> Conjoint (STT m k) (O f g) ~> O (Conjoint (STT m k) g) (Conjoint (STT m k) f) Source Comments #

conjFromCompose :: forall {j1 :: ()} {j2 :: ()} {k0 :: ()} (f :: MonK m j2 k0) (g :: MonK m j1 j2). Obj f -> Obj g -> O (Conjoint (STT m k) g) (Conjoint (STT m k) f) ~> Conjoint (STT m k) (O f g) Source Comments #

comConUnit :: forall {j :: ()} {k0 :: ()} (f :: MonK m j k0). Obj f -> (I :: STT m k j j) ~> O (Conjoint (STT m k) f) (Companion (STT m k) f) Source Comments #

comConCounit :: forall {j :: ()} {k0 :: ()} (f :: MonK m j k0). Obj f -> O (Companion (STT m k) f) (Conjoint (STT m k) f) ~> (I :: STT m k k k) Source Comments #

(MonoidalAction m k, SymMonoidal m, Ob (Unit :: m)) => HasCompanions (STT m k :: () -> () -> Type) (MonK m :: () -> () -> Type) Source Comments #

Stateful transformers. https://arxiv.org/pdf/2305.16899 definition 6 Generalized to any monoidal action.

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Methods

mapCompanion :: forall {j :: ()} {k0 :: ()} (f :: MonK m j k0) (g :: MonK m j k0). (f ~> g) -> Companion (STT m k) f ~> Companion (STT m k) g Source Comments #

withObCompanion :: forall {j :: ()} {k0 :: ()} (f :: MonK m j k0) r. Ob f => (Ob (Companion (STT m k) f) => r) -> r Source Comments #

compToId :: forall (k0 :: ()). Ob0 (MonK m) k0 => Companion (STT m k) (I :: MonK m k k) ~> (I :: STT m k k k) Source Comments #

compFromId :: forall (k0 :: ()). Ob0 (MonK m) k0 => (I :: STT m k k k) ~> Companion (STT m k) (I :: MonK m k k) Source Comments #

compToCompose :: forall {i :: ()} {j :: ()} {k0 :: ()} (f :: MonK m j k0) (g :: MonK m i j). Obj f -> Obj g -> Companion (STT m k) (O f g) ~> O (Companion (STT m k) f) (Companion (STT m k) g) Source Comments #

compFromCompose :: forall {j1 :: ()} {j2 :: ()} {k0 :: ()} (f :: MonK m j2 k0) (g :: MonK m j1 j2). Obj f -> Obj g -> O (Companion (STT m k) f) (Companion (STT m k) g) ~> Companion (STT m k) (O f g) Source Comments #

MonoidalAction m k => CategoryOf (STT m k i j) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

Associated Types

type (~>) 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

type (~>) = StT :: STT m k i j -> STT m k i j -> Type
MonoidalAction m k => Promonad (StT :: STT m k i j -> STT m k i j -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

Methods

id :: forall (a :: STT m k i j). Ob a => StT a a Source Comments #

(.) :: forall (b :: STT m k i j) (c :: STT m k i j) (a :: STT m k i j). StT b c -> StT a b -> StT a c Source Comments #

MonoidalAction m k => Profunctor (StT :: STT m k i j -> STT m k i j -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

Methods

dimap :: forall (c :: STT m k i j) (a :: STT m k i j) (b :: STT m k i j) (d :: STT m k i j). (c ~> a) -> (b ~> d) -> StT a b -> StT c d Source Comments #

(\\) :: forall (a :: STT m k i j) (b :: STT m k i j) r. ((Ob a, Ob b) => r) -> StT a b -> r Source Comments #

type Ob0 (STT m k1 :: () -> () -> Type) (j :: k2) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

type Ob0 (STT m k1 :: () -> () -> Type) (j :: k2) = ()
type Companion (STT m k2 :: () -> () -> Type) ('MK a :: MonK m j k1) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

type Companion (STT m k2 :: () -> () -> Type) ('MK a :: MonK m j k1) = 'ST (Writer a :: k2 -> k2 -> Type) :: STT m k2 j k1
type Conjoint (STT m k2 :: () -> () -> Type) ('MK a :: MonK m j k1) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

type Conjoint (STT m k2 :: () -> () -> Type) ('MK a :: MonK m j k1) = 'ST (Reader ('OP a) :: k2 -> k2 -> Type) :: STT m k2 k1 j
type I Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

type I = 'ST (Id :: k -> k -> Type) :: STT m k i i
type O ('ST a :: STT m k1 j k2) ('ST b :: STT m k1 i j) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

type O ('ST a :: STT m k1 j k2) ('ST b :: STT m k1 i j) = 'ST (a :.: b) :: STT m k1 i k2
type UN ('ST :: (k +-> k) -> STT m k i j) ('ST p :: STT m k i j) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

type UN ('ST :: (k +-> k) -> STT m k i j) ('ST p :: STT m k i j) = p
type (~>) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

type (~>) = StT :: STT m k i j -> STT m k i j -> Type
type Ob (a :: STT m k i j) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

type Ob (a :: STT m k i j) = (Is ('ST :: (k +-> k) -> STT m k i j) a, Strong m (UN ('ST :: (k +-> k) -> STT m k i j) a))

data StT (a :: STT m k i j) (b :: STT m k i j) where Source Comments #

Constructors

StT :: forall m k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()). (Strong m p, Strong m q) => (p :~> q) -> StT ('ST p :: STT m k i j) ('ST q :: STT m k i j) 

Instances

Instances details
MonoidalAction m k => Promonad (StT :: STT m k i j -> STT m k i j -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

Methods

id :: forall (a :: STT m k i j). Ob a => StT a a Source Comments #

(.) :: forall (b :: STT m k i j) (c :: STT m k i j) (a :: STT m k i j). StT b c -> StT a b -> StT a c Source Comments #

MonoidalAction m k => Profunctor (StT :: STT m k i j -> STT m k i j -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

Methods

dimap :: forall (c :: STT m k i j) (a :: STT m k i j) (b :: STT m k i j) (d :: STT m k i j). (c ~> a) -> (b ~> d) -> StT a b -> StT c d Source Comments #

(\\) :: forall (a :: STT m k i j) (b :: STT m k i j) r. ((Ob a, Ob b) => r) -> StT a b -> r Source Comments #

type STSq (p :: k +-> k) (q :: k +-> k) (a :: m) (b :: m) = Sq '('ST p :: STT m k '() '(), 'MK a :: MonK m '() '()) '('ST q :: STT m k '() '(), 'MK b :: MonK m '() '()) Source Comments #

crossing :: forall {k} {m} (p :: k +-> k) (a :: m). (Strong m p, Ob a, MonoidalAction m k, SymMonoidal m) => STSq p p a a Source Comments #