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

-- | The __getter__ and its mirror the __review__: the one-leg optics @s '~>' a@ ('GetterRes' \/
-- 'getP') and @b '~>' t@ (its 'Flip'). A getter is an affine fold that always succeeds; a review
-- is what remains of a prism's build leg. Build them from a single morphism with 'to' \/ 'unto',
-- and eliminate with 'view' \/ '(^.)' and 'review' \/ '(#)', via the @'Rep'@\/@'Corep'@
-- 'Constant' carriers.
module Proarrow.Optic.Getter where

import Data.Kind (Type)

import Proarrow.Colimit.BinaryCoproduct (Coproduct, HasCoproducts, rgt)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), (\\), type (+->))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts, Product, snd)
import Proarrow.Optic
  ( CompactFlavor
  , ExOptic (..)
  , FLAVOR
  , Flip
  , Optic
  , Optic_ (..)
  , Prostrong (..)
  , SubFlavor (..)
  , ex2prof
  )
import Proarrow.Optic.AffineFold (AffineFoldRes)
import Proarrow.Optic.Fold (FoldRes)
import Proarrow.Profunctor.Corepresentable (Corep (..), corep)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Constant (Constant)
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Instance.Terminal (TerminalProfunctor (..))
import Proarrow.Profunctor.Representable (Rep (..), rep)

type GetterRes :: forall {j} {k}. FLAVOR j k
class (AffineFoldRes p q) => GetterRes (p :: k +-> k) (q :: j +-> j) where
  getP :: p s a -> s ~> a
instance (HasBinaryProducts k, Ob (s :: k)) => GetterRes (Rep (Product s)) (Corep (Product s)) where
  getP :: forall (s :: k) (a :: k). Rep (Product s) s a -> s ~> a
getP @_ @a (Rep s ~> (Product s @ a)
p) = forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @s @a ((s && a) ~> a) -> (s ~> (s && a)) -> s ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (Product s @ a)
s ~> (s && a)
p
instance (CategoryOf k, CategoryOf j) => GetterRes (Id :: k +-> k) (Id :: j +-> j) where
  getP :: forall (s :: k) (a :: k). Id s a -> s ~> a
getP = Id s a -> s ~> a
forall k (a :: k) (b :: k). Id a b -> a ~> b
unId
instance (CategoryOf k, CategoryOf j) => GetterRes (Id :: k +-> k) (TerminalProfunctor :: j +-> j) where
  getP :: forall (s :: k) (a :: k). Id s a -> s ~> a
getP = Id s a -> s ~> a
forall k (a :: k) (b :: k). Id a b -> a ~> b
unId
instance (GetterRes f g, GetterRes f' g') => GetterRes (f :.: f') (g' :.: g) where
  getP :: forall (s :: k) (a :: k). (:.:) f f' s a -> s ~> a
