{-# LANGUAGE AllowAmbiguousTypes #-}

-- | The thin category @CONSTRAINT@ of type class constraints, with entailment @(':-')@ as arrows:
-- @a ':-' b@ holds when @a@ implies @b@. Constraint conjunction is both the categorical product and
-- the tensor of a closed symmetric monoidal structure, with @()@ as unit and terminal object.
module Proarrow.Category.Instance.Constraint (CONSTRAINT (..), (:-) (..), (:=>) (..), reifyExp, eqIsSuperOrd, maybeLiftsSemigroup) where

import Data.Kind (Constraint)
import GHC.Exts (withDict)
import Prelude qualified as P

import Proarrow.Category.Enriched.Thin (ThinProfunctor (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Closed (Closed (..))
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard)
import Proarrow.Core (CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault)
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Limit.BinaryProduct qualified as P
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Monoid (CocommutativeComonoid, Comonoid (..), Monoid (..))

type data CONSTRAINT = CNSTRNT Constraint

data (:-) a b where
  Entails :: {forall (a :: Constraint) (b :: Constraint).
(CNSTRNT a :- CNSTRNT b) -> forall r. a => (b => r) -> r
unEntails :: forall r. (a) => ((b) => r) -> r} -> CNSTRNT a :- CNSTRNT b

-- | The category of type class constraints. An arrow from constraint a to constraint b
-- means that a implies b, i.e. if a holds then b holds.
instance CategoryOf CONSTRAINT where
  type (~>) = (:-)
  type Ob a = (Is CNSTRNT a)

instance Promonad (:-) where
  id :: forall (a :: CONSTRAINT). Ob a => a :- a
id = (forall r. UN CNSTRNT a => (UN CNSTRNT a => r) -> r)
-> CNSTRNT (UN CNSTRNT a) :- CNSTRNT (UN CNSTRNT a)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> CNSTRNT a :- CNSTRNT b
Entails \UN CNSTRNT a => r
r -> r
UN CNSTRNT a => r
r
  Entails forall r. a => (b => r) -> r
f . :: forall (b :: CONSTRAINT) (c :: CONSTRAINT) (a :: CONSTRAINT).
(b :- c) -> (a :- b) -> a :- c
. Entails forall r. a => (b => r) -> r
g = (forall r. a => (b => r) -> r) -> CNSTRNT a :- CNSTRNT b
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> CNSTRNT a :- CNSTRNT b
Entails \b => r
r -> (b => r) -> r
forall r. a => (b => r) -> r
g ((b => r) -> r
forall r. a => (b => r) -> r
f r
b => r
r)

instance Profunctor (:-) where
  dimap :: forall (c :: CONSTRAINT) (a :: CONSTRAINT) (b :: CONSTRAINT)
       (d :: CONSTRAINT).
(c ~> a) -> (b ~> d) -> (a :- b) -> c :- d
dimap = (c ~> a) -> (b ~> d) -> (a :- b) -> c :- d
(c :- a) -> (b :- d) -> (a :- b) -> c :- d
forall {k} (p :: CAT k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) r.
((Ob a, Ob b) => r) -> (a :- b) -> r
\\ Entails{} = r
(Ob a, Ob b) => r
r

instance ThinProfunctor (:-) where
  type HasArrow (:-) a b = UN CNSTRNT a :=> UN CNSTRNT b
  arr :: forall (a :: CONSTRAINT) (b :: CONSTRAINT).
(Ob a, Ob b, HasArrow (:-) a b) =>
a :- b
arr @(CNSTRNT a) @(CNSTRNT b) = (forall r. UN CNSTRNT a => (UN CNSTRNT b => r) -> r)
-> CNSTRNT (UN CNSTRNT a) :- CNSTRNT (UN CNSTRNT b)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> CNSTRNT a :- CNSTRNT b
Entails \UN CNSTRNT b => r
r -> (CNSTRNT (UN CNSTRNT a) :- CNSTRNT (UN CNSTRNT b))
-> forall r. UN CNSTRNT a => (UN CNSTRNT b => r) -> r
forall (a :: Constraint) (b :: Constraint).
(CNSTRNT a :- CNSTRNT b) -> forall r. a => (b => r) -> r
unEntails (forall (b :: Constraint) (c :: Constraint).
(b :=> c) =>
CNSTRNT b :- CNSTRNT c
entails @a @b) r
UN CNSTRNT b => r
r
  withArr :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) r.
(a :- b) -> ((HasArrow (:-) a b, Ob a, Ob b) => r) -> r
withArr p :: a :- b
p@Entails{} (HasArrow (:-) a b, Ob a, Ob b) => r
r = (CNSTRNT a :- CNSTRNT b) -> ((a :=> b) => r) -> r
forall (b :: Constraint) (c :: Constraint) r.
(CNSTRNT b :- CNSTRNT c) -> ((b :=> c) => r) -> r
reifyExp a :- b
CNSTRNT a :- CNSTRNT b
p r
(HasArrow (:-) a b, Ob a, Ob b) => r
(a :=> b) => r
r

instance HasTerminalObject CONSTRAINT where
  type TerminalObject = CNSTRNT ()
  terminate :: forall (a :: CONSTRAINT). Ob a => a ~> TerminalObject
terminate = (forall r. UN CNSTRNT a => ((() :: Constraint) => r) -> r)
-> CNSTRNT (UN CNSTRNT a) :- CNSTRNT (() :: Constraint)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> CNSTRNT a :- CNSTRNT b
Entails \(() :: Constraint) => r
r -> r
(() :: Constraint) => r
r

instance HasBinaryProducts CONSTRAINT where
  type CNSTRNT l && CNSTRNT r = CNSTRNT (l, r)
  withObProd :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd Ob (a && b) => r
r = r
Ob (a && b) => r
r
  fst :: forall (a :: CONSTRAINT) (b :: CONSTRAINT).
(Ob a, Ob b) =>
(a && b) ~> a
fst = (forall r.
 (UN CNSTRNT a, UN CNSTRNT b) =>
 (UN CNSTRNT a => r) -> r)
-> CNSTRNT (UN CNSTRNT a, UN CNSTRNT b) :- CNSTRNT (UN CNSTRNT a)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> CNSTRNT a :- CNSTRNT b
Entails \UN CNSTRNT a => r
r -> r
UN CNSTRNT a => r
r
  snd :: forall (a :: CONSTRAINT) (b :: CONSTRAINT).
(Ob a, Ob b) =>
(a && b) ~> b
snd = (forall r.
 (UN CNSTRNT a, UN CNSTRNT b) =>
 (UN CNSTRNT b => r) -> r)
-> CNSTRNT (UN CNSTRNT a, UN CNSTRNT b) :- CNSTRNT (UN CNSTRNT b)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> CNSTRNT a :- CNSTRNT b
Entails \UN CNSTRNT b => r
r -> r
UN CNSTRNT b => r
r
  Entails forall r. a => (b => r) -> r
f &&& :: forall (a :: CONSTRAINT) (x :: CONSTRAINT) (y :: CONSTRAINT).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Entails forall r. a => (b => r) -> r
g = (forall r. a => ((b, b) => r) -> r) -> CNSTRNT a :- CNSTRNT (b, b)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> CNSTRNT a :- CNSTRNT b
Entails \(b, b) => r
r -> (b => r) -> r
forall r. a => (b => r) -> r
f ((b => r) -> r
forall r. a => (b => r) -> r
g r
b => r
(b, b) => r
r)

instance MonoidalProfunctor (:-) where
  one :: Unit :- Unit
one = Unit :- Unit
CNSTRNT (() :: Constraint) :- CNSTRNT (() :: Constraint)
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: CONSTRAINT). Ob a => a :- a
id
  x1 :- x2
