{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Totally ordered, integral quantales, as far as computing closures of enriched profunctors
-- needs them: 'Proarrow.Category.Instance.Bool.BOOL' (relations, reachability) and
-- 'Proarrow.Category.Instance.Cost.COST' (metric spaces, shortest paths). Besides the structure
-- their classes already provide, the closure needs a handful of facts reflected to the value level,
-- collected in 'Quantale'.
module Proarrow.Category.Enriched.Quantale where

import Data.Kind (Type)
import Data.Proxy (Proxy (..))
import Data.Type.Ord (OrderingI (..))
import GHC.TypeNats (cmpNat)
import Prelude (error, type (~))

import Proarrow.Category.Enriched.Thin (Decidable, Decision (..), decide)
import Proarrow.Category.Instance.Bool (BOOL (..), Booleans (..))
import Proarrow.Category.Instance.Cost (COST (..), GTE (..), IsCost (..), SCost (..))
import Proarrow.Category.Monoidal (Monoidal (..), leftUnitorWith, rightUnitorWith)
import Proarrow.Category.Monoidal.Distributive (Distributive (..))
import Proarrow.Colimit.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Core (CategoryOf (..), Hom, Promonad (..), obj)
import Proarrow.Limit.Terminal (HasTerminalObject (..), Semicartesian)

-- | As much of a quantale as a closure needs, and a totally ordered, integral one at that: a
-- 'Semicartesian' 'Distributive' category, so that the unit is the top element and the bottom
-- absorbs, in which the join of two objects is one of them ('minIs') and the order is decidable.
-- Totality is what makes a single best walk exist; in a quantale of, say, sets of paths, a join is
-- attained by no one summand. Infinite joins are not needed, since there are finitely many objects.
--
-- The methods reflect to the value level facts that GHC cannot see through the type families:
-- 'minIs' is totality, and 'unitIsNotBottom' and 'unitIsTop' say the order is nondegenerate and
-- skeletal -- the latter is antisymmetry at the unit, since 'Semicartesian' already gives the
-- arrow the other way.
class (Semicartesian v, Distributive v, Decidable v) => Quantale v where
  minIs :: forall (x :: v) y. (Ob x, Ob y) => MinIs x y
  unitIsNotBottom :: forall r. (Unit :: v) ~> InitialObject -> r
  unitIsTop :: forall (w :: v) r. (Ob w) => (Unit ~> w) -> ((w ~ Unit) => r) -> r

-- | Which of two objects their join is.
type MinIs :: forall {v}. v -> v -> Type
data MinIs x y where
  MinLeft :: ((x || y) ~ x) => MinIs x y
  MinRight :: ((x || y) ~ y) => MinIs x y

-- | In an integral quantale a tensor lies below each of its factors, since the other factor is at
-- most the unit, so a unit into a tensor is a unit into each factor.
splitUnit :: forall {v} (x :: v) y. (Quantale v, Ob x, Ob y) => Unit ~> (x ** y) -> (Unit ~> x, Unit ~> y)
splitUnit :: forall {v} (x :: v) (y :: v).
(Quantale v, Ob x, Ob y) =>
(Unit ~> (x ** y)) -> (Unit ~> x, Unit ~> y)
splitUnit Unit ~> (x ** y)
f = (forall (a :: v) (b :: v).
(Monoidal v, Ob a) =>
(b ~> Unit) -> (a ** b) ~> a
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (a ** b) ~> a
rightUnitorWith @x (forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate @v @y) ((x ** y) ~> x)
-> (TerminalObject ~> (x ** y)) -> TerminalObject ~> x
forall (b :: v) (c :: v) (a :: v). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Unit ~> (x ** y)
TerminalObject ~> (x ** y)
f, forall (a :: v) (b :: v).
(Monoidal v, Ob a) =>
(b ~> Unit) -> (b ** a) ~> a
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (b ** a) ~> a
leftUnitorWith @y (forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate @v @x) ((x ** y) ~> y)
-> (TerminalObject ~> (x ** y)) -> TerminalObject ~> y
forall (b :: v) (c :: v) (a :: v). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Unit ~> (x ** y)
TerminalObject ~> (x ** y)
f)

-- | The bottom absorbs the tensor, and nothing lies below the bottom.
bottomTensor :: forall {v} (x :: v) y. (Quantale v, Ob x, Ob y) => (InitialObject ** x) ~> y
bottomTensor :: forall {v} (x :: v) (y :: v).
(Quantale v, Ob x, Ob y) =>
(InitialObject ** x) ~> y
bottomTensor = forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @v @y (InitialObject ~> y)
-> ((InitialObject ** x) ~> InitialObject)
-> (InitialObject ** x) ~> y
forall (b :: v) (c :: v) (a :: v). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k).
(Distributive k, Ob a) =>
(InitialObject ** a) ~> InitialObject
absorbR @v @x

