{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE IncoherentInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Category.Monoidal.Optic where

import Data.Bifunctor (bimap)
import Data.Kind (Type)
import Prelude (Either, Maybe (..), Monad (..), Traversable, const, either, fmap, fst, snd, uncurry, ($), type (~))

import Proarrow.Category.Instance.Kleisli (KLEISLI (..), Kleisli (..))
import Proarrow.Category.Instance.Nat (Nat (..), (!))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Sub (SUBCAT (..), Sub (..))
import Proarrow.Category.Monoidal (MonoidalProfunctor (..))
import Proarrow.Category.Monoidal.Action (Strong (..), MonoidalAction (..), composeActs, decomposeActs)
import Proarrow.Core (CAT, CategoryOf (..), Kind, PRO, Profunctor (..), Promonad (..), dimapDefault, obj)
import Proarrow.Functor (Prelude (..))
import Proarrow.Object (src, tgt)
import Proarrow.Object.BinaryCoproduct (COPROD (..), Coprod (..))
import Proarrow.Object.BinaryProduct ()
import Proarrow.Profunctor.Star (Star (..))

type Optic :: PRO m m' -> c -> d -> c -> d -> Type
data Optic w a b s t where
  Optic
    :: forall {c} {d} {m} {m'} (x :: m) (x' :: m') a b s t w
     . (Ob (a :: c), Ob (b :: d))
    => s ~> (x `Act` a)
    -> w x x'
    -> (x' `Act` b) ~> t
    -> Optic (w :: PRO m m') a b s t

type IsOptic (w :: PRO m m') c d = (MonoidalProfunctor w, MonoidalAction m c, MonoidalAction m' d)

instance (CategoryOf c, CategoryOf d) => Profunctor (Optic w a b :: PRO c d) where
  dimap :: forall (c :: c) (a :: c) (b :: d) (d :: d).
(c ~> a) -> (b ~> d) -> Optic w a b a b -> Optic w a b c d
dimap c ~> a
l b ~> d
r (Optic a ~> Act x a
f w x x'
w Act x' b ~> b
g) = (c ~> Act x a) -> w x x' -> (Act x' b ~> d) -> Optic w a b c d
forall {c} {d} {m} {m'} (b :: m) (t :: m') (a :: c) (b :: d)
       (s :: c) (t :: d) (w :: PRO m m').
(Ob a, Ob b) =>
(s ~> Act b a) -> w b t -> (Act t b ~> t) -> Optic w a b s t
Optic (a ~> Act x a
f (a ~> Act x a) -> (c ~> a) -> c ~> Act x a
forall (b :: c) (c :: c) (a :: c). (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
l) w x x'
w (b ~> d
r (b ~> d) -> (Act x' b ~> b) -> Act x' b ~> d
forall (b :: d) (c :: d) (a :: d). (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
. Act x' b ~> b
g)
  (Ob a, Ob b) => r
r \\ :: forall (a :: c) (b :: d) r.
((Ob a, Ob b) => r) -> Optic w a b a b -> r
\\ Optic a ~> Act x a
f w x x'
_ Act x' b ~> b
g = r
(Ob a, Ob (Act x a)) => r
(Ob a, Ob b) => r
r ((Ob a, Ob (Act x a)) => r) -> (a ~> Act x a) -> r
forall (a :: c) (b :: c) 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 ~> Act x a
f ((Ob (Act x' b), Ob b) => r) -> (Act x' b ~> b) -> r
forall (a :: d) (b :: d) 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
\\ Act x' b ~> b
g

instance (IsOptic w c d) => Strong (w :: PRO m m') (Optic w a b :: PRO c d) where
  act :: forall (a1 :: m) (b1 :: m') (s :: c) (t :: d). w a1 b1 -> Optic w a b s t -> Optic w a b (Act a1 s) (Act b1 t)
  act :: forall (a :: m) (b :: m') (x :: c) (y :: d).
w a b -> Optic w a b x y -> Optic w a b (Act a x) (Act b y)
act w a1 b1
w (Optic @x @x' s ~> Act x a
f w x x'
w' Act x' b ~> t
g) = (Act a1 s ~> Act (a1 ** x) a)
-> w (a1 ** x) (b1 ** x')
-> (Act (b1 ** x') b ~> Act b1 t)
-> Optic w a b (Act a1 s) (Act b1 t)
forall {c} {d} {m} {m'} (b :: m) (t :: m') (a :: c) (b :: d)
       (s :: c) (t :: d) (w :: PRO m m').
(Ob a, Ob b) =>
(s ~> Act b a) -> w b t -> (Act t b ~> t) -> Optic w a b s t
Optic (forall (x :: m) (y :: m) (c :: c) (a :: c) (b :: c).
(MonoidalAction m c, Ob x, Ob y, Ob c) =>
(a ~> Act x b) -> (b ~> Act y c) -> a ~> Act (x ** y) c
forall {m} {k} (x :: m) (y :: m) (c :: k) (a :: k) (b :: k).
(MonoidalAction m k, Ob x, Ob y, Ob c) =>
(a ~> Act x b) -> (b ~> Act y c) -> a ~> Act (x ** y) c
composeActs @a1 @x @a (w a1 b1 -> a1 ~> a1
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src w a1 b1
w (a1 ~> a1) -> (s ~> s) -> Act a1 s ~> Act a1 s
forall (a :: m) (b :: m) (x :: c) (y :: c).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {m} {m'} {c} {d} (w :: m +-> m') (p :: c +-> d) (a :: m')
       (b :: m) (x :: d) (y :: c).
Strong w p =>
w a b -> p x y -> p (Act a x) (Act b y)
`act` (s ~> Act x a) -> s ~> s
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src s ~> Act x a
f) s ~> Act x a
f) (w a1 b1
w w a1 b1 -> w x x' -> w (a1 ** x) (b1 ** x')
forall (x1 :: m) (x2 :: m') (y1 :: m) (y2 :: m').
w x1 x2 -> w y1 y2 -> w (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` w x x'
w') (forall (x :: m') (y :: m') (c :: d) (a :: d) (b :: d).
(MonoidalAction m' d, Ob x, Ob y, Ob c) =>
(Act y c ~> b) -> (Act x b ~> a) -> Act (x ** y) c ~> a
forall {m} {k} (x :: m) (y :: m) (c :: k) (a :: k) (b :: k).
(MonoidalAction m k, Ob x, Ob y, Ob c) =>
(Act y c ~> b) -> (Act x b ~> a) -> Act (x ** y) c ~> a
decomposeActs @b1 @x' @b Act x' b ~> t
g (w a1 b1 -> b1 ~> b1
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt w a1 b1
w (b1 ~> b1) -> (t ~> t) -> Act b1 t ~> Act b1 t
forall (a :: m') (b :: m') (x :: d) (y :: d).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {m} {m'} {c} {d} (w :: m +-> m') (p :: c +-> d) (a :: m')
       (b :: m) (x :: d) (y :: c).
Strong w p =>
w a b -> p x y -> p (Act a x) (Act b y)
`act` (Act x' b ~> t) -> t ~> t
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt Act x' b ~> t
g)) ((Ob a1, Ob b1) => Optic w a b (Act a1 s) (Act b1 t))
-> w a1 b1 -> Optic w a b (Act a1 s) (Act b1 t)
forall (a :: m) (b :: m') r. ((Ob a, Ob b) => r) -> w 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
\\ w a1 b1
w ((Ob x, Ob x') => Optic w a b (Act a1 s) (Act b1 t))
-> w x x' -> Optic w a b (Act a1 s) (Act b1 t)
forall (a :: m) (b :: m') r. ((Ob a, Ob b) => r) -> w 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
\\ w x x'
w'

parallel :: Optic w a b s t -> Optic w' c d u v -> Optic (w :**: w') '(a, c) '(b, d) '(s, u) '(t, v)
parallel :: forall {k1} {j1} {k} {k} {k2} {j2} {k} {k} (w :: PRO k1 j1)
       (a :: k) (b :: k) (s :: k) (t :: k) (w' :: PRO k2 j2) (c :: k)
       (d :: k) (u :: k) (v :: k).
Optic w a b s t
-> Optic w' c d u v
-> Optic (w :**: w') '(a, c) '(b, d) '(s, u) '(t, v)
parallel (Optic s ~> Act x a
f w x x'
w Act x' b ~> t
g) (Optic u ~> Act x c
h w' x x'
w' Act x' d ~> v
i) = ('(s, u) ~> Act '(x, x) '(a, c))
-> (:**:) w w' '(x, x) '(x', x')
-> (Act '(x', x') '(b, d) ~> '(t, v))
-> Optic (w :**: w') '(a, c) '(b, d) '(s, u) '(t, v)
forall {c} {d} {m} {m'} (b :: m) (t :: m') (a :: c) (b :: d)
       (s :: c) (t :: d) (w :: PRO m m').
(Ob a, Ob b) =>
(s ~> Act b a) -> w b t -> (Act t b ~> t) -> Optic w a b s t
Optic (s ~> Act x a
f (s ~> Act x a)
-> (u ~> Act x c) -> (:**:) (~>) (~>) '(s, u) '(Act x a, Act x c)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: u ~> Act x c
h) (w x x'
w w x x' -> w' x x' -> (:**:) w w' '(x, x) '(x', x')
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: w' x x'
w') (Act x' b ~> t
g (Act x' b ~> t)
-> (Act x' d ~> v)
-> (:**:) (~>) (~>) '(Act x' b, Act x' d) '(t, v)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: Act x' d ~> v
i)

type data OPTIC (w :: PRO m m') (c :: Kind) (d :: Kind) = OPT c d
type family LCat (p :: OPTIC w c d) where
  LCat (OPT c d) = c
type family RCat (p :: OPTIC w c d) where
  RCat (OPT c d) = d
type OpticCat :: CAT (OPTIC w c d)
data OpticCat ab st where
  OpticCat :: Optic w a b s t -> OpticCat (OPT a b :: OPTIC w c d) (OPT s t)

instance (IsOptic w c d) => Profunctor (OpticCat :: CAT (OPTIC w c d)) where
  dimap :: forall (c :: OPTIC w c d) (a :: OPTIC w c d) (b :: OPTIC w c d)
       (d :: OPTIC w c d).
(c ~> a) -> (b ~> d) -> OpticCat a b -> OpticCat c d
dimap = (c ~> a) -> (b ~> d) -> OpticCat a b -> OpticCat c d
OpticCat c a -> OpticCat b d -> OpticCat a b -> OpticCat c d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: OPTIC w c d) (b :: OPTIC w c d) r.
((Ob a, Ob b) => r) -> OpticCat a b -> r
\\ OpticCat (Optic s ~> Act x a
f w x x'
_ Act x' b ~> t
g) = r
(Ob s, Ob (Act x a)) => r
(Ob a, Ob b) => r
r ((Ob s, Ob (Act x a)) => r) -> (s ~> Act x a) -> r
forall (a :: c) (b :: c) 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
\\ s ~> Act x a
f ((Ob (Act x' b), Ob t) => r) -> (Act x' b ~> t) -> r
forall (a :: d) (b :: d) 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
\\ Act x' b ~> t
g
instance (IsOptic w c d) => Promonad (OpticCat :: CAT (OPTIC w c d)) where
  id :: forall (a :: OPTIC w c d). Ob a => OpticCat a a
id = Optic w (LCat a) (RCat a) (LCat a) (RCat a)
-> OpticCat (OPT (LCat a) (RCat a)) (OPT (LCat a) (RCat a))
forall {m} {m'} (w :: PRO m m') c (b :: c) d (t :: d) (b :: c)
       (t :: d).
Optic w b t b t -> OpticCat (OPT b t) (OPT b t)
OpticCat (ProfOptic w (LCat a) (RCat a) (LCat a) (RCat a)
-> Optic w (LCat a) (RCat a) (LCat a) (RCat a)
forall {c} {d} m m' (w :: m' +-> m) (a :: c) (b :: d) (s :: c)
       (t :: d).
(MonoidalProfunctor w, MonoidalAction m c, MonoidalAction m' d,
 Ob a, Ob b) =>
ProfOptic w a b s t -> Optic w a b s t
prof2ex p (LCat a) (RCat a) -> p (LCat a) (RCat a)
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
ProfOptic w (LCat a) (RCat a) (LCat a) (RCat a)
id)
  OpticCat l :: Optic w a b s t
l@Optic{} . :: forall (b :: OPTIC w c d) (c :: OPTIC w c d) (a :: OPTIC w c d).
OpticCat b c -> OpticCat a b -> OpticCat a c
. OpticCat r :: Optic w a b s t
r@Optic{} = Optic w a b s t -> OpticCat (OPT a b) (OPT s t)
forall {m} {m'} (w :: PRO m m') c (b :: c) d (t :: d) (b :: c)
       (t :: d).
Optic w b t b t -> OpticCat (OPT b t) (OPT b t)
OpticCat (Optic w a b s t -> OpticCat (OPT a b) (OPT s t))
-> Optic w a b s t -> OpticCat (OPT a b) (OPT s t)
forall a b. (a -> b) -> a -> b
$ ProfOptic w a b s t -> Optic w a b s t
forall {c} {d} m m' (w :: m' +-> m) (a :: c) (b :: d) (s :: c)
       (t :: d).
(MonoidalProfunctor w, MonoidalAction m c, MonoidalAction m' d,
 Ob a, Ob b) =>
ProfOptic w a b s t -> Optic w a b s t
prof2ex (Optic w a b s t -> ProfOptic w a b s t
forall {m'} {m} {k} {k} (w :: PRO m' m) (a :: k) (b :: k) (s :: k)
       (t :: k).
Optic w a b s t -> ProfOptic w a b s t
ex2prof Optic w a b s t
l (p a b -> p s t) -> (p a b -> p a b) -> p a b -> p s t
forall b c a. (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
. Optic w a b s t -> ProfOptic w a b s t
forall {m'} {m} {k} {k} (w :: PRO m' m) (a :: k) (b :: k) (s :: k)
       (t :: k).
Optic w a b s t -> ProfOptic w a b s t
ex2prof Optic w a b s t
r)
instance (IsOptic w c d) => CategoryOf (OPTIC w c d) where
  type (~>) = OpticCat
  type Ob a = (a ~ OPT (LCat a) (RCat a), Ob (LCat a), Ob (RCat a))

type ProfOptic w a b s t = forall p. (Strong w p) => p a b -> p s t
type MixedOptic m a b s t = ProfOptic ((~>) @m) a b s t

ex2prof :: forall w a b s t. Optic w a b s t -> ProfOptic w a b s t
ex2prof :: forall {m'} {m} {k} {k} (w :: PRO m' m) (a :: k) (b :: k) (s :: k)
       (t :: k).
Optic w a b s t -> ProfOptic w a b s t
ex2prof (Optic s ~> Act x a
l w x x'
w Act x' b ~> t
r) p a b
p = (s ~> Act x a)
-> (Act x' b ~> t) -> p (Act x a) (Act x' b) -> p s t
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap s ~> Act x a
l Act x' b ~> t
r (w x x' -> p a b -> p (Act x a) (Act x' b)
forall (a :: m') (b :: m) (x :: k) (y :: k).
w a b -> p x y -> p (Act a x) (Act b y)
forall {m} {m'} {c} {d} (w :: m +-> m') (p :: c +-> d) (a :: m')
       (b :: m) (x :: d) (y :: c).
Strong w p =>
w a b -> p x y -> p (Act a x) (Act b y)
act w x x'
w p a b
p)

prof2ex
  :: forall {c} {d} m m' w a b s t
   . (MonoidalProfunctor w, MonoidalAction m c, MonoidalAction m' d, Ob a, Ob b)
  => ProfOptic (w :: PRO m m') (a :: c) (b :: d) (s :: c) (t :: d)
  -> Optic w a b s t
prof2ex :: forall {c} {d} m m' (w :: m' +-> m) (a :: c) (b :: d) (s :: c)
       (t :: d).
(MonoidalProfunctor w, MonoidalAction m c, MonoidalAction m' d,
 Ob a, Ob b) =>
ProfOptic w a b s t -> Optic w a b s t
prof2ex ProfOptic w a b s t
p2p = Optic w a b a b -> Optic w a b s t
ProfOptic w a b s t
p2p ((a ~> Act Unit a)
-> w Unit Unit -> (Act Unit b ~> b) -> Optic w a b a b
forall {c} {d} {m} {m'} (b :: m) (t :: m') (a :: c) (b :: d)
       (s :: c) (t :: d) (w :: PRO m m').
(Ob a, Ob b) =>
(s ~> Act b a) -> w b t -> (Act t b ~> t) -> Optic w a b s t
Optic (forall m k (x :: k). (MonoidalAction m k, Ob x) => x ~> Act Unit x
unitorInv @m) w Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0 (forall m k (x :: k). (MonoidalAction m k, Ob x) => Act Unit x ~> x
unitor @m'))

type Lens s t a b = MixedOptic Type a b s t
mkLens :: (s -> a) -> (s -> b -> t) -> Lens s t a b
mkLens :: forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
mkLens s -> a
sa s -> b -> t
sbt = Optic (~>) a b s t -> ProfOptic (~>) a b s t
forall {m'} {m} {k} {k} (w :: PRO m' m) (a :: k) (b :: k) (s :: k)
       (t :: k).
Optic w a b s t -> ProfOptic w a b s t
ex2prof ((s ~> Act s a) -> (s ~> s) -> (Act s b ~> t) -> Optic (~>) a b s t
forall {c} {d} {m} {m'} (b :: m) (t :: m') (a :: c) (b :: d)
       (s :: c) (t :: d) (w :: PRO m m').
(Ob a, Ob b) =>
(s ~> Act b a) -> w b t -> (Act t b ~> t) -> Optic w a b s t
Optic (\s
s -> (s
s, s -> a
sa s
s)) ((s -> a) -> s ~> s
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src s -> a
sa) ((s -> b -> t) -> (s, b) -> t
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry s -> b -> t
sbt))

type Prism s t a b = MixedOptic (COPROD Type) (COPR a) (COPR b) (COPR s) (COPR t)
mkPrism :: (s -> Either t a) -> (b -> t) -> Prism s t a b
mkPrism :: forall s t a b. (s -> Either t a) -> (b -> t) -> Prism s t a b
mkPrism s -> Either t a
sat b -> t
bt = Optic (Coprod (~>)) ('COPR a) ('COPR b) ('COPR s) ('COPR t)
-> ProfOptic (Coprod (~>)) ('COPR a) ('COPR b) ('COPR s) ('COPR t)
forall {m'} {m} {k} {k} (w :: PRO m' m) (a :: k) (b :: k) (s :: k)
       (t :: k).
Optic w a b s t -> ProfOptic w a b s t
ex2prof (('COPR s ~> Act ('COPR t) ('COPR a))
-> Coprod (~>) ('COPR t) ('COPR t)
-> (Act ('COPR t) ('COPR b) ~> 'COPR t)
-> Optic (Coprod (~>)) ('COPR a) ('COPR b) ('COPR s) ('COPR t)
forall {c} {d} {m} {m'} (b :: m) (t :: m') (a :: c) (b :: d)
       (s :: c) (t :: d) (w :: PRO m m').
(Ob a, Ob b) =>
(s ~> Act b a) -> w b t -> (Act t b ~> t) -> Optic w a b s t
Optic ((s -> Either t a) -> Coprod (->) ('COPR s) ('COPR (Either t a))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod s -> Either t a
sat) ((t ~> t) -> Coprod (~>) ('COPR t) ('COPR t)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod ((b -> t) -> t ~> t
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt b -> t
bt)) ((Either t b -> t) -> Coprod (->) ('COPR (Either t b)) ('COPR t)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod ((t -> t) -> (b -> t) -> Either t b -> t
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either t -> t
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id b -> t
bt)))

type Traversal s t a b = MixedOptic (Type -> Type) a b s t
traversing :: (Traversable f) => Traversal (f a) (f b) a b
traversing :: forall (f :: Type -> Type) a b.
Traversable f =>
Traversal (f a) (f b) a b
traversing = forall {m'} {m} {k} {k} (w :: PRO m' m) (a :: k) (b :: k) (s :: k)
       (t :: k).
Optic w a b s t -> ProfOptic w a b s t
forall (w :: PRO (Type -> Type) (Type -> Type)) a b s t.
Optic w a b s t -> ProfOptic w a b s t
ex2prof @((~>) @(Type -> Type)) ((f a ~> Act (Prelude f) a)
-> Nat (Prelude f) (Prelude f)
-> (Act (Prelude f) b ~> f b)
-> Optic Nat a b (f a) (f b)
forall {c} {d} {m} {m'} (b :: m) (t :: m') (a :: c) (b :: d)
       (s :: c) (t :: d) (w :: PRO m m').
(Ob a, Ob b) =>
(s ~> Act b a) -> w b t -> (Act t b ~> t) -> Optic w a b s t
Optic f a ~> Act (Prelude f) a
f a -> Prelude f a
forall {k} (f :: k -> Type) (a :: k). f a -> Prelude f a
Prelude Nat (Prelude f) (Prelude f)
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Type -> Type). Ob a => Nat a a
id Act (Prelude f) b ~> f b
Prelude f b -> f b
forall {k} (f :: k -> Type) (a :: k). Prelude f a -> f a
unPrelude)

class (Monad m) => Algebra m a where algebra :: m a -> a
instance (Monad m) => Algebra m (m a) where algebra :: m (m a) -> m a
algebra = (m (m a) -> (m a -> m a) -> m a
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= m a -> m a
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)
instance (Monad m) => Algebra m () where algebra :: m () -> ()
algebra m ()
_ = ()
instance (Monad m, Algebra m a, Algebra m b) => Algebra m (a, b) where
  algebra :: m (a, b) -> (a, b)
algebra m (a, b)
mab = (m a -> a
forall (m :: Type -> Type) a. Algebra m a => m a -> a
algebra (((a, b) -> a) -> m (a, b) -> m a
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, b) -> a
forall a b. (a, b) -> a
fst m (a, b)
mab), m b -> b
forall (m :: Type -> Type) a. Algebra m a => m a -> a
algebra (((a, b) -> b) -> m (a, b) -> m b
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, b) -> b
forall a b. (a, b) -> b
snd m (a, b)
mab))

type AlgebraicLens m s t a b = MixedOptic (SUBCAT (Algebra m)) a b s t
mkAlgebraicLens :: forall m s t a b. (Monad m) => (s -> a) -> (m s -> b -> t) -> AlgebraicLens m s t a b
mkAlgebraicLens :: forall (m :: Type -> Type) s t a b.
Monad m =>
(s -> a) -> (m s -> b -> t) -> AlgebraicLens m s t a b
mkAlgebraicLens s -> a
v m s -> b -> t
u = forall {m'} {m} {k} {k} (w :: PRO m' m) (a :: k) (b :: k) (s :: k)
       (t :: k).
Optic w a b s t -> ProfOptic w a b s t
forall (w :: PRO (SUBCAT (Algebra m)) (SUBCAT (Algebra m))) a b s
       t.
Optic w a b s t -> ProfOptic w a b s t
ex2prof @((~>) @(SUBCAT (Algebra m))) ((s ~> Act (SUB (m s)) a)
-> Sub (->) (SUB (m s)) (SUB (m s))
-> (Act (SUB (m s)) b ~> t)
-> Optic (Sub (->)) a b s t
forall {c} {d} {m} {m'} (b :: m) (t :: m') (a :: c) (b :: d)
       (s :: c) (t :: d) (w :: PRO m m').
(Ob a, Ob b) =>
(s ~> Act b a) -> w b t -> (Act t b ~> t) -> Optic w a b s t
Optic (\s
s -> (forall (m :: Type -> Type) a. Monad m => a -> m a
return @m s
s, s -> a
v s
s)) ((m s -> m s) -> Sub (->) (SUB (m s)) (SUB (m s))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub Obj (m s)
m s -> m s
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj) ((m s -> b -> t) -> (m s, b) -> t
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry m s -> b -> t
u))

newtype Viewing a (b :: Type) s (t :: Type) = Viewing {forall a b s t. Viewing a b s t -> s -> a
unView :: s -> a}
instance Profunctor (Viewing a b) where
  dimap :: forall c a b d.
(c ~> a) -> (b ~> d) -> Viewing a b a b -> Viewing a b c d
dimap c ~> a
l b ~> d
_ (Viewing a -> a
f) = (c -> a) -> Viewing a b c d
forall a b s t. (s -> a) -> Viewing a b s t
Viewing (a -> a
f (a -> a) -> (c -> a) -> c -> a
forall b c a. (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
c -> a
l)
instance Strong (->) (Viewing a b) where
  act :: forall a b x y.
(a -> b) -> Viewing a b x y -> Viewing a b (Act a x) (Act b y)
act a -> b
_ (Viewing x -> a
f) = ((a, x) -> a) -> Viewing a b (a, x) (b, y)
forall a b s t. (s -> a) -> Viewing a b s t
Viewing (x -> a
f (x -> a) -> ((a, x) -> x) -> (a, x) -> a
forall b c a. (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, x) -> x
forall a b. (a, b) -> b
snd)

infixl 8 ^.
(^.) :: s -> (Viewing a b a b -> Viewing a b s t) -> a
^. :: forall s a b t. s -> (Viewing a b a b -> Viewing a b s t) -> a
(^.) s
s Viewing a b a b -> Viewing a b s t
l = Viewing a b s t -> s -> a
forall a b s t. Viewing a b s t -> s -> a
unView (Viewing a b a b -> Viewing a b s t
l (Viewing a b a b -> Viewing a b s t)
-> Viewing a b a b -> Viewing a b s t
forall a b. (a -> b) -> a -> b
$ (a -> a) -> Viewing a b a b
forall a b s t. (s -> a) -> Viewing a b s t
Viewing a -> a
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id) s
s

data Previewing a (b :: COPROD Type) s (t :: COPROD Type) where
  Previewing :: {forall b t b t.
Previewing ('COPR t) ('COPR b) ('COPR b) ('COPR t) -> b -> Maybe t
unPreview :: s -> Maybe a} -> Previewing (COPR a) (COPR b) (COPR s) (COPR t)
instance Profunctor (Previewing a b) where
  dimap :: forall (c :: COPROD Type) (a :: COPROD Type) (b :: COPROD Type)
       (d :: COPROD Type).
(c ~> a) -> (b ~> d) -> Previewing a b a b -> Previewing a b c d
dimap (Coprod a1 -> b1
l) Coprod{} (Previewing s -> Maybe a
f) = (a1 -> Maybe a)
-> Previewing ('COPR a) ('COPR b) ('COPR a1) ('COPR b1)
forall b t b t.
(b -> Maybe t)
-> Previewing ('COPR t) ('COPR b) ('COPR b) ('COPR t)
Previewing (b1 -> Maybe a
s -> Maybe a
f (b1 -> Maybe a) -> (a1 -> b1) -> a1 -> Maybe a
forall b c a. (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
. a1 -> b1
l)
  (Ob a, Ob b) => r
r \\ :: forall (a :: COPROD Type) (b :: COPROD Type) r.
((Ob a, Ob b) => r) -> Previewing a b a b -> r
\\ Previewing s -> Maybe a
f = r
(Ob s, Ob (Maybe a)) => r
(Ob a, Ob b) => r
r ((Ob s, Ob (Maybe a)) => r) -> (s -> Maybe a) -> r
forall a b 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
\\ s -> Maybe a
f
instance Strong (Coprod (->)) (Previewing a b) where
  act :: forall (a :: COPROD Type) (b :: COPROD Type) (x :: COPROD Type)
       (y :: COPROD Type).
Coprod (->) a b
-> Previewing a b x y -> Previewing a b (Act a x) (Act b y)
act Coprod (->) a b
_ (Previewing s -> Maybe a
f) = (Either (UN 'COPR a) s -> Maybe a)
-> Previewing
     ('COPR a)
     ('COPR b)
     ('COPR (Either (UN 'COPR a) s))
     ('COPR (Either (UN 'COPR b) t))
forall b t b t.
(b -> Maybe t)
-> Previewing ('COPR t) ('COPR b) ('COPR b) ('COPR t)
Previewing ((UN 'COPR a -> Maybe a)
-> (s -> Maybe a) -> Either (UN 'COPR a) s -> Maybe a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe a -> UN 'COPR a -> Maybe a
forall a b. a -> b -> a
const Maybe a
forall a. Maybe a
Nothing) s -> Maybe a
f)
instance Strong (->) (Previewing a b) where
  act :: forall a b (x :: COPROD Type) (y :: COPROD Type).
(a -> b)
-> Previewing a b x y -> Previewing a b (Act a x) (Act b y)
act a -> b
_ (Previewing s -> Maybe a
f) = ((a, s) -> Maybe a)
-> Previewing ('COPR a) ('COPR b) ('COPR (a, s)) ('COPR (b, t))
forall b t b t.
(b -> Maybe t)
-> Previewing ('COPR t) ('COPR b) ('COPR b) ('COPR t)
Previewing (s -> Maybe a
f (s -> Maybe a) -> ((a, s) -> s) -> (a, s) -> Maybe a
forall b c a. (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, s) -> s
forall a b. (a, b) -> b
snd)

infixl 8 ?.
(?.)
  :: s -> (Previewing (COPR a) (COPR b) (COPR a) (COPR b) -> Previewing (COPR a) (COPR b) (COPR s) (COPR t)) -> Maybe a
?. :: forall s a b t.
s
-> (Previewing ('COPR a) ('COPR b) ('COPR a) ('COPR b)
    -> Previewing ('COPR a) ('COPR b) ('COPR s) ('COPR t))
-> Maybe a
(?.) s
s Previewing ('COPR a) ('COPR b) ('COPR a) ('COPR b)
-> Previewing ('COPR a) ('COPR b) ('COPR s) ('COPR t)
l = Previewing ('COPR a) ('COPR b) ('COPR s) ('COPR t) -> s -> Maybe a
forall b t b t.
Previewing ('COPR t) ('COPR b) ('COPR b) ('COPR t) -> b -> Maybe t
unPreview (Previewing ('COPR a) ('COPR b) ('COPR a) ('COPR b)
-> Previewing ('COPR a) ('COPR b) ('COPR s) ('COPR t)
l (Previewing ('COPR a) ('COPR b) ('COPR a) ('COPR b)
 -> Previewing ('COPR a) ('COPR b) ('COPR s) ('COPR t))
-> Previewing ('COPR a) ('COPR b) ('COPR a) ('COPR b)
-> Previewing ('COPR a) ('COPR b) ('COPR s) ('COPR t)
forall a b. (a -> b) -> a -> b
$ (a -> Maybe a)
-> Previewing ('COPR a) ('COPR b) ('COPR a) ('COPR b)
forall b t b t.
(b -> Maybe t)
-> Previewing ('COPR t) ('COPR b) ('COPR b) ('COPR t)
Previewing a -> Maybe a
forall a. a -> Maybe a
Just) s
s

newtype Setting a b s t = Setting {forall a b s t. Setting a b s t -> (a -> b) -> s -> t
unSet :: (a -> b) -> (s -> t)}
instance Profunctor (Setting a b) where
  dimap :: forall c a b d.
(c ~> a) -> (b ~> d) -> Setting a b a b -> Setting a b c d
dimap c ~> a
l b ~> d
r (Setting (a -> b) -> a -> b
f) = ((a -> b) -> c -> d) -> Setting a b c d
forall a b s t. ((a -> b) -> s -> t) -> Setting a b s t
Setting (\a -> b
u -> b ~> d
b -> d
r (b -> d) -> (c -> b) -> c -> d
forall b c a. (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 -> b) -> a -> b
f a -> b
u (a -> b) -> (c -> a) -> c -> b
forall b c a. (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
c -> a
l)
instance Strong (->) (Setting a b) where
  act :: forall a b x y.
(a -> b) -> Setting a b x y -> Setting a b (Act a x) (Act b y)
act a -> b
w (Setting (a -> b) -> x -> y
f) = ((a -> b) -> (a, x) -> (b, y)) -> Setting a b (a, x) (b, y)
forall a b s t. ((a -> b) -> s -> t) -> Setting a b s t
Setting (\a -> b
u -> (a -> b) -> (x -> y) -> (a, x) -> (b, y)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: Type -> Type -> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> b
w ((a -> b) -> x -> y
f a -> b
u))
instance Strong (Coprod (->)) (Setting a b) where
  act :: forall (a :: COPROD Type) (b :: COPROD Type) x y.
Coprod (->) a b
-> Setting a b x y -> Setting a b (Act a x) (Act b y)
act (Coprod a1 -> b1
w) (Setting (a -> b) -> x -> y
f) = ((a -> b) -> Either a1 x -> Either b1 y)
-> Setting a b (Either a1 x) (Either b1 y)
forall a b s t. ((a -> b) -> s -> t) -> Setting a b s t
Setting (\a -> b
u -> (a1 -> b1) -> (x -> y) -> Either a1 x -> Either b1 y
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: Type -> Type -> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a1 -> b1
w ((a -> b) -> x -> y
f a -> b
u))

infixl 8 .~
(.~) :: (Setting a b a b -> Setting a b s t) -> b -> s -> t
.~ :: forall a b s t. (Setting a b a b -> Setting a b s t) -> b -> s -> t
(.~) Setting a b a b -> Setting a b s t
l b
b = Setting a b s t -> (a -> b) -> s -> t
forall a b s t. Setting a b s t -> (a -> b) -> s -> t
unSet (Setting a b a b -> Setting a b s t
l (Setting a b a b -> Setting a b s t)
-> Setting a b a b -> Setting a b s t
forall a b. (a -> b) -> a -> b
$ ((a -> b) -> a -> b) -> Setting a b a b
forall a b s t. ((a -> b) -> s -> t) -> Setting a b s t
Setting (a -> b) -> a -> b
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id) (b -> a -> b
forall a b. a -> b -> a
const b
b)

type KlCat m = KLEISLI (Star (Prelude m))
data Updating a b s t where
  Update :: {forall {k} b s (m :: Type -> Type) t (a :: k).
Updating a ('KL b) s ('KL t) -> b -> s -> m t
unUpdate :: b -> s -> m t} -> Updating a (KL b :: KlCat m) s (KL t :: KlCat m)
instance (Monad m) => Profunctor (Updating a b :: PRO Type (KlCat m)) where
  dimap :: forall c a (b :: KlCat m) (d :: KlCat m).
(c ~> a) -> (b ~> d) -> Updating a b a b -> Updating a b c d
dimap c ~> a
l (Kleisli (Star a1 ~> Prelude m b1
r)) (Update b -> a -> m t
u) = (b -> c -> m b1) -> Updating a ('KL b) c ('KL b1)
forall {k} b s (m :: Type -> Type) t (a :: k).
(b -> s -> m t) -> Updating a ('KL b) s ('KL t)
Update (\b
b c
x -> b -> a -> m t
u b
b (c ~> a
c -> a
l c
x) m t -> (t -> m b1) -> m b1
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Prelude m b1 -> m b1
forall {k} (f :: k -> Type) (a :: k). Prelude f a -> f a
unPrelude (Prelude m b1 -> m b1) -> (a1 -> Prelude m b1) -> a1 -> m b1
forall b c a. (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
. a1 ~> Prelude m b1
a1 -> Prelude m b1
r)
  (Ob a, Ob b) => r
r \\ :: forall a (b :: KlCat m) r.
((Ob a, Ob b) => r) -> Updating a b a b -> r
\\ Update b -> a -> m t
u = r
(Ob a, Ob b) => r
(Ob b, Ob (a -> m t)) => r
r ((Ob b, Ob (a -> m t)) => r) -> (b -> a -> m t) -> r
forall a b 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
\\ b -> a -> m t
u
instance (Monad m) => Strong (->) (Updating a b :: PRO Type (KlCat m)) where
  act :: forall a b x (y :: KlCat m).
(a -> b) -> Updating a b x y -> Updating a b (Act a x) (Act b y)
act a -> b
f (Update b -> x -> m t
u) = (b -> (a, x) -> m (b, t)) -> Updating a ('KL b) (a, x) ('KL (b, t))
forall {k} b s (m :: Type -> Type) t (a :: k).
(b -> s -> m t) -> Updating a ('KL b) s ('KL t)
Update (\b
b (a
a, x
x) -> (a -> b
f a
a,) (t -> (b, t)) -> m t -> m (b, t)
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
`fmap` b -> x -> m t
u b
b x
x)

mupdate
  :: (Monad m)
  => (Updating a (KL b :: KlCat m) a (KL b :: KlCat m) -> Updating a (KL b :: KlCat m) s (KL t :: KlCat m))
  -> b
  -> s
  -> m t
mupdate :: forall (m :: Type -> Type) a b s t.
Monad m =>
(Updating a ('KL b) a ('KL b) -> Updating a ('KL b) s ('KL t))
-> b -> s -> m t
mupdate Updating a ('KL b) a ('KL b) -> Updating a ('KL b) s ('KL t)
f = Updating a ('KL b) s ('KL t) -> b -> s -> m t
forall {k} b s (m :: Type -> Type) t (a :: k).
Updating a ('KL b) s ('KL t) -> b -> s -> m t
unUpdate (Updating a ('KL b) s ('KL t) -> b -> s -> m t)
-> Updating a ('KL b) s ('KL t) -> b -> s -> m t
forall a b. (a -> b) -> a -> b
$ Updating a ('KL b) a ('KL b) -> Updating a ('KL b) s ('KL t)
f ((b -> a -> m b) -> Updating a ('KL b) a ('KL b)
forall {k} b s (m :: Type -> Type) t (a :: k).
(b -> s -> m t) -> Updating a ('KL b) s ('KL t)
Update (\b
b a
_ -> b -> m b
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return b
b))

newtype Replacing a b s t = Replace {forall a b s t. Replacing a b s t -> (a -> b) -> s -> t
unReplace :: (a -> b) -> (s -> t)}
instance Profunctor (Replacing a b) where
  dimap :: forall c a b d.
(c ~> a) -> (b ~> d) -> Replacing a b a b -> Replacing a b c d
dimap c ~> a
l b ~> d
r (Replace (a -> b) -> a -> b
f) = ((a -> b) -> c -> d) -> Replacing a b c d
forall a b s t. ((a -> b) -> s -> t) -> Replacing a b s t
Replace (\a -> b
ab -> b ~> d
b -> d
r (b -> d) -> (c -> b) -> c -> d
forall b c a. (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 -> b) -> a -> b
f a -> b
ab (a -> b) -> (c -> a) -> c -> b
forall b c a. (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
c -> a
l)
instance Strong (->) (Replacing a b) where
  act :: forall a b x y.
(a -> b) -> Replacing a b x y -> Replacing a b (Act a x) (Act b y)
act a -> b
w (Replace (a -> b) -> x -> y
f) = ((a -> b) -> (a, x) -> (b, y)) -> Replacing a b (a, x) (b, y)
forall a b s t. ((a -> b) -> s -> t) -> Replacing a b s t
Replace (\a -> b
u -> (a -> b) -> (x -> y) -> (a, x) -> (b, y)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: Type -> Type -> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> b
w ((a -> b) -> x -> y
f a -> b
u))
instance Strong (Coprod (->)) (Replacing a b) where
  act :: forall (a :: COPROD Type) (b :: COPROD Type) x y.
Coprod (->) a b
-> Replacing a b x y -> Replacing a b (Act a x) (Act b y)
act (Coprod a1 -> b1
w) (Replace (a -> b) -> x -> y
f) = ((a -> b) -> Either a1 x -> Either b1 y)
-> Replacing a b (Either a1 x) (Either b1 y)
forall a b s t. ((a -> b) -> s -> t) -> Replacing a b s t
Replace (\a -> b
u -> (a1 -> b1) -> (x -> y) -> Either a1 x -> Either b1 y
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: Type -> Type -> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a1 -> b1
w ((a -> b) -> x -> y
f a -> b
u))
instance Strong (Nat :: CAT (Type -> Type)) (Replacing a b) where
  act :: forall (a :: Type -> Type) (b :: Type -> Type) x y.
Nat a b -> Replacing a b x y -> Replacing a b (Act a x) (Act b y)
act Nat a b
w (Replace (a -> b) -> x -> y
f) = ((a -> b) -> a x -> b y) -> Replacing a b (a x) (b y)
forall a b s t. ((a -> b) -> s -> t) -> Replacing a b s t
Replace (\a -> b
g -> Nat a b
w Nat a b -> (x ~> y) -> a x ~> b y
forall {j} {k} (f :: j -> k) (g :: j -> k) (a :: j) (b :: j).
Nat f g -> (a ~> b) -> f a ~> g b
! (a -> b) -> x -> y
f a -> b
g)

infixl 8 %~
(%~) :: (Replacing a b a b -> Replacing a b s t) -> (a -> b) -> (s -> t)
%~ :: forall a b s t.
(Replacing a b a b -> Replacing a b s t) -> (a -> b) -> s -> t
(%~) Replacing a b a b -> Replacing a b s t
l = Replacing a b s t -> (a -> b) -> s -> t
forall a b s t. Replacing a b s t -> (a -> b) -> s -> t
unReplace (Replacing a b a b -> Replacing a b s t
l (Replacing a b a b -> Replacing a b s t)
-> Replacing a b a b -> Replacing a b s t
forall a b. (a -> b) -> a -> b
$ ((a -> b) -> a -> b) -> Replacing a b a b
forall a b s t. ((a -> b) -> s -> t) -> Replacing a b s t
Replace (a -> b) -> a -> b
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)

newtype Classifying m a b s t = Classifying
  {forall {k} (m :: Type -> Type) (a :: k) b s t.
Classifying m a b s t -> Monad m => m s -> b -> t
unClassify :: (Monad m) => m s -> b -> t}
instance (Monad m) => Profunctor (Classifying m a b) where
  dimap :: forall c a b d.
(c ~> a)
-> (b ~> d) -> Classifying m a b a b -> Classifying m a b c d
dimap c ~> a
l b ~> d
r (Classifying Monad m => m a -> b -> b
f) = (Monad m => m c -> b -> d) -> Classifying m a b c d
forall {k} (m :: Type -> Type) (a :: k) b s t.
(Monad m => m s -> b -> t) -> Classifying m a b s t
Classifying (\m c
u -> b ~> d
b -> d
r (b -> d) -> (b -> b) -> b -> d
forall b c a. (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 a -> b -> b
Monad m => m a -> b -> b
f ((c -> a) -> m c -> m a
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap c ~> a
c -> a
l m c
u))
instance (Monad m) => Strong (Sub (->) :: CAT (SUBCAT (Algebra m))) (Classifying m a b) where
  act :: forall (a :: SUBCAT (Algebra m)) (b :: SUBCAT (Algebra m)) x y.
Sub (->) a b
-> Classifying m a b x y -> Classifying m a b (Act a x) (Act b y)
act (Sub a1 -> b1
w) (Classifying Monad m => m x -> b -> y
f) = (Monad m => m (a1, x) -> b -> (b1, y))
-> Classifying m a b (a1, x) (b1, y)
forall {k} (m :: Type -> Type) (a :: k) b s t.
(Monad m => m s -> b -> t) -> Classifying m a b s t
Classifying (\m (a1, x)
m b
b -> (m b1 -> b1
forall (m :: Type -> Type) a. Algebra m a => m a -> a
algebra (((a1, x) -> b1) -> m (a1, x) -> m b1
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (a1 -> b1
w (a1 -> b1) -> ((a1, x) -> a1) -> (a1, x) -> b1
forall b c a. (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
. (a1, x) -> a1
forall a b. (a, b) -> a
fst) m (a1, x)
m), m x -> b -> y
Monad m => m x -> b -> y
f (((a1, x) -> x) -> m (a1, x) -> m x
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (a1, x) -> x
forall a b. (a, b) -> b
snd m (a1, x)
m) b
b))

infixl 8 .?
(.?) :: (Monad m) => (Classifying m a b a b -> Classifying m a b s t) -> b -> m s -> t
.? :: forall (m :: Type -> Type) a b s t.
Monad m =>
(Classifying m a b a b -> Classifying m a b s t) -> b -> m s -> t
(.?) Classifying m a b a b -> Classifying m a b s t
l b
b m s
ms = Classifying m a b s t -> Monad m => m s -> b -> t
forall {k} (m :: Type -> Type) (a :: k) b s t.
Classifying m a b s t -> Monad m => m s -> b -> t
unClassify (Classifying m a b a b -> Classifying m a b s t
l (Classifying m a b a b -> Classifying m a b s t)
-> Classifying m a b a b -> Classifying m a b s t
forall a b. (a -> b) -> a -> b
$ (Monad m => m a -> b -> b) -> Classifying m a b a b
forall {k} (m :: Type -> Type) (a :: k) b s t.
(Monad m => m s -> b -> t) -> Classifying m a b s t
Classifying ((b -> b) -> m a -> b -> b
forall a b. a -> b -> a
const b -> b
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)) m s
ms b
b