{-# LANGUAGE AllowAmbiguousTypes #-}

-- | The __fold__: the weakest read-side optic, reducing the foci to any 'Monoid' object of the
-- category ('FoldRes' \/ 'foldMapP'). It sits at the read-only top of the subtyping lattice --
-- everything that can view, preview or traverse is a fold -- so it has no builder of its own
-- (reach it by 'Proarrow.Optic.convert' from a stronger optic). Its canonical eliminator is
-- 'foldMapOf', via the 'Forget' carrier, with 'unfold' as the 'Proarrow.Optic.re'-mirror that
-- builds from a 'Comonoid' seed.
module Proarrow.Optic.Fold where

import Proarrow.Category.Instance.Opposite (OPPOSITE (..), Op (..), UnOp)
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard (..))
import Proarrow.Category.Monoidal.Distributive
  ( Bicartesian
  , Cotraversable (..)
  , Traversable (..)
  , corepTraverse
  , repTraverse
  )
import Proarrow.Colimit.BinaryCoproduct (Coproduct, HasCoproducts, rgt, (|||))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), (\\), type (+->))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts, Product, snd)
import Proarrow.Monoid (Comonoid, Monoid (..))
import Proarrow.Optic
  ( CompactFlavor
  , FLAVOR
  , OpConstraint
  , Optic
  , Optic_ (..)
  , Prostrong (..)
  , SubFlavor (..)
  , opOptic
  )
