| Safe Haskell | None |
|---|---|
| Language | GHC2024 |
Proarrow.Squares
Description
Squares, specialized to profunctors.
This is the profunctor-specific counterpart of Proarrow.Equipment.Squares in
proarrow-equipment: instead of squares over an arbitrary proarrow equipment, the
legs here are Paths of plain profunctors (horizontal) or
Representable profunctors (vertical, playing the role of the tight morphisms of the
Prof equipment). Proarrow.Path does the associator/unitor bookkeeping once, by
induction over the path, so the combinators below never have to. A square's payload is
stated as Fold (p +++ f) :~> Fold (g +++ q)Fold f :.: Fold p :~> Fold q :.: Fold gNilNil +++ psps both reduce to +++ Nilps for free.
Synopsis
- data Sq (p :: Path j h) (q :: Path k i) (f :: Path h i) (g :: Path j k) where
- object :: CategoryOf k => Sq ('Nil :: Path k k) ('Nil :: Path k k) ('Nil :: Path k k) ('Nil :: Path k k)
- hArr :: forall {k} {i} (p :: k +-> i) (q :: k +-> i). (Profunctor p, Profunctor q) => (p :~> q) -> Sq (p '::: ('Nil :: Path i i)) (q '::: ('Nil :: Path i i)) ('Nil :: Path i i) ('Nil :: Path k k)
- hId :: forall {k} {i} (p :: k +-> i). Profunctor p => Sq (p '::: ('Nil :: Path i i)) (p '::: ('Nil :: Path i i)) ('Nil :: Path i i) ('Nil :: Path k k)
- vArr :: forall {j} {k} (f :: j +-> k) (g :: j +-> k). (Representable f, Representable g) => (f :~> g) -> Sq ('Nil :: Path j j) ('Nil :: Path k k) (f '::: ('Nil :: Path k k)) (g '::: ('Nil :: Path k k))
- vId :: forall {j} {k} (f :: j +-> k). Representable f => Sq ('Nil :: Path j j) ('Nil :: Path k k) (f '::: ('Nil :: Path k k)) (f '::: ('Nil :: Path k k))
- (|||) :: forall {a1} {a2} {b1} {b2} {c1} {c2} (ps :: Path a1 a2) (qs :: Path b1 b2) (rs :: Path c1 c2) (ds :: Path a2 b2) (es :: Path a1 b1) (fs :: Path b2 c2) (gs :: Path b1 c1). Sq ps qs ds es -> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
- (===) :: forall {b1} {h} {b2} {i} {j} {k} (rs :: Path b1 h) (ss :: Path b2 i) (es :: Path h i) (fs :: Path b1 b2) (ps :: Path j b1) (qs :: Path k b2) (gs :: Path j k). Sq rs ss es fs -> Sq ps qs fs gs -> Sq (ps +++ rs) (qs +++ ss) es gs
- toRight :: forall {h} {k} (f :: h +-> k). Representable f => Sq ('Nil :: Path h h) (f '::: ('Nil :: Path k k)) (f '::: ('Nil :: Path k k)) ('Nil :: Path h h)
- toLeft :: forall {j} {i} (f :: j +-> i) (f' :: i +-> j). (Proadjunction f f', Representable f) => Sq (f' '::: ('Nil :: Path j j)) ('Nil :: Path i i) (f '::: ('Nil :: Path i i)) ('Nil :: Path i i)
- fromLeft :: forall {j} {k} (f :: j +-> k). Representable f => Sq (f '::: ('Nil :: Path k k)) ('Nil :: Path k k) ('Nil :: Path k k) (f '::: ('Nil :: Path k k))
- fromRight :: forall {j} {k} (f :: j +-> k) (f' :: k +-> j). (Proadjunction f f', Representable f) => Sq ('Nil :: Path j j) (f' '::: ('Nil :: Path j j)) ('Nil :: Path j j) (f '::: ('Nil :: Path k k))
- unitNat :: forall {k1} {j} (p :: k1 +-> j) (q :: j +-> k1). Proadjunction p q => (Id :: k1 -> k1 -> Type) :~> (q :.: p)
- counitNat :: forall {j} {k1} (p :: j +-> k1) (q :: k1 +-> j). Proadjunction p q => (p :.: q) :~> (Id :: k1 -> k1 -> Type)
- vUnitor :: CategoryOf k => Sq ('Nil :: Path k k) ('Nil :: Path k k) ((Id :: k -> k -> Type) '::: ('Nil :: Path k k)) ('Nil :: Path k k)
- vUnitorInv :: CategoryOf k => Sq ('Nil :: Path k k) ('Nil :: Path k k) ('Nil :: Path k k) ((Id :: k -> k -> Type) '::: ('Nil :: Path k k))
- vCombine :: forall {j1} {j2} {k} (p :: j1 +-> j2) (q :: j2 +-> k). (Representable p, Representable q) => Sq ('Nil :: Path j1 j1) ('Nil :: Path k k) (p '::: (q '::: ('Nil :: Path k k))) ((q :.: p) '::: ('Nil :: Path k k))
- vSplit :: forall {j1} {j2} {k} (p :: j1 +-> j2) (q :: j2 +-> k). (Representable p, Representable q) => Sq ('Nil :: Path j1 j1) ('Nil :: Path k k) ((q :.: p) '::: ('Nil :: Path k k)) (p '::: (q '::: ('Nil :: Path k k)))
- vCombineAll :: forall {j} {k} (ps :: Path j k). IsTight ps => Sq ('Nil :: Path j j) ('Nil :: Path k k) ps (Fold ps '::: ('Nil :: Path k k))
- vSplitAll :: forall {h} {i} (ps :: Path h i). IsTight ps => Sq ('Nil :: Path h h) ('Nil :: Path i i) (Fold ps '::: ('Nil :: Path i i)) ps
- hCombineAll :: forall {k} {i} (ps :: Path k i). IsPath ps => Sq ps (Fold ps '::: ('Nil :: Path i i)) ('Nil :: Path i i) ('Nil :: Path k k)
- hSplitAll :: forall {k} {i} (ps :: Path k i). IsPath ps => Sq (Fold ps '::: ('Nil :: Path i i)) ps ('Nil :: Path i i) ('Nil :: Path k k)
- unit :: forall {i} {j} (p :: i +-> j) (q :: j +-> i). Proadjunction p q => Sq ('Nil :: Path i i) (p '::: (q '::: ('Nil :: Path i i))) ('Nil :: Path i i) ('Nil :: Path i i)
- counit :: forall {j} {i} (p :: j +-> i) (q :: i +-> j). Proadjunction p q => Sq (q '::: (p '::: ('Nil :: Path i i))) ('Nil :: Path i i) ('Nil :: Path i i) ('Nil :: Path i i)
- type EqpOptic (a :: j1 +-> i) (b :: k +-> j1) (s :: j2 +-> i) (t :: k +-> j2) = IsOptic a b s t => Sq (t '::: (s '::: ('Nil :: Path i i))) (b '::: (a '::: ('Nil :: Path i i))) ('Nil :: Path i i) ('Nil :: Path k k)
- type IsOptic (a :: j +-> k) (b :: j1 +-> k1) (s :: j2 +-> k2) (t :: j3 +-> k3) = (Representable s, Corepresentable t, Representable a, Corepresentable b)
- mkOptic :: forall {j2} {i} {k} {j3} (a :: j2 +-> i) (b :: k +-> j2) (s :: j3 +-> i) (t :: k +-> j3). IsOptic a b s t => (forall (x :: j3) r. Ob x => (forall (y :: j2). Ob y => ((s % x) ~> (a % y)) -> ((b %% y) ~> (t %% x)) -> r) -> r) -> EqpOptic a b s t
- seq :: forall {j1} {i} {j2} {j3} {j4} {k} (a :: j1 +-> i) (b :: j2 +-> j1) (s :: j3 +-> i) (t :: j2 +-> j3) (a' :: j4 +-> j2) (b' :: k +-> j4) (u :: j3 +-> j2) (v :: k +-> j3). (Proadjunction u t, IsOptic a b s t, IsOptic a' b' u v) => EqpOptic a b s t -> EqpOptic a' b' u v -> Sq (v '::: (s '::: ('Nil :: Path i i))) (b' '::: (a' '::: (b '::: (a '::: ('Nil :: Path i i))))) ('Nil :: Path i i) ('Nil :: Path k k)
- data family Action :: ((m, k) +-> k) -> k -> m +-> k
- type ActionOptic (act :: (j, k) +-> k) (a :: k) (b :: k) (s :: k) (t :: k) = EqpOptic (Rep (Action act a)) (Corep (Action act b)) (Rep (Action act s)) (Corep (Action act t))
- fromOptic :: forall {j} {k} (act :: (j, k) +-> k) (a :: k) (b :: k) (s :: k) (t :: k). (MonoidalAction act, Ob a, Ob b, Ob s, Ob t) => ExOptic (ActFl act) a b s t -> ActionOptic act a b s t
- toOptic :: forall h x (s :: x +-> h) (t :: h +-> x) (a :: x +-> h) (b :: h +-> x). (CategoryOf h, CategoryOf x, Representable s, Corepresentable t, Representable a, Corepresentable b) => EqpOptic a b s t -> ExOptic (ActFl (Rep Precomp)) a (CorepStar b) s (CorepStar t)
Documentation
data Sq (p :: Path j h) (q :: Path k i) (f :: Path h i) (g :: Path j k) where Source Github #
The kind of a square p q f g.
h--f--i | v | p--@--q | v | j--g--k
object :: CategoryOf k => Sq ('Nil :: Path k k) ('Nil :: Path k k) ('Nil :: Path k k) ('Nil :: Path k k) Source Github #
The empty square for an object.
K-----K | | | | | | K-----K
hArr :: forall {k} {i} (p :: k +-> i) (q :: k +-> i). (Profunctor p, Profunctor q) => (p :~> q) -> Sq (p '::: ('Nil :: Path i i)) (q '::: ('Nil :: Path i i)) ('Nil :: Path i i) ('Nil :: Path k k) Source Github #
Make a square from a horizontal proarrow.
K-----K | | p--@--q | | J-----J
hId :: forall {k} {i} (p :: k +-> i). Profunctor p => Sq (p '::: ('Nil :: Path i i)) (p '::: ('Nil :: Path i i)) ('Nil :: Path i i) ('Nil :: Path k k) Source Github #
A horizontal identity square.
J-----J | | p-----p | | K-----K
vArr :: forall {j} {k} (f :: j +-> k) (g :: j +-> k). (Representable f, Representable g) => (f :~> g) -> Sq ('Nil :: Path j j) ('Nil :: Path k k) (f '::: ('Nil :: Path k k)) (g '::: ('Nil :: Path k k)) Source Github #
Make a square from a vertical arrow.
J--f--K | v | | @ | | v | J--g--K
vId :: forall {j} {k} (f :: j +-> k). Representable f => Sq ('Nil :: Path j j) ('Nil :: Path k k) (f '::: ('Nil :: Path k k)) (f '::: ('Nil :: Path k k)) Source Github #
A vertical identity square.
J--f--K | v | | | | | v | J--f--K
(|||) :: forall {a1} {a2} {b1} {b2} {c1} {c2} (ps :: Path a1 a2) (qs :: Path b1 b2) (rs :: Path c1 c2) (ds :: Path a2 b2) (es :: Path a1 b1) (fs :: Path b2 c2) (gs :: Path b1 c1). Sq ps qs ds es -> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs) infixl 6 Source Github #
Horizontal composition.
L--d--H H--f--I L-d+f-I | v | | v | | v | p--@--q ||| q--@--r = p--@--r | v | | v | | v | M--e--J J--g--K M-e+g-K
(===) :: forall {b1} {h} {b2} {i} {j} {k} (rs :: Path b1 h) (ss :: Path b2 i) (es :: Path h i) (fs :: Path b1 b2) (ps :: Path j b1) (qs :: Path k b2) (gs :: Path j k). Sq rs ss es fs -> Sq ps qs fs gs -> Sq (ps +++ rs) (qs +++ ss) es gs infixl 5 Source Github #
Vertical composition.
H--e--I | v | r--@--s | v | J--f--K === J--f--K | v | p--@--q | v | L--g--M v v H--e--I | v | p+r-@-q+s | v | J--g--K
toRight :: forall {h} {k} (f :: h +-> k). Representable f => Sq ('Nil :: Path h h) (f '::: ('Nil :: Path k k)) (f '::: ('Nil :: Path k k)) ('Nil :: Path h h) Source Github #
Bend a vertical arrow in the companion direction.
J--f--K | v | | \->f | | J-----J
toLeft :: forall {j} {i} (f :: j +-> i) (f' :: i +-> j). (Proadjunction f f', Representable f) => Sq (f' '::: ('Nil :: Path j j)) ('Nil :: Path i i) (f '::: ('Nil :: Path i i)) ('Nil :: Path i i) Source Github #
Bend a vertical arrow in the conjoint direction.
J--f--K | v | f<-/ | | | K-----K
fromLeft :: forall {j} {k} (f :: j +-> k). Representable f => Sq (f '::: ('Nil :: Path k k)) ('Nil :: Path k k) ('Nil :: Path k k) (f '::: ('Nil :: Path k k)) Source Github #
Bend a companion proarrow back to a vertical arrow.
K-----K | | f>-\ | | v | J--f--K
fromRight :: forall {j} {k} (f :: j +-> k) (f' :: k +-> j). (Proadjunction f f', Representable f) => Sq ('Nil :: Path j j) (f' '::: ('Nil :: Path j j)) ('Nil :: Path j j) (f '::: ('Nil :: Path k k)) Source Github #
Bend a conjoint proarrow back to a vertical arrow.
J-----J | | | /-<f | v | J--f--K
unitNat :: forall {k1} {j} (p :: k1 +-> j) (q :: j +-> k1). Proadjunction p q => (Id :: k1 -> k1 -> Type) :~> (q :.: p) Source Github #
counitNat :: forall {j} {k1} (p :: j +-> k1) (q :: k1 +-> j). Proadjunction p q => (p :.: q) :~> (Id :: k1 -> k1 -> Type) Source Github #
vUnitor :: CategoryOf k => Sq ('Nil :: Path k k) ('Nil :: Path k k) ((Id :: k -> k -> Type) '::: ('Nil :: Path k k)) ('Nil :: Path k k) Source Github #
vUnitorInv :: CategoryOf k => Sq ('Nil :: Path k k) ('Nil :: Path k k) ('Nil :: Path k k) ((Id :: k -> k -> Type) '::: ('Nil :: Path k k)) Source Github #
vCombine :: forall {j1} {j2} {k} (p :: j1 +-> j2) (q :: j2 +-> k). (Representable p, Representable q) => Sq ('Nil :: Path j1 j1) ('Nil :: Path k k) (p '::: (q '::: ('Nil :: Path k k))) ((q :.: p) '::: ('Nil :: Path k k)) Source Github #
vSplit :: forall {j1} {j2} {k} (p :: j1 +-> j2) (q :: j2 +-> k). (Representable p, Representable q) => Sq ('Nil :: Path j1 j1) ('Nil :: Path k k) ((q :.: p) '::: ('Nil :: Path k k)) (p '::: (q '::: ('Nil :: Path k k))) Source Github #
vCombineAll :: forall {j} {k} (ps :: Path j k). IsTight ps => Sq ('Nil :: Path j j) ('Nil :: Path k k) ps (Fold ps '::: ('Nil :: Path k k)) Source Github #
Combine a whole bunch of vertical arrows into one composed arrow.
J-p..-K | vvv | | \@/ | | v | J--f--K
vSplitAll :: forall {h} {i} (ps :: Path h i). IsTight ps => Sq ('Nil :: Path h h) ('Nil :: Path i i) (Fold ps '::: ('Nil :: Path i i)) ps Source Github #
Split one composed arrow into a whole bunch of vertical arrows.
J--f--K | v | | /@\ | | vvv | J-p..-K
hCombineAll :: forall {k} {i} (ps :: Path k i). IsPath ps => Sq ps (Fold ps '::: ('Nil :: Path i i)) ('Nil :: Path i i) ('Nil :: Path k k) Source Github #
Combine a whole bunch of horizontal proarrows into one composed proarrow.
K-----K p--\ | :--@--F :--/ | J-----J
hSplitAll :: forall {k} {i} (ps :: Path k i). IsPath ps => Sq (Fold ps '::: ('Nil :: Path i i)) ps ('Nil :: Path i i) ('Nil :: Path k k) Source Github #
Split one composed proarrow into a whole bunch of horizontal proarrows.
K-----K | /--p F--@--: | \--: J-----J
unit :: forall {i} {j} (p :: i +-> j) (q :: j +-> i). Proadjunction p q => Sq ('Nil :: Path i i) (p '::: (q '::: ('Nil :: Path i i))) ('Nil :: Path i i) ('Nil :: Path i i) Source Github #
The unit of an adjunction.
J-------J | /---q | @ | | \---p J-------J
counit :: forall {j} {i} (p :: j +-> i) (q :: i +-> j). Proadjunction p q => Sq (q '::: (p '::: ('Nil :: Path i i))) ('Nil :: Path i i) ('Nil :: Path i i) ('Nil :: Path i i) Source Github #
The counit of an adjunction.
K-------K p---\ | | @ | q---/ | K-------K
type EqpOptic (a :: j1 +-> i) (b :: k +-> j1) (s :: j2 +-> i) (t :: k +-> j2) = IsOptic a b s t => Sq (t '::: (s '::: ('Nil :: Path i i))) (b '::: (a '::: ('Nil :: Path i i))) ('Nil :: Path i i) ('Nil :: Path k k) Source Github #
Optics in the Prof equipment.
J-------J s>--@-->a | @ | t<--@--<b K-------K
type IsOptic (a :: j +-> k) (b :: j1 +-> k1) (s :: j2 +-> k2) (t :: j3 +-> k3) = (Representable s, Corepresentable t, Representable a, Corepresentable b) Source Github #
mkOptic :: forall {j2} {i} {k} {j3} (a :: j2 +-> i) (b :: k +-> j2) (s :: j3 +-> i) (t :: k +-> j3). IsOptic a b s t => (forall (x :: j3) r. Ob x => (forall (y :: j2). Ob y => ((s % x) ~> (a % y)) -> ((b %% y) ~> (t %% x)) -> r) -> r) -> EqpOptic a b s t Source Github #
seq :: forall {j1} {i} {j2} {j3} {j4} {k} (a :: j1 +-> i) (b :: j2 +-> j1) (s :: j3 +-> i) (t :: j2 +-> j3) (a' :: j4 +-> j2) (b' :: k +-> j4) (u :: j3 +-> j2) (v :: k +-> j3). (Proadjunction u t, IsOptic a b s t, IsOptic a' b' u v) => EqpOptic a b s t -> EqpOptic a' b' u v -> Sq (v '::: (s '::: ('Nil :: Path i i))) (b' '::: (a' '::: (b '::: (a '::: ('Nil :: Path i i))))) ('Nil :: Path i i) ('Nil :: Path k k) Source Github #
Sequential composition of optics, with 2 holes.
data family Action :: ((m, k) +-> k) -> k -> m +-> k Source Github #
Instances
| (MonoidalAction act, Ob a) => FunctorForRep (Action act a :: m +-> k) Source Github # | |
| type (Action act a :: m +-> k) @ (x :: m) Source Github # | |
Defined in Proarrow.Squares | |
type ActionOptic (act :: (j, k) +-> k) (a :: k) (b :: k) (s :: k) (t :: k) = EqpOptic (Rep (Action act a)) (Corep (Action act b)) (Rep (Action act s)) (Corep (Action act t)) Source Github #
fromOptic :: forall {j} {k} (act :: (j, k) +-> k) (a :: k) (b :: k) (s :: k) (t :: k). (MonoidalAction act, Ob a, Ob b, Ob s, Ob t) => ExOptic (ActFl act) a b s t -> ActionOptic act a b s t Source Github #
toOptic :: forall h x (s :: x +-> h) (t :: h +-> x) (a :: x +-> h) (b :: h +-> x). (CategoryOf h, CategoryOf x, Representable s, Corepresentable t, Representable a, Corepresentable b) => EqpOptic a b s t -> ExOptic (ActFl (Rep Precomp)) a (CorepStar b) s (CorepStar t) Source Github #