proarrow
Safe HaskellNone
LanguageGHC2024

Proarrow.Category.Instance.Cps

Description

A closed symmetric monoidal category with a chosen answer object r is a dialogue category, with Dual a = a ~~> r. CPS wraps the category to say which object. The morphisms are those of the category itself, so with r an object of effects, as IO () in Type, a morphism is pure and a term of Up a is a computation (a -> IO ()) -> IO (): call by push value, with the effects in the computations only.

CPS r is isomix exactly when r is the unit (answerUnit), and *-autonomous only in degenerate cases, since (a ~~> r) ~~> r is rarely a.

Synopsis

Documentation

data CPS (r :: k) Source Github #

Constructors

C k 

Instances

Instances details
Monoidal k => Monoidal (CPS r) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cps

Associated Types

type Unit 
Instance details

Defined in Proarrow.Category.Instance.Cps

type Unit = 'C (Unit :: k) :: CPS r

Methods

withOb2 :: forall (a :: CPS r) (b :: CPS r) r0. (Ob a, Ob b) => (Ob (a ** b) => r0) -> r0 Source Github #

leftUnitor :: forall (a :: CPS r). Ob a => ((Unit :: CPS r) ** a) ~> a Source Github #

leftUnitorInv :: forall (a :: CPS r). Ob a => a ~> ((Unit :: CPS r) ** a) Source Github #

rightUnitor :: forall (a :: CPS r). Ob a => (a ** (Unit :: CPS r)) ~> a Source Github #

rightUnitorInv :: forall (a :: CPS r). Ob a => a ~> (a ** (Unit :: CPS r)) Source Github #

associator :: forall (a :: CPS r) (b :: CPS r) (c :: CPS r). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Github #

associatorInv :: forall (a :: CPS r) (b :: CPS r) (c :: CPS r). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Github #

SymMonoidal k => SymMonoidal (CPS r) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cps

Methods

swap :: forall (a :: CPS r) (b :: CPS r). (Ob a, Ob b) => (a ** b) ~> (b ** a) Source Github #

Closed k => Closed (CPS r) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cps

Methods

withObExp :: forall (a :: CPS r) (b :: CPS r) r0. (Ob a, Ob b) => (Ob (a ~~> b) => r0) -> r0 Source Github #

curry :: forall (a :: CPS r) (b :: CPS r) (c :: CPS r). (Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) Source Github #

apply :: forall (a :: CPS r) (b :: CPS r). (Ob a, Ob b) => ((a ~~> b) ** a) ~> b Source Github #

(^^^) :: forall (a :: CPS r) (b :: CPS r) (x :: CPS r) (y :: CPS r). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) Source Github #

(Closed k, SymMonoidal k, Ob r) => Dialogue (CPS r) Source Github #

The dual of a is a ~~> r, the functor Not r on objects: linear distribution is uncurrying, reassociating and currying.

Instance details

Defined in Proarrow.Category.Instance.Cps

Methods

withObDual :: forall (a :: CPS r) r0. Ob a => (Ob (Dual a) => r0) -> r0 Source Github #

dual :: forall (a :: CPS r) (b :: CPS r). (a ~> b) -> Dual b ~> Dual a Source Github #

linDist :: forall (a :: CPS r) (b :: CPS r) (c :: CPS r). (Ob a, Ob b, Ob c) => ((a ** b) ~> Dual c) -> a ~> Dual (b ** c) Source Github #

linDistInv :: forall (a :: CPS r) (b :: CPS r) (c :: CPS r). (Ob a, Ob b, Ob c) => (a ~> Dual (b ** c)) -> (a ** b) ~> Dual c Source Github #

doubleNegInv :: forall (a :: CPS r). Ob a => a ~> Dual (Dual a) Source Github #

(Closed k, SymMonoidal k, r ~ (Unit :: k)) => IsoMix (CPS r) Source Github #

With the unit as the answer object, Dual Unit = Unit ~~> Unit ≅ Unit, and a consumer meets its value in apply. With any other answer object the units differ, so this is the only isomix instance; the constraint on r says so, since Unit is a type family and cannot head an instance.

Instance details

Defined in Proarrow.Category.Instance.Cps

Methods

dualUnit :: Dual (Unit :: CPS r) ~> (Unit :: CPS r) Source Github #

dualUnitInv :: (Unit :: CPS r) ~> Dual (Unit :: CPS r) Source Github #

dualityCounit :: forall (a :: CPS r). Ob a => (Dual a ** a) ~> (Unit :: CPS r) Source Github #

CategoryOf k => CategoryOf (CPS r) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cps

Associated Types

type (~>) 
Instance details

Defined in Proarrow.Category.Instance.Cps

