{-# 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 ((!))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Sub (SUBCAT (..), Sub (..))
import Proarrow.Category.Monoidal (MonoidalProfunctor (..), SymMonoidal, swap)
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), Strong (..), composeActs, decomposeActs)
import Proarrow.Category.Opposite (OPPOSITE (..))
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 :: Kind -> c -> d -> c -> d -> Type
data Optic m a b s t where
  Optic
    :: forall {c} {d} {m} (x :: m) (x' :: m) a b s t
     . (Ob (a :: c), Ob (b :: d))
    => s ~> (x `Act` a)
    -> x ~> x'
    -> (x' `Act` b) ~> t
    -> Optic m a b s t

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

parallel :: Optic m a b s t -> Optic m' c d u v -> Optic (m, m') '(a, c) '(b, d) '(s, u) '(t, v)
parallel :: forall {k} {k} {k} {k} m (a :: k) (b :: k) (s :: k) (t :: k) m'
       (c :: k) (d :: k) (u :: k) (v :: k).
Optic m a b s t
-> Optic m' c d u v
-> Optic (m, m') '(a, c) '(b, d) '(s, u) '(t, v)
parallel (Optic s ~> Act x a
f x ~> x'
w Act x' b ~> t
g) (Optic u ~> Act x c
h x ~> x'
w' Act x' d ~> v
i) = ('(s, u) ~> Act '(x, x) '(a, c))
-> ('(x, x) ~> '(x', x'))
-> (Act '(x', x') '(b, d) ~> '(t, v))
-> Optic (m, m') '(a, c) '(b, d) '(s, u) '(t, v)
forall {c} {d} {m} (m :: m) (a :: m) (a :: c) (b :: d) (s :: c)
       (t :: d).
(Ob a, Ob b) =>
(s ~> Act m a) -> (m ~> a) -> (Act a b ~> t) -> Optic m 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) (x ~> x'
w (x ~> x') -> (x ~> x') -> (:**:) (~>) (~>) '(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)
:**: 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 m (c :: Kind) (d :: Kind) = OPT c d
type family OptL (p :: OPTIC w c d) where
  OptL (OPT c d) = c
type family OptR (p :: OPTIC w c d) where
  OptR (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 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
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
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 (OptL a) (OptR a) (OptL a) (OptR a)
-> OpticCat (OPT (OptL a) (OptR a)) (OPT (OptL a) (OptR a))
forall m c (a :: c) d (t :: d) (s :: c) (b :: d).
Optic m a t s b -> OpticCat (OPT a t) (OPT s b)
OpticCat (MixedOptic w (OptL a) (OptR a) (OptL a) (OptR a)
-> Optic w (OptL a) (OptR a) (OptL a) (OptR a)
forall {c} {d} m (a :: c) (b :: d) (s :: c) (t :: d).
(MonoidalAction m c, MonoidalAction m d, Ob a, Ob b) =>
MixedOptic m a b s t -> Optic m a b s t
prof2ex p (OptL a) (OptR a) -> p (OptL a) (OptR a)
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
MixedOptic w (OptL a) (OptR a) (OptL a) (OptR 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 c (a :: c) d (t :: d) (s :: c) (b :: d).
Optic m a t s b -> OpticCat (OPT a t) (OPT s b)
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
$ MixedOptic w a b s t -> Optic w a b s t
forall {c} {d} m (a :: c) (b :: d) (s :: c) (t :: d).
(MonoidalAction m c, MonoidalAction m d, Ob a, Ob b) =>
MixedOptic m a b s t -> Optic m a b s t
prof2ex (Optic w a b s t -> MixedOptic w a b s t
forall {k} {k} w (a :: k) (b :: k) (s :: k) (t :: k).
Optic w a b s t -> MixedOptic 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 -> MixedOptic w a b s t
forall {k} {k} w (a :: k) (b :: k) (s :: k) (t :: k).
Optic w a b s t -> MixedOptic 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 (OptL a) (OptR a), Ob (OptL a), Ob (OptR a))

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

ex2prof :: forall w a b s t. Optic w a b s t -> MixedOptic w a b s t
ex2prof :: forall {k} {k} w (a :: k) (b :: k) (s :: k) (t :: k).
Optic w a b s t -> MixedOptic w a b s t
ex2prof (Optic s ~> Act x a
l 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 ((x ~> x') -> p a b -> p (Act x a) (Act x' b)
forall (a :: w) (b :: w) (x :: k) (y :: k).
(a ~> b) -> p x y -> p (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 x ~> x'
w p a b
p)

prof2ex
  :: forall {c} {d} m a b s t
   . (MonoidalAction m c, MonoidalAction m d, Ob a, Ob b)
  => MixedOptic m (a :: c) (b :: d) (s :: c) (t :: d)
  -> Optic m a b s t
prof2ex :: forall {c} {d} m (a :: c) (b :: d) (s :: c) (t :: d).
(MonoidalAction m c, MonoidalAction m d, Ob a, Ob b) =>
MixedOptic m a b s t -> Optic m a b s t
prof2ex MixedOptic m a b s t
p2p = Optic m a b a b -> Optic m a b s t
MixedOptic m a b s t
p2p ((a ~> Act Unit a)
-> (Unit ~> Unit) -> (Act Unit b ~> b) -> Optic m a b a b
forall {c} {d} {m} (m :: m) (a :: m) (a :: c) (b :: d) (s :: c)
       (t :: d).
(Ob a, Ob b) =>
(s ~> Act m a) -> (m ~> a) -> (Act a b ~> t) -> Optic m a b s t
Optic (forall m k (x :: k). (MonoidalAction m k, Ob x) => x ~> Act Unit x
unitorInv @m) 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 Type a b s t -> MixedOptic Type a b s t
forall {k} {k} w (a :: k) (b :: k) (s :: k) (t :: k).
Optic w a b s t -> MixedOptic w a b s t
ex2prof ((s ~> Act s a) -> (s ~> s) -> (Act s b ~> t) -> Optic Type a b s t
forall {c} {d} {m} (m :: m) (a :: m) (a :: c) (b :: d) (s :: c)
       (t :: d).
(Ob a, Ob b) =>
(s ~> Act m a) -> (m ~> a) -> (Act a b ~> t) -> Optic m 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 Type) ('COPR a) ('COPR b) ('COPR s) ('COPR t)
-> MixedOptic (COPROD Type) ('COPR a) ('COPR b) ('COPR s) ('COPR t)
forall {k} {k} w (a :: k) (b :: k) (s :: k) (t :: k).
Optic w a b s t -> MixedOptic w a b s t
ex2prof (('COPR s ~> Act ('COPR t) ('COPR a))
-> ('COPR t ~> 'COPR t)
-> (Act ('COPR t) ('COPR b) ~> 'COPR t)
-> Optic (COPROD Type) ('COPR a) ('COPR b) ('COPR s) ('COPR t)
forall {c} {d} {m} (m :: m) (a :: m) (a :: c) (b :: d) (s :: c)
       (t :: d).
(Ob a, Ob b) =>
(s ~> Act m a) -> (m ~> a) -> (Act a b ~> t) -> Optic m 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 {k} {k} w (a :: k) (b :: k) (s :: k) (t :: k).
Optic w a b s t -> MixedOptic w a b s t
forall w a b s t. Optic w a b s t -> MixedOptic w a b s t
ex2prof @(Type -> Type) ((f a ~> Act (Prelude f) a)
-> (Prelude f ~> Prelude f)
-> (Act (Prelude f) b ~> f b)
-> Optic (Type -> Type) a b (f a) (f b)
forall {c} {d} {m} (m :: m) (a :: m) (a :: c) (b :: d) (s :: c)
       (t :: d).
(Ob a, Ob b) =>
(s ~> Act m a) -> (m ~> a) -> (Act a b ~> t) -> Optic m 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 Prelude f ~> Prelude f
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 {k} {k} w (a :: k) (b :: k) (s :: k) (t :: k).
Optic w a b s t -> MixedOptic w a b s t
forall w a b s t. Optic w a b s t -> MixedOptic w a b s t
ex2prof @(SUBCAT (Algebra m)) ((s ~> Act (SUB (m s)) a)
-> (SUB (m s) ~> SUB (m s))
-> (Act (SUB (m s)) b ~> t)
-> Optic (SUBCAT (Algebra m)) a b s t
forall {c} {d} {m} (m :: m) (a :: m) (a :: c) (b :: d) (s :: c)
       (t :: d).
(Ob a, Ob b) =>
(s ~> Act m a) -> (m ~> a) -> (Act a b ~> t) -> Optic m 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 Type (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 m a t s.
Previewing ('COPR a) ('COPR t) ('COPR m) ('COPR s) -> m -> Maybe a
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 m a t s.
(m -> Maybe a)
-> Previewing ('COPR a) ('COPR t) ('COPR m) ('COPR s)
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 Type) (Previewing a b) where
  act :: forall (a :: COPROD Type) (b :: COPROD Type) (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) = (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 m a t s.
(m -> Maybe a)
-> Previewing ('COPR a) ('COPR t) ('COPR m) ('COPR s)
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 Type (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 m a t s.
(m -> Maybe a)
-> Previewing ('COPR a) ('COPR t) ('COPR m) ('COPR s)
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 m a t s.
Previewing ('COPR a) ('COPR t) ('COPR m) ('COPR s) -> m -> Maybe a
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 m a t s.
(m -> Maybe a)
-> Previewing ('COPR a) ('COPR t) ('COPR m) ('COPR s)
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 Type (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
a -> b
w ((a -> b) -> x -> y
f a -> b
u))
instance Strong (COPROD Type) (Setting a b) where
  act :: forall (a :: COPROD Type) (b :: COPROD Type) x y.
(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} m s (m :: Type -> Type) a (a :: k).
Updating a ('KL m) s ('KL a) -> m -> s -> m a
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} m s (m :: Type -> Type) a (a :: k).
(m -> s -> m a) -> Updating a ('KL m) s ('KL a)
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 Type (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} m s (m :: Type -> Type) a (a :: k).
(m -> s -> m a) -> Updating a ('KL m) s ('KL a)
Update (\b
b (a
a, x
x) -> (a ~> b
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} m s (m :: Type -> Type) a (a :: k).
Updating a ('KL m) s ('KL a) -> m -> s -> m a
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} m s (m :: Type -> Type) a (a :: k).
(m -> s -> m a) -> Updating a ('KL m) s ('KL a)
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 Type (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
a -> b
w ((a -> b) -> x -> y
f a -> b
u))
instance Strong (COPROD Type) (Replacing a b) where
  act :: forall (a :: COPROD Type) (b :: COPROD Type) x y.
(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 (Type -> Type) (Replacing a b) where
  act :: forall (a :: Type -> Type) (b :: Type -> Type) 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
g -> a ~> b
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 (SUBCAT (Algebra m)) (Classifying m a b) where
  act :: forall (a :: SUBCAT (Algebra m)) (b :: SUBCAT (Algebra m)) x y.
(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

-- Charts, a kind of dual to optics.
type IsChart m c d = (IsOptic m c d, SymMonoidal m)

type data CHART m (c :: Kind) (d :: Kind) = CHA c (OPPOSITE d)
type family ChaL (p :: CHART w c d) where
  ChaL (CHA c d) = c
type family ChaR (p :: CHART w c d) where
  ChaR (CHA c d) = d
type ChartCat :: CAT (CHART w c d)
data ChartCat ab st where
  ChartCat :: Optic m a t s b -> ChartCat (CHA a (OP b) :: CHART m c d) (CHA s (OP t))

instance (IsChart m c d) => Profunctor (ChartCat :: CAT (CHART m c d)) where
  dimap :: forall (c :: CHART m c d) (a :: CHART m c d) (b :: CHART m c d)
       (d :: CHART m c d).
(c ~> a) -> (b ~> d) -> ChartCat a b -> ChartCat c d
dimap = (c ~> a) -> (b ~> d) -> ChartCat a b -> ChartCat c d
ChartCat c a -> ChartCat b d -> ChartCat a b -> ChartCat 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 :: CHART m c d) (b :: CHART m c d) r.
((Ob a, Ob b) => r) -> ChartCat a b -> r
\\ ChartCat (Optic s ~> Act x a
f x ~> x'
_ Act x' t ~> b
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
s ~> Act x a
f ((Ob (Act x' t), Ob b) => r) -> (Act x' t ~> 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' t ~> b
Act x' t ~> b
g
instance (IsChart m c d) => Promonad (ChartCat :: CAT (CHART m c d)) where
  id :: forall (a :: CHART m c d). Ob a => ChartCat a a
id = Optic m (ChaL a) (UN 'OP (ChaR a)) (ChaL a) (UN 'OP (ChaR a))
-> ChartCat
     (CHA (ChaL a) ('OP (UN 'OP (ChaR a))))
     (CHA (ChaL a) ('OP (UN 'OP (ChaR a))))
forall m c (a :: c) d (t :: d) (s :: c) (b :: d).
Optic m a t s b -> ChartCat (CHA a ('OP b)) (CHA s ('OP t))
ChartCat (MixedOptic m (ChaL a) (UN 'OP (ChaR a)) (ChaL a) (UN 'OP (ChaR a))
-> Optic m (ChaL a) (UN 'OP (ChaR a)) (ChaL a) (UN 'OP (ChaR a))
forall {c} {d} m (a :: c) (b :: d) (s :: c) (t :: d).
(MonoidalAction m c, MonoidalAction m d, Ob a, Ob b) =>
MixedOptic m a b s t -> Optic m a b s t
prof2ex p (ChaL a) (UN 'OP (ChaR a)) -> p (ChaL a) (UN 'OP (ChaR a))
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
MixedOptic m (ChaL a) (UN 'OP (ChaR a)) (ChaL a) (UN 'OP (ChaR a))
id)
  ChartCat (Optic @x @x' @_ @t s ~> Act x a
ll x ~> x'
lw Act x' t ~> b
lr) . :: forall (b :: CHART m c d) (c :: CHART m c d) (a :: CHART m c d).
ChartCat b c -> ChartCat a b -> ChartCat a c
. ChartCat (Optic @y @y' @a s ~> Act x a
rl x ~> x'
rw Act x' t ~> b
rr) =
    Optic m a t s b -> ChartCat (CHA a ('OP b)) (CHA s ('OP t))
forall m c (a :: c) d (t :: d) (s :: c) (b :: d).
Optic m a t s b -> ChartCat (CHA a ('OP b)) (CHA s ('OP t))
ChartCat (Optic m a t s b -> ChartCat (CHA a ('OP b)) (CHA s ('OP t)))
-> Optic m a t s b -> ChartCat (CHA a ('OP b)) (CHA s ('OP t))
forall a b. (a -> b) -> a -> b
$
      (s ~> Act (x ** x) a)
-> ((x ** x) ~> (x' ** x'))
-> (Act (x' ** x') t ~> b)
-> Optic m a t s b
forall {c} {d} {m} (m :: m) (a :: m) (a :: c) (b :: d) (s :: c)
       (t :: d).
(Ob a, Ob b) =>
(s ~> Act m a) -> (m ~> a) -> (Act a b ~> t) -> Optic m 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 @x @y @a s ~> Act x a
ll a ~> Act x a
s ~> Act x a
rl) (x ~> x'
x ~> x'
lw (x ~> x') -> (x ~> x') -> (x ** x) ~> (x' ** x')
forall (x1 :: m) (x2 :: m) (y1 :: m) (y2 :: m).
(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` x ~> x'
x ~> x'
rw) (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 @y' @x' @t Act x' t ~> b
Act x' t ~> b
lr Act x' b ~> b
Act x' t ~> b
rr (Act (x' ** x') t ~> b)
-> (Act (x' ** x') t ~> Act (x' ** x') t) -> Act (x' ** x') t ~> b
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
. (forall (a :: m) (b :: m).
(SymMonoidal m, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @x' @y' ((x' ** x') ~> (x' ** x'))
-> (t ~> t) -> Act (x' ** x') t ~> Act (x' ** x') t
forall (a :: m) (b :: m) (x :: d) (y :: d).
(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 (a :: d). (CategoryOf d, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @t))
        ((Ob x, Ob x') => Optic m a t s b) -> (x ~> x') -> Optic m a t s b
forall (a :: m) (b :: m) 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
\\ x ~> x'
x ~> x'
lw
        ((Ob x, Ob x') => Optic m a t s b) -> (x ~> x') -> Optic m a t s b
forall (a :: m) (b :: m) 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
\\ x ~> x'
x ~> x'
rw
instance (IsChart m c d) => CategoryOf (CHART m c d) where
  type (~>) = ChartCat
  type Ob a = (a ~ CHA (ChaL a) (ChaR a), Ob (ChaL a), Ob (ChaR a))