-- | The arrow between two objects of a decidable order, when the caller knows it exists but its
-- existence is not derived structurally -- the triangle inequality for closures, for instance. As
-- elsewhere in "Proarrow.Category.Instance.Cost", it is checked at runtime.
checkedArrow :: forall v (x :: v) y. (Decidable v, Ob x, Ob y) => x ~> y
checkedArrow :: forall v (x :: v) (y :: v). (Decidable v, Ob x, Ob y) => x ~> y
checkedArrow = case forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: v +-> v) (a :: v) (b :: v).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @(Hom v) @x @y of
  Yes x ~> y
f -> x ~> y
f
  Decision (~>) x y (Holds (~>) x y)
No -> [Char] -> x ~> y
forall a. HasCallStack => [Char] -> a
error [Char]
"checkedArrow: the checked arrow does not exist"

-- | The walking arrow: the tensor is conjunction, the join disjunction.
instance Quantale BOOL where
  minIs :: forall (x :: BOOL) (y :: BOOL). (Ob x, Ob y) => MinIs x y
minIs @x = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @x of
    Obj x
Booleans x x
Tru -> MinIs x y
forall {v} (x :: v) (y :: v). ((x || y) ~ x) => MinIs x y
MinLeft
    Obj x
Booleans x x
Fls -> MinIs x y
forall {v} (x :: v) (y :: v). ((x || y) ~ y) => MinIs x y
MinRight
  unitIsNotBottom :: forall r. (Unit ~> InitialObject) -> r
unitIsNotBottom = \case {}
  unitIsTop :: forall (w :: BOOL) r. Ob w => (Unit ~> w) -> ((w ~ Unit) => r) -> r
unitIsTop Unit ~> w
Booleans 'TRU w
Tru (w ~ Unit) => r
r = r
(w ~ Unit) => r
r

-- | Costs: the tensor is addition, the join the minimum. Distances are compared with 'cmpNat', whose
-- evidence makes the type-level 'Data.Type.Ord.Min' reduce; that a natural below @0@ is @0@ is
-- arithmetic GHC cannot see, so it is checked at runtime.
instance Quantale COST where
  minIs :: forall (x :: COST) (y :: COST). (Ob x, Ob y) => MinIs x y
minIs @x @y = case (forall (a :: COST). IsCost a => SCost a
sing @x, forall (a :: COST). IsCost a => SCost a
sing @y) of
    (SCost x
SINF, SCost y
_) -> MinIs x y
forall {v} (x :: v) (y :: v). ((x || y) ~ y) => MinIs x y
MinRight
    (SCost x
SC, SCost y
SINF) -> MinIs x y
forall {v} (x :: v) (y :: v). ((x || y) ~ x) => MinIs x y
MinLeft
    (SC @m, SC @m') -> case Proxy n1 -> Proxy n1 -> OrderingI n1 n1
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @m) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @m') of
      OrderingI n1 n1
LTI -> MinIs x y
forall {v} (x :: v) (y :: v). ((x || y) ~ x) => MinIs x y
MinLeft
      OrderingI n1 n1
EQI -> MinIs x y
forall {v} (x :: v) (y :: v). ((x || y) ~ x) => MinIs x y
MinLeft
      OrderingI n1 n1
GTI -> MinIs x y
forall {v} (x :: v) (y :: v). ((x || y) ~ y) => MinIs x y
MinRight
  unitIsNotBottom :: forall r. (Unit ~> InitialObject) -> r
unitIsNotBottom = \case {}
  unitIsTop :: forall (w :: COST) r. Ob w => (Unit ~> w) -> ((w ~ Unit) => r) -> r
unitIsTop @w Unit ~> w
f (w ~ Unit) => r
r = case forall (a :: COST). IsCost a => SCost a
sing @w of
    SCost w
SINF -> case Unit ~> w
f of {}
    SC @m -> case Unit ~> w
f of
      Unit ~> w
GTE (C 0) (C n1)
GTE -> case Proxy n1 -> Proxy 0 -> OrderingI n1 0
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @m) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @0) of
        OrderingI n1 0
EQI -> r
(w ~ Unit) => r
r
        OrderingI n1 0
LTI -> [Char] -> r
forall a. HasCallStack => [Char] -> a
error [Char]
"COST: a natural below 0"