module Proarrow.Profunctor.Constant where

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

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) (t :: k) a b. (CategoryOf k, Ob a, Ob b, c (Rep (Constant a))) => Optic c s t a b -> s ~> a
view :: forall {k} {c :: (k -> k -> Type) -> Constraint} (s :: k) (t :: k)
       (a :: k) (b :: k).
(CategoryOf k, Ob a, Ob b, c (Rep (Constant a))) =>
Optic c s t a b -> s ~> a
view Optic c s t a b
l = 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 b -> Rep (Constant a) s t
Optic c s t a b
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

review :: forall {k} {c} (s :: k) (t :: k) a b. (CategoryOf k, Ob a, Ob b, c (Corep (Constant b))) => Optic c s t a b -> b ~> t
review :: forall {k} {c :: (k -> k -> Type) -> Constraint} (s :: k) (t :: k)
       (a :: k) (b :: k).
(CategoryOf k, Ob a, Ob b, c (Corep (Constant b))) =>
Optic c s t a b -> b ~> t
review Optic c s t a b
l = 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) a b -> Corep (Constant b) s t
Optic c s t a b
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