module Proarrow.Optic where

import Data.Kind (Constraint)
import Prelude (type (~))

import Proarrow.Core (CAT, CategoryOf (..), Kind, Profunctor (..), Promonad (..), dimapDefault, type (+->))

type data OPTIC (j :: Kind) (k :: Kind) (c :: j +-> k -> Constraint) = OPT k j
type family OptL (p :: OPTIC j k c) where
  OptL (OPT j k) = j
type family OptR (p :: OPTIC j k c) where
  OptR (OPT j k) = k
type Optic_ :: CAT (OPTIC j k c)
data Optic_ ab st where
  Optic
    :: (Ob a, Ob b, Ob s, Ob t) => {forall (k :: Kind) (a :: k) (j :: Kind) (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
over :: forall p. (c p) => p a b -> p s t} -> Optic_ (OPT a b :: OPTIC j k c) (OPT s t)

instance (CategoryOf j, CategoryOf k) => Profunctor (Optic_ :: CAT (OPTIC j k c)) where
  dimap :: forall (c :: OPTIC j k c) (a :: OPTIC j k c) (b :: OPTIC j k c)
       (d :: OPTIC j k c).
(c ~> a) -> (b ~> d) -> Optic_ a b -> Optic_ c d
dimap = (c ~> a) -> (b ~> d) -> Optic_ a b -> Optic_ c d
Optic_ c a -> Optic_ b d -> Optic_ a b -> Optic_ c d
forall {k :: Kind} (p :: k +-> k) (c :: k) (a :: k) (b :: k)
       (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: OPTIC j k c) (b :: OPTIC j k c) (r :: Kind).
((Ob a, Ob b) => r) -> Optic_ a b -> r
\\ Optic{} = r
(Ob a, Ob b) => r
r
instance (CategoryOf j, CategoryOf k) => Promonad (Optic_ :: CAT (OPTIC j k c)) where
  id :: forall (a :: OPTIC j k c). Ob a => Optic_ a a
id = (forall (p :: j +-> k).
 c p =>
 p (OptL a) (OptR a) -> p (OptL a) (OptR a))
-> Optic_ (OPT (OptL a) (OptR a)) (OPT (OptL a) (OptR a))
forall (k :: Kind) (a :: k) (j :: Kind) (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic p (OptL a) (OptR a) -> p (OptL a) (OptR a)
forall (a :: Kind). Ob a => a -> a
forall {k :: Kind} (p :: k +-> k) (a :: k).
(Promonad p, Ob a) =>
p a a
forall (p :: j +-> k).
c p =>
p (OptL a) (OptR a) -> p (OptL a) (OptR a)
id
  Optic forall (p :: j +-> k). c p => p a b -> p s t
n . :: forall (b :: OPTIC j k c) (c :: OPTIC j k c) (a :: OPTIC j k c).
Optic_ b c -> Optic_ a b -> Optic_ a c
. Optic forall (p :: j +-> k). c p => p a b -> p s t
m = (forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
forall (k :: Kind) (a :: k) (j :: Kind) (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic \p a b
p -> p a b -> p s t
forall (p :: j +-> k). c p => p a b -> p s t
n (p a b -> p s t
forall (p :: j +-> k). c p => p a b -> p s t
m p a b
p)
instance (CategoryOf j, CategoryOf k) => CategoryOf (OPTIC j k c) where
  type (~>) = Optic_
  type Ob opt = (opt ~ OPT (OptL opt) (OptR opt), Ob (OptL opt), Ob (OptR opt))

type Optic (c :: j +-> k -> Constraint) s t a b = Optic_ (OPT a b) (OPT s t :: OPTIC j k c)
type Optic' c s a = Optic c s s a a

class (c1 p, c2 p) => (c1 :&&: c2) p
instance (c1 p, c2 p) => (c1 :&&: c2) p
-- | Compose optics if different kinds
(%) :: Optic c1 s t a b -> Optic c2 a b c d -> Optic (c1 :&&: c2) s t c d
Optic forall (p :: j +-> k). c1 p => p a b -> p s t
n % :: forall {j :: Kind} {k :: Kind} (c1 :: (j +-> k) -> Constraint)
       (s :: k) (t :: j) (a :: k) (b :: j) (c2 :: (j +-> k) -> Constraint)
       (c :: k) (d :: j).
Optic c1 s t a b -> Optic c2 a b c d -> Optic (c1 :&&: c2) s t c d
% Optic forall (p :: j +-> k). c2 p => p a b -> p s t
m = (forall (p :: j +-> k). (:&&:) c1 c2 p => p c d -> p s t)
-> Optic_ (OPT c d) (OPT s t)
forall (k :: Kind) (a :: k) (j :: Kind) (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic (p a b -> p s t
p a b -> p s t
forall (p :: j +-> k). c1 p => p a b -> p s t
n (p a b -> p s t) -> (p c d -> p a b) -> p c d -> p s t
forall (b :: Kind) (c :: Kind) (a :: Kind).
(b -> c) -> (a -> b) -> a -> c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p c d -> p a b
p a b -> p s t
forall (p :: j +-> k). c2 p => p a b -> p s t
m)

type (:=>) :: ((j +-> k) -> Constraint) -> ((j +-> k) -> Constraint) -> Constraint
type c :=> d = forall p. (c p) => d p

type Iso s t a b = Optic Profunctor s t a b
type Iso' s a = Iso s s a a

iso :: forall {j} {k} (s :: k) (t :: j) a b. (CategoryOf j, CategoryOf k) => (s ~> a) -> (b ~> t) -> Iso s t a b
iso :: forall {j :: Kind} {k :: Kind} (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k) =>
(s ~> a) -> (b ~> t) -> Iso s t a b
iso s ~> a
sa b ~> t
bt = (forall (p :: j +-> k). Profunctor p => p a b -> p s t)
-> Iso s t a b
forall (k :: Kind) (a :: k) (j :: Kind) (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic ((s ~> a) -> (b ~> t) -> p a b -> p s t
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (c :: k) (a :: k)
       (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap s ~> a
sa b ~> t
bt) ((Ob s, Ob a) => Iso s t a b) -> (s ~> a) -> Iso s t a b
forall (a :: k) (b :: k) (r :: Kind).
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ s ~> a
sa ((Ob b, Ob t) => Iso s t a b) -> (b ~> t) -> Iso s t a b
forall (a :: j) (b :: j) (r :: Kind).
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> t
bt

data Re p s t a b where
  Re :: (Ob a, Ob b) => {forall {k :: Kind} {k :: Kind} (a :: k) (b :: k)
       (p :: k -> k -> Kind) (t :: k) (s :: k).
Re p s t a b -> p b a -> p t s
unRe :: p b a -> p t s} -> Re p s t a b

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

class
  (forall p a b. (coc p) => c (Re p a b)) =>
  InvertableOptic (c :: j +-> k -> Constraint) (coc :: k +-> j -> Constraint)
    | c -> coc

instance InvertableOptic Profunctor Profunctor
instance (InvertableOptic l l', InvertableOptic r r') => InvertableOptic (l :&&: r) (l' :&&: r')

re :: (Ob a, Ob b, InvertableOptic c coc) => Optic c s t a b -> Optic coc b a t s
re :: forall {j :: Kind} {k :: Kind} (a :: j) (b :: k)
       (c :: (k +-> j) -> Constraint) (coc :: (j +-> k) -> Constraint)
       (s :: j) (t :: k).
(Ob a, Ob b, InvertableOptic c coc) =>
Optic c s t a b -> Optic coc b a t s
re (Optic forall (p :: k +-> j). c p => p a b -> p s t
l) = (forall (p :: j +-> k). coc p => p t s -> p b a)
-> Optic_ (OPT t s) (OPT b a)
forall (k :: Kind) (a :: k) (j :: Kind) (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic (Re p a b s t -> p t s -> p b a
forall {k :: Kind} {k :: Kind} (a :: k) (b :: k)
       (p :: k -> k -> Kind) (t :: k) (s :: k).
Re p s t a b -> p b a -> p t s
unRe (Re p a b a b -> Re p a b s t
forall (p :: k +-> j). c p => p a b -> p s t
l ((p b a -> p b a) -> Re p a b a b
forall {k :: Kind} {k :: Kind} (a :: k) (b :: k)
       (p :: k -> k -> Kind) (t :: k) (s :: k).
(Ob a, Ob b) =>
(p b a -> p t s) -> Re p s t a b
Re p b a -> p b a
p b a -> p b a
forall (a :: Kind). Ob a => a -> a
forall {k :: Kind} (p :: k +-> k) (a :: k).
(Promonad p, Ob a) =>
p a a
id)))