{-# LANGUAGE AllowAmbiguousTypes #-}

-- | The __affine fold__: a fold that sees at most one focus, @s '~>' (a '||' 'TerminalObject')@
-- ('AffineFoldFl' \/ 'previewP'). Every 'Proarrow.Optic.Getter.Getter' and
-- 'Proarrow.Optic.AffineTraversal.AffineTraversal' is one, and it subtypes to
-- 'Proarrow.Optic.Fold.Fold'. Like all read-only flavors it has no builder of its own
-- ('Proarrow.Optic.convert' a stronger optic). Its canonical eliminator is 'preview' \/ '(^?)',
-- via the generic 'ExOptic' carrier.
module Proarrow.Optic.AffineFold where

import Data.Kind (Type)
import Prelude (Maybe (..), either)
import Prelude qualified as P

import Proarrow.Category.Monoidal.Cartesian (Bicartesian)
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard (..))
import Proarrow.Colimit.BinaryCoproduct (Coproduct, HasBinaryCoproducts (..), HasCoproducts)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), (\\), type (+->))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts, Product, snd)
import Proarrow.Limit.Terminal (HasTerminalObject (..), const)
import Proarrow.Optic (ExOptic, FLAVOR, Optic, Prostrong (..), withLegs)
import Proarrow.Optic.Fold (FoldFl)
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 (..))

-- | An affine fold is a fold that can see at most one @a@ (0-or-1, never 0-or-many). A getter
-- is an affine fold that always succeeds; an affine traversal is one that additionally knows how
-- to reconstruct a @t@ when it fails to match.
type AffineFoldFl :: forall {j} {k}. FLAVOR j k
class (FoldFl p q) => AffineFoldFl (p :: k +-> k) (q :: j +-> j) where
  previewP :: (Bicartesian k) => p s a -> s ~> (a || TerminalObject)

instance (HasBinaryProducts k, Ob (s :: k)) => AffineFoldFl (Rep (Product s)) (Corep (Product s)) where
  previewP :: forall (s :: k) (a :: k).
Bicartesian k =>
Rep (Product s) s a -> s ~> (a || TerminalObject)
previewP @_ @a (Rep s ~> (Product s @ a)
p) = forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @TerminalObject (a ~> (a || TerminalObject))
-> (s ~> a) -> s ~> (a || TerminalObject)
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).
(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) => AffineFoldFl (Id :: k +-> k) (Id :: j +-> j) where
  previewP :: forall (s :: k) (a :: k).
Bicartesian k =>
Id s a -> s ~> (a || TerminalObject)
previewP @_ @a (Id s ~> a
sa) = forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @TerminalObject (a ~> (a || TerminalObject))
-> (s ~> a) -> s ~> (a || TerminalObject)
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 ~> a
sa ((Ob s, Ob a) => s ~> (a || TerminalObject))
-> (s ~> a) -> s ~> (a || TerminalObject)
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
instance (CategoryOf k, CategoryOf j) => AffineFoldFl (Id :: k +-> k) (TerminalProfunctor :: j +-> j) where
  previewP :: forall (s :: k) (a :: k).
Bicartesian k =>
Id s a -> s ~> (a || TerminalObject)
previewP @_ @a (Id s ~> a
sa) = forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @TerminalObject (a ~> (a || TerminalObject))
-> (s ~> a) -> s ~> (a || TerminalObject)
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 ~> a
sa ((Ob s, Ob a) => s ~> (a || TerminalObject))
-> (s ~> a) -> s ~> (a || TerminalObject)
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
instance (AffineFoldFl f g, AffineFoldFl f' g') => AffineFoldFl (f :.: f') (g' :.: g) where
  previewP :: forall (s :: k) (a :: k).
