proarrow
Safe HaskellNone
LanguageGHC2024

Proarrow.Optic.Sum

Description

Dual to ProdRes: combine over the coproduct of two categories via :++:. This lives in its own module (rather than next to ProdRes) only because Proarrow.Category.Instance.Coproduct transitively imports Proarrow.Optic already (via Corepresentable), so Optic can't import it back.

Unlike ProdRes, this doesn't let you combine two different optics into one -- an (p :++: q) (L a) (L b) can only ever hold a p, never a q. Instead it lets any single w1- or w2-flavored optic be injected into a shared SumRes w1 w2 type, with the unused side witnessed trivially by Id (demanded via ClosedUnder).

Synopsis

Documentation

class SumRes (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2) (p :: COPRODUCT k1 k2 +-> COPRODUCT k1 k2) (q :: COPRODUCT j1 j2 +-> COPRODUCT j1 j2) where Source Github #

Unlike ProdRes, a SumRes witness can be decomposed back: the trick is that withSumL/withSumR only fix the one endpoint anchored from outside (s via p's first slot, t via q's second slot) -- the other endpoint (a, b) comes back refined by the continuation instead of being required upfront. That's what lets the :.: case recurse: the existential "middle" object introduced there is exactly the next call's anchored endpoint, so its tag is established by the previous step's own guarantee before it's ever needed as input.

Methods

withSumL :: forall (s :: k1) (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) (t :: j1) r. p ('L s :: COPRODUCT k1 k2) a -> q b ('L t :: COPRODUCT j1 j2) -> (forall (p1 :: k1 +-> k1) (q1 :: j1 +-> j1) (a' :: k1) (b' :: j1). (w1 p1 q1, Profunctor p1, Profunctor q1, a ~ ('L a' :: COPRODUCT k1 k2), b ~ ('L b' :: COPRODUCT j1 j2)) => p1 s a' -> q1 b' t -> r) -> r Source Github #

withSumR :: forall (s :: k2) (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) (t :: j2) r. p ('R s :: COPRODUCT k1 k2) a -> q b ('R t :: COPRODUCT j1 j2) -> (forall (p2 :: k2 +-> k2) (q2 :: j2 +-> j2) (a' :: k2) (b' :: j2). (w2 p2 q2, Profunctor p2, Profunctor q2, a ~ ('R a' :: COPRODUCT k1 k2), b ~ ('R b' :: COPRODUCT j1 j2)) => p2 s a' -> q2 b' t -> r) -> r Source Github #

Instances

Instances details
(CategoryOf k1, CategoryOf k2, CategoryOf j1, CategoryOf j2, ClosedUnder w1, ClosedUnder w2) => SumRes (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2) (Id :: COPRODUCT k1 k2 -> COPRODUCT k1 k2 -> Type) (Id :: COPRODUCT j1 j2 -> COPRODUCT j1 j2 -> Type) Source Github # 
Instance details

Defined in Proarrow.Optic.Sum

Methods

withSumL :: forall (s :: k1) (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) (t :: j1) r. Id ('L s :: COPRODUCT k1 k2) a -> Id b ('L t :: COPRODUCT j1 j2) -> (forall (p1 :: k1 +-> k1) (q1 :: j1 +-> j1) (a' :: k1) (b' :: j1). (w1 p1 q1, Profunctor p1, Profunctor q1, a ~ ('L a' :: COPRODUCT k1 k2), b ~ ('L b' :: COPRODUCT j1 j2)) => p1 s a' -> q1 b' t -> r) -> r Source Github #

withSumR :: forall (s :: k2) (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) (t :: j2) r. Id ('R s :: COPRODUCT k1 k2) a -> Id b ('R t :: COPRODUCT j1 j2) -> (forall (p2 :: k2 +-> k2) (q2 :: j2 +-> j2) (a' :: k2) (b' :: j2). (w2 p2 q2, Profunctor p2, Profunctor q2, a ~ ('R a' :: COPRODUCT k1 k2), b ~ ('R b' :: COPRODUCT j1 j2)) => p2 s a' -> q2 b' t -> r) -> r Source Github #

(SumRes w1 w2 f f', SumRes w1 w2 g g', ClosedUnder w1, ClosedUnder w2) => SumRes (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2) (f :.: g :: COPRODUCT k1 k2 -> COPRODUCT k1 k2 -> Type) (g' :.: f' :: COPRODUCT j1 j2 -> COPRODUCT j1 j2 -> Type) Source Github # 
Instance details

Defined in Proarrow.Optic.Sum

Methods

withSumL :: forall (s :: k1) (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) (t :: j1) r. (f :.: g) ('L s :: COPRODUCT k1 k2) a -> (g' :.: f') b ('L t :: COPRODUCT j1 j2) -> (forall (p1 :: k1 +-> k1) (q1 :: j1 +-> j1) (a' :: k1) (b' :: j1). (w1 p1 q1, Profunctor p1, Profunctor q1, a ~ ('L a' :: COPRODUCT k1 k2), b ~ ('L b' :: COPRODUCT j1 j2)) => p1 s a' -> q1 b' t -> r) -> r Source Github #

