{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.InternalCategory(
  -- * Internal categories
  ICategory(..),
  -- * Path
  Path(Path, EmptyPath, NonEmptyPath),
  dom, cod, (>?>),

  -- * Reexport
  IQuiver(..),
) where

import Data.InternalQuiver
import Data.Void
import Data.Bifunctor (Bifunctor(..))

import Data.InternalQuiver.Path

-- * Internal Category

{- | @ICategory ob mor@ defines a category "internal to" @Type@.

There are two ways to define @ICategory@: with 'identity' and 'compose' or with 'foldPath'.

==== Definition by @'identity', 'compose'@

This is how internal categories are usually defined: by giving identity morphisms
and composition of two morphisms, satisfying the following laws:

/Domain and codomain of @identity v@/:

    @
    dom (identity v) == cod (identity v) == v
    @

/@compose@ is defined exactly on matching morphisms/:

    @
    isJust (compose f g) == (cod f == dom g)
    @

/Domain and codomain of @compose f g@/:


    For all @f,g,h@ such that @compose f g == Just h@,
    
    @
    dom h == dom f, cod h == cod g
    @

/Left and Right Unit/:

    @
    identity (dom f) `compose` f == Just f
    @

    @
    f `compose` identity (cod f) == Just f
    @

/Associativity/:

    For all @f,g,h@,

    @
    (compose f g >>= \fg -> compose fg h)
      ==
    (compose g h >>= \gh -> compose f gh)
    @

Given @identity@ and @compose@ operation, @foldPath p@
can be defined as the composition @morAll@ of all morphisms in @p@
(and the identity at source in a case of empty path,) which
is guaranteed to be @Just morAll@ and not @Nothing@.

==== Definition by @'foldPath'@:

This is an alternative definition by giving how to collapse any path on
@IQuiver ob mor@ into @mor@, satisfying the following laws.

/folding doesn't change endpoints/:

    @
    dom (foldPath p) == dom p
    @

    @
    cod (foldPath p) == cod p
    @

/folding commutes with 'concatPath'/:

    For any @pp :: Path ob (Path ob mor)@,

    @
    foldPath (concatPath pp) = foldPath (errMapPath id foldPath pp)
    @

    Note that from /folding doesn't change endpoints/ law,
    @errMapPath id foldPath@ must be a total function.

/folding single edge does nothing/:

    @
    foldPath (singlePath f) = f
    @

Given @foldPath@, one can defined @identity@ and @compose@ satisfying
the laws above, as

@
identity :: ob -> mor
identity = foldPath . emptyPath

compose :: mor -> mor -> Maybe mor
compose f g = foldPath <$> composePath (singlePath f) (singlePath g)
@

-}
class (IQuiver ob mor, Eq ob) => ICategory ob mor | mor -> ob where
  {-# MINIMAL foldPath | identity, compose #-}

  foldPath :: Path ob mor -> mor
  foldPath Path ob mor
p = case Path ob mor
p of
    EmptyPath ob
v0 -> ob -> mor
forall ob mor. ICategory ob mor => ob -> mor
identity ob
v0
    NonEmptyPath mor
e [mor]
es -> mor -> [mor] -> mor
forall {ob} {t}. ICategory ob t => t -> [t] -> t
loop mor
e [mor]
es
    where
      loop :: t -> [t] -> t
loop t
e [] = t
e
      loop t
e (t
e':[t]
rest) = case t -> t -> Maybe t
forall ob mor. ICategory ob mor => mor -> mor -> Maybe mor
compose t
e t
e' of
        Maybe t
Nothing -> [Char] -> t
forall a. HasCallStack => [Char] -> a
error [Char]
"Invalid Path"
        Just t
e'' -> t -> [t] -> t
loop t
e'' [t]
rest

  identity :: ob -> mor
  identity = Path ob mor -> mor
forall ob mor. ICategory ob mor => Path ob mor -> mor
foldPath (Path ob mor -> mor) -> (ob -> Path ob mor) -> ob -> mor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ob -> Path ob mor
forall v e. v -> Path v e
emptyPath

  compose :: mor -> mor -> Maybe mor
  compose mor
f mor
g = Path ob mor -> mor
forall ob mor. ICategory ob mor => Path ob mor -> mor
foldPath (Path ob mor -> mor) -> Maybe (Path ob mor) -> Maybe mor
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Path ob mor -> Path ob mor -> Maybe (Path ob mor)
forall v e. Eq v => Path v e -> Path v e -> Maybe (Path v e)
composePath (mor -> Path ob mor
forall v e. IQuiver v e => e -> Path v e
singlePath mor
f) (mor -> Path ob mor
forall v e. IQuiver v e => e -> Path v e
singlePath mor
g)

dom, cod :: ICategory ob mor => mor -> ob
dom :: forall ob mor. ICategory ob mor => mor -> ob
dom = mor -> ob
forall v e. IQuiver v e => e -> v
src
cod :: forall ob mor. ICategory ob mor => mor -> ob
cod = mor -> ob
forall v e. IQuiver v e => e -> v
tgt

infixr 1 >?>
(>?>) :: ICategory ob mor => mor -> mor -> Maybe mor
>?> :: forall ob mor. ICategory ob mor => mor -> mor -> Maybe mor
(>?>) = mor -> mor -> Maybe mor
forall ob mor. ICategory ob mor => mor -> mor -> Maybe mor
compose

---- Instances

-- | @Path@ is the free category
instance Eq ob => ICategory ob (Path ob mor) where
  foldPath :: Path ob (Path ob mor) -> Path ob mor
foldPath = Path ob (Path ob mor) -> Path ob mor
forall v e. Path v (Path v e) -> Path v e
concatPath
  identity :: ob -> Path ob mor
identity = ob -> Path ob mor
forall v e. v -> Path v e
emptyPath
  compose :: Path ob mor -> Path ob mor -> Maybe (Path ob mor)
compose = Path ob mor -> Path ob mor -> Maybe (Path ob mor)
forall v e. Eq v => Path v e -> Path v e -> Maybe (Path v e)
composePath

-- | Empty graph
instance ICategory Void Void where
  foldPath :: Path Void Void -> Void
foldPath (Path Void
v [Void]
_ Void
_) = Void -> Void
forall a. Void -> a
absurd Void
v
  identity :: Void -> Void
identity = Void -> Void
forall a. Void -> a
absurd
  compose :: Void -> Void -> Maybe Void
compose = Void -> Void -> Maybe Void
forall a. Void -> a
absurd

-- | A graph with one vertex and one loop on it
instance ICategory () () where
  foldPath :: Path () () -> ()
foldPath Path () ()
_ = ()
  identity :: () -> ()
identity ()
_ = ()
  compose :: () -> () -> Maybe ()
compose ()
_ ()
_ = () -> Maybe ()
forall a. a -> Maybe a
Just ()

-- | Coproduct of category
instance (ICategory v e, ICategory w f) => ICategory (Either v w) (Either e f) where
  foldPath :: Path (Either v w) (Either e f) -> Either e f
foldPath Path (Either v w) (Either e f)
p = case Path (Either v w) (Either e f) -> Either (Path v e) (Path w f)
forall v w e f.
Path (Either v w) (Either e f) -> Either (Path v e) (Path w f)
separateSumPath Path (Either v w) (Either e f)
p of
    Left Path v e
leftP   -> e -> Either e f
forall a b. a -> Either a b
Left (Path v e -> e
forall ob mor. ICategory ob mor => Path ob mor -> mor
foldPath Path v e
leftP)
    Right Path w f
rightP -> f -> Either e f
forall a b. b -> Either a b
Right (Path w f -> f
forall ob mor. ICategory ob mor => Path ob mor -> mor
foldPath Path w f
rightP)
  
  identity :: Either v w -> Either e f
identity = (v -> e) -> (w -> f) -> Either v w -> Either e f
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap v -> e
forall ob mor. ICategory ob mor => ob -> mor
identity w -> f
forall ob mor. ICategory ob mor => ob -> mor
identity
  compose :: Either e f -> Either e f -> Maybe (Either e f)
compose (Left e
f) (Left e
g) = e -> Either e f
forall a b. a -> Either a b
Left (e -> Either e f) -> Maybe e -> Maybe (Either e f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> e -> e -> Maybe e
forall ob mor. ICategory ob mor => mor -> mor -> Maybe mor
compose e
f e
g
  compose (Right f
f) (Right f
g) = f -> Either e f
forall a b. b -> Either a b
Right (f -> Either e f) -> Maybe f -> Maybe (Either e f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f -> f -> Maybe f
forall ob mor. ICategory ob mor => mor -> mor -> Maybe mor
compose f
f f
g
  compose Either e f
_ Either e f
_ = Maybe (Either e f)
forall a. Maybe a
Nothing

-- | Product of category
instance (ICategory v e, ICategory w f) => ICategory (v,w) (e,f) where
  foldPath :: Path (v, w) (e, f) -> (e, f)
foldPath Path (v, w) (e, f)
p = (Path v e -> e
forall ob mor. ICategory ob mor => Path ob mor -> mor
foldPath (Path (v, w) (e, f) -> Path v e
forall v w e f. Path (v, w) (e, f) -> Path v e
fstPath Path (v, w) (e, f)
p), Path w f -> f
forall ob mor. ICategory ob mor => Path ob mor -> mor
foldPath (Path (v, w) (e, f) -> Path w f
forall v w e f. Path (v, w) (e, f) -> Path w f
sndPath Path (v, w) (e, f)
p))
  identity :: (v, w) -> (e, f)
identity (v
v,w
w) = (v -> e
forall ob mor. ICategory ob mor => ob -> mor
identity v
v, w -> f
forall ob mor. ICategory ob mor => ob -> mor
identity w
w)
  compose :: (e, f) -> (e, f) -> Maybe (e, f)
compose (e
f,f
f') (e
g,f
g') = (,) (e -> f -> (e, f)) -> Maybe e -> Maybe (f -> (e, f))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> e -> e -> Maybe e
forall ob mor. ICategory ob mor => mor -> mor -> Maybe mor
compose e
f e
g Maybe (f -> (e, f)) -> Maybe f -> Maybe (e, f)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f -> f -> Maybe f
forall ob mor. ICategory ob mor => mor -> mor -> Maybe mor
compose f
f' f
g'