Bicartesian k =>
(:.:) f f' s a -> s ~> (a || TerminalObject)
previewP @_ @a (f s b
f :.: f' b a
f') = (forall {j} {k} (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
(AffineFoldFl p q, Bicartesian k) =>
p s a -> s ~> (a || TerminalObject)
forall (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
(AffineFoldFl p q, Bicartesian k) =>
p s a -> s ~> (a || TerminalObject)
previewP @f' @g' f' b a
f' (b ~> (a || TerminalObject))
-> (TerminalObject ~> (a || TerminalObject))
-> (b || TerminalObject) ~> (a || TerminalObject)
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @a @TerminalObject) ((b || TerminalObject) ~> (a || TerminalObject))
-> (s ~> (b || TerminalObject)) -> s ~> (a || TerminalObject)
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).
(AffineFoldFl p q, Bicartesian k) =>
p s a -> s ~> (a || TerminalObject)
forall (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
(AffineFoldFl p q, Bicartesian k) =>
p s a -> s ~> (a || TerminalObject)
previewP @f @g f s b
f ((Ob b, Ob a) => s ~> (a || TerminalObject))
-> f' b a -> s ~> (a || TerminalObject)
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' b a
f'
instance (HasCoproducts k, Ob t) => AffineFoldFl (Corep (Coproduct t) :: k +-> k) (Rep (Coproduct t)) where
  previewP :: forall (s :: k) (a :: k).
Bicartesian k =>
Corep (Coproduct t) s a -> s ~> (a || TerminalObject)
previewP @_ @a (Corep (Coproduct t @ s) ~> a
f) = forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @TerminalObject (a ~> (a || TerminalObject))
-> (s ~> a) -> s ~> (a || TerminalObject)
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
. (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 ((Ob (t || s), Ob a) => s ~> (a || TerminalObject))
-> ((t || s) ~> a) -> s ~> (a || TerminalObject)
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
\\ (Coproduct t @ s) ~> a
(t || s) ~> a
f
instance (CopyDiscard k, HasCoproducts k, Ob t) => AffineFoldFl (Rep (Coproduct t) :: k +-> k) (Corep (Coproduct t)) where
  previewP :: forall (s :: k) (a :: k).
Bicartesian k =>
Rep (Coproduct t) s a -> s ~> (a || TerminalObject)
previewP @_ @a (Rep s ~> (Coproduct t @ a)
p) = (forall (a :: k) (b :: k).
(HasTerminalObject k, Ob a) =>
El b -> a ~> b
forall {k} (a :: k) (b :: k).
(HasTerminalObject k, Ob a) =>
El b -> a ~> b
const @t (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @TerminalObject) (t ~> (a || TerminalObject))
-> (a ~> (a || TerminalObject))
-> (t || a) ~> (a || TerminalObject)
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @TerminalObject) ((t || a) ~> (a || TerminalObject))
-> (s ~> (t || a)) -> s ~> (a || TerminalObject)
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 ~> (Coproduct t @ a)
s ~> (t || a)
p

type AffineFold (s :: k) (t :: j) a b = Optic (Prostrong AffineFoldFl) s t a b

-- | Preview through any optic that can act as an affine fold, in either encoding: run it at its
-- witness pair ('ExOptic' 'AffineFoldFl', via 'withLegs') and apply 'previewP'.
preview
  :: forall {j} {k} c (s :: k) (t :: j) a b
   . (Bicartesian k, CategoryOf j, (Ob a, Ob b) => c (ExOptic AffineFoldFl a b))
  => Optic c s t a b -> s ~> (a || TerminalObject)
preview :: forall {j} {k} (c :: (k -> j -> Type) -> Constraint) (s :: k)
       (t :: j) (a :: k) (b :: j).
(Bicartesian k, CategoryOf j,
 (Ob a, Ob b) => c (ExOptic AffineFoldFl a b)) =>
Optic c s t a b -> s ~> (a || TerminalObject)
preview 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 @AffineFoldFl 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).
(AffineFoldFl p q, Bicartesian k) =>
p s a -> s ~> (a || TerminalObject)
forall (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
(AffineFoldFl p q, Bicartesian k) =>
p s a -> s ~> (a || TerminalObject)
previewP @p @q p s a
p

infixl 8 ^?

-- | Preview the focus of a concrete, @Type@-level optic (a getter that might not match).
(^?) :: forall s (t :: Type) a b c. (c (ExOptic AffineFoldFl a b)) => s -> Optic c s t a b -> Maybe a
s
s ^? :: forall s t a b (c :: (Type -> Type -> Type) -> Constraint).
c (ExOptic AffineFoldFl a b) =>
s -> Optic c s t a b -> Maybe a
^? Optic c s t a b
l = (a -> Maybe a) -> (() -> Maybe a) -> Either a () -> Maybe a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> Maybe a
forall a. a -> Maybe a
Just (Maybe a -> () -> Maybe a
forall a b. a -> b -> a
P.const Maybe a
forall a. Maybe a
Nothing) (Optic c s t a b -> s ~> (a || TerminalObject)
forall {j} {k} (c :: (k -> j -> Type) -> Constraint) (s :: k)
       (t :: j) (a :: k) (b :: j).
(Bicartesian k, CategoryOf j,
 (Ob a, Ob b) => c (ExOptic AffineFoldFl a b)) =>
Optic c s t a b -> s ~> (a || TerminalObject)
preview Optic c s t a b
l s
s)