type (~>) = Cps :: CPS r -> CPS r -> Type
CategoryOf k => Promonad (Cps :: CPS r -> CPS r -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cps

Methods

id :: forall (a :: CPS r). Ob a => Cps a a Source Github #

(.) :: forall (b :: CPS r) (c :: CPS r) (a :: CPS r). Cps b c -> Cps a b -> Cps a c Source Github #

Monoidal k => MonoidalProfunctor (Cps :: CPS r -> CPS r -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cps

Methods

one :: Cps (Unit :: CPS r) (Unit :: CPS r) Source Github #

(**) :: forall (x1 :: CPS r) (x2 :: CPS r) (y1 :: CPS r) (y2 :: CPS r). Cps x1 x2 -> Cps y1 y2 -> Cps (x1 ** y1) (x2 ** y2) Source Github #

CategoryOf k => Profunctor (Cps :: CPS r -> CPS r -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cps

Methods

dimap :: forall (c :: CPS r) (a :: CPS r) (b :: CPS r) (d :: CPS r). (c ~> a) -> (b ~> d) -> Cps a b -> Cps c d Source Github #

lmap :: forall (c :: CPS r) (a :: CPS r) (b :: CPS r). (c ~> a) -> Cps a b -> Cps c b Source Github #

rmap :: forall (b :: CPS r) (d :: CPS r) (a :: CPS r). (b ~> d) -> Cps a b -> Cps a d Source Github #

(\\) :: forall (a :: CPS r) (b :: CPS r) r0. ((Ob a, Ob b) => r0) -> Cps a b -> r0 Source Github #

CocommutativeComonoid a => CocommutativeComonoid ('C a :: CPS r) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cps

Comonoid a => Comonoid ('C a :: CPS r) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cps

Methods

counit :: ('C a :: CPS r) ~> (Unit :: CPS r) Source Github #

comult :: ('C a :: CPS r) ~> (('C a :: CPS r) ** ('C a :: CPS r)) Source Github #

type Unit Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cps

type Unit = 'C (Unit :: k) :: CPS r
type (~>) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cps

type (~>) = Cps :: CPS r -> CPS r -> Type
type Dual (a :: CPS r) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cps

type Dual (a :: CPS r) = 'C (UN ('C :: k -> CPS r) a ~~> r) :: CPS r
type Ob (a :: CPS r) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cps

type Ob (a :: CPS r) = WrappedOb ('C :: k -> CPS r) a
type (a :: CPS r) ** (b :: CPS r) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cps

type (a :: CPS r) ** (b :: CPS r) = 'C (UN ('C :: k -> CPS r) a ** UN ('C :: k -> CPS r) b) :: CPS r
type (a :: CPS r) ~~> (b :: CPS r) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cps

type (a :: CPS r) ~~> (b :: CPS r) = 'C (UN ('C :: k -> CPS r) a ~~> UN ('C :: k -> CPS r) b) :: CPS r

data Cps (a :: CPS r) (b :: CPS r) where Source Github #

The arrows of the category, wrapped as a category on the CPS-wrapped kind.

Constructors

Cps 

Fields

  • :: forall {k} (a1 :: k) (b1 :: k) (r :: k). { unCps :: a1 ~> b1
     
  •    } -> Cps ('C a1 :: CPS r) ('C b1 :: CPS r)
     

Instances

Instances details
CategoryOf k => Promonad (Cps :: CPS r -> CPS r -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cps

Methods

id :: forall (a :: CPS r). Ob a => Cps a a Source Github #

(.) :: forall (b :: CPS r) (c :: CPS r) (a :: CPS r). Cps b c -> Cps a b -> Cps a c Source Github #

Monoidal k => MonoidalProfunctor (Cps :: CPS r -> CPS r -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cps

Methods

one :: Cps (Unit :: CPS r) (Unit :: CPS r) Source Github #

(**) :: forall (x1 :: CPS r) (x2 :: CPS r) (y1 :: CPS r) (y2 :: CPS r). Cps x1 x2 -> Cps y1 y2 -> Cps (x1 ** y1) (x2 ** y2) Source Github #

CategoryOf k => Profunctor (Cps :: CPS r -> CPS r -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cps

Methods

dimap :: forall (c :: CPS r) (a :: CPS r) (b :: CPS r) (d :: CPS r). (c ~> a) -> (b ~> d) -> Cps a b -> Cps c d Source Github #

lmap :: forall (c :: CPS r) (a :: CPS r) (b :: CPS r). (c ~> a) -> Cps a b -> Cps c b Source Github #

rmap :: forall (b :: CPS r) (d :: CPS r) (a :: CPS r). (b ~> d) -> Cps a b -> Cps a d Source Github #

(\\) :: forall (a :: CPS r) (b :: CPS r) r0. ((Ob a, Ob b) => r0) -> Cps a b -> r0 Source Github #

answerUnit :: forall {k} (r :: k). (Closed k, Ob r, IsoMix (CPS r)) => PIso' r (Unit :: k) Source Github #

The converse: an isomix structure on CPS r makes r the unit, through Unit ~~> r ≅ r.