module Proarrow.Profunctor.Constant where

import Proarrow.Core (CategoryOf (..), Promonad (..), type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Optic (Optic', Optic_(..))
import Proarrow.Profunctor.Corepresentable (Corep (..), corep)
import Proarrow.Profunctor.Representable (Rep (..), rep)

data family Constant :: k -> j +-> k
instance (CategoryOf j, CategoryOf k, Ob c) => FunctorForRep (Constant c :: j +-> k) where
  type Constant c @ a = c
  fmap :: forall (a :: j) (b :: j).
(a ~> b) -> (Constant c @ a) ~> (Constant c @ b)
fmap a ~> b
_ = c ~> c
(Constant c @ a) ~> (Constant c @ b)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

view :: forall {k} c (s :: k) a. (CategoryOf k, Ob a => c (Rep (Constant a))) => Optic' c s a -> s ~> a
view :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (a :: k).
(CategoryOf k, Ob a => c (Rep (Constant a))) =>
Optic' c s a -> s ~> a
view (Optic forall (p :: k +-> k). c p => p a b -> p s t
l) = Optic_
  (OPT (Rep (Constant a) a a) (Rep (Constant a) s s))
  (OPT (a ~> a) (s ~> a))
-> forall (p :: Type +-> Type).
   Profunctor p =>
   p (Rep (Constant a) a a) (Rep (Constant a) s s)
   -> p (a ~> a) (s ~> a)
forall k (a :: k) j (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 {j} {k} (f :: j +-> k) (a :: k) (b :: j) (a' :: k)
       (b' :: j).
Ob b =>
Iso (a ~> (f @ b)) (a' ~> (f @ b')) (Rep f a b) (Rep f a' b')
forall (f :: k +-> k) (a :: k) (b :: k) (a' :: k) (b' :: k).
Ob b =>
Iso (a ~> (f @ b)) (a' ~> (f @ b')) (Rep f a b) (Rep f a' b')
rep @(Constant a)) Rep (Constant a) a a -> Rep (Constant a) s s
Rep (Constant a) a b -> Rep (Constant a) s t
forall (p :: k +-> k). c p => p a b -> p s t
l a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

infixl 8 ^.
(^.) :: (c (Rep (Constant a))) => s -> Optic' c s a -> a
^. :: forall (c :: (Type +-> Type) -> Constraint) a s.
c (Rep (Constant a)) =>
s -> Optic' c s a -> a
(^.) s
s Optic' c s a
l = Optic' c s a -> s ~> a
forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (a :: k).
(CategoryOf k, Ob a => c (Rep (Constant a))) =>
Optic' c s a -> s ~> a
view Optic' c s a
l s
s

review :: forall {k} c (t :: k) b. (CategoryOf k, Ob b => c (Corep (Constant b))) => Optic' c t b -> b ~> t
review :: forall {k} (c :: (k -> k -> Type) -> Constraint) (t :: k) (b :: k).
(CategoryOf k, Ob b => c (Corep (Constant b))) =>
Optic' c t b -> b ~> t
review (Optic forall (p :: k +-> k). c p => p a b -> p s t
l) = Optic_
  (OPT (Corep (Constant b) b b) (Corep (Constant b) t t))
  (OPT (b ~> b) (b ~> t))
-> forall (p :: Type +-> Type).
   Profunctor p =>
   p (Corep (Constant b) b b) (Corep (Constant b) t t)
   -> p (b ~> b) (b ~> t)
forall k (a :: k) j (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 {j} {k} (f :: j +-> k) (a :: j) (b :: k) (a' :: j)
       (b' :: k).
Ob a =>
Iso ((f @ a) ~> b) ((f @ a') ~> b') (Corep f a b) (Corep f a' b')
forall (f :: k +-> k) (a :: k) (b :: k) (a' :: k) (b' :: k).
Ob a =>
Iso ((f @ a) ~> b) ((f @ a') ~> b') (Corep f a b) (Corep f a' b')
corep @(Constant b)) Corep (Constant b) b b -> Corep (Constant b) t t
Corep (Constant b) a b -> Corep (Constant b) s t
forall (p :: k +-> k). c p => p a b -> p s t
l b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

infixr 8 #
(#) :: forall {k} c (t :: k) b. (CategoryOf k, c (Corep (Constant b))) => Optic' c t b -> b ~> t
# :: forall {k} (c :: (k -> k -> Type) -> Constraint) (t :: k) (b :: k).
(CategoryOf k, c (Corep (Constant b))) =>
Optic' c t b -> b ~> t
(#) = Optic' c t b -> b ~> t
forall {k} (c :: (k -> k -> Type) -> Constraint) (t :: k) (b :: k).
(CategoryOf k, Ob b => c (Corep (Constant b))) =>
Optic' c t b -> b ~> t
review