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

-- | The __getter__ and its mirror the __review__: the one-leg optics @s '~>' a@ ('GetterFl' \/
-- '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 generic 'ExOptic' carrier.
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
  ( ExOptic
  , FLAVOR
  , Flip
  , Optic
  , Prostrong (..)
  , legs2prof
  , withLegs
  )
import Proarrow.Optic.AffineFold (AffineFoldFl)
import Proarrow.Profunctor.Corepresentable (Corep (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Instance.Terminal (TerminalProfunctor (..))
import Proarrow.Profunctor.Representable (Rep (..))

type GetterFl :: forall {j} {k}. FLAVOR j k
class (AffineFoldFl p q) => GetterFl (p :: k +-> k) (q :: j +-> j) where
  getP :: p s a -> s ~> a
instance (HasBinaryProducts k, Ob (s :: k)) => GetterFl (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 :: CAT 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) => GetterFl (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) => GetterFl (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 (GetterFl f g, GetterFl f' g') => GetterFl (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).
GetterFl p q =>
p s a -> s ~> a
forall (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
GetterFl 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 :: CAT 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).
GetterFl p q =>
p s a -> s ~> a
forall (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
GetterFl p q =>
p s a -> s ~> a
getP @f @g f s b
f
instance (HasCoproducts k, Ob t) => GetterFl (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 :: CAT 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

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

-- | View through any optic that can act as a getter, in either encoding: run it at its witness
-- pair ('ExOptic' 'GetterFl', via 'withLegs') and read the get leg off with 'getP'.
view
  :: forall {j} {k} c (s :: k) (t :: j) a b
   . (CategoryOf j, CategoryOf k, (Ob a, Ob b) => c (ExOptic GetterFl a b))
  => 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, Ob b) => c (ExOptic GetterFl a b)) =>
Optic c s t a b -> s ~> a
view Optic c s t a b
o = forall {j} {k} (w :: FLAVOR j k)
       (c :: (k -> j -> Type) -> Constraint) (s :: k) (t :: j) (a :: k)
       (b :: j) r.
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall (w :: FLAVOR j k) (c :: (k -> j -> Type) -> Constraint)
       (s :: k) (t :: j) (a :: k) (b :: j) r.
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
withLegs @GetterFl Optic c s t a b
o \ @p @q p s a
p q b t
_ -> forall {j} {k} (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
GetterFl p q =>
p s a -> s ~> a
forall (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
GetterFl p q =>
p s a -> s ~> a
getP @p @q p s a
p

infixl 8 ^.

-- | View the focus of a concrete, @Type@-level optic.
(^.) :: (c (ExOptic GetterFl a b)) => s -> Optic c (s :: Type) (t :: Type) a b -> a
s
s ^. :: forall (c :: (Type -> Type -> Type) -> Constraint) a b s t.
c (ExOptic GetterFl a b) =>
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, Ob b) => c (ExOptic GetterFl a b)) =>
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 = forall {j} {k} (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
forall (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j) (s :: k)
       (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
legs2prof @GetterFl ((s ~> a) -> Id s a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id s ~> a
sa) 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 GetterFl) s t a b)
-> (s ~> a) -> Optic (Prostrong GetterFl) 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 GetterFl)) s t a b

-- | Review through any optic that can act as a review, in either encoding: 'getP' on the flipped
-- witness pair.
review
  :: forall {j} {k} c (s :: k) (t :: j) a b
   . (CategoryOf j, CategoryOf k, (Ob a, Ob b) => c (ExOptic (Flip GetterFl) a 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 a, Ob b) => c (ExOptic (Flip GetterFl) a b)) =>
Optic c s t a b -> b ~> t
review Optic c s t a b
o = forall {j} {k} (w :: FLAVOR j k)
       (c :: (k -> j -> Type) -> Constraint) (s :: k) (t :: j) (a :: k)
       (b :: j) r.
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall (w :: FLAVOR j k) (c :: (k -> j -> Type) -> Constraint)
       (s :: k) (t :: j) (a :: k) (b :: j) r.
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
withLegs @(Flip GetterFl) Optic c s t a b
o \ @p @q p s a
_ q b t
q -> forall {j} {k} (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
GetterFl p q =>
p s a -> s ~> a
forall (p :: j +-> j) (q :: k +-> k) (s :: j) (a :: j).
GetterFl p q =>
p s a -> s ~> a
getP @q @p q b t
q

infixr 8 #

-- | Review through a concrete, @Type@-level optic.
(#) :: (c (ExOptic (Flip GetterFl) a b)) => Optic c (s :: Type) (t :: Type) a b -> b -> t
# :: forall (c :: (Type -> Type -> Type) -> Constraint) a b s t.
c (ExOptic (Flip GetterFl) a 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 a, Ob b) => c (ExOptic (Flip GetterFl) a 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 = forall {j} {k} (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
forall (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j) (s :: k)
       (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
legs2prof @(Flip GetterFl) TerminalProfunctor s a
forall {j} {k} (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor ((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 GetterFl)) s t a b)
-> (b ~> t) -> Optic (Prostrong (Flip GetterFl)) 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