proarrow
Safe HaskellNone
LanguageGHC2024

Proarrow.Optic.Sum

Description

Dual to ProdFl: combine over the coproduct of two categories via :++:. It has its own module because Proarrow.Category.Instance.Coproduct already imports Proarrow.Optic transitively.

It does not combine two different optics into one: an (p :++: q) (L a) (L b) only ever holds a p. It lets any w1- or w2-flavored optic be injected into a shared SumFl w1 w2, the unused side witnessed by Id (demanded via Flavor).

Synopsis

Documentation

class SumFl (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 ProdFl, a SumFl witness can be decomposed back. 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. So the :.: case can recurse: the existential "middle" object introduced there is 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, Flavor w1, Flavor w2) => SumFl (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 #

(SumFl w1 w2 f f', SumFl w1 w2 g g', Flavor w1, Flavor w2) => SumFl (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) => SumFl (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). (Flavor 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 (SumFl 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). (Flavor 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 (SumFl 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, Flavor w1, Flavor w2, Ob a, Ob b) => Optic (Prostrong (SumFl 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 SumFl 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, Flavor w1, Flavor w2, Ob a, Ob b) => Optic (Prostrong (SumFl 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.