getP (f s b
f :.: f' b a
f') = forall {j} {k} (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
GetterRes p q =>
p s a -> s ~> a
forall (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
GetterRes p q =>
p s a -> s ~> a
getP @f' @g' f' b a
f' (b ~> a) -> (s ~> b) -> s ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {j} {k} (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
GetterRes p q =>
p s a -> s ~> a
forall (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
GetterRes p q =>
p s a -> s ~> a
getP @f @g f s b
f
instance (HasCoproducts k, Ob t) => GetterRes (Corep (Coproduct t) :: k +-> k) (Rep (Coproduct t)) where
  getP :: forall (s :: k) (a :: k). Corep (Coproduct t) s a -> s ~> a
getP (Corep (Coproduct t @ s) ~> a
f) = (Coproduct t @ s) ~> a
(t || s) ~> a
f ((t || s) ~> a) -> (s ~> (t || s)) -> s ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @t

instance CompactFlavor GetterRes
instance CompactFlavor (Flip GetterRes)

instance SubFlavor GetterRes AffineFoldRes where subFlavor :: forall (p :: k +-> k) (q :: j +-> j) r.
GetterRes p q =>
(AffineFoldRes p q => r) -> r
subFlavor AffineFoldRes p q => r
r = r
AffineFoldRes p q => r
r
instance SubFlavor GetterRes FoldRes where subFlavor :: forall (p :: k +-> k) (q :: j +-> j) r.
GetterRes p q =>
(FoldRes p q => r) -> r
subFlavor FoldRes p q => r
r = r
FoldRes p q => r
r

type Getter (s :: k) (t :: j) a b = Optic (Prostrong GetterRes) s t a b

-- | Any flavor whose optics can view has strength for the viewing carrier @'Rep' ('Constant' a)@.
-- This is the bridge that lets the encoding-agnostic 'view' below consume 'Prostrong'-flavored
-- optics; profunctor-class-flavored optics discharge the same @c ('Rep' ('Constant' a))@
-- constraint through the carrier's ordinary class instances instead.
instance
  (CategoryOf j, CategoryOf k, Ob (a :: k), SubFlavor w GetterRes)
  => Prostrong (w :: FLAVOR j k) (Rep (Constant a) :: j +-> k)
  where
  proact :: forall (f :: k +-> k) (g :: j +-> j).
(w f g, Profunctor f, Profunctor g) =>
((f :.: Rep (Constant a)) :.: g) :~> Rep (Constant a)
proact @f @g (f a b
f :.: Rep b ~> (Constant a @ b)
h :.: g b b
g) = forall {j} {k} (w1 :: FLAVOR j k) (w2 :: FLAVOR j k) (p :: k +-> k)
       (q :: j +-> j) r.
(SubFlavor w1 w2, w1 p q) =>
(w2 p q => r) -> r
forall (w1 :: FLAVOR j k) (w2 :: FLAVOR j k) (p :: k +-> k)
       (q :: j +-> j) r.
(SubFlavor w1 w2, w1 p q) =>
(w2 p q => r) -> r
subFlavor @w @GetterRes @f @g ((a ~> (Constant a @ b)) -> Rep (Constant a) a b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (b ~> a
b ~> (Constant a @ b)
h (b ~> a) -> (a ~> b) -> a ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {j} {k} (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
GetterRes p q =>
p s a -> s ~> a
forall (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
GetterRes p q =>
p s a -> s ~> a
getP @f @g f a b
f)) ((Ob b, Ob b) => Rep (Constant a) a b)
-> g b b -> Rep (Constant a) a b
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> g a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ g b b
g

-- | The reviewing dual of the bridge above, over the carrier @'Corep' ('Constant' b)@.
instance
  (CategoryOf j, CategoryOf k, Ob (b :: j), SubFlavor w (Flip GetterRes))
  => Prostrong (w :: FLAVOR j k) (Corep (Constant b) :: j +-> k)
  where
  proact :: forall (f :: k +-> k) (g :: j +-> j).
(w f g, Profunctor f, Profunctor g) =>
((f :.: Corep (Constant b)) :.: g) :~> Corep (Constant b)
proact @f @g (f a b
f :.: Corep (Constant b @ b) ~> b
h :.: g b b
g) = forall {j} {k} (w1 :: FLAVOR j k) (w2 :: FLAVOR j k) (p :: k +-> k)
       (q :: j +-> j) r.
(SubFlavor w1 w2, w1 p q) =>
(w2 p q => r) -> r
forall (w1 :: FLAVOR j k) (w2 :: FLAVOR j k) (p :: k +-> k)
       (q :: j +-> j) r.
(SubFlavor w1 w2, w1 p q) =>
(w2 p q => r) -> r
subFlavor @w @(Flip GetterRes) @f @g (((Constant b @ a) ~> b) -> Corep (Constant b) a b
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep (forall {j} {k} (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
GetterRes p q =>
p s a -> s ~> a
forall (p :: j +-> j) (q :: k +-> k) (s :: j) (a :: j).
GetterRes p q =>
p s a -> s ~> a
getP @g @f g b b
g (b ~> b) -> (b ~> b) -> b ~> b
forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b ~> b
(Constant b @ b) ~> b
h)) ((Ob a, Ob b) => Corep (Constant b) a b)
-> f a b -> Corep (Constant b) a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> f a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ f a b
f

-- | View through any optic that can act as a getter, in either encoding: a 'Prostrong'-flavored
-- optic needs @'SubFlavor' w 'GetterRes'@ (discharged by the bridge instance above), a
-- profunctor-class-flavored optic needs its class to hold for the carrier.
view
  :: forall {j} {k} c (s :: k) (t :: j) a b
   . (CategoryOf j, CategoryOf k, (Ob a) => c (Rep (Constant a)))
  => Optic c s t a b -> s ~> a
view :: forall {j} {k} (c :: (k -> j -> Type) -> Constraint) (s :: k)
       (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, Ob a => c (Rep (Constant a))) =>
Optic c s t a b -> s ~> a
view (Optic forall (p :: j +-> k). c p => p a b -> p s t
l) = Optic_
  (OPT (Rep (Constant a) a b) (Rep (Constant a) s t))
  (OPT (a ~> a) (s ~> a))
-> forall (p :: Type +-> Type).
   Profunctor p =>
   p (Rep (Constant a) a b) (Rep (Constant a) s t)
   -> p (a ~> a) (s ~> a)
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
Optic_ (OPT a b) (OPT s t)
-> forall (p :: j +-> k). c p => p a b -> p s t
unOptic (forall {j} {k} (f :: j +-> k) (a :: k) (b :: j) (a' :: k)
       (b' :: j).
(FunctorForRep f, Ob b) =>
PIso (a ~> (f @ b)) (a' ~> (f @ b')) (Rep f a b) (Rep f a' b')
forall (f :: j +-> k) (a :: k) (b :: j) (a' :: k) (b' :: j).
(FunctorForRep f, Ob b) =>
PIso (a ~> (f @ b)) (a' ~> (f @ b')) (Rep f a b) (Rep f a' b')
rep @(Constant a)) Rep (Constant a) a b -> Rep (Constant a) s t
Rep (Constant a) a b -> Rep (Constant a) s t
forall (p :: j +-> k). c p => p a b -> p s t
l a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

infixl 8 ^.

-- | View the focus of a concrete, @Type@-level optic.
(^.) :: (c (Rep (Constant a))) => s -> Optic c (s :: Type) (t :: Type) a b -> a
s
s ^. :: forall (c :: (Type +-> Type) -> Constraint) a s t b.
c (Rep (Constant a)) =>
s -> Optic c s t a b -> a
^. Optic c s t a b
l = Optic c s t a b -> s ~> a
forall {j} {k} (c :: (k -> j -> Type) -> Constraint) (s :: k)
       (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, Ob a => c (Rep (Constant a))) =>
Optic c s t a b -> s ~> a
view Optic c s t a b
l s
s

to :: forall {k} {j} (s :: k) (t :: j) a b. (CategoryOf k, CategoryOf j, Ob b, Ob t) => (s ~> a) -> Getter s t a b
to :: forall {k} {j} (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf k, CategoryOf j, Ob b, Ob t) =>
(s ~> a) -> Getter s t a b
to s ~> a
sa = ExOptic GetterRes a b s t -> Optic (Prostrong GetterRes) s t a b
forall {j} {k} {w :: FLAVOR j k} (a :: k) (b :: j) (s :: k)
       (t :: j).
(CategoryOf j, CategoryOf k) =>
ExOptic w a b s t -> Optic (Prostrong w) s t a b
ex2prof (forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic w a b) q s t -> ExOptic w a b s t
forall (p :: k +-> k) (q :: j +-> j) (s :: k) (t :: j) (a :: k)
       (b :: j).
(GetterRes p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic GetterRes a b) q s t
-> ExOptic GetterRes a b s t
ExProstrong @Id @TerminalProfunctor ((s ~> a) -> Id s a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id s ~> a
sa Id s a
-> ExOptic GetterRes a b a b
-> (:.:) Id (ExOptic GetterRes a b) s b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (a ~> a) -> (b ~> b) -> ExOptic GetterRes a b a b
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (:.:) Id (ExOptic GetterRes a b) s b
-> TerminalProfunctor b t
-> (:.:) (Id :.: ExOptic GetterRes a b) TerminalProfunctor s t
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: TerminalProfunctor b t
forall {j} {k} (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor)) ((Ob s, Ob a) => Optic (Prostrong GetterRes) s t a b)
-> (s ~> a) -> Optic (Prostrong GetterRes) s t a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ s ~> a
sa

type Review (s :: k) (t :: j) a b = Optic (Prostrong (Flip GetterRes)) s t a b

-- | Review through any optic that can act as a review, in either encoding.
review
  :: forall {j} {k} c (s :: k) (t :: j) a b
   . (CategoryOf j, CategoryOf k, (Ob b) => c (Corep (Constant b)))
  => Optic c s t a b -> b ~> t
review :: forall {j} {k} (c :: (k -> j -> Type) -> Constraint) (s :: k)
       (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, Ob b => c (Corep (Constant b))) =>
Optic c s t a b -> b ~> t
review (Optic forall (p :: j +-> k). c p => p a b -> p s t
l) = Optic_
  (OPT (Corep (Constant b) a b) (Corep (Constant b) s t))
  (OPT (b ~> b) (b ~> t))
-> forall (p :: Type +-> Type).
   Profunctor p =>
   p (Corep (Constant b) a b) (Corep (Constant b) s t)
   -> p (b ~> b) (b ~> t)
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
Optic_ (OPT a b) (OPT s t)
-> forall (p :: j +-> k). c p => p a b -> p s t
unOptic (forall {j} {k} (f :: j +-> k) (a :: j) (b :: k) (a' :: j)
       (b' :: k).
(FunctorForRep f, Ob a) =>
PIso ((f @ a) ~> b) ((f @ a') ~> b') (Corep f a b) (Corep f a' b')
forall (f :: k +-> j) (a :: k) (b :: j) (a' :: k) (b' :: j).
(FunctorForRep f, Ob a) =>
PIso ((f @ a) ~> b) ((f @ a') ~> b') (Corep f a b) (Corep f a' b')
corep @(Constant b)) Corep (Constant b) a b -> Corep (Constant b) s t
Corep (Constant b) a b -> Corep (Constant b) s t
forall (p :: j +-> k). c p => p a b -> p s t
l b ~> b
forall (a :: j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

infixr 8 #

-- | Review through a concrete, @Type@-level optic.
(#) :: (c (Corep (Constant b))) => Optic c (s :: Type) (t :: Type) a b -> b -> t
# :: forall (c :: (Type +-> Type) -> Constraint) b s t a.
c (Corep (Constant b)) =>
Optic c s t a b -> b -> t
(#) = Optic c s t a b -> b ~> t
Optic c s t a b -> b -> t
forall {j} {k} (c :: (k -> j -> Type) -> Constraint) (s :: k)
       (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, Ob b => c (Corep (Constant b))) =>
Optic c s t a b -> b ~> t
review

unto :: forall {k} {j} (s :: k) (t :: j) a b. (CategoryOf k, CategoryOf j, Ob s, Ob a) => (b ~> t) -> Review s t a b
unto :: forall {k} {j} (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf k, CategoryOf j, Ob s, Ob a) =>
(b ~> t) -> Review s t a b
unto b ~> t
bt = ExOptic (Flip GetterRes) a b s t
-> Optic (Prostrong (Flip GetterRes)) s t a b
forall {j} {k} {w :: FLAVOR j k} (a :: k) (b :: j) (s :: k)
       (t :: j).
(CategoryOf j, CategoryOf k) =>
ExOptic w a b s t -> Optic (Prostrong w) s t a b
ex2prof (forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic w a b) q s t -> ExOptic w a b s t
forall (p :: k +-> k) (q :: j +-> j) (s :: k) (t :: j) (a :: k)
       (b :: j).
(Flip GetterRes p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic (Flip GetterRes) a b) q s t
-> ExOptic (Flip GetterRes) a b s t
ExProstrong @TerminalProfunctor @Id (TerminalProfunctor s a
forall {j} {k} (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor TerminalProfunctor s a
-> ExOptic (Flip GetterRes) a b a b
-> (:.:) TerminalProfunctor (ExOptic (Flip GetterRes) a b) s b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (a ~> a) -> (b ~> b) -> ExOptic (Flip GetterRes) a b a b
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (:.:) TerminalProfunctor (ExOptic (Flip GetterRes) a b) s b
-> Id b t
-> (:.:)
     (TerminalProfunctor :.: ExOptic (Flip GetterRes) a b) Id s t
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (b ~> t) -> Id b t
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id b ~> t
bt)) ((Ob b, Ob t) => Optic (Prostrong (Flip GetterRes)) s t a b)
-> (b ~> t) -> Optic (Prostrong (Flip GetterRes)) s t a b
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> t
bt