module Proarrow.Profunctor.Constant where

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

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, Ob c) => 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) -> (b ~> d) -> Constant c a b -> Constant c c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (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

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

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

instance (CategoryOf j, CategoryOf k, Ob c) => Corepresentable (ConstIn c :: j +-> k) where
  type ConstIn c %% a = c
  coindex :: forall (a :: k) (b :: j). ConstIn c a b -> (ConstIn c %% a) ~> b
coindex (ConstIn c ~> b
f) = c ~> b
(ConstIn c %% a) ~> b
f
  cotabulate :: forall (a :: k) (b :: j).
Ob a =>
((ConstIn c %% a) ~> b) -> ConstIn c a b
cotabulate (ConstIn c %% a) ~> b
f = (c ~> b) -> ConstIn c a b
forall {k} {k} (a :: k) (c :: k) (b :: k).
Ob a =>
(c ~> b) -> ConstIn c a b
ConstIn c ~> b
(ConstIn c %% a) ~> b
f
  corepMap :: forall (a :: k) (b :: k).
(a ~> b) -> (ConstIn c %% a) ~> (ConstIn c %% b)
corepMap a ~> b
_ = c ~> c
(ConstIn c %% a) ~> (ConstIn c %% b)
forall (a :: j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id