f ** :: forall (x1 :: CONSTRAINT) (x2 :: CONSTRAINT) (y1 :: CONSTRAINT)
       (y2 :: CONSTRAINT).
(x1 :- x2) -> (y1 :- y2) -> (x1 ** y1) :- (x2 ** y2)
** y1 :- y2
g = x1 ~> x2
x1 :- x2
f (x1 ~> x2) -> (y1 ~> y2) -> (x1 && y1) ~> (x2 && y2)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall (a :: CONSTRAINT) (b :: CONSTRAINT) (x :: CONSTRAINT)
       (y :: CONSTRAINT).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** y1 ~> y2
y1 :- y2
g

-- | Products as monoidal structure.
instance Monoidal CONSTRAINT where
  type Unit = TerminalObject
  type a ** b = a && b
  withOb2 :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 Ob (a ** b) => r
r = r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: CONSTRAINT). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
(TerminalObject && CNSTRNT (UN CNSTRNT a))
~> CNSTRNT (UN CNSTRNT a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(TerminalObject && a) ~> a
P.leftUnitorProd
  leftUnitorInv :: forall (a :: CONSTRAINT). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
CNSTRNT (UN CNSTRNT a)
~> (TerminalObject && CNSTRNT (UN CNSTRNT a))
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (TerminalObject && a)
P.leftUnitorProdInv
  rightUnitor :: forall (a :: CONSTRAINT). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
(CNSTRNT (UN CNSTRNT a) && TerminalObject)
~> CNSTRNT (UN CNSTRNT a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(a && TerminalObject) ~> a
P.rightUnitorProd
  rightUnitorInv :: forall (a :: CONSTRAINT). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
CNSTRNT (UN CNSTRNT a)
~> (CNSTRNT (UN CNSTRNT a) && TerminalObject)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (a && TerminalObject)
P.rightUnitorProdInv
  associator :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) (c :: CONSTRAINT).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = ((a ** b) ** c) ~> (a ** (b ** c))
((CNSTRNT (UN CNSTRNT a) && CNSTRNT (UN CNSTRNT b))
 && CNSTRNT (UN CNSTRNT c))
~> (CNSTRNT (UN CNSTRNT a)
    && (CNSTRNT (UN CNSTRNT b) && CNSTRNT (UN CNSTRNT c)))
forall {k} (a :: k) (b :: k) (c :: k).
(HasBinaryProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
P.associatorProd
  associatorInv :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) (c :: CONSTRAINT).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = (a ** (b ** c)) ~> ((a ** b) ** c)
(CNSTRNT (UN CNSTRNT a)
 && (CNSTRNT (UN CNSTRNT b) && CNSTRNT (UN CNSTRNT c)))
~> ((CNSTRNT (UN CNSTRNT a) && CNSTRNT (UN CNSTRNT b))
    && CNSTRNT (UN CNSTRNT c))
forall {k} (a :: k) (b :: k) (c :: k).
(HasBinaryProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
P.associatorProdInv

instance SymMonoidal CONSTRAINT where
  swap :: forall (a :: CONSTRAINT) (b :: CONSTRAINT).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap = (forall r.
 (UN CNSTRNT a, UN CNSTRNT b) =>
 ((UN CNSTRNT b, UN CNSTRNT a) => r) -> r)
-> CNSTRNT (UN CNSTRNT a, UN CNSTRNT b)
   :- CNSTRNT (UN CNSTRNT b, UN CNSTRNT a)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> CNSTRNT a :- CNSTRNT b
Entails \(UN CNSTRNT b, UN CNSTRNT a) => r
r -> r
(UN CNSTRNT b, UN CNSTRNT a) => r
r

instance Monoid (CNSTRNT ()) where
  mempty :: Unit ~> CNSTRNT (() :: Constraint)
mempty = Unit ~> CNSTRNT (() :: Constraint)
CNSTRNT (() :: Constraint) :- CNSTRNT (() :: Constraint)
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: CONSTRAINT). Ob a => a :- a
id
  mappend :: (CNSTRNT (() :: Constraint) ** CNSTRNT (() :: Constraint))
~> CNSTRNT (() :: Constraint)
mappend = (forall r.
 (() :: Constraint, () :: Constraint) =>
 ((() :: Constraint) => r) -> r)
-> CNSTRNT (() :: Constraint, () :: Constraint)
   :- CNSTRNT (() :: Constraint)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> CNSTRNT a :- CNSTRNT b
Entails \(() :: Constraint) => r
r -> r
(() :: Constraint) => r
r

instance Comonoid (CNSTRNT a) where
  counit :: CNSTRNT a ~> Unit
counit = (forall r. a => ((() :: Constraint) => r) -> r)
-> CNSTRNT a :- CNSTRNT (() :: Constraint)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> CNSTRNT a :- CNSTRNT b
Entails \(() :: Constraint) => r
r -> r
(() :: Constraint) => r
r
  comult :: CNSTRNT a ~> (CNSTRNT a ** CNSTRNT a)
comult = (forall r. a => ((a, a) => r) -> r) -> CNSTRNT a :- CNSTRNT (a, a)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> CNSTRNT a :- CNSTRNT b
Entails \(a, a) => r
r -> r
(a, a) => r
r
instance CocommutativeComonoid (CNSTRNT a)
instance CopyDiscard CONSTRAINT

class b :=> c where
  entails :: CNSTRNT b :- CNSTRNT c
instance ((b) => c) => (b :=> c) where
  entails :: CNSTRNT b :- CNSTRNT c
entails = (forall r. b => (c => r) -> r) -> CNSTRNT b :- CNSTRNT c
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> CNSTRNT a :- CNSTRNT b
Entails \c => r
r -> r
c => r
r

reifyExp :: forall b c r. CNSTRNT b :- CNSTRNT c -> ((b :=> c) => r) -> r
reifyExp :: forall (b :: Constraint) (c :: Constraint) r.
(CNSTRNT b :- CNSTRNT c) -> ((b :=> c) => r) -> r
reifyExp = forall (cls :: Constraint) meth r.
WithDict cls meth =>
meth -> (cls => r) -> r
withDict @(b :=> c)

instance Closed CONSTRAINT where
  type a ~~> b = CNSTRNT (UN CNSTRNT a :=> UN CNSTRNT b)
  withObExp :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp Ob (a ~~> b) => r
r = r
Ob (a ~~> b) => r
r
  curry :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) (c :: CONSTRAINT).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @_ @(CNSTRNT b) (Entails @_ @c forall r. a => (b => r) -> r
f) = (forall r. UN CNSTRNT a => ((UN CNSTRNT b :=> b) => r) -> r)
-> CNSTRNT (UN CNSTRNT a) :- CNSTRNT (UN CNSTRNT b :=> b)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> CNSTRNT a :- CNSTRNT b
Entails \(UN CNSTRNT b :=> b) => r
r -> (CNSTRNT (UN CNSTRNT b) :- CNSTRNT b)
-> ((UN CNSTRNT b :=> b) => r) -> r
forall (b :: Constraint) (c :: Constraint) r.
(CNSTRNT b :- CNSTRNT c) -> ((b :=> c) => r) -> r
reifyExp (forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> CNSTRNT a :- CNSTRNT b
Entails @b @c (b => r) -> r
forall r. a => (b => r) -> r
forall {r}. UN CNSTRNT b => (b => r) -> r
f) r
(UN CNSTRNT b :=> b) => r
r
  apply :: forall (a :: CONSTRAINT) (b :: CONSTRAINT).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @(CNSTRNT a) @(CNSTRNT b) = (forall r.
 (UN CNSTRNT a :=> UN CNSTRNT b, UN CNSTRNT a) =>
 (UN CNSTRNT b => r) -> r)
-> CNSTRNT (UN CNSTRNT a :=> UN CNSTRNT b, UN CNSTRNT a)
   :- CNSTRNT (UN CNSTRNT b)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> CNSTRNT a :- CNSTRNT b
Entails \UN CNSTRNT b => r
r -> (CNSTRNT (UN CNSTRNT a) :- CNSTRNT (UN CNSTRNT b))
-> forall r. UN CNSTRNT a => (UN CNSTRNT b => r) -> r
forall (a :: Constraint) (b :: Constraint).
(CNSTRNT a :- CNSTRNT b) -> forall r. a => (b => r) -> r
unEntails (forall (b :: Constraint) (c :: Constraint).
(b :=> c) =>
CNSTRNT b :- CNSTRNT c
entails @a @b) r
UN CNSTRNT b => r
r

eqIsSuperOrd :: CNSTRNT (P.Ord a) :- CNSTRNT (P.Eq a)
eqIsSuperOrd :: forall a. CNSTRNT (Ord a) :- CNSTRNT (Eq a)
eqIsSuperOrd = (forall r. Ord a => (Eq a => r) -> r)
-> CNSTRNT (Ord a) :- CNSTRNT (Eq a)
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> CNSTRNT a :- CNSTRNT b
Entails \Eq a => r
r -> r
Eq a => r
r

maybeLiftsSemigroup :: CNSTRNT (P.Semigroup a) :- CNSTRNT (Monoid (P.Maybe a))
maybeLiftsSemigroup :: forall a. CNSTRNT (Semigroup a) :- CNSTRNT (Monoid (Maybe a))
maybeLiftsSemigroup = (forall r. Semigroup a => (Monoid (Maybe a) => r) -> r)
-> CNSTRNT (Semigroup a) :- CNSTRNT (Monoid (Maybe a))
forall (a :: Constraint) (b :: Constraint).
(forall r. a => (b => r) -> r) -> CNSTRNT a :- CNSTRNT b
Entails \Monoid (Maybe a) => r
r -> r
Monoid (Maybe a) => r
r