{-# LANGUAGE AllowAmbiguousTypes #-}

-- | The __affine fold__: a fold that sees at most one focus, @s '~>' (a '||' 'TerminalObject')@
-- ('AffineFoldRes' \/ '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 'PreviewP' carrier.
module Proarrow.Optic.AffineFold where

import Data.Kind (Type)
import Prelude (Maybe (..), const, either)

import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard (..))
import Proarrow.Category.Monoidal.Distributive (Bicartesian)
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 (..))
import Proarrow.Optic (CompactFlavor, FLAVOR, Optic, Optic_ (..), Prostrong (..), SubFlavor (..))
import Proarrow.Optic.Fold (FoldRes)
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 AffineFoldRes :: forall {j} {k}. FLAVOR j k
class (FoldRes p q) => AffineFoldRes (p :: k +-> k) (q :: j +-> j) where
  previewP :: (Bicartesian k) => p s a -> s ~> (a || TerminalObject)

instance (HasBinaryProducts k, Ob (s :: k)) => AffineFoldRes (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 :: 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).
(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) => AffineFoldRes (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 :: k +-> 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) => AffineFoldRes (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 :: k +-> 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 (AffineFoldRes f g, AffineFoldRes f' g') => AffineFoldRes (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).
(AffineFoldRes p q, Bicartesian k) =>
p s a -> s ~> (a || TerminalObject)
forall (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
(AffineFoldRes 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 :: 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).
(AffineFoldRes p q, Bicartesian k) =>
p s a -> s ~> (a || TerminalObject)
forall (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
(AffineFoldRes 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) => AffineFoldRes (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 :: k +-> 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 :: 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 ((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) => AffineFoldRes (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 k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @TerminalObject (TerminalObject ~> (a || TerminalObject))
-> (t ~> TerminalObject) -> t ~> (a || TerminalObject)
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).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate @k @t) (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 :: k +-> 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

instance CompactFlavor AffineFoldRes

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

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

-- | The carrier profunctor for 'preview': a generalized @s -> Maybe a@.
type PreviewP :: forall {j} {k}. k -> j +-> k
data PreviewP (a :: k) (s :: k) (t :: j) where
  PreviewP :: (Ob t) => {forall {j} {k} (t :: j) (s :: k) (a :: k).
PreviewP a s t -> s ~> (a || TerminalObject)
unPreviewP :: s ~> (a || TerminalObject)} -> PreviewP a s t

instance (Bicartesian k, CategoryOf j, Ob (a :: k)) => Profunctor (PreviewP a :: j +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> PreviewP a a b -> PreviewP a c d
dimap c ~> a
l b ~> d
r (PreviewP a ~> (a || TerminalObject)
f) = (c ~> (a || TerminalObject)) -> PreviewP a c d
forall {j} {k} (t :: j) (s :: k) (a :: k).
Ob t =>
(s ~> (a || TerminalObject)) -> PreviewP a s t
PreviewP (a ~> (a || TerminalObject)
f (a ~> (a || TerminalObject))
-> (c ~> a) -> c ~> (a || TerminalObject)
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
. c ~> a
l) ((Ob b, Ob d) => PreviewP a c d) -> (b ~> d) -> PreviewP a c d
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 ~> d
r
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> PreviewP a a b -> r
\\ PreviewP a ~> (a || TerminalObject)
f = r
(Ob a, Ob (a || TerminalObject)) => r
(Ob a, Ob b) => r
r ((Ob a, Ob (a || TerminalObject)) => r)
-> (a ~> (a || TerminalObject)) -> r
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
\\ a ~> (a || TerminalObject)
f

-- | Any flavor whose optics can preview has strength for the 'PreviewP' carrier.
instance
  (Bicartesian k, CategoryOf j, Ob (a :: k), SubFlavor w AffineFoldRes)
  => Prostrong (w :: FLAVOR j k) (PreviewP a :: j +-> k)
  where
  proact :: forall (f :: k +-> k) (g :: j +-> j).
(w f g, Profunctor f, Profunctor g) =>
((f :.: PreviewP a) :.: g) :~> PreviewP a
proact @f @g (f a b
f :.: PreviewP b ~> (a || TerminalObject)
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 @AffineFoldRes @f @g ((a ~> (a || TerminalObject)) -> PreviewP a a b
forall {j} {k} (t :: j) (s :: k) (a :: k).
Ob t =>
(s ~> (a || TerminalObject)) -> PreviewP a s t
PreviewP ((b ~> (a || TerminalObject)
h (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 @k @a @TerminalObject) ((b || TerminalObject) ~> (a || TerminalObject))
-> (a ~> (b || TerminalObject)) -> a ~> (a || TerminalObject)
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).
(AffineFoldRes p q, Bicartesian k) =>
p s a -> s ~> (a || TerminalObject)
forall (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
(AffineFoldRes p q, Bicartesian k) =>
p s a -> s ~> (a || TerminalObject)
previewP @f @g f a b
f)) ((Ob b, Ob b) => PreviewP a a b) -> g b b -> PreviewP 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

-- | Preview through any optic that can act as an affine fold, in either encoding.
preview
  :: forall {j} {k} c (s :: k) (t :: j) a b
   . (Bicartesian k, CategoryOf j, c (PreviewP a))
  => 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, c (PreviewP a)) =>
Optic c s t a b -> s ~> (a || TerminalObject)
preview (Optic forall (p :: j +-> k). c p => p a b -> p s t
l) = PreviewP a s t -> s ~> (a || TerminalObject)
forall {j} {k} (t :: j) (s :: k) (a :: k).
PreviewP a s t -> s ~> (a || TerminalObject)
unPreviewP (forall (p :: j +-> k). c p => p a b -> p s t
l @(PreviewP a) ((a ~> (a || TerminalObject)) -> PreviewP a a b
forall {j} {k} (t :: j) (s :: k) (a :: k).
Ob t =>
(s ~> (a || TerminalObject)) -> PreviewP a s t
PreviewP (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @TerminalObject)))

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 (PreviewP a)) => s -> Optic c s t a b -> Maybe a
s
s ^? :: forall s t a b (c :: (Type -> Type -> Type) -> Constraint).
c (PreviewP a) =>
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
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, c (PreviewP a)) =>
Optic c s t a b -> s ~> (a || TerminalObject)
preview Optic c s t a b
l s
s)