Safe Haskell	None
Language	GHC2024

Proarrow.Category.Equipment.Stateful

Documentation

newtype STT' k (i :: ()) (j :: ()) Source Github #

Constructors

ST (k +-> k)

Instances

Instances details

SelfAction k => WithObO2 Cotight (STT' k :: () -> () -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Methods

withObO2 :: forall {i :: ()} {j :: ()} {k0 :: ()} (a :: STT' k j k0) (b :: STT' 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 Github #

SelfAction k => WithObO2 Tight (STT' k :: () -> () -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Methods

withObO2 :: forall {i :: ()} {j :: ()} {k0 :: ()} (a :: STT' k j k0) (b :: STT' 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 Github #

SelfAction k => Bicategory (STT' k :: () -> () -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Methods

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

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

withOb0s :: forall {j :: ()} {k0 :: ()} (a :: STT' k j k0) r. Ob a => ((Ob0 (STT' k) j, Ob0 (STT' k) k0) => r) -> r Source Github #

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

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

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

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

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

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

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

SelfAction k => Equipment (STT' k :: () -> () -> Type) Source Github #

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' k j k1) r. IsTight f => ((Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) => r) -> r Source Github #

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

(SelfAction k, Adjunction ('PK l) ('PK r), Ob l, Ob r, Strong k r, Strong k l) => Adjunction_ ('ST l :: STT' k i j) ('ST r :: STT' k j i) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Methods

adj :: Adj ('ST l :: STT' k i j) ('ST r :: STT' k j i) Source Github #

SelfAction k => CategoryOf (STT' k i j) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Equipment.Stateful type (~>) = StT :: STT' k i j -> STT' k i j -> Type

SelfAction k => Promonad (StT :: STT' k i j -> STT' k i j -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Methods

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

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

SelfAction k => Profunctor (StT :: STT' k i j -> STT' k i j -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Methods

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

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

type Ob0 (STT' k1 :: () -> () -> Type) (j :: k2) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

type Ob0 (STT' k1 :: () -> () -> Type) (j :: k2) = ()

type IsOb Cotight (p :: STT' k i j) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

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

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

Instance details

Defined in Proarrow.Category.Equipment.Stateful

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

type I Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

type I = 'ST (Id :: k -> k -> Type) :: STT' k i i

type CotightAdjoint (p :: STT' k i j) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

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

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

Instance details

Defined in Proarrow.Category.Equipment.Stateful

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

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

Instance details

Defined in Proarrow.Category.Equipment.Stateful

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

type UN ('ST :: (k +-> k) -> STT' k i j) ('ST p :: STT' k i j) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

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

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

type (~>) = StT :: STT' k i j -> STT' k i j -> Type

type Ob (a :: STT' k i j) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

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

type STT k = STT' k '() '() Source Github #

data StT (a :: STT' k i j) (b :: STT' k i j) where Source Github #

Constructors

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

Instances

Instances details

SelfAction k => Promonad (StT :: STT' k i j -> STT' k i j -> Type) Source Github #
Instance details Defined in Proarrow.Category.Equipment.Stateful Methods id :: forall (a :: STT' k i j). Ob a => StT a a Source Github # (.) :: forall (b :: STT' k i j) (c :: STT' k i j) (a :: STT' k i j). StT b c -> StT a b -> StT a c Source Github #
SelfAction k => Profunctor (StT :: STT' k i j -> STT' k i j -> Type) Source Github #
Instance details Defined in Proarrow.Category.Equipment.Stateful Methods dimap :: forall (c :: STT' k i j) (a :: STT' k i j) (b :: STT' k i j) (d :: STT' k i j). (c ~> a) -> (b ~> d) -> StT a b -> StT c d Source Github # (\\) :: forall (a :: STT' k i j) (b :: STT' k i j) r. ((Ob a, Ob b) => r) -> StT a b -> r Source Github #

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

Associated Types

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

Instances

Instances details

SelfAction k => IsWriter (Id :: k -> k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Associated Types

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

(SelfAction k, Ob a) => IsWriter (Writer a :: k -> k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Associated Types

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

(IsWriter p, IsWriter q) => IsWriter (p :.: q :: k -> k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Associated Types

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

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

Associated Types

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

Instances

Instances details

SelfAction k => IsReader (Id :: k -> k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Associated Types

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

(SelfAction k, Ob a) => IsReader (Reader ('OP a) :: k -> k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Associated Types

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

(IsReader p, IsReader q) => IsReader (p :.: q :: k -> k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Associated Types

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

type STSq (p :: k +-> k) (q :: k +-> k) (a :: k) (b :: k) = O ('ST (Writer a) :: STT' k '() '()) ('ST p :: STT' k '() '()) ~> O ('ST q :: STT' k '() '()) ('ST (Writer a) :: STT' k '() '()) Source Github #

crossing :: forall {k} (p :: k +-> k) (a :: k). (Strong k p, Ob a, SelfAction k) => STSq p p a a Source Github #

pi0 :: forall {k} (p :: STT k) (q :: STT k). (Ob p, Ob q, SelfAction k) => ('ST (UN ('ST :: (k +-> k) -> STT' k '() '()) p :*: UN ('ST :: (k +-> k) -> STT' k '() '()) q) :: STT' k '() '()) ~> p Source Github #

pi1 :: forall {k} (p :: STT k) (q :: STT k). (Ob p, Ob q, SelfAction k) => ('ST (UN ('ST :: (k +-> k) -> STT' k '() '()) p :*: UN ('ST :: (k +-> k) -> STT' k '() '()) q) :: STT' k '() '()) ~> q Source Github #

mult :: forall {k1} {k2} (p :: STT k2) (q :: STT k2) (r :: STT k2) (a :: k2) (b :: k1). (Ob p, Ob q, Ob r, SelfAction k2, Ob a, Ob b) => (p ~> q) -> (p ~> r) -> p ~> ('ST (UN ('ST :: (k2 +-> k2) -> STT' k2 '() '()) q :*: UN ('ST :: (k2 +-> k2) -> STT' k2 '() '()) r) :: STT' k2 '() '()) Source Github #

ip0 :: forall {i :: ()} {j :: ()} {k} (p :: STT k) (q :: STT' k i j). (Ob p, Ob q, SelfAction k) => p ~> ('ST (UN ('ST :: (k +-> k) -> STT' k '() '()) p :+: UN ('ST :: (k +-> k) -> STT' k i j) q) :: STT' k '() '()) Source Github #

ip1 :: forall {i :: ()} {j :: ()} {k} (p :: STT k) (q :: STT' k i j). (Ob p, Ob q, SelfAction k) => q ~> ('ST (UN ('ST :: (k +-> k) -> STT' k '() '()) p :+: UN ('ST :: (k +-> k) -> STT' k i j) q) :: STT' k i j) Source Github #