{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Enriched where

import Data.Kind (Constraint, Type)
import Prelude (Maybe (..))

import Proarrow.Category.Dagger (DaggerProfunctor (..))
import Proarrow.Category.Instance.Constraint (CONSTRAINT (..), (:-) (..))
import Proarrow.Category.Instance.PointedHask (POINTED (..), Pointed (..))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Sub (SUBCAT (..), Sub (..))
import Proarrow.Category.Monoidal (Monoidal (..))
import Proarrow.Core (Any, CAT, CategoryOf (..), Kind, Profunctor (..), type (+->))
import Proarrow.Monoid (MONOIDK (..), Mon (..), Monoid (..))
import Proarrow.Object.BinaryProduct ()
import Proarrow.Object.Exponential (Closed (..), lower, mkExponential)
import Proarrow.Object.Initial (HasZeroObject (..))
import Proarrow.Preorder.ThinCategory (ThinProfunctor (..), CodiscreteProfunctor (..))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Wrapped (Wrapped (..))
import qualified Proarrow.Category.Instance.Unit as U

-- | Working with enriched categories and profunctors in Haskell is hard.
-- Instead we encode them using the underlying regular category/profunctor,
-- and show that the enriched structure can be recovered.
type Enriched :: forall {j} {k}. Kind -> j +-> k -> Constraint
class (Monoidal v, Profunctor p) => Enriched v (p :: j +-> k) where
  type Hom v (p :: j +-> k) (a :: k) (b :: j) :: v
  underlying :: p a b -> Unit ~> Hom v p a b
  enriched :: (Ob a, Ob b) => Unit ~> Hom v p a b -> p a b

-- abusing SUBCAT Any as a cheap wrapper to prevent overlapping instances
type Self k = SUBCAT (Any :: k -> Constraint)

-- | Closed monoidal categories are enriched in themselves.
instance (Closed k) => Enriched (Self k) (Id :: k +-> k) where
  type Hom (Self k) (Id :: k +-> k) (a :: k) (b :: k) = SUB (a ~~> b)
  underlying :: forall (a :: k) (b :: k). Id a b -> Unit ~> Hom (Self k) Id a b
underlying (Id a ~> b
f) = (Unit ~> (a ~~> b)) -> Sub (~>) (SUB Unit) (SUB (a ~~> b))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub ((a ~> b) -> Unit ~> (a ~~> b)
forall {k} (a :: k) (b :: k).
Closed k =>
(a ~> b) -> Unit ~> (a ~~> b)
mkExponential a ~> b
f)
  enriched :: forall (a :: k) (b :: k).
(Ob a, Ob b) =>
(Unit ~> Hom (Self k) Id a b) -> Id a b
enriched (Sub a1 ~> b1
f) = (a ~> b) -> Id a b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id ((Unit ~> (a ~~> b)) -> a ~> b
forall {k} (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
(Unit ~> (a ~~> b)) -> a ~> b
lower a1 ~> b1
Unit ~> (a ~~> b)
f)

instance (Profunctor p) => Enriched Type (Wrapped p) where
  type Hom Type (Wrapped p) a b = p a b
  underlying :: forall (a :: k) (b :: j).
Wrapped p a b -> Unit ~> Hom Type (Wrapped p) a b
underlying (Wrapped p a b
p) () = p a b
p
  enriched :: forall (a :: k) (b :: j).
(Ob a, Ob b) =>
(Unit ~> Hom Type (Wrapped p) a b) -> Wrapped p a b
enriched Unit ~> Hom Type (Wrapped p) a b
f = p a b -> Wrapped p a b
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> Wrapped p a b
Wrapped (Unit ~> Hom Type (Wrapped p) a b
() -> p a b
f ())

instance (DaggerProfunctor p) => Enriched (Type, Type) (Wrapped p) where
  type Hom (Type, Type) (Wrapped p) a b = '(p a b, p b a)
  underlying :: forall (a :: j) (b :: j).
Wrapped p a b -> Unit ~> Hom (Type, Type) (Wrapped p) a b
underlying (Wrapped p a b
p) = (\() -> p a b
p) (() -> p a b)
-> (() -> p b a) -> (:**:) (->) (->) '((), ()) '(p a b, p b a)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (\() -> p a b -> p b a
forall (a :: j) (b :: j). p a b -> p b a
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
dagger p a b
p)
  enriched :: forall (a :: j) (b :: j).
(Ob a, Ob b) =>
(Unit ~> Hom (Type, Type) (Wrapped p) a b) -> Wrapped p a b
enriched (a1 -> b1
f :**: a2 -> b2
_) = p a b -> Wrapped p a b
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> Wrapped p a b
Wrapped (a1 -> b1
() -> p a b
f ())

instance (ThinProfunctor p) => Enriched CONSTRAINT (Wrapped p) where
  type Hom CONSTRAINT (Wrapped p) a b = CNSTRNT (HasArrow p a b)
  underlying :: forall (a :: k) (b :: j).
Wrapped p a b -> Unit ~> Hom CONSTRAINT (Wrapped p) a b
underlying (Wrapped p a b
p) = (forall r. (((() :: Constraint) => HasArrow p a b) => r) -> r)
-> 'CNSTRNT (() :: Constraint) :- 'CNSTRNT (HasArrow p a b)
forall (a1 :: Constraint) (b1 :: Constraint).
(forall r. ((a1 => b1) => r) -> r) -> 'CNSTRNT a1 :- 'CNSTRNT b1
Entails (p a b -> (HasArrow p a b => r) -> r
forall (a :: k) (b :: j) r. p a b -> (HasArrow p a b => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> (HasArrow p a b => r) -> r
withArr p a b
p)
  enriched :: forall (a :: k) (b :: j).
(Ob a, Ob b) =>
(Unit ~> Hom CONSTRAINT (Wrapped p) a b) -> Wrapped p a b
enriched (Entails forall r. ((a1 => b1) => r) -> r
f) = p a b -> Wrapped p a b
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> Wrapped p a b
Wrapped (((a1 => b1) => p a b) -> p a b
forall r. ((a1 => b1) => r) -> r
f p a b
(a1 => b1) => p a b
forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow p a b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr)

instance (CodiscreteProfunctor p) => Enriched () (Wrapped p) where
  type Hom () (Wrapped p) a b = '()
  underlying :: forall (a :: k) (b :: j).
Wrapped p a b -> Unit ~> Hom () (Wrapped p) a b
underlying Wrapped p a b
_ = Unit ~> Hom () (Wrapped p) a b
Unit '() '()
U.Unit
  enriched :: forall (a :: k) (b :: j).
(Ob a, Ob b) =>
(Unit ~> Hom () (Wrapped p) a b) -> Wrapped p a b
enriched Unit ~> Hom () (Wrapped p) a b
Unit '() '()
U.Unit = p a b -> Wrapped p a b
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> Wrapped p a b
Wrapped p a b
forall (a :: k) (b :: j). (Ob a, Ob b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(CodiscreteProfunctor p, Ob a, Ob b) =>
p a b
anyArr

instance (HasZeroObject k) => Enriched POINTED (Id :: k +-> k) where
  type Hom POINTED (Id :: k +-> k) (a :: k) (b :: k) = P (a ~> b)
  underlying :: forall (a :: k) (b :: k). Id a b -> Unit ~> Hom POINTED Id a b
underlying (Id a ~> b
f) = (() -> Maybe (a ~> b)) -> Pointed (P ()) (P (a ~> b))
forall a1 b1. (a1 -> Maybe b1) -> Pointed (P a1) (P b1)
Pt \() -> (a ~> b) -> Maybe (a ~> b)
forall a. a -> Maybe a
Just a ~> b
f
  enriched :: forall (a :: k) (b :: k).
(Ob a, Ob b) =>
(Unit ~> Hom POINTED Id a b) -> Id a b
enriched (Pt a1 -> Maybe b1
f) = (a ~> b) -> Id a b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (case a1 -> Maybe b1
f () of Just b1
g -> b1
a ~> b
g; Maybe b1
Nothing -> a ~> b
forall (a :: k) (b :: k). (Ob a, Ob b) => a ~> b
forall k (a :: k) (b :: k). (HasZeroObject k, Ob a, Ob b) => a ~> b
zero)

-- | A monoid is a one object enriched category.
instance (Monoid (m :: k)) => Enriched k (Mon :: CAT (MONOIDK m)) where
  type Hom k (Mon :: MONOIDK m +-> MONOIDK m) M M = m
  underlying :: forall (a :: MONOIDK m) (b :: MONOIDK m).
Mon a b -> Unit ~> Hom k Mon a b
underlying (Mon Unit ~> m
f) = Unit ~> m
Unit ~> Hom k Mon a b
f
  enriched :: forall (a :: MONOIDK m) (b :: MONOIDK m).
(Ob a, Ob b) =>
(Unit ~> Hom k Mon a b) -> Mon a b
enriched Unit ~> Hom k Mon a b
f = (Unit ~> m) -> Mon M M
forall {k} {k1} {m1 :: k1} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
Unit ~> Hom k Mon a b
f