| Safe Haskell | None |
|---|---|
| Language | GHC2024 |
Proarrow.Category.Monoidal.EndoProf
Description
The monoidal category of endo-profunctors on k under composition ((:.:)/Id),
with functor composition as the tensor. This is the profunctor-specific counterpart of
Proarrow.Category.Monoidal.Endo (in proarrow-equipment, which builds the analogous
structure for an arbitrary Bicategory), hardcoded here to
Prof/:.:/Id instead, and reusing Proarrow.Path's associators/unitors so they
aren't proved twice.
Note this is a genuinely different monoidal structure on k +-> k than
Proarrow.Profunctor.Instance.Day's Monoidal (j +-> k) instance (Day convolution) --
hence the need for a fresh wrapper type rather than another instance for the same kind.
Synopsis
- data ENDO k = E (k +-> k)
- data Endo (p :: ENDO k) (q :: ENDO k) where
- Endo :: forall {k} (p1 :: k +-> k) (q1 :: k +-> k). (Profunctor p1, Profunctor q1) => (p1 :~> q1) -> Endo ('E p1) ('E q1)
- class (Is ('E :: (k +-> k) -> ENDO k) a, c (UN ('E :: (k +-> k) -> ENDO k) a)) => OnE (c :: (k +-> k) -> Constraint) (a :: ENDO k)
- type RepSub k = SUBCAT (OnE (Representable :: (k +-> k) -> Constraint))
- type RepAction = Rep (RepAction' :: (RepSub k, k) +-> k)
- data family RepAction' :: (RepSub k, k) +-> k
- type TravSub k = SUBCAT (OnE ((Representable :: (k +-> k) -> Constraint) :&&: (Traversable :: (k +-> k) -> Constraint)))
- type TravAction = Rep (TravAction' :: (TravSub k, k) +-> k)
- data family TravAction' :: (TravSub k, k) +-> k
- data family Precomp :: forall x h. (REV (ENDO x), x +-> h) +-> (x +-> h)
Documentation
An object of is an endo-profunctor ENDO kk +-> k, i.e. (not necessarily
representable) a functor k -> k under the profunctor encoding.
Instances
| CategoryOf k => Monoidal (ENDO k) Source Github # | |||||
Defined in Proarrow.Category.Monoidal.EndoProf Associated Types
Methods withOb2 :: forall (a :: ENDO k) (b :: ENDO k) r. (Ob a, Ob b) => (Ob (a ** b) => r) -> r Source Github # leftUnitor :: forall (a :: ENDO k). Ob a => ((Unit :: ENDO k) ** a) ~> a Source Github # leftUnitorInv :: forall (a :: ENDO k). Ob a => a ~> ((Unit :: ENDO k) ** a) Source Github # rightUnitor :: forall (a :: ENDO k). Ob a => (a ** (Unit :: ENDO k)) ~> a Source Github # rightUnitorInv :: forall (a :: ENDO k). Ob a => a ~> (a ** (Unit :: ENDO k)) Source Github # associator :: forall (a :: ENDO k) (b :: ENDO k) (c :: ENDO k). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Github # associatorInv :: forall (a :: ENDO k) (b :: ENDO k) (c :: ENDO k). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Github # | |||||
| CategoryOf k => CategoryOf (ENDO k) Source Github # | The category of endoprofunctors on | ||||
Defined in Proarrow.Category.Monoidal.EndoProf | |||||
| CategoryOf k => MonoidalAction (RepAction :: k -> (RepSub k, k) -> Type) Source Github # | |||||
Defined in Proarrow.Category.Monoidal.EndoProf Methods unitor :: forall (x :: k). Ob x => Act (RepAction :: k -> (RepSub k, k) -> Type) (Unit :: RepSub k) x ~> x Source Github # unitorInv :: forall (x :: k). Ob x => x ~> Act (RepAction :: k -> (RepSub k, k) -> Type) (Unit :: RepSub k) x Source Github # multiplicator :: forall (a :: RepSub k) (b :: RepSub k) (x :: k). (Ob a, Ob b, Ob x) => Act (RepAction :: k -> (RepSub k, k) -> Type) (a ** b) x ~> Act (RepAction :: k -> (RepSub k, k) -> Type) a (Act (RepAction :: k -> (RepSub k, k) -> Type) b x) Source Github # multiplicatorInv :: forall (a :: RepSub k) (b :: RepSub k) (x :: k). (Ob a, Ob b, Ob x) => Act (RepAction :: k -> (RepSub k, k) -> Type) a (Act (RepAction :: k -> (RepSub k, k) -> Type) b x) ~> Act (RepAction :: k -> (RepSub k, k) -> Type) (a ** b) x Source Github # | |||||
| CategoryOf k => MonoidalAction (TravAction :: k -> (TravSub k, k) -> Type) Source Github # | |||||
Defined in Proarrow.Category.Monoidal.EndoProf Methods unitor :: forall (x :: k). Ob x => Act (TravAction :: k -> (TravSub k, k) -> Type) (Unit :: TravSub k) x ~> x Source Github # unitorInv :: forall (x :: k). Ob x => x ~> Act (TravAction :: k -> (TravSub k, k) -> Type) (Unit :: TravSub k) x Source Github # multiplicator :: forall (a :: TravSub k) (b :: TravSub k) (x :: k). (Ob a, Ob b, Ob x) => Act (TravAction :: k -> (TravSub k, k) -> Type) (a ** b) x ~> Act (TravAction :: k -> (TravSub k, k) -> Type) a (Act (TravAction :: k -> (TravSub k, k) -> Type) b x) Source Github # multiplicatorInv :: forall (a :: TravSub k) (b :: TravSub k) (x :: k). (Ob a, Ob b, Ob x) => Act (TravAction :: k -> (TravSub k, k) -> Type) a (Act (TravAction :: k -> (TravSub k, k) -> Type) b x) ~> Act (TravAction :: k -> (TravSub k, k) -> Type) (a ** b) x Source Github # | |||||
| CategoryOf k => Promonad (Endo :: ENDO k -> ENDO k -> Type) Source Github # | |||||
| CategoryOf k => MonoidalProfunctor (Endo :: ENDO k -> ENDO k -> Type) Source Github # | |||||
| CategoryOf k => Profunctor (Endo :: ENDO k -> ENDO k -> Type) Source Github # | |||||
Defined in Proarrow.Category.Monoidal.EndoProf Methods dimap :: forall (c :: ENDO k) (a :: ENDO k) (b :: ENDO k) (d :: ENDO k). (c ~> a) -> (b ~> d) -> Endo a b -> Endo c d Source Github # lmap :: forall (c :: ENDO k) (a :: ENDO k) (b :: ENDO k). (c ~> a) -> Endo a b -> Endo c b Source Github # rmap :: forall (b :: ENDO k) (d :: ENDO k) (a :: ENDO k). (b ~> d) -> Endo a b -> Endo a d Source Github # (\\) :: forall (a :: ENDO k) (b :: ENDO k) r. ((Ob a, Ob b) => r) -> Endo a b -> r Source Github # | |||||
| (CategoryOf h, CategoryOf x) => MonoidalAction (Rep Precomp :: (x +-> h) -> (REV (ENDO x), x +-> h) -> Type) Source Github # | |||||
Defined in Proarrow.Category.Monoidal.EndoProf Methods unitor :: forall (x0 :: x +-> h). Ob x0 => Act (Rep Precomp) (Unit :: REV (ENDO x)) x0 ~> x0 Source Github # unitorInv :: forall (x0 :: x +-> h). Ob x0 => x0 ~> Act (Rep Precomp) (Unit :: REV (ENDO x)) x0 Source Github # multiplicator :: forall (a :: REV (ENDO x)) (b :: REV (ENDO x)) (x0 :: x +-> h). (Ob a, Ob b, Ob x0) => Act (Rep Precomp) (a ** b) x0 ~> Act (Rep Precomp) a (Act (Rep Precomp) b x0) Source Github # multiplicatorInv :: forall (a :: REV (ENDO x)) (b :: REV (ENDO x)) (x0 :: x +-> h). (Ob a, Ob b, Ob x0) => Act (Rep Precomp) a (Act (Rep Precomp) b x0) ~> Act (Rep Precomp) (a ** b) x0 Source Github # | |||||
| CategoryOf k => FunctorForRep (RepAction' :: (RepSub k, k) +-> k) Source Github # | |||||
| CategoryOf k => FunctorForRep (TravAction' :: (TravSub k, k) +-> k) Source Github # | |||||
| (CategoryOf h, CategoryOf x) => FunctorForRep (Precomp :: (REV (ENDO x), x +-> h) +-> (x +-> h)) Source Github # | |||||
| type Unit Source Github # | |||||
Defined in Proarrow.Category.Monoidal.EndoProf | |||||
| type (~>) Source Github # | |||||
| type Ob (a :: ENDO k) Source Github # | |||||
| type ('E p :: ENDO k) ** ('E q :: ENDO k) Source Github # | |||||
| type (RepAction' :: (RepSub k, k) +-> k) @ ('('SUB ('E p) :: SUBCAT (OnE (Representable :: (k +-> k) -> Constraint)), x) :: (SUBCAT (OnE (Representable :: (k +-> k) -> Constraint)), k)) Source Github # | |||||
Defined in Proarrow.Category.Monoidal.EndoProf type (RepAction' :: (RepSub k, k) +-> k) @ ('('SUB ('E p) :: SUBCAT (OnE (Representable :: (k +-> k) -> Constraint)), x) :: (SUBCAT (OnE (Representable :: (k +-> k) -> Constraint)), k)) = p % x | |||||
| type (TravAction' :: (TravSub k, k) +-> k) @ ('('SUB ('E p) :: SUBCAT (OnE ((Representable :: (k +-> k) -> Constraint) :&&: (Traversable :: (k +-> k) -> Constraint))), x) :: (SUBCAT (OnE ((Representable :: (k +-> k) -> Constraint) :&&: (Traversable :: (k +-> k) -> Constraint))), k)) Source Github # | |||||
Defined in Proarrow.Category.Monoidal.EndoProf type (TravAction' :: (TravSub k, k) +-> k) @ ('('SUB ('E p) :: SUBCAT (OnE ((Representable :: (k +-> k) -> Constraint) :&&: (Traversable :: (k +-> k) -> Constraint))), x) :: (SUBCAT (OnE ((Representable :: (k +-> k) -> Constraint) :&&: (Traversable :: (k +-> k) -> Constraint))), k)) = p % x | |||||
| type (Precomp :: (REV (ENDO x), x +-> h) +-> (x +-> h)) @ ('('R ('E g), q) :: (REV (ENDO x), x +-> h)) Source Github # | |||||
data Endo (p :: ENDO k) (q :: ENDO k) where Source Github #
Morphisms of are natural transformations between the underlying profunctors.ENDO k
Constructors
| Endo :: forall {k} (p1 :: k +-> k) (q1 :: k +-> k). (Profunctor p1, Profunctor q1) => (p1 :~> q1) -> Endo ('E p1) ('E q1) |
Instances
| CategoryOf k => Promonad (Endo :: ENDO k -> ENDO k -> Type) Source Github # | |
| CategoryOf k => MonoidalProfunctor (Endo :: ENDO k -> ENDO k -> Type) Source Github # | |
| CategoryOf k => Profunctor (Endo :: ENDO k -> ENDO k -> Type) Source Github # | |
Defined in Proarrow.Category.Monoidal.EndoProf Methods dimap :: forall (c :: ENDO k) (a :: ENDO k) (b :: ENDO k) (d :: ENDO k). (c ~> a) -> (b ~> d) -> Endo a b -> Endo c d Source Github # lmap :: forall (c :: ENDO k) (a :: ENDO k) (b :: ENDO k). (c ~> a) -> Endo a b -> Endo c b Source Github # rmap :: forall (b :: ENDO k) (d :: ENDO k) (a :: ENDO k). (b ~> d) -> Endo a b -> Endo a d Source Github # (\\) :: forall (a :: ENDO k) (b :: ENDO k) r. ((Ob a, Ob b) => r) -> Endo a b -> r Source Github # | |
class (Is ('E :: (k +-> k) -> ENDO k) a, c (UN ('E :: (k +-> k) -> ENDO k) a)) => OnE (c :: (k +-> k) -> Constraint) (a :: ENDO k) Source Github #
Lift a constraint on profunctors k +-> k to the corresponding ENDO objects.
type RepSub k = SUBCAT (OnE (Representable :: (k +-> k) -> Constraint)) Source Github #
The subcategory of representable endo-profunctors -- i.e. ordinary functors
k -> k under the profunctor encoding. The most permissive restriction of ENDO for
which an Action even makes sense ( needs
%Representable), so every other MonoidalAction on k embeds into this one -- see
TravSub for a further restriction.
data family RepAction' :: (RepSub k, k) +-> k Source Github #
Instances
type TravSub k = SUBCAT (OnE ((Representable :: (k +-> k) -> Constraint) :&&: (Traversable :: (k +-> k) -> Constraint))) Source Github #
The subcategory of representable, traversable endo-profunctors -- exactly the
functors repTraverse can traverse with.
Monoidal for free via Proarrow.Category.Instance.Sub's generic
Monoidal (SUBCAT ob), since both Representable and Traversable already have
instances closing them under :.:/Id.
type TravAction = Rep (TravAction' :: (TravSub k, k) +-> k) Source Github #
The action of TravSub on k by application: .Act TravAction (SUB (E f)) x = f % x
data family TravAction' :: (TravSub k, k) +-> k Source Github #
Instances
data family Precomp :: forall x h. (REV (ENDO x), x +-> h) +-> (x +-> h) Source Github #
Endo-profunctors on x (any, not just representable ones) act on profunctors
x +-> h by precomposition: . Unlike Act Precomp (E g) q = q :.: gRepAction/
TravAction, the acted-upon kind here isn't x or h itself but the whole profunctor
kind x +-> h, so the witness g never has to be Representable -- only the assembled
action () does, which is automatic. This is what lets
Rep PrecomptoPrecompOptic turn any OpticSq (not just ones
already shaped like an Action) into a genuine
Optic.
The index category is , not REV (ENDO x), because precomposition
reverses the order composition happens in: ENDO x on
** composes its two arguments left-to-right, but composing two precomposition
actions in sequence applies them right-to-left.ENDO x