-- | Working with objects through their identity arrows: 'Obj' @a@ is @a '~>' a@ used as a witness that
-- @a@ is an object, with 'obj', 'src' and 'tgt' to produce them and the 'Obj'\/'Objs' pattern synonyms
-- to recover 'Ob' constraints from arrows and profunctor values.
module Proarrow.Object
  ( Obj
  , pattern Obj
  , pattern Objs
  , obj
  , src
  , tgt
  , Ob'
  , VacuousOb
  , objDicts
  , ObjDict (..)
  ) where

import Data.Kind (Type)

import Proarrow.Core (CategoryOf (..), Ob', Obj, Profunctor, VacuousOb, obj, src, tgt, (\\))

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

objDicts :: (Profunctor p) => p a a' -> (ObjDict a, ObjDict a')
objDicts :: forall {k} {k} (p :: k +-> k) (a :: k) (a' :: k).
Profunctor p =>
p a a' -> (ObjDict a, ObjDict a')
objDicts p 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) -> p a a' -> ObjDict a
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p 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') -> p a a' -> ObjDict a'
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a a'
a)

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

{-# COMPLETE Obj #-}

-- | Matching a profunctor value @p a b@ against 'Objs' brings @('Ob' a, 'Ob' b)@ into scope --
-- the pattern form of '(\\)', handy in function equations.
pattern Objs :: (Profunctor p) => (Ob a, Ob b) => p a b
pattern $mObjs :: forall {r} {j} {k} {p :: j +-> k} {a :: k} {b :: j}.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> ((# #) -> r) -> r
Objs <- (objDicts -> (ObjDict, ObjDict))

{-# COMPLETE Objs #-}