import Proarrow.Profunctor.Corepresentable (Corep (..), Corepresentable (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Constant (Constant)
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Instance.Terminal (TerminalProfunctor (..))
import Proarrow.Profunctor.Representable (CorepStar (..), Rep (..), RepCostar, Representable (..))

-- | A fold is a getter or traversal that forgets everything except the ability to reduce the
-- @a@'s it can see into any monoid object of @k@ -- it can never reconstruct a @t@.
type FoldRes :: forall {j} {k}. FLAVOR j k
class (Profunctor p, Profunctor q) => FoldRes (p :: k +-> k) (q :: j +-> j) where
  foldMapP :: (Monoid m) => p s a -> (a ~> m) -> (s ~> m)

instance (HasBinaryProducts k, Ob (s :: k)) => FoldRes (Rep (Product s)) (Corep (Product s)) where
  foldMapP :: forall (m :: k) (s :: k) (a :: k).
Monoid m =>
Rep (Product s) s a -> (a ~> m) -> s ~> m
foldMapP (Rep s ~> (Product s @ a)
p) a ~> m
am = a ~> m
am (a ~> m) -> (s ~> a) -> s ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @s ((s && a) ~> a) -> (s ~> (s && a)) -> s ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (Product s @ a)
s ~> (s && a)
p
instance (CategoryOf k, CategoryOf j) => FoldRes (Id :: k +-> k) (Id :: j +-> j) where
  foldMapP :: forall (m :: k) (s :: k) (a :: k).
Monoid m =>
Id s a -> (a ~> m) -> s ~> m
foldMapP (Id s ~> a
sa) a ~> m
am = a ~> m
am (a ~> m) -> (s ~> a) -> s ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> a
sa
instance (CategoryOf k, CategoryOf j) => FoldRes (Id :: k +-> k) (TerminalProfunctor :: j +-> j) where
  foldMapP :: forall (m :: k) (s :: k) (a :: k).
Monoid m =>
Id s a -> (a ~> m) -> s ~> m
foldMapP (Id s ~> a
sa) a ~> m
am = a ~> m
am (a ~> m) -> (s ~> a) -> s ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> a
sa
instance (FoldRes f g, FoldRes f' g') => FoldRes (f :.: f') (g' :.: g) where
  foldMapP :: forall (m :: k) (s :: k) (a :: k).
Monoid m =>
(:.:) f f' s a -> (a ~> m) -> s ~> m
foldMapP (f s b
f :.: f' b a
f') = forall {j} {k} (p :: k +-> k) (q :: j +-> j) (m :: k) (s :: k)
       (a :: k).
(FoldRes p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
forall (p :: k +-> k) (q :: j +-> j) (m :: k) (s :: k) (a :: k).
(FoldRes p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
foldMapP @f @g f s b
f ((b ~> m) -> s ~> m) -> ((a ~> m) -> b ~> m) -> (a ~> m) -> s ~> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {j} {k} (p :: k +-> k) (q :: j +-> j) (m :: k) (s :: k)
       (a :: k).
(FoldRes p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
forall (p :: k +-> k) (q :: j +-> j) (m :: k) (s :: k) (a :: k).
(FoldRes p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
foldMapP @f' @g' f' b a
f'
instance (Bicartesian k, Traversable t, Representable t) => FoldRes (t :: k +-> k) (RepCostar t) where
  foldMapP :: forall (m :: k) (s :: k) (a :: k).
Monoid m =>
t s a -> (a ~> m) -> s ~> m
foldMapP @m @_ @a t s a
l a ~> m
am = (case forall {k} (t :: k +-> k) (p :: k +-> k) (a :: k) (b :: k).
(Traversable t, Representable t, StrongDistributiveProfunctor p) =>
p a b -> p (t % a) (t % b)
forall (t :: k +-> k) (p :: k +-> k) (a :: k) (b :: k).
(Traversable t, Representable t, StrongDistributiveProfunctor p) =>
p a b -> p (t % a) (t % b)
repTraverse @t @(Rep (Constant m)) (forall (b :: k) (f :: k +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep @a a ~> m
a ~> (Constant m @ a)
am) of Rep (t % a) ~> (Constant m @ (t % a))
sm -> (t % a) ~> m
(t % a) ~> (Constant m @ (t % a))
sm ((t % a) ~> m) -> (s ~> (t % a)) -> s ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. t s a -> s ~> (t % a)
forall (a :: k) (b :: k). t a b -> a ~> (t % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index t s a
l) ((Ob a, Ob m) => s ~> m) -> (a ~> m) -> s ~> m
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> m
am

-- | The corepresentable-cotraversable witness folds by cotraversing at the fold profunctor @'Rep' ('Constant' m)@
-- -- the residual shape is simply discarded.
instance (Bicartesian k, Cotraversable t, Corepresentable t) => FoldRes (CorepStar t) (t :: k +-> k) where
  foldMapP :: forall (m :: k) (s :: k) (a :: k).
Monoid m =>
CorepStar t s a -> (a ~> m) -> s ~> m
foldMapP @m @_ @a (CorepStar s ~> (t %% a)
l) a ~> m
am = (case forall {k} (t :: k +-> k) (p :: k +-> k) (a :: k) (b :: k).
(Cotraversable t, Corepresentable t,
 StrongDistributiveProfunctor p) =>
p a b -> p (t %% a) (t %% b)
forall (t :: k +-> k) (p :: k +-> k) (a :: k) (b :: k).
(Cotraversable t, Corepresentable t,
 StrongDistributiveProfunctor p) =>
p a b -> p (t %% a) (t %% b)
corepTraverse @t @(Rep (Constant m)) (forall (b :: k) (f :: k +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep @a a ~> m
a ~> (Constant m @ a)
am) of Rep (t %% a) ~> (Constant m @ (t %% a))
sm -> (t %% a) ~> m
(t %% a) ~> (Constant m @ (t %% a))
sm ((t %% a) ~> m) -> (s ~> (t %% a)) -> s ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (t %% a)
l) ((Ob a, Ob m) => s ~> m) -> (a ~> m) -> s ~> m
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> m
am

instance (HasCoproducts k, Ob t) => FoldRes (Corep (Coproduct t) :: k +-> k) (Rep (Coproduct t)) where
  foldMapP :: forall (m :: k) (s :: k) (a :: k).
Monoid m =>
Corep (Coproduct t) s a -> (a ~> m) -> s ~> m
foldMapP (Corep (Coproduct t @ s) ~> a
f) a ~> m
am = a ~> m
am (a ~> m) -> (s ~> a) -> s ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Coproduct t @ s) ~> a
(t || s) ~> a
f ((t || s) ~> a) -> (s ~> (t || s)) -> s ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @t
instance (CopyDiscard k, HasCoproducts k, Ob t) => FoldRes (Rep (Coproduct t) :: k +-> k) (Corep (Coproduct t)) where
  foldMapP :: forall (m :: k) (s :: k) (a :: k).
Monoid m =>
Rep (Coproduct t) s a -> (a ~> m) -> s ~> m
foldMapP @m (Rep s ~> (Coproduct t @ a)
p) a ~> m
am = (forall (m :: k). Monoid m => Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty @m (Unit ~> m) -> (t ~> Unit) -> t ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard @k @t (t ~> m) -> (a ~> m) -> (t || a) ~> m
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| a ~> m
am) ((t || a) ~> m) -> (s ~> (t || a)) -> s ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (Coproduct t @ a)
s ~> (t || a)
p

instance CompactFlavor FoldRes

type Fold (s :: k) (t :: j) a b = Optic (Prostrong FoldRes) s t a b

-- | The carrier profunctor for 'foldMapOf': a generalized @s -> m@ (the @Forget@ of the
-- @optics@ library).
type Forget :: forall {j} {k}. k -> j +-> k
data Forget (m :: k) (s :: k) (t :: j) where
  Forget :: (Ob t) => {forall {j} {k} (t :: j) (s :: k) (m :: k). Forget m s t -> s ~> m
unForget :: s ~> m} -> Forget m s t

instance (CategoryOf j, CategoryOf k, Ob (m :: k)) => Profunctor (Forget m :: j +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Forget m a b -> Forget m c d
dimap c ~> a
l b ~> d
r (Forget a ~> m
f) = (c ~> m) -> Forget m c d
forall {j} {k} (t :: j) (s :: k) (m :: k).
Ob t =>
(s ~> m) -> Forget m s t
Forget (a ~> m
f (a ~> m) -> (c ~> a) -> c ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c ~> a
l) ((Ob b, Ob d) => Forget m c d) -> (b ~> d) -> Forget m c d
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> d
r
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> Forget m a b -> r
\\ Forget a ~> m
f = r
(Ob a, Ob b) => r
(Ob a, Ob m) => r
r ((Ob a, Ob m) => r) -> (a ~> m) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> m
f

-- | Any flavor whose optics can fold has strength for the 'Forget' carrier.
instance (CategoryOf j, Monoid m, SubFlavor w FoldRes) => Prostrong (w :: FLAVOR j k) (Forget m :: j +-> k) where
  proact :: forall (f :: k +-> k) (g :: j +-> j).
(w f g, Profunctor f, Profunctor g) =>
((f :.: Forget m) :.: g) :~> Forget m
proact @f @g (f a b
f :.: Forget b ~> m
h :.: g b b
g) = forall {j} {k} (w1 :: FLAVOR j k) (w2 :: FLAVOR j k) (p :: k +-> k)
       (q :: j +-> j) r.
(SubFlavor w1 w2, w1 p q) =>
(w2 p q => r) -> r
forall (w1 :: FLAVOR j k) (w2 :: FLAVOR j k) (p :: k +-> k)
       (q :: j +-> j) r.
(SubFlavor w1 w2, w1 p q) =>
(w2 p q => r) -> r
subFlavor @w @FoldRes @f @g ((a ~> m) -> Forget m a b
forall {j} {k} (t :: j) (s :: k) (m :: k).
Ob t =>
(s ~> m) -> Forget m s t
Forget (forall {j} {k} (p :: k +-> k) (q :: j +-> j) (m :: k) (s :: k)
       (a :: k).
(FoldRes p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
forall (p :: k +-> k) (q :: j +-> j) (m :: k) (s :: k) (a :: k).
(FoldRes p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
foldMapP @f @g f a b
f b ~> m
h)) ((Ob b, Ob b) => Forget m a b) -> g b b -> Forget m a b
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> g a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ g b b
g

-- | Fold through any optic that can act as a fold, in either encoding.
foldMapOf
  :: forall {j} {k} c m (s :: k) (t :: j) a b
   . (CategoryOf j, CategoryOf k, Ob m, c (Forget m))
  => Optic c s t a b -> (a ~> m) -> (s ~> m)
foldMapOf :: forall {j} {k} (c :: (k -> j -> Type) -> Constraint) (m :: k)
       (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, Ob m, c (Forget m)) =>
Optic c s t a b -> (a ~> m) -> s ~> m
foldMapOf (Optic forall (p :: j +-> k). c p => p a b -> p s t
l) a ~> m
am = Forget m s t -> s ~> m
forall {j} {k} (t :: j) (s :: k) (m :: k). Forget m s t -> s ~> m
unForget (forall (p :: j +-> k). c p => p a b -> p s t
l @(Forget m) ((a ~> m) -> Forget m a b
forall {j} {k} (t :: j) (s :: k) (m :: k).
Ob t =>
(s ~> m) -> Forget m s t
Forget a ~> m
a ~> m
am))

-- | The genuine unfold: build @t@ from a 'Comonoid' seed @cm@ through the @b@-foci. It is
-- 'foldMapOf' run in @'OPPOSITE' k@, where 'Monoid' becomes 'Comonoid' and consumption becomes
-- construction. (Inhabitable once the flavor's 'Prostrong' transports through 'OP'.)
unfold
  :: forall {k} c (cm :: k) (s :: k) t a b
   . (Comonoid cm, Ob cm, forall p. (c p) => c (Op (UnOp p)), c (Forget (OP cm)))
  => Optic (OpConstraint c) s t a b -> (cm ~> b) -> (cm ~> t)
unfold :: forall {k} (c :: (OPPOSITE k -> OPPOSITE k -> Type) -> Constraint)
       (cm :: k) (s :: k) (t :: k) (a :: k) (b :: k).
(Comonoid cm, Ob cm,
 forall (p :: OPPOSITE k -> OPPOSITE k -> Type).
 c p =>
 c (Op (UnOp p)),
 c (Forget ('OP cm))) =>
Optic (OpConstraint c) s t a b -> (cm ~> b) -> cm ~> t
unfold Optic (OpConstraint c) s t a b
o cm ~> b
cb = Op (~>) ('OP t) ('OP cm) -> cm ~> t
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
Op p ('OP a) ('OP b) -> p b a
unOp (forall {j} {k} (c :: (k -> j -> Type) -> Constraint) (m :: k)
       (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, Ob m, c (Forget m)) =>
Optic c s t a b -> (a ~> m) -> s ~> m
forall (c :: (OPPOSITE k +-> OPPOSITE k) -> Constraint)
       (m :: OPPOSITE k) (s :: OPPOSITE k) (t :: OPPOSITE k)
       (a :: OPPOSITE k) (b :: OPPOSITE k).
(CategoryOf (OPPOSITE k), CategoryOf (OPPOSITE k), Ob m,
 c (Forget m)) =>
Optic c s t a b -> (a ~> m) -> s ~> m
foldMapOf @c (Optic (OpConstraint c) s t a b
-> Optic c ('OP t) ('OP s) ('OP b) ('OP a)
forall {k1} {k2}
       (c :: (OPPOSITE k1 -> OPPOSITE k2 -> Type) -> Constraint) (s :: k2)
       (t :: k1) (a :: k2) (b :: k1).
(forall (p :: OPPOSITE k1 -> OPPOSITE k2 -> Type).
 c p =>
 c (Op (UnOp p))) =>
Optic (OpConstraint c) s t a b
-> Optic c ('OP t) ('OP s) ('OP b) ('OP a)
opOptic Optic (OpConstraint c) s t a b
o) ((cm ~> b) -> Op (~>) ('OP b) ('OP cm)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op cm ~> b
cb))