{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Equalizers: 'HasEqualizers' with 'equalize' in continuation-passing style (the equalizer object's
-- type depends on the given arrows, so it is hidden behind an existential) and 'factorEqualizer' for
-- the universal property.
module Proarrow.Limit.Equalizer where

import Proarrow.Category.Enriched.Thin (Thin)
import Proarrow.Category.Instance.Bool (BOOL (..), Booleans (..))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit (Unit (..))
import Proarrow.Colimit.Initial (HasZeroObject (..))
import Proarrow.Core (CategoryOf (..), Promonad (..))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..), HasProducts, PROD, Prod (..))
import Proarrow.Object (pattern Objs)
import Prelude qualified as P

-- | Equalizers are an inherently dependently typed concept:
-- The type of the base object depends on the values of the given arrows.
-- But at runtime we can still calculate the arrow and the type, which we hide behind an existential.
class (CategoryOf k) => HasEqualizers k where
  equalize :: forall (a :: k) b r. a ~> b -> a ~> b -> (forall e. e ~> a -> r) -> r

  -- | @factorEqualizer incl h@ requires @incl@ to be mono and @h@'s image to lie within @incl@'s
  -- image; @incl@ is typically (though not necessarily) the equalizer arrow produced by 'equalize'.
  factorEqualizer :: forall (e :: k) x e'. e ~> x -> e' ~> x -> e' ~> e

instance HasEqualizers () where
  equalize :: forall (a :: ()) (b :: ()) r.