withSumR :: forall (s :: k2) (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2) (t :: j2) r. (f :.: g) ('R s :: COPRODUCT k1 k2) a -> (g' :.: f') b ('R t :: COPRODUCT j1 j2) -> (forall (p2 :: k2 +-> k2) (q2 :: j2 +-> j2) (a' :: k2) (b' :: j2). (w2 p2 q2, Profunctor p2, Profunctor q2, a ~ ('R a' :: COPRODUCT k1 k2), b ~ ('R b' :: COPRODUCT j1 j2)) => p2 s a' -> q2 b' t -> r) -> r Source Github #

(w1 p1 q1, w2 p2 q2, Profunctor p1, Profunctor p2, Profunctor q1, Profunctor q2) => SumRes (w1 :: (j4 +-> j4) -> (j5 +-> j5) -> Constraint) (w2 :: (j6 +-> j6) -> (j7 +-> j7) -> Constraint) (p1 :++: p2 :: COPRODUCT j4 j6 -> COPRODUCT j4 j6 -> Type) (q1 :++: q2 :: COPRODUCT j5 j7 -> COPRODUCT j5 j7 -> Type) Source Github # 
Instance details

Defined in Proarrow.Optic.Sum

Methods

withSumL :: forall (s :: j4) (a :: COPRODUCT j4 j6) (b :: COPRODUCT j5 j7) (t :: j5) r. (p1 :++: p2) ('L s :: COPRODUCT j4 j6) a -> (q1 :++: q2) b ('L t :: COPRODUCT j5 j7) -> (forall (p10 :: j4 +-> j4) (q10 :: j5 +-> j5) (a' :: j4) (b' :: j5). (w1 p10 q10, Profunctor p10, Profunctor q10, a ~ ('L a' :: COPRODUCT j4 j6), b ~ ('L b' :: COPRODUCT j5 j7)) => p10 s a' -> q10 b' t -> r) -> r Source Github #

withSumR :: forall (s :: j6) (a :: COPRODUCT j4 j6) (b :: COPRODUCT j5 j7) (t :: j7) r. (p1 :++: p2) ('R s :: COPRODUCT j4 j6) a -> (q1 :++: q2) b ('R t :: COPRODUCT j5 j7) -> (forall (p20 :: j6 +-> j6) (q20 :: j7 +-> j7) (a' :: j6) (b' :: j7). (w2 p20 q20, Profunctor p20, Profunctor q20, a ~ ('R a' :: COPRODUCT j4 j6), b ~ ('R b' :: COPRODUCT j5 j7)) => p20 s a' -> q20 b' t -> r) -> r Source Github #

injLOptic :: forall {j1} {k1} {j2} {k2} (w2 :: FLAVOR j2 k2) (w1 :: FLAVOR j1 k1) (s :: k1) (t :: j1) (a :: k1) (b :: j1). (CompactFlavor w1, w2 (Id :: k2 -> k2 -> Type) (Id :: j2 -> j2 -> Type), CategoryOf j1, CategoryOf k1, CategoryOf j2, CategoryOf k2) => Optic (Prostrong w1) s t a b -> Optic (Prostrong (SumRes w1 w2)) ('L s :: COPRODUCT k1 k2) ('L t :: COPRODUCT j1 j2) ('L a :: COPRODUCT k1 k2) ('L b :: COPRODUCT j1 j2) Source Github #

injROptic :: forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2) (s :: k2) (t :: j2) (a :: k2) (b :: j2). (CompactFlavor w2, w1 (Id :: k1 -> k1 -> Type) (Id :: j1 -> j1 -> Type), CategoryOf j1, CategoryOf k1, CategoryOf j2, CategoryOf k2) => Optic (Prostrong w2) s t a b -> Optic (Prostrong (SumRes w1 w2)) ('R s :: COPRODUCT k1 k2) ('R t :: COPRODUCT j1 j2) ('R a :: COPRODUCT k1 k2) ('R b :: COPRODUCT j1 j2) Source Github #

withSumOpticL :: forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2) (s :: k1) (t :: j1) (a :: k1) (b :: j1) r. (CategoryOf j1, CategoryOf k1, CategoryOf j2, CategoryOf k2, ClosedUnder w1, ClosedUnder w2, Ob a, Ob b) => Optic (Prostrong (SumRes w1 w2)) ('L s :: COPRODUCT k1 k2) ('L t :: COPRODUCT j1 j2) ('L a :: COPRODUCT k1 k2) ('L b :: COPRODUCT j1 j2) -> (Optic (Prostrong w1) s t a b -> r) -> r Source Github #

The inverse of injLOptic: every SumRes witness of an (L s) (L t) (L a) (L b)-shaped optic actually comes from an underlying w1-flavored optic on s t a b.

withSumOpticR :: forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2) (s :: k2) (t :: j2) (a :: k2) (b :: j2) r. (CategoryOf j1, CategoryOf k1, CategoryOf j2, CategoryOf k2, ClosedUnder w1, ClosedUnder w2, Ob a, Ob b) => Optic (Prostrong (SumRes w1 w2)) ('R s :: COPRODUCT k1 k2) ('R t :: COPRODUCT j1 j2) ('R a :: COPRODUCT k1 k2) ('R b :: COPRODUCT j1 j2) -> (Optic (Prostrong w2) s t a b -> r) -> r Source Github #

The inverse of injROptic.