module Proarrow.Object
  ( Obj
  , pattern Obj
  , pattern Objs
  , obj
  , src
  , tgt
  , Ob'
  , VacuusOb
  ) where

import Data.Kind (Type)

import Proarrow.Core (CategoryOf (..), Obj, obj, src, tgt, (\\))

class (Ob a, CategoryOf k) => Ob' (a :: k)
instance (Ob a, CategoryOf k) => Ob' (a :: k)
type VacuusOb k = forall a. Ob' (a :: k)

type ObjDict :: forall {k}. k -> Type
data ObjDict a where
  ObjDict :: (Ob a) => ObjDict a

objDict :: (CategoryOf k) => a ~> a' -> (ObjDict (a :: k), ObjDict a')
objDict :: forall k (a :: k) (a' :: k).
CategoryOf k =>
(a ~> a') -> (ObjDict a, ObjDict a')
objDict a ~> a'
a = (ObjDict a
(Ob a, Ob a') => ObjDict a
forall {k} (a :: k). Ob a => ObjDict a
ObjDict ((Ob a, Ob a') => ObjDict a) -> (a ~> a') -> ObjDict a
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> a'
a, ObjDict a'
(Ob a, Ob a') => ObjDict a'
forall {k} (a :: k). Ob a => ObjDict a
ObjDict ((Ob a, Ob a') => ObjDict a') -> (a ~> a') -> ObjDict a'
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> a'
a)

pattern Obj :: (CategoryOf k) => (Ob (a :: k)) => Obj a
pattern $mObj :: forall {r} {k} {a :: k}.
CategoryOf k =>
Obj a -> (Ob a => r) -> ((# #) -> r) -> r
$bObj :: forall k (a :: k). (CategoryOf k, Ob a) => Obj a
Obj <- (objDict -> (ObjDict, ObjDict))
  where
    Obj = Obj a
forall k (a :: k). (CategoryOf k, Ob a) => Obj a
obj

pattern Objs :: (CategoryOf k) => (Ob (a :: k), Ob (b :: k)) => a ~> b
pattern $mObjs :: forall {r} {k} {a :: k} {b :: k}.
CategoryOf k =>
(a ~> b) -> ((Ob a, Ob b) => r) -> ((# #) -> r) -> r
Objs <- (objDict -> (ObjDict, ObjDict))