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

-- | The __iso__: the bottom of the subtyping lattice, usable as every other flavor. 'IsoFl' is
-- simply the conjunction of the five maximal flavors ('Proarrow.Optic.Lens.LensFl',
-- 'Proarrow.Optic.Prism.PrismFl', 'Proarrow.Optic.PowerGrate.PowerGrateFl',
-- 'Proarrow.Optic.MonoidalLens.MonLensFl' and 'Proarrow.Optic.Tracer.TracerFl'). Build with 'iso', eliminate to the two legs with
-- 'withIso' via the 'Yo' carrier -- which also eliminates 'Proarrow.Optic.re'-versed isos, a
-- conversion the subtyping lattice itself cannot express; 'fromPIso'\/'toPIso' mediate with the
-- profunctor-class-flavored 'PIso'.
module Proarrow.Optic.Iso where

import Proarrow.Category.Instance.Opposite (OPPOSITE (..))
import Proarrow.Core (CategoryOf (..), Promonad (..), type (+->))
import Proarrow.Optic
  ( FLAVOR
  , Flip
  , Optic
  , Optic_ (..)
  , PIso
  , Prostrong (..)
  , Sub (..)
  , convert
  , iso
  )
import Proarrow.Optic.Getter (getP)
import Proarrow.Optic.Lens (LensFl)
import Proarrow.Optic.MonoidalLens (MonLensFl)
import Proarrow.Optic.PowerGrate (PowerGrateFl)
import Proarrow.Optic.Prism (PrismFl)
import Proarrow.Optic.Tracer (TracerFl)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Yoneda (Yo (..))

-- | The iso flavor. Reversed isos still view\/preview\/fold (@'Proarrow.Optic.re' iso@ is a getter,
-- and more), through the @'Proarrow.Optic.Getter.GetterFl' q p@ superclass of 'PrismFl'.
class (LensFl p q, PrismFl p q, PowerGrateFl p q, MonLensFl p q, TracerFl p q) => IsoFl p q

instance (LensFl p q, PrismFl p q, PowerGrateFl p q, MonLensFl p q, TracerFl p q) => IsoFl p q

-- | The 'Prostrong'-flavored iso; for the profunctor-class-flavored encoding see 'Proarrow.Optic.PIso'.
type Iso (s :: k) (t :: k) a b = Optic (Prostrong IsoFl) s t a b

type Iso' s a = Iso s s a a

-- | Any flavor whose optics are isos has strength for the 'Yo' profunctor.
instance (CategoryOf k, forall p q. (w p q) => Sub IsoFl p q) => Prostrong (w :: FLAVOR k k) (Yo a (OP b) :: k +-> k) where
  proact :: forall (f :: k +-> k) (g :: k +-> k).
