{-# LANGUAGE AllowAmbiguousTypes #-}
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.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Core (CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault)
import Proarrow.Monoid (Comonoid (..), Monoid (..), CopyDiscard)
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Object.BinaryProduct qualified as P
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Category.Enriched.ThinCategory (ThinProfunctor (..))
newtype CONSTRAINT = CNSTRNT Constraint
type instance UN CNSTRNT (CNSTRNT a) = a
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
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 :: 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
(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 => r) -> r
withArr p :: a :- b
p@Entails{} = ('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
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
par0 :: Unit :- Unit
par0 = Unit :- Unit
'CNSTRNT (() :: Constraint) :- 'CNSTRNT (() :: Constraint)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: CONSTRAINT). Ob a => a :- a
id
x1 :- x2
f par :: forall (x1 :: CONSTRAINT) (x2 :: CONSTRAINT) (y1 :: CONSTRAINT)
(y2 :: CONSTRAINT).
(x1 :- x2) -> (y1 :- y2) -> (x1 ** y1) :- (x2 ** y2)
`par` 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
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).
(HasProducts 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).
(HasProducts 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 :: k +-> 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 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