module Proarrow.Category.Instance.Discrete where

import Data.Type.Equality (type (~~))

import Proarrow.Category.Enriched.Dagger (DaggerProfunctor (..))
import Proarrow.Category.Enriched.Thin qualified as Thin
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault)

newtype DISCRETE k = D k

type Discrete :: CAT (DISCRETE k)
data Discrete a b where
  Refl :: Discrete a a

-- | The discrete category with only identity arrows, every type of kind @k@ is an object.
instance CategoryOf (DISCRETE k) where
  type (~>) = Discrete

instance Profunctor Discrete where
  dimap :: forall (c :: DISCRETE k) (a :: DISCRETE k) (b :: DISCRETE k)
       (d :: DISCRETE k).
(c ~> a) -> (b ~> d) -> Discrete a b -> Discrete c d
dimap = (c ~> a) -> (b ~> d) -> Discrete a b -> Discrete c d
Discrete c a -> Discrete b d -> Discrete a b -> Discrete c d
forall {k} (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
instance Promonad Discrete where
  id :: forall (a :: DISCRETE k). Ob a => Discrete a a
id = Discrete a a
forall {k} (a :: DISCRETE k). Discrete a a
Refl
  Discrete b c
Refl . :: forall (b :: DISCRETE k) (c :: DISCRETE k) (a :: DISCRETE k).
Discrete b c -> Discrete a b -> Discrete a c
. Discrete a b
Refl = Discrete a c
Discrete a a
forall {k} (a :: DISCRETE k). Discrete a a
Refl

instance Thin.ThinProfunctor Discrete where
  type HasArrow Discrete a b = (a ~~ b)
  arr :: forall (a :: DISCRETE k) (b :: DISCRETE k).
(Ob a, Ob b, HasArrow Discrete a b) =>
Discrete a b
arr = Discrete a a
Discrete a b
forall {k} (a :: DISCRETE k). Discrete a a
Refl
  withArr :: forall (a :: DISCRETE k) (b :: DISCRETE k) r.
Discrete a b -> ((HasArrow Discrete a b, Ob a, Ob b) => r) -> r
withArr Discrete a b
Refl (HasArrow Discrete a b, Ob a, Ob b) => r
r = r
(HasArrow Discrete a b, Ob a, Ob b) => r
r

withEq :: Discrete a b -> ((a ~~ b) => r) -> r
withEq :: forall {k} (a :: DISCRETE k) (b :: DISCRETE k) r.
Discrete a b -> ((a ~~ b) => r) -> r
withEq Discrete a b
p (a ~~ b) => r
r = (a ~> b) -> ((a ~ b) => r) -> r
forall k (a :: k) (b :: k) r.
Discrete k =>
(a ~> b) -> ((a ~ b) => r) -> r
forall (a :: DISCRETE k) (b :: DISCRETE k) r.
(a ~> b) -> ((a ~ b) => r) -> r
Thin.withEq a ~> b
Discrete a b
p r
(a ~ b) => r
(a ~~ b) => r
r

instance DaggerProfunctor Discrete where
  dagger :: forall (a :: DISCRETE k) (b :: DISCRETE k).
Discrete a b -> Discrete b a
dagger Discrete a b
Refl = Discrete b a
Discrete b b
forall {k} (a :: DISCRETE k). Discrete a a
Refl

newtype CODISCRETE k = CD k

type Codiscrete :: CAT (CODISCRETE k)
data Codiscrete a b where
  Arr :: Codiscrete a b

-- | The codiscrete category has exactly one arrow between every object, every type of kind @k@ is an object.
instance CategoryOf (CODISCRETE k) where
  type (~>) = Codiscrete

instance Profunctor Codiscrete where
  dimap :: forall (c :: CODISCRETE k) (a :: CODISCRETE k) (b :: CODISCRETE k)
       (d :: CODISCRETE k).
(c ~> a) -> (b ~> d) -> Codiscrete a b -> Codiscrete c d
dimap = (c ~> a) -> (b ~> d) -> Codiscrete a b -> Codiscrete c d
Codiscrete c a
-> Codiscrete b d -> Codiscrete a b -> Codiscrete c d
forall {k} (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
instance Promonad Codiscrete where
  id :: forall (a :: CODISCRETE k). Ob a => Codiscrete a a
id = Codiscrete a a
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k). Codiscrete a b
Arr
  Codiscrete b c
Arr . :: forall (b :: CODISCRETE k) (c :: CODISCRETE k) (a :: CODISCRETE k).
Codiscrete b c -> Codiscrete a b -> Codiscrete a c
. Codiscrete a b
Arr = Codiscrete a c
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k). Codiscrete a b
Arr

instance Thin.ThinProfunctor Codiscrete where
  type HasArrow Codiscrete a b = ()
  arr :: forall (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b, HasArrow Codiscrete a b) =>
Codiscrete a b
arr = Codiscrete a b
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k). Codiscrete a b
Arr
  withArr :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) r.
Codiscrete a b -> ((HasArrow Codiscrete a b, Ob a, Ob b) => r) -> r
withArr Codiscrete a b
Arr (HasArrow Codiscrete a b, Ob a, Ob b) => r
r = r
(HasArrow Codiscrete a b, Ob a, Ob b) => r
r

anyArr :: Codiscrete a b
anyArr :: forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k). Codiscrete a b
anyArr = Codiscrete a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(CodiscreteProfunctor p, Ob a, Ob b) =>
p a b
forall (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Codiscrete a b
Thin.anyArr

instance DaggerProfunctor Codiscrete where
  dagger :: forall (a :: CODISCRETE k) (b :: CODISCRETE k).
Codiscrete a b -> Codiscrete b a
dagger Codiscrete a b
Arr = Codiscrete b a
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k). Codiscrete a b
Arr