{-# LANGUAGE AllowAmbiguousTypes #-}

-- from Data.Fold.M of the Folds package
module Proarrow.Profunctor.Fold where

import Data.Kind (Type)
import Prelude qualified as P

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal, swapInner)
import Proarrow.Category.Monoidal.Action (Strong (..), Costrong (..), MonoidalAction (..))
import Proarrow.Category.Monoidal.Applicative (Applicative (..))
import Proarrow.Category.Monoidal.Distributive (distLProd, distRProd)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), (//), type (+->), obj)
import Proarrow.Functor (map)
import Proarrow.Monoid (Monoid (..))
import Proarrow.Object.BinaryCoproduct (COPROD (..), Coprod (..), CoprodAction, HasBinaryCoproducts (..), right)
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..), ProdAction)
import Proarrow.Object.Exponential (BiCCC)
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))
import Proarrow.Promonad (Procomonad (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Identity (Id(..))



data Fold a b where
  Fold :: (Ob m) => (m ~> b) -> (a ~> m) -> (m ** m ~> m) -> (Unit ~> m) -> Fold a b

instance (CategoryOf k) => Profunctor (Fold :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Fold a b -> Fold c d
dimap c ~> a
f b ~> d
g (Fold m ~> b
k a ~> m
h (m ** m) ~> m
m Unit ~> m
z) = (m ~> d) -> (c ~> m) -> ((m ** m) ~> m) -> (Unit ~> m) -> Fold c d
forall {k} (m :: k) (b :: k) (a :: k).
Ob m =>
(m ~> b) -> (a ~> m) -> ((m ** m) ~> m) -> (Unit ~> m) -> Fold a b
Fold (b ~> d
g (b ~> d) -> (m ~> b) -> m ~> d
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. m ~> b
k) (a ~> m
h (a ~> m) -> (c ~> a) -> c ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c ~> a
f) (m ** m) ~> m
m Unit ~> m
z
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> Fold a b -> r
\\ Fold m ~> b
f a ~> m
g (m ** m) ~> m
_ Unit ~> m
_ = r
(Ob a, Ob b) => r
(Ob m, Ob b) => r
r ((Ob m, Ob b) => r) -> (m ~> b) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ m ~> b
f ((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 :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> m
g

instance CategoryOf k => Procomonad (Fold :: k +-> k) where
  extract :: Fold :~> (~>)
extract (Fold m ~> b
f a ~> m
g (m ** m) ~> m
_ Unit ~> m
_) = m ~> b
f (m ~> b) -> (a ~> m) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> m
g
  duplicate :: Fold :~> (Fold :.: Fold)
duplicate (Fold m ~> b
f a ~> m
g (m ** m) ~> m
m Unit ~> m
z) = (m ~> m) -> (a ~> m) -> ((m ** m) ~> m) -> (Unit ~> m) -> Fold a m
forall {k} (m :: k) (b :: k) (a :: k).
Ob m =>
(m ~> b) -> (a ~> m) -> ((m ** m) ~> m) -> (Unit ~> m) -> Fold a b
Fold m ~> m
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id a ~> m
g (m ** m) ~> m
m Unit ~> m
z Fold a m -> Fold m b -> (:.:) Fold Fold a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (m ~> b) -> (m ~> m) -> ((m ** m) ~> m) -> (Unit ~> m) -> Fold m b
forall {k} (m :: k) (b :: k) (a :: k).
Ob m =>
(m ~> b) -> (a ~> m) -> ((m ** m) ~> m) -> (Unit ~> m) -> Fold a b
Fold m ~> b
f m ~> m
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id (m ** m) ~> m
m Unit ~> m
z

instance (SymMonoidal k) => MonoidalProfunctor (Fold :: k +-> k) where
  par0 :: Fold Unit Unit
par0 = (Unit ~> Unit)
-> (Unit ~> Unit)
-> ((Unit ** Unit) ~> Unit)
-> (Unit ~> Unit)
-> Fold Unit Unit
forall {k} (m :: k) (b :: k) (a :: k).
Ob m =>
(m ~> b) -> (a ~> m) -> ((m ** m) ~> m) -> (Unit ~> m) -> Fold a b
Fold Unit ~> Unit
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id Unit ~> Unit
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id (Unit ** Unit) ~> Unit
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor Unit ~> Unit
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  Fold @m m ~> x2
f x1 ~> m
g (m ** m) ~> m
m Unit ~> m
z par :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
Fold x1 x2 -> Fold y1 y2 -> Fold (x1 ** y1) (x2 ** y2)
`par` Fold @n m ~> y2
f' y1 ~> m
g' (m ** m) ~> m
m' Unit ~> m
z' =
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @m @n ((Ob (m ** m) => Fold (x1 ** y1) (x2 ** y2))
 -> Fold (x1 ** y1) (x2 ** y2))
-> (Ob (m ** m) => Fold (x1 ** y1) (x2 ** y2))
-> Fold (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
P.$
      ((m ** m) ~> (x2 ** y2))
-> ((x1 ** y1) ~> (m ** m))
-> (((m ** m) ** (m ** m)) ~> (m ** m))
-> (Unit ~> (m ** m))
-> Fold (x1 ** y1) (x2 ** y2)
forall {k} (m :: k) (b :: k) (a :: k).
Ob m =>
(m ~> b) -> (a ~> m) -> ((m ** m) ~> m) -> (Unit ~> m) -> Fold a b
Fold (m ~> x2
f (m ~> x2) -> (m ~> y2) -> (m ** m) ~> (x2 ** y2)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` m ~> y2
f') (x1 ~> m
g (x1 ~> m) -> (y1 ~> m) -> (x1 ** y1) ~> (m ** m)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` y1 ~> m
g') (((m ** m) ~> m
m ((m ** m) ~> m)
-> ((m ** m) ~> m) -> ((m ** m) ** (m ** m)) ~> (m ** m)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` (m ** m) ~> m
m') (((m ** m) ** (m ** m)) ~> (m ** m))
-> (((m ** m) ** (m ** m)) ~> ((m ** m) ** (m ** m)))
-> ((m ** m) ** (m ** m)) ~> (m ** m)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
swapInner @m @n @m @n) ((Unit ~> m
z (Unit ~> m) -> (Unit ~> m) -> (Unit ** Unit) ~> (m ** m)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` Unit ~> m
z') ((Unit ** Unit) ~> (m ** m))
-> (Unit ~> (Unit ** Unit)) -> Unit ~> (m ** m)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Unit ~> (Unit ** Unit)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv)

instance (CoprodAction k, BiCCC k) => Strong (COPROD k) (Fold :: k +-> k) where
  act :: forall (a :: COPROD k) (b :: COPROD k) (x :: k) (y :: k).
(a ~> b) -> Fold x y -> Fold (Act a x) (Act b y)
act (Coprod @_ @a (Id a1 ~> b1
f)) (Fold @m m ~> y
k x ~> m
h (m ** m) ~> m
m Unit ~> m
z) = a1 ~> b1
f (a1 ~> b1)
-> ((Ob a1, Ob b1) => Fold (Act ('COPR a1) x) (Act ('COPR b1) y))
-> Fold (Act ('COPR a1) x) (Act ('COPR b1) y)
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a @m ((Ob (a1 || m) => Fold (Act ('COPR a1) x) (Act ('COPR b1) y))
 -> Fold (Act ('COPR a1) x) (Act ('COPR b1) y))
-> (Ob (a1 || m) => Fold (Act ('COPR a1) x) (Act ('COPR b1) y))
-> Fold (Act ('COPR a1) x) (Act ('COPR b1) y)
forall a b. (a -> b) -> a -> b
P.$ ((a1 || m) ~> Act ('COPR b1) y)
-> (Act ('COPR a1) x ~> (a1 || m))
-> (((a1 || m) ** (a1 || m)) ~> (a1 || m))
-> (Unit ~> (a1 || m))
-> Fold (Act ('COPR a1) x) (Act ('COPR b1) y)
forall {k} (m :: k) (b :: k) (a :: k).
Ob m =>
(m ~> b) -> (a ~> m) -> ((m ** m) ~> m) -> (Unit ~> m) -> Fold a b
Fold (a1 ~> b1
f (a1 ~> b1) -> (m ~> y) -> (a1 || m) ~> (b1 || y)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryCoproducts k =>
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
+++ m ~> y
k) (forall (c :: k) (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob c) =>
(a ~> b) -> (c || a) ~> (c || b)
forall {k} (c :: k) (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob c) =>
(a ~> b) -> (c || a) ~> (c || b)
right @a x ~> m
h) (((m && m) ~> m) -> ((a1 || m) && (a1 || m)) ~> (a1 || m)
(Ob m, Ob a1, Ob (a1 || m)) =>
((m && m) ~> m) -> ((a1 || m) && (a1 || m)) ~> (a1 || m)
step (m ** m) ~> m
(m && m) ~> m
m) (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @a @m (m ~> (a1 || m))
-> (TerminalObject ~> m) -> TerminalObject ~> (a1 || m)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Unit ~> m
TerminalObject ~> m
z)
    where
      step :: (Ob m, Ob a, Ob (a || m)) => (m && m) ~> m -> (a || m) && (a || m) ~> (a || m)
      step :: (Ob m, Ob a1, Ob (a1 || m)) =>
((m && m) ~> m) -> ((a1 || m) && (a1 || m)) ~> (a1 || m)
step (m && m) ~> m
mult = (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @m (a1 ~> (a1 || m))
-> ((a1 && (a1 || m)) ~> a1) -> (a1 && (a1 || m)) ~> (a1 || m)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO 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) ~> a
fst @k @a @(a || m) ((a1 && (a1 || m)) ~> (a1 || m))
-> ((m && (a1 || m)) ~> (a1 || m))
-> ((a1 && (a1 || m)) || (m && (a1 || m))) ~> (a1 || 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
||| (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @m @a ((m && a1) ~> a1)
-> ((m && m) ~> m) -> ((m && a1) || (m && m)) ~> (a1 || m)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryCoproducts k =>
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
+++ (m && m) ~> m
mult) (((m && a1) || (m && m)) ~> (a1 || m))
-> ((m && (a1 || m)) ~> ((m && a1) || (m && m)))
-> (m && (a1 || m)) ~> (a1 || m)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
forall {k} (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
distLProd @m @a @m) (((a1 && (a1 || m)) || (m && (a1 || m))) ~> (a1 || m))
-> (((a1 || m) && (a1 || m))
    ~> ((a1 && (a1 || m)) || (m && (a1 || m))))
-> ((a1 || m) && (a1 || m)) ~> (a1 || m)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
((a || b) && c) ~> ((a && c) || (b && c))
forall {k} (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
((a || b) && c) ~> ((a && c) || (b && c))
distRProd @a @m @(a || m)

instance (ProdAction k) => Costrong k (Fold :: k +-> k) where
  coact :: forall (a :: k) (x :: k) (y :: k).
(Ob a, Ob x, Ob y) =>
Fold (Act a x) (Act a y) -> Fold x y
coact @a @x @y (Fold m ~> Act a y
f Act a x ~> m
g (m ** m) ~> m
m Unit ~> m
z) = (m ~> y) -> (x ~> m) -> ((m ** m) ~> m) -> (Unit ~> m) -> Fold x y
forall {k} (m :: k) (b :: k) (a :: k).
Ob m =>
(m ~> b) -> (a ~> m) -> ((m ** m) ~> m) -> (Unit ~> m) -> Fold a b
Fold (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @a @y ((a && y) ~> y) -> (m ~> (a && y)) -> m ~> y
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. m ~> Act a y
m ~> (a && y)
f) (Act a x ~> m
g (Act a x ~> m) -> (x ~> Act a x) -> x ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (TerminalObject ~> a)
-> (x ~> x) -> Act TerminalObject x ~> Act a x
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @a @y ((a && y) ~> a)
-> (TerminalObject ~> (a && y)) -> TerminalObject ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. m ~> Act a y
m ~> (a && y)
f (m ~> (a && y))
-> (TerminalObject ~> m) -> TerminalObject ~> (a && y)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Unit ~> m
TerminalObject ~> m
z) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x) (Act TerminalObject x ~> Act a x)
-> (x ~> Act TerminalObject x) -> x ~> Act a x
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall m k (x :: k). (MonoidalAction m k, Ob x) => x ~> Act Unit x
unitorInv @k @k @x) (m ** m) ~> m
m Unit ~> m
z

trav :: (Applicative f) => Fold a b -> Fold (f a) (f b)
trav :: forall {j} {k} (f :: j -> k) (a :: j) (b :: j).
Applicative f =>
Fold a b -> Fold (f a) (f b)
trav (Fold @m m ~> b
k a ~> m
h (m ** m) ~> m
m Unit ~> m
z) = (f m ~> f b)
-> (f a ~> f m)
-> ((f m ** f m) ~> f m)
-> (Unit ~> f m)
-> Fold (f a) (f b)
forall {k} (m :: k) (b :: k) (a :: k).
Ob m =>
(m ~> b) -> (a ~> m) -> ((m ** m) ~> m) -> (Unit ~> m) -> Fold a b
Fold ((m ~> b) -> f m ~> f b
forall (a :: j) (b :: j). (a ~> b) -> f a ~> f b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map m ~> b
k) ((a ~> m) -> f a ~> f m
forall (a :: j) (b :: j). (a ~> b) -> f a ~> f b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map a ~> m
h) (forall {j} {k} (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Applicative f, Ob a, Ob b) =>
((a ** b) ~> c) -> (f a ** f b) ~> f c
forall (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Applicative f, Ob a, Ob b) =>
((a ** b) ~> c) -> (f a ** f b) ~> f c
liftA2 @_ @m @m (m ** m) ~> m
m) ((Unit ~> m) -> Unit ~> f m
forall (a :: j). (Unit ~> a) -> Unit ~> f a
forall {j} {k} (f :: j -> k) (a :: j).
Applicative f =>
(Unit ~> a) -> Unit ~> f a
pure Unit ~> m
z)

instance Corepresentable (Fold :: Type +-> Type) where
  type Fold %% a = [a]
  cotabulate :: forall a b. Ob a => ((Fold %% a) ~> b) -> Fold a b
cotabulate (Fold %% a) ~> b
f = ([a] ~> b)
-> (a ~> [a]) -> (([a] ** [a]) ~> [a]) -> (Unit ~> [a]) -> Fold a b
forall {k} (m :: k) (b :: k) (a :: k).
Ob m =>
(m ~> b) -> (a ~> m) -> ((m ** m) ~> m) -> (Unit ~> m) -> Fold a b
Fold [a] ~> b
(Fold %% a) ~> b
f (a -> [a] -> [a]
forall a. a -> [a] -> [a]
: []) ([a] ** [a]) ~> [a]
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend Unit ~> [a]
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  coindex :: forall a b. Fold a b -> (Fold %% a) ~> b
coindex (Fold m ~> b
f a ~> m
g (m ** m) ~> m
m Unit ~> m
z) [a]
xs = m ~> b
m -> b
f ([a] -> m
go [a]
xs)
    where
      go :: [a] -> m
go [] = Unit ~> m
() -> m
z ()
      go (a
x : [a]
xs') = (m ** m) ~> m
(m, m) -> m
m (a ~> m
a -> m
g a
x, [a] -> m
go [a]
xs')
  corepMap :: forall a b. (a ~> b) -> (Fold %% a) ~> (Fold %% b)
corepMap = (a ~> b) -> [a] ~> [b]
(a ~> b) -> (Fold %% a) ~> (Fold %% b)
forall a b. (a ~> b) -> [a] ~> [b]
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map