module Proarrow.Profunctor.Constant where

import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), type (+->))
import Proarrow.Profunctor.Representable (Representable (..))

type Constant :: k -> j +-> k
data Constant c a b where
  Constant :: (Ob b) => a ~> c -> Constant c a b

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

instance (CategoryOf j, CategoryOf k, Ob c) => Representable (Constant c :: j +-> k) where
  type Constant c % a = c
  index :: forall (a :: k) (b :: j). Constant c a b -> a ~> (Constant c % b)
index (Constant a ~> c
f) = a ~> c
a ~> (Constant c % b)
f
  tabulate :: forall (b :: j) (a :: k).
Ob b =>
(a ~> (Constant c % b)) -> Constant c a b
tabulate a ~> (Constant c % b)
f = (a ~> c) -> Constant c a b
forall {j} {k} (b :: j) (a :: k) (c :: k).
Ob b =>
(a ~> c) -> Constant c a b
Constant a ~> c
a ~> (Constant c % b)
f
  repMap :: forall (a :: j) (b :: j).
(a ~> b) -> (Constant c % a) ~> (Constant c % b)
repMap 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