{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Preorder.ThinCategory where

import Data.Kind (Constraint)
import Prelude (type (~))

import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, obj, type (+->))
import Proarrow.Preorder
  ( CProfunctor (..)
  , CPromonad (..)
  , Dict (..)
  , POS
  , PreorderOf (..)
  , cdimapDefault
  , type (:-) (..)
  )

type ThinProfunctor :: forall {j} {k}. j +-> k -> Constraint
class (Profunctor p, Thin j, Thin k) => ThinProfunctor (p :: j +-> k) where
  type HasArrow (p :: j +-> k) (a :: k) (b :: j) :: Constraint
  type HasArrow p a b = ()
  arr :: (Ob a, Ob b, HasArrow p a b) => p a b
  withArr :: p a b -> ((HasArrow p a b) => r) -> r

class (ThinProfunctor ((~>) :: CAT k)) => Thin k
instance (ThinProfunctor ((~>) :: CAT k)) => Thin k

class (HasArrow p a b) => HasArrow' p a b
instance (HasArrow p a b) => HasArrow' p a b

type CodiscreteProfunctor :: forall {j} {k}. j +-> k -> Constraint
class
  (ThinProfunctor p, forall c d. (Ob c, Ob d) => HasArrow' p c d, Codiscrete j, Codiscrete k) =>
  CodiscreteProfunctor (p :: j +-> k)
  where
  anyArr :: (Ob a, Ob b) => p a b
instance
  (ThinProfunctor p, forall c d. (Ob c, Ob d) => HasArrow' p c d, Codiscrete j, Codiscrete k)
  => CodiscreteProfunctor (p :: j +-> k)
  where
  anyArr :: forall (a :: k) (b :: j). (Ob a, Ob b) => p a b
anyArr = 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

class (CodiscreteProfunctor ((~>) :: CAT k)) => Codiscrete k
instance (CodiscreteProfunctor ((~>) :: CAT k)) => Codiscrete k

class ((HasArrow p c d) ~ (c ~ d)) => ArrowIsId p c d where
  arrowIsIdProof :: HasArrow p c d => (c ~ d => r) -> r
instance ((HasArrow p c d) ~ (c ~ d)) => ArrowIsId p c d where
  arrowIsIdProof :: forall r. HasArrow p c d => ((c ~ d) => r) -> r
arrowIsIdProof (c ~ d) => r
r = r
(c ~ d) => r
r

type DiscreteProfunctor :: forall {k}. k +-> k -> Constraint
class (ThinProfunctor p, forall c d. ArrowIsId p c d, Discrete k) => DiscreteProfunctor (p :: k +-> k) where
  withEq :: p a b -> ((a ~ b) => r) -> r
instance (ThinProfunctor p, forall c d. ArrowIsId p c d, Discrete k) => DiscreteProfunctor (p :: k +-> k) where
  withEq :: forall (a :: k) (b :: k) r. p a b -> ((a ~ b) => r) -> r
withEq @a @b p a b
p (a ~ b) => r
r = p a b -> (HasArrow p a b => r) -> r
forall (a :: k) (b :: k) 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 (forall {k} (p :: k +-> k) (c :: k) (d :: k) r.
(ArrowIsId p c d, HasArrow p c d) =>
((c ~ d) => r) -> r
forall (p :: k +-> k) (c :: k) (d :: k) r.
(ArrowIsId p c d, HasArrow p c d) =>
((c ~ d) => r) -> r
arrowIsIdProof @p @a @b r
(a ~ b) => r
r)

class (DiscreteProfunctor ((~>) :: CAT k)) => Discrete k
instance (DiscreteProfunctor ((~>) :: CAT k)) => Discrete k

newtype THIN k = T k
type instance UN T (T a) = a

class (Thin k, HasArrow (~>) (UN T a) (UN T b), COb a, COb b) => ThinCategory (a :: THIN k) b
instance (Thin k, HasArrow (~>) (UN T a) (UN T b), COb a, COb b) => ThinCategory (a :: THIN k) b

instance (Thin k) => CProfunctor (ThinCategory :: POS (THIN k)) where
  cdimap :: forall (c :: THIN k) (a :: THIN k) (b :: THIN k) (d :: THIN k).
(c <= a, b <= d, ThinCategory a b) :- ThinCategory c d
cdimap = (c <= a, b <= d, ThinCategory a b) :- ThinCategory c d
(ThinCategory c a, ThinCategory b d, ThinCategory a b)
:- ThinCategory c d
forall {k} (p :: k -> k -> Constraint) (a :: k) (b :: k) (c :: k)
       (d :: k).
CPromonad p =>
(p c a, p b d, p a b) :- p c d
cdimapDefault
  obs :: forall (a :: THIN k) (b :: THIN k).
ThinCategory a b :- (COb a, COb b)
obs = (ThinCategory a b =>
 Dict
   ((a ~ 'T (UN 'T a), Ob (UN 'T a)),
    (b ~ 'T (UN 'T b), Ob (UN 'T b))))
-> ThinCategory a b
   :- ((a ~ 'T (UN 'T a), Ob (UN 'T a)),
       (b ~ 'T (UN 'T b), Ob (UN 'T b)))
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict
  ((a ~ 'T (UN 'T a), Ob (UN 'T a)),
   (b ~ 'T (UN 'T b), Ob (UN 'T b)))
ThinCategory a b =>
Dict
  ((a ~ 'T (UN 'T a), Ob (UN 'T a)),
   (b ~ 'T (UN 'T b), Ob (UN 'T b)))
forall (a :: Constraint). a => Dict a
Dict
instance (Thin k) => CPromonad (ThinCategory :: POS (THIN k)) where
  cid :: forall (a :: THIN k).
COb a =>
(() :: Constraint) :- ThinCategory a a
cid @(T a) = ((() :: Constraint) => Dict (ThinCategory a a))
-> (() :: Constraint) :- ThinCategory a a
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((UN 'T a ~> UN 'T a)
-> (HasArrow (~>) (UN 'T a) (UN 'T a) => Dict (ThinCategory a a))
-> Dict (ThinCategory a a)
forall (a :: k) (b :: k) r.
(a ~> b) -> (HasArrow (~>) 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 (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) Dict (ThinCategory a a)
HasArrow (~>) (UN 'T a) (UN 'T a) => Dict (ThinCategory a a)
forall (a :: Constraint). a => Dict a
Dict)
  ccomp :: forall (a :: THIN k) (b :: THIN k) (c :: THIN k).
(ThinCategory b c, ThinCategory a b) :- ThinCategory a c
ccomp @a @b @c = ((ThinCategory b c, ThinCategory a b) => Dict (ThinCategory a c))
-> (ThinCategory b c, ThinCategory a b) :- ThinCategory a c
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((UN 'T a ~> UN 'T c)
-> (HasArrow (~>) (UN 'T a) (UN 'T c) => Dict (ThinCategory a c))
-> Dict (ThinCategory a c)
forall (a :: k) (b :: k) r.
(a ~> b) -> (HasArrow (~>) 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 (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
forall (p :: k +-> k) (a :: k) (b :: k).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr @(~>) @(UN T b) @(UN T c) (UN 'T b ~> UN 'T c) -> (UN 'T a ~> UN 'T b) -> UN 'T a ~> UN 'T c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
forall (p :: k +-> k) (a :: k) (b :: k).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr @(~>) @(UN T a) @(UN T b)) Dict (ThinCategory a c)
HasArrow (~>) (UN 'T a) (UN 'T c) => Dict (ThinCategory a c)
forall (a :: Constraint). a => Dict a
Dict)

-- | A thin category as a preorder.
instance (Thin k) => PreorderOf (THIN k) where
  type (<=) = ThinCategory
  type COb a = (Is T a, Ob (UN T a))