(w f g, Profunctor f, Profunctor g) =>
((f :.: Yo a ('OP b)) :.: g) :~> Yo a ('OP b)
proact @f @g (f a b
f :.: Yo b ~> a
sa b1 ~> b
bt :.: g b b
g) = forall {j} {k} (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j) r.
Sub w p q =>
(w p q => r) -> r
forall (w :: FLAVOR k k) (p :: k +-> k) (q :: k +-> k) r.
Sub w p q =>
(w p q => r) -> r
sub @IsoFl @f @g ((a ~> a) -> (b ~> b) -> Yo a ('OP b) a b
forall {k} {j} (c :: k) (a :: k) (b1 :: j) (d :: j).
(c ~> a) -> (b1 ~> d) -> Yo a ('OP b1) c d
Yo (b ~> a
sa (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).
GetterFl p q =>
p s a -> s ~> a
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k).
GetterFl p q =>
p s a -> s ~> a
getP @f @g f a b
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 :: k +-> k) (s :: k) (a :: k).
GetterFl p q =>
p s a -> s ~> a
getP @g @f g b b
g (b ~> b) -> (b ~> b) -> b ~> b
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
. b ~> b
b1 ~> b
bt))

-- | 'Proarrow.Optic.re'-versed isos are still isos: the same carrier eliminates them by reading
-- the witness pair backwards. This is a conversion the subtyping lattice cannot express (the
-- entailment @IsoFl q p => IsoFl p q@ doesn't hold), but the carrier can compute it.
instance {-# OVERLAPPING #-} (CategoryOf k) => Prostrong (Flip IsoFl) (Yo (a :: k) (OP b) :: k +-> k) where
  proact :: forall (f :: k +-> k) (g :: k +-> k).
(Flip IsoFl f g, Profunctor f, Profunctor g) =>
((f :.: Yo a ('OP b)) :.: g) :~> Yo a ('OP b)
proact @f @g (f a b
f :.: Yo b ~> a
sa b1 ~> b
bt :.: g b b
g) = (a ~> a) -> (b ~> b) -> Yo a ('OP b) a b
forall {k} {j} (c :: k) (a :: k) (b1 :: j) (d :: j).
(c ~> a) -> (b1 ~> d) -> Yo a ('OP b1) c d
Yo (b ~> a
sa (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).
GetterFl p q =>
p s a -> s ~> a
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k).
GetterFl p q =>
p s a -> s ~> a
getP @f @g f a b
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 :: k +-> k) (s :: k) (a :: k).
GetterFl p q =>
p s a -> s ~> a
getP @g @f g b b
g (b ~> b) -> (b ~> b) -> b ~> b
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
. b ~> b
b1 ~> b
bt)

-- | Eliminate any iso-flavored optic to its two legs, in either encoding -- including the
-- profunctor-class-flavored 'Proarrow.Optic.PIso' and reversed ('Proarrow.Optic.re') isos.
withIso
  :: forall {k} c (s :: k) (t :: k) a b r
   . (CategoryOf k, (Ob a, Ob b) => c (Yo a (OP b)))
  => Optic c s t a b -> ((s ~> a) -> (b ~> t) -> r) -> r
withIso :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k) r.
(CategoryOf k, (Ob a, Ob b) => c (Yo a ('OP b))) =>
Optic c s t a b -> ((s ~> a) -> (b ~> t) -> r) -> r
withIso (Optic forall (p :: k +-> k). (c p, Profunctor p) => p a b -> p s t
l) (s ~> a) -> (b ~> t) -> r
k = case forall (p :: k +-> k). (c p, Profunctor p) => p a b -> p s t
l @(Yo a (OP b)) ((a ~> a) -> (b ~> b) -> Yo a ('OP b) a b
forall {k} {j} (c :: k) (a :: k) (b1 :: j) (d :: j).
(c ~> a) -> (b1 ~> d) -> Yo a ('OP b1) c d
Yo a ~> a
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
b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id) of Yo s ~> a
sa b1 ~> t
bt -> (s ~> a) -> (b ~> t) -> r
k s ~> a
s ~> a
sa b ~> t
b1 ~> t
bt

-- | The two iso encodings are equivalent: this direction instantiates the
-- profunctor-class-flavored iso at the free 'IsoFl'-strong profunctor @ExOptic 'IsoFl' a b@,
-- which needs nothing beyond its 'Proarrow.Core.Profunctor' instance.
fromPIso :: forall {k} (s :: k) (t :: k) a b. (CategoryOf k) => PIso s t a b -> Iso s t a b
fromPIso :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
CategoryOf k =>
PIso s t a b -> Iso s t a b
fromPIso = Optic Profunctor s t a b -> Optic (Prostrong IsoFl) s t a b
forall {j} {k} (c :: (k -> j -> Type) -> Constraint)
       (w :: FLAVOR j k) (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b -> Optic (Prostrong w) s t a b
convert

-- | The other direction of the equivalence, by eliminating to legs and rebuilding.
toPIso :: forall {k} (s :: k) (t :: k) a b. (CategoryOf k) => Iso s t a b -> PIso s t a b
toPIso :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
CategoryOf k =>
Iso s t a b -> PIso s t a b
toPIso Iso s t a b
o = Iso s t a b
-> ((s ~> a) -> (b ~> t) -> PIso s t a b) -> PIso s t a b
forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k) r.
(CategoryOf k, (Ob a, Ob b) => c (Yo a ('OP b))) =>
Optic c s t a b -> ((s ~> a) -> (b ~> t) -> r) -> r
withIso Iso s t a b
o (s ~> a) -> (b ~> t) -> PIso s t a b
forall {j} {k} (c :: (j +-> k) -> Constraint) (s :: k) (t :: j)
       (a :: k) (b :: j).
(CategoryOf j, CategoryOf k) =>
(s ~> a) -> (b ~> t) -> Optic c s t a b
iso