Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.IntConstruction

Documentation

data INT k Source Comments #

Constructors

I k k

Instances

Instances details

HasFreeK TracedMonoidal' CompactClosed INT Source Comments #

Instance details

Defined in Proarrow.Profunctor.Free

Associated Types

type Lift TracedMonoidal' CompactClosed INT (a :: k)
Instance details Defined in Proarrow.Profunctor.Free type Lift TracedMonoidal' CompactClosed INT (a :: k) = 'I a (Unit :: k)
type Retract TracedMonoidal' CompactClosed INT ('I a b :: INT k)
Instance details Defined in Proarrow.Profunctor.Free type Retract TracedMonoidal' CompactClosed INT ('I a b :: INT k) = a ** Dual b

Methods

liftK :: forall k (x :: k) (y :: k). TracedMonoidal' k => (x ~> y) -> Lift TracedMonoidal' CompactClosed INT x ~> Lift TracedMonoidal' CompactClosed INT y Source Comments #

retractK :: forall k (x :: INT k) (y :: INT k). CompactClosed k => (x ~> y) -> Retract TracedMonoidal' CompactClosed INT x ~> Retract TracedMonoidal' CompactClosed INT y Source Comments #

TracedMonoidal' k => Monoidal (INT k) Source Comments #

The monoidal tensor is pointwise, tensoring of the plus and minus parts.

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

Associated Types

type Unit
Instance details Defined in Proarrow.Category.Instance.IntConstruction type Unit = 'I (Unit :: k) (Unit :: k)

Methods

withOb2 :: forall (a :: INT k) (b :: INT k) r. (Ob a, Ob b) => (Ob (a ** b) => r) -> r Source Comments #

leftUnitor :: forall (a :: INT k). Ob a => ((Unit :: INT k) ** a) ~> a Source Comments #

leftUnitorInv :: forall (a :: INT k). Ob a => a ~> ((Unit :: INT k) ** a) Source Comments #

rightUnitor :: forall (a :: INT k). Ob a => (a ** (Unit :: INT k)) ~> a Source Comments #

rightUnitorInv :: forall (a :: INT k). Ob a => a ~> (a ** (Unit :: INT k)) Source Comments #

associator :: forall (a :: INT k) (b :: INT k) (c :: INT k). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Comments #

associatorInv :: forall (a :: INT k) (b :: INT k) (c :: INT k). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Comments #

TracedMonoidal' k => SymMonoidal (INT k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

Methods

swap :: forall (a :: INT k) (b :: INT k). (Ob a, Ob b) => (a ** b) ~> (b ** a) Source Comments #

TracedMonoidal k => CategoryOf (INT k) Source Comments #

The Int construction, a.k.a. the geometry of interaction, the free compact closed category on a traced monoidal category.

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.IntConstruction type (~>) = IntConstruction :: INT k -> INT k -> Type

TracedMonoidal' k => CompactClosed (INT k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

Methods

distribDual :: forall (a :: INT k) (b :: INT k). (Ob a, Ob b) => Dual (a ** b) ~> (Dual a ** Dual b) Source Comments #

dualUnit :: Dual (Unit :: INT k) ~> (Unit :: INT k) Source Comments #

TracedMonoidal' k => StarAutonomous (INT k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

Methods

dual :: forall (a :: INT k) (b :: INT k). (a ~> b) -> Dual b ~> Dual a Source Comments #

dualInv :: forall (a :: INT k) (b :: INT k). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> a Source Comments #

linDist :: forall (a :: INT k) (b :: INT k) (c :: INT k). (Ob a, Ob b, Ob c) => ((a ** b) ~> Dual c) -> a ~> Dual (b ** c) Source Comments #

linDistInv :: forall (a :: INT k) (b :: INT k) (c :: INT k). (Ob a, Ob b, Ob c) => (a ~> Dual (b ** c)) -> (a ** b) ~> Dual c Source Comments #

TracedMonoidal' k => Closed (INT k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

Methods

withObExp :: forall (a :: INT k) (b :: INT k) r. (Ob a, Ob b) => (Ob (a ~~> b) => r) -> r Source Comments #

curry :: forall (a :: INT k) (b :: INT k) (c :: INT k). (Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) Source Comments #

apply :: forall (a :: INT k) (b :: INT k). (Ob a, Ob b) => ((a ~~> b) ** a) ~> b Source Comments #

(^^^) :: forall (a :: INT k) (b :: INT k) (x :: INT k) (y :: INT k). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) Source Comments #

TracedMonoidal k => Promonad (IntConstruction :: INT k -> INT k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

Methods

id :: forall (a :: INT k). Ob a => IntConstruction a a Source Comments #

(.) :: forall (b :: INT k) (c :: INT k) (a :: INT k). IntConstruction b c -> IntConstruction a b -> IntConstruction a c Source Comments #

TracedMonoidal' k => MonoidalProfunctor (IntConstruction :: INT k -> INT k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

Methods

par0 :: IntConstruction (Unit :: INT k) (Unit :: INT k) Source Comments #

par :: forall (x1 :: INT k) (x2 :: INT k) (y1 :: INT k) (y2 :: INT k). IntConstruction x1 x2 -> IntConstruction y1 y2 -> IntConstruction (x1 ** y1) (x2 ** y2) Source Comments #

TracedMonoidal k => Profunctor (IntConstruction :: INT k -> INT k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

Methods

dimap :: forall (c :: INT k) (a :: INT k) (b :: INT k) (d :: INT k). (c ~> a) -> (b ~> d) -> IntConstruction a b -> IntConstruction c d Source Comments #

(\\) :: forall (a :: INT k) (b :: INT k) r. ((Ob a, Ob b) => r) -> IntConstruction a b -> r Source Comments #

type Lift TracedMonoidal' CompactClosed INT (a :: k) Source Comments #

Instance details

Defined in Proarrow.Profunctor.Free

type Lift TracedMonoidal' CompactClosed INT (a :: k) = 'I a (Unit :: k)

type Retract TracedMonoidal' CompactClosed INT ('I a b :: INT k) Source Comments #

Instance details

Defined in Proarrow.Profunctor.Free

type Retract TracedMonoidal' CompactClosed INT ('I a b :: INT k) = a ** Dual b

type Unit Source Comments #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

type Unit = 'I (Unit :: k) (Unit :: k)

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

type (~>) = IntConstruction :: INT k -> INT k -> Type

type Ob (a :: INT k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

type Ob (a :: INT k) = (a ~ 'I (IntPlus a) (IntMinus a), Ob (IntPlus a), Ob (IntMinus a))

type (a :: INT k) ** (b :: INT k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

type (a :: INT k) ** (b :: INT k) = 'I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b)

type (a :: INT k) ~~> (b :: INT k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

type (a :: INT k) ~~> (b :: INT k) = ExpSA a b

type Dual ('I p n :: INT k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.IntConstruction

type Dual ('I p n :: INT k) = 'I n p

type family IntPlus (i :: INT k) :: k where ... Source Comments #

Equations

IntPlus ('I a b :: INT k) = a

type family IntMinus (i :: INT k) :: k where ... Source Comments #

Equations

IntMinus ('I a b :: INT k) = b

data IntConstruction (a :: INT k) (b :: INT k) where Source Comments #

Constructors

Int :: forall {k} (ap :: k) (am :: k) (bp :: k) (bm :: k). (Ob ap, Ob am, Ob bp, Ob bm) => ((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)

Instances

Instances details

TracedMonoidal k => Promonad (IntConstruction :: INT k -> INT k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.IntConstruction Methods id :: forall (a :: INT k). Ob a => IntConstruction a a Source Comments # (.) :: forall (b :: INT k) (c :: INT k) (a :: INT k). IntConstruction b c -> IntConstruction a b -> IntConstruction a c Source Comments #
TracedMonoidal' k => MonoidalProfunctor (IntConstruction :: INT k -> INT k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.IntConstruction Methods par0 :: IntConstruction (Unit :: INT k) (Unit :: INT k) Source Comments # par :: forall (x1 :: INT k) (x2 :: INT k) (y1 :: INT k) (y2 :: INT k). IntConstruction x1 x2 -> IntConstruction y1 y2 -> IntConstruction (x1 y1) (x2 y2) Source Comments #
TracedMonoidal k => Profunctor (IntConstruction :: INT k -> INT k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.IntConstruction Methods dimap :: forall (c :: INT k) (a :: INT k) (b :: INT k) (d :: INT k). (c ~> a) -> (b ~> d) -> IntConstruction a b -> IntConstruction c d Source Comments # (\\) :: forall (a :: INT k) (b :: INT k) r. ((Ob a, Ob b) => r) -> IntConstruction a b -> r Source Comments #

toInt :: forall {k} (a :: k) (b :: k). TracedMonoidal' k => (a ~> b) -> 'I a (Unit :: k) ~> 'I b (Unit :: k) Source Comments #

isoToInt :: forall {k} (a :: k) (b :: k). TracedMonoidal k => (a ~> b) -> (b ~> a) -> 'I a a ~> 'I b b Source Comments #

fromInt :: forall {k} (a :: k) (b :: k) (m :: k). TracedMonoidal k => ('I a m ~> 'I b m) -> a ~> b Source Comments #

class (TracedMonoidal k, Ob (Unit :: k)) => TracedMonoidal' k Source Comments #

Instances

Instances details

(TracedMonoidal k, Ob (Unit :: k)) => TracedMonoidal' k Source Comments #
Instance details Defined in Proarrow.Category.Instance.IntConstruction