{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
module Data.InternalCategory.Morphism(
  Mor(..), identityMorphism, composeMorphism
) where

import Prelude hiding ((.), id)
import qualified Data.List
import Data.Maybe (fromMaybe)
import Control.Category

import Data.Singletons
import Data.Singletons.Decide
import Data.InternalCategory
    ( IQuiver(..), ICategory(..), Path(Path) )
import Data.Kind (Type)

-- | Sum of all morphisms in @cat@.
data Mor k (cat :: k -> k -> Type) where
  Morphism :: Sing a -> Sing b -> cat a b -> Mor k cat

instance IQuiver (SomeSing k) (Mor k cat) where
  src :: Mor k cat -> SomeSing k
src (Morphism Sing a
sa Sing b
_ cat a b
_) = Sing a -> SomeSing k
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing a
sa
  tgt :: Mor k cat -> SomeSing k
tgt (Morphism Sing a
_ Sing b
sb cat a b
_) = Sing b -> SomeSing k
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing b
sb

identityMorphism :: (Category cat) => SomeSing k -> Mor k cat
identityMorphism :: forall k (cat :: k -> k -> *).
Category cat =>
SomeSing k -> Mor k cat
identityMorphism (SomeSing Sing a
sa) = Sing a -> Sing a -> cat a a -> Mor k cat
forall k (a :: k) (b :: k) (cat :: k -> k -> *).
Sing a -> Sing b -> cat a b -> Mor k cat
Morphism Sing a
sa Sing a
sa cat a a
forall (a :: k). cat a a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

composeMorphism :: (Category cat, SDecide k) => Mor k cat -> Mor k cat -> Maybe (Mor k cat)
composeMorphism :: forall k (cat :: k -> k -> *).
(Category cat, SDecide k) =>
Mor k cat -> Mor k cat -> Maybe (Mor k cat)
composeMorphism (Morphism Sing a
sa Sing b
sb cat a b
f) (Morphism Sing a
sb' Sing b
sc cat a b
g) = case Sing b
sb Sing b -> Sing a -> Decision (b :~: a)
forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing a
sb' of
  Proved b :~: a
Refl -> Mor k cat -> Maybe (Mor k cat)
forall a. a -> Maybe a
Just (Mor k cat -> Maybe (Mor k cat)) -> Mor k cat -> Maybe (Mor k cat)
forall a b. (a -> b) -> a -> b
$ Sing a -> Sing b -> cat a b -> Mor k cat
forall k (a :: k) (b :: k) (cat :: k -> k -> *).
Sing a -> Sing b -> cat a b -> Mor k cat
Morphism Sing a
sa Sing b
sc (cat a b
g cat a b -> cat a a -> cat a b
forall (b :: k) (c :: k) (a :: k). cat b c -> cat a b -> cat a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. cat a b
cat a a
f)
  Disproved Refuted (b :~: a)
_ -> Maybe (Mor k cat)
forall a. Maybe a
Nothing

composeMorphism' :: (Category cat, SDecide k) => Mor k cat -> Mor k cat -> Mor k cat
composeMorphism' :: forall k (cat :: k -> k -> *).
(Category cat, SDecide k) =>
Mor k cat -> Mor k cat -> Mor k cat
composeMorphism' Mor k cat
f Mor k cat
g = Mor k cat -> Maybe (Mor k cat) -> Mor k cat
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> Mor k cat
forall a. HasCallStack => [Char] -> a
error [Char]
"Invalid Path") (Maybe (Mor k cat) -> Mor k cat) -> Maybe (Mor k cat) -> Mor k cat
forall a b. (a -> b) -> a -> b
$ Mor k cat -> Mor k cat -> Maybe (Mor k cat)
forall k (cat :: k -> k -> *).
(Category cat, SDecide k) =>
Mor k cat -> Mor k cat -> Maybe (Mor k cat)
composeMorphism Mor k cat
f Mor k cat
g

instance (Category cat, SDecide k) => ICategory (SomeSing k) (Mor k cat) where
  foldPath :: Path (SomeSing k) (Mor k cat) -> Mor k cat
foldPath (Path SomeSing k
s0 [Mor k cat]
mors SomeSing k
_) = (Mor k cat -> Mor k cat -> Mor k cat)
-> Mor k cat -> [Mor k cat] -> Mor k cat
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Data.List.foldl' Mor k cat -> Mor k cat -> Mor k cat
forall k (cat :: k -> k -> *).
(Category cat, SDecide k) =>
Mor k cat -> Mor k cat -> Mor k cat
composeMorphism' (SomeSing k -> Mor k cat
forall k (cat :: k -> k -> *).
Category cat =>
SomeSing k -> Mor k cat
identityMorphism SomeSing k
s0) [Mor k cat]
mors