Safe Haskell	None
Language	GHC2024

Proarrow.Category.Equipment.Stateful

Documentation

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

Constructors

ST (k +-> k)

Instances

Instances details

(MonoidalAction m k, m ~ Type) => WithObO2 Cotight (STT' m k :: () -> () -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Methods

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

(MonoidalAction m k, m ~ Type) => WithObO2 Tight (STT' m k :: () -> () -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Methods

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

(MonoidalAction m k, m ~ Type) => 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 #

withOb0s :: forall {j :: ()} {k0 :: ()} (a :: STT' m k j k0) r. Ob a => ((Ob0 (STT' m k) j, Ob0 (STT' m k) k0) => 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 #

(SymMonoidalAction m k, m ~ Type) => Equipment (STT' m k :: () -> () -> Type) Source Comments #

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

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Methods

withCotightAdjoint :: forall {j :: ()} {k1 :: ()} (f :: STT' m k j k1) r. IsTight f => ((Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) => r) -> r Source Comments #

withTightAdjoint :: forall {j :: ()} {k1 :: ()} (f :: STT' m k j k1) r. IsCotight f => ((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r Source Comments #

(MonoidalAction m k, Adjunction ('PK l) ('PK r), Ob l, Ob r, Strong m r, Strong m l, m ~ Type) => 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

adj :: Adj ('ST l :: STT' m k i j) ('ST r :: STT' m k j i) 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 IsOb Cotight (p :: STT' m k i j) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

type IsOb Cotight (p :: STT' m k i j) = IsReader m (UN ('ST :: (k +-> k) -> STT' m k i j) p)

type IsOb Tight (p :: STT' m k i j) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

type IsOb Tight (p :: STT' m k i j) = IsWriter m (UN ('ST :: (k +-> k) -> STT' m k i j) p)

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 CotightAdjoint (p :: STT' m k i j) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

type CotightAdjoint (p :: STT' m k i j) = 'ST (WithReader m (UN ('ST :: (k +-> k) -> STT' m k i j) p)) :: STT' m k j i

type TightAdjoint (p :: STT' m k i j) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

type TightAdjoint (p :: STT' m k i j) = 'ST (WithWriter m (UN ('ST :: (k +-> k) -> STT' m k i j) p)) :: STT' m k j i

type O (a :: STT' m k j1 j2) (b :: STT' m k i j1) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

type O (a :: STT' m k j1 j2) (b :: STT' m k i j1) = 'ST (UN ('ST :: (k +-> k) -> STT' m k j1 j2) a :.: UN ('ST :: (k +-> k) -> STT' m k i j1) b) :: STT' m k i j2

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))

type STT m k = STT' m k '() '() Source Comments #

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 #

class (IsReader m (WithReader m p), Strong m (WithReader m p), Proadjunction p (WithReader m p), WithWriter m (WithReader m p) ~ p) => IsWriter m (p :: k +-> k) Source Comments #

Associated Types

type WithReader m (p :: k +-> k) :: k +-> k Source Comments #

Instances

Instances details

SymMonoidalAction m k => IsWriter m (Id :: k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Associated Types

type WithReader m (Id :: k -> k -> Type)
Instance details Defined in Proarrow.Category.Equipment.Stateful type WithReader m (Id :: k -> k -> Type) = Id :: k -> k -> Type

(SymMonoidalAction m k, Ob a) => IsWriter m (Writer a :: k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Associated Types

type WithReader m (Writer a :: k -> k -> Type)
Instance details Defined in Proarrow.Category.Equipment.Stateful type WithReader m (Writer a :: k -> k -> Type) = Reader ('OP a) :: k -> k -> Type

(IsWriter m p, IsWriter m q, m ~ Type) => IsWriter m (p :.: q :: k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Associated Types

type WithReader m (p :.: q :: k -> k -> Type)
Instance details Defined in Proarrow.Category.Equipment.Stateful type WithReader m (p :.: q :: k -> k -> Type) = WithReader m q :.: WithReader m p

class (IsWriter m (WithWriter m p), Strong m (WithWriter m p), Proadjunction (WithWriter m p) p, WithReader m (WithWriter m p) ~ p) => IsReader m (p :: k +-> k) Source Comments #

Associated Types

type WithWriter m (p :: k +-> k) :: k +-> k Source Comments #

Instances

Instances details

SymMonoidalAction m k => IsReader m (Id :: k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Associated Types

type WithWriter m (Id :: k -> k -> Type)
Instance details Defined in Proarrow.Category.Equipment.Stateful type WithWriter m (Id :: k -> k -> Type) = Id :: k -> k -> Type

(SymMonoidalAction m k, Ob a) => IsReader m (Reader ('OP a) :: k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Associated Types

type WithWriter m (Reader ('OP a) :: k -> k -> Type)
Instance details Defined in Proarrow.Category.Equipment.Stateful type WithWriter m (Reader ('OP a) :: k -> k -> Type) = Writer a :: k -> k -> Type

(IsReader m p, IsReader m q, m ~ Type) => IsReader m (p :.: q :: k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Associated Types

type WithWriter m (p :.: q :: k -> k -> Type)
Instance details Defined in Proarrow.Category.Equipment.Stateful type WithWriter m (p :.: q :: k -> k -> Type) = WithWriter m q :.: WithWriter m p