(a ~> b) -> (a ~> b) -> (forall (e :: ()). (e ~> a) -> r) -> r
equalize a ~> b
Unit a b
Unit a ~> b
Unit '() '()
Unit forall (e :: ()). (e ~> a) -> r
k = ('() ~> a) -> r
forall (e :: ()). (e ~> a) -> r
k '() ~> a
Unit '() '()
Unit
  factorEqualizer :: forall (e :: ()) (x :: ()) (e' :: ()).
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer e ~> x
Unit e x
Unit e' ~> x
Unit e' '()
Unit = e' ~> e
Unit '() '()
Unit

-- | @factorEqualizer incl h@ requires @h@'s image to lie within @incl@'s. Since @BOOL@ is the
-- 2-element total order @FLS <= TRU@, that means @h@'s domain is @<=@ @incl@'s domain. That's always
-- true when @incl@ came from 'equalize' (which only ever produces the identity), but since 'BOOL' is
-- totally ordered we can case on the shapes directly (at most 5 are reachable, since both share a
-- codomain).
instance HasEqualizers BOOL where
  equalize :: forall (a :: BOOL) (b :: BOOL) r.
(a ~> b) -> (a ~> b) -> (forall (e :: BOOL). (e ~> a) -> r) -> r
equalize = (a ~> b) -> (a ~> b) -> (forall (e :: BOOL). (e ~> a) -> r) -> r
forall {k} (a :: k) (b :: k) r.
Thin k =>
(a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
thinEqualize
  factorEqualizer :: forall (e :: BOOL) (x :: BOOL) (e' :: BOOL).
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer e ~> x
Booleans e x
Fls e' ~> x
Booleans e' 'FLS
Fls = e' ~> e
Booleans 'FLS 'FLS
Fls
  factorEqualizer e ~> x
Booleans e x
F2T e' ~> x
Booleans e' 'TRU
F2T = e' ~> e
Booleans 'FLS 'FLS
Fls
  factorEqualizer e ~> x
Booleans e x
Tru e' ~> x
Booleans e' 'TRU
F2T = e' ~> e
Booleans 'FLS 'TRU
F2T
  factorEqualizer e ~> x
Booleans e x
Tru e' ~> x
Booleans e' 'TRU
Tru = e' ~> e
Booleans 'TRU 'TRU
Tru
  factorEqualizer e ~> x
Booleans e x
F2T e' ~> x
Booleans e' 'TRU
Tru = [Char] -> Booleans 'TRU 'FLS
forall a. HasCallStack => [Char] -> a
P.error [Char]
"factorEqualizer: h's image must lie within incl's image"

instance (HasEqualizers k1, HasEqualizers k2) => HasEqualizers (k1, k2) where
  equalize :: forall (a :: (k1, k2)) (b :: (k1, k2)) r.
(a ~> b)
-> (a ~> b) -> (forall (e :: (k1, k2)). (e ~> a) -> r) -> r
equalize (a1 ~> b1
l1 :**: a2 ~> b2
l2) (a1 ~> b1
r1 :**: a2 ~> b2
r2) forall (e :: (k1, k2)). (e ~> a) -> r
k = (a1 ~> b1) -> (a1 ~> b1) -> (forall (e :: k1). (e ~> a1) -> r) -> r
forall (a :: k1) (b :: k1) r.
(a ~> b) -> (a ~> b) -> (forall (e :: k1). (e ~> a) -> r) -> r
forall k (a :: k) (b :: k) r.
HasEqualizers k =>
(a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
equalize a1 ~> b1
l1 a1 ~> b1
a1 ~> b1
r1 \e ~> a1
f1 -> (a2 ~> b2) -> (a2 ~> b2) -> (forall (e :: k2). (e ~> a2) -> r) -> r
forall (a :: k2) (b :: k2) r.
(a ~> b) -> (a ~> b) -> (forall (e :: k2). (e ~> a) -> r) -> r
forall k (a :: k) (b :: k) r.
HasEqualizers k =>
(a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
equalize a2 ~> b2
l2 a2 ~> b2
a2 ~> b2
r2 \e ~> a2
f2 -> ('(e, e) ~> a) -> r
forall (e :: (k1, k2)). (e ~> a) -> r
k (e ~> a1
f1 (e ~> a1) -> (e ~> a2) -> (:**:) (~>) (~>) '(e, e) '(a1, a2)
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)
:**: e ~> a2
f2)
  factorEqualizer :: forall (e :: (k1, k2)) (x :: (k1, k2)) (e' :: (k1, k2)).
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer (a1 ~> b1
i1 :**: a2 ~> b2
i2) (a1 ~> b1
h1 :**: a2 ~> b2
h2) = (a1 ~> b1) -> (a1 ~> b1) -> a1 ~> a1
forall (e :: k1) (x :: k1) (e' :: k1).
(e ~> x) -> (e' ~> x) -> e' ~> e
forall k (e :: k) (x :: k) (e' :: k).
HasEqualizers k =>
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer a1 ~> b1
i1 a1 ~> b1
a1 ~> b1
h1 (a1 ~> a1) -> (a2 ~> a2) -> (:**:) (~>) (~>) '(a1, a2) '(a1, a2)
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)
:**: (a2 ~> b2) -> (a2 ~> b2) -> a2 ~> a2
forall (e :: k2) (x :: k2) (e' :: k2).
(e ~> x) -> (e' ~> x) -> e' ~> e
forall k (e :: k) (x :: k) (e' :: k).
HasEqualizers k =>
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer a2 ~> b2
i2 a2 ~> b2
a2 ~> b2
h2

-- | Equalizers are unchanged by making the tensor the product.
instance (HasEqualizers k) => HasEqualizers (PROD k) where
  equalize :: forall (a :: PROD k) (b :: PROD k) r.
(a ~> b) -> (a ~> b) -> (forall (e :: PROD k). (e ~> a) -> r) -> r
equalize (Prod a1 ~> b1
f) (Prod a1 ~> b1
g) forall (e :: PROD k). (e ~> a) -> r
k = (a1 ~> b1) -> (a1 ~> b1) -> (forall (e :: k). (e ~> a1) -> r) -> r
forall (a :: k) (b :: k) r.
(a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
forall k (a :: k) (b :: k) r.
HasEqualizers k =>
(a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
equalize a1 ~> b1
f a1 ~> b1
a1 ~> b1
g \e ~> a1
e -> (PR e ~> a) -> r
forall (e :: PROD k). (e ~> a) -> r
k ((e ~> a1) -> Prod (~>) (PR e) (PR a1)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod e ~> a1
e)
  factorEqualizer :: forall (e :: PROD k) (x :: PROD k) (e' :: PROD k).
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer (Prod a1 ~> b1
incl) (Prod a1 ~> b1
h) = (a1 ~> a1) -> Prod (~>) (PR a1) (PR a1)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod ((a1 ~> b1) -> (a1 ~> b1) -> a1 ~> a1
forall (e :: k) (x :: k) (e' :: k).
(e ~> x) -> (e' ~> x) -> e' ~> e
forall k (e :: k) (x :: k) (e' :: k).
HasEqualizers k =>
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer a1 ~> b1
incl a1 ~> b1
a1 ~> b1
h)

-- | In a thin category, arrows don't carry information, so equalizers are just identities.
thinEqualize :: forall {k} (a :: k) b r. (Thin k) => a ~> b -> a ~> b -> (forall e. e ~> a -> r) -> r
thinEqualize :: forall {k} (a :: k) (b :: k) r.
Thin k =>
(a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
thinEqualize a ~> b
Objs a ~> b
_ forall (e :: k). (e ~> a) -> r
k = (a ~> a) -> r
forall (e :: k). (e ~> a) -> r
k a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id

-- | Standalone helper (not a class method) usable as the @default@ implementation of
-- 'Proarrow.Limit.Pullback.pullback' wherever @(HasEqualizers k, HasProducts k)@ happen to hold.
-- Not every 'Proarrow.Limit.Pullback.HasPullbacks' instance needs it or is required to have it.
pullbackDefault
  :: forall {k} (o :: k) a b r
   . (HasEqualizers k, HasProducts k) => a ~> o -> b ~> o -> (forall p. p ~> a -> p ~> b -> r) -> r
pullbackDefault :: forall {k} (o :: k) (a :: k) (b :: k) r.
(HasEqualizers k, HasProducts k) =>
(a ~> o)
-> (b ~> o) -> (forall (p :: k). (p ~> a) -> (p ~> b) -> r) -> r
pullbackDefault f :: a ~> o
f@a ~> o
Objs g :: b ~> o
g@b ~> o
Objs forall (p :: k). (p ~> a) -> (p ~> b) -> r
k = ((a && b) ~> o)
-> ((a && b) ~> o) -> (forall (e :: k). (e ~> (a && b)) -> r) -> r
forall (a :: k) (b :: k) r.
(a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
forall k (a :: k) (b :: k) r.
HasEqualizers k =>
(a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
equalize (a ~> o
f (a ~> o) -> ((a && b) ~> a) -> (a && b) ~> o
forall (b :: k) (c :: k) (a :: k). (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) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @a @b) (b ~> o
g (b ~> o) -> ((a && b) ~> b) -> (a && b) ~> o
forall (b :: k) (c :: k) (a :: k). (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) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @a @b) \e :: e ~> (a && b)
e@e ~> (a && b)
Objs -> (e ~> a) -> (e ~> b) -> r
forall (p :: k). (p ~> a) -> (p ~> b) -> r
k (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @a @b ((a && b) ~> a) -> (e ~> (a && b)) -> e ~> a
forall (b :: k) (c :: k) (a :: k). (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
. e ~> (a && b)
e) (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @a @b ((a && b) ~> b) -> (e ~> (a && b)) -> e ~> b
forall (b :: k) (c :: k) (a :: k). (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
. e ~> (a && b)
e)

-- | Given a pullback's own legs @p1, p2@ and a compatible cone @k1, k2@ on some @q@ (with
-- @f . k1 == g . k2@ for whichever cospan @p1, p2@ are a pullback of), produces the unique
-- @q ~> p@ through which the cone factors. Standalone helper (not a class method), usable as the
-- @default@ implementation of 'Proarrow.Limit.Pullback.factorPullback' wherever
-- @(HasEqualizers k, HasProducts k)@ happen to hold, like 'pullbackDefault' itself.
factorPullbackDefault
  :: forall {k} (a :: k) b p q
   . (HasEqualizers k, HasProducts k)
  => p ~> a -> p ~> b -> q ~> a -> q ~> b -> q ~> p
factorPullbackDefault :: forall {k} (a :: k) (b :: k) (p :: k) (q :: k).
(HasEqualizers k, HasProducts k) =>
(p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p
factorPullbackDefault p1 :: p ~> a
p1@p ~> a
Objs p2 :: p ~> b
p2@p ~> b
Objs q ~> a
k1 q ~> b
k2 = (p ~> (a && b)) -> (q ~> (a && b)) -> q ~> p
forall (e :: k) (x :: k) (e' :: k).
(e ~> x) -> (e' ~> x) -> e' ~> e
forall k (e :: k) (x :: k) (e' :: k).
HasEqualizers k =>
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer (p ~> a
p1 (p ~> a) -> (p ~> b) -> p ~> (a && b)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& p ~> b
p2) (q ~> a
k1 (q ~> a) -> (q ~> b) -> q ~> (a && b)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& q ~> b
k2)

kernel :: (HasEqualizers k, HasZeroObject k) => (a :: k) ~> b -> (forall e. e ~> a -> r) -> r
kernel :: forall k (a :: k) (b :: k) r.
(HasEqualizers k, HasZeroObject k) =>
(a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
kernel f :: a ~> b
f@a ~> b
Objs = (a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
forall (a :: k) (b :: k) r.
(a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
forall k (a :: k) (b :: k) r.
HasEqualizers k =>
(a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
equalize 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 ~> b
f