{-# LANGUAGE MultiParamTypeClasses #-}

{-| Module  : FiniteCategories
Description : A discrete category is a category with no morphism other than identities.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A discrete category is a category with no morphism other than identities.
-}

module UsualCategories.DiscreteCategory 
(
    DiscreteObject(..),
    DiscreteIdentity(..),
    DiscreteCategory(..)
)
where
    import          FiniteCategory.FiniteCategory
    import          IO.PrettyPrint
    
    -- | A discrete object is just an usual object.

    data DiscreteObject a = DiscreteObject a deriving (DiscreteObject a -> DiscreteObject a -> Bool
(DiscreteObject a -> DiscreteObject a -> Bool)
-> (DiscreteObject a -> DiscreteObject a -> Bool)
-> Eq (DiscreteObject a)
forall a. Eq a => DiscreteObject a -> DiscreteObject a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DiscreteObject a -> DiscreteObject a -> Bool
$c/= :: forall a. Eq a => DiscreteObject a -> DiscreteObject a -> Bool
== :: DiscreteObject a -> DiscreteObject a -> Bool
$c== :: forall a. Eq a => DiscreteObject a -> DiscreteObject a -> Bool
Eq, Int -> DiscreteObject a -> ShowS
[DiscreteObject a] -> ShowS
DiscreteObject a -> String
(Int -> DiscreteObject a -> ShowS)
-> (DiscreteObject a -> String)
-> ([DiscreteObject a] -> ShowS)
-> Show (DiscreteObject a)
forall a. Show a => Int -> DiscreteObject a -> ShowS
forall a. Show a => [DiscreteObject a] -> ShowS
forall a. Show a => DiscreteObject a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DiscreteObject a] -> ShowS
$cshowList :: forall a. Show a => [DiscreteObject a] -> ShowS
show :: DiscreteObject a -> String
$cshow :: forall a. Show a => DiscreteObject a -> String
showsPrec :: Int -> DiscreteObject a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> DiscreteObject a -> ShowS
Show)
    
    instance (PrettyPrintable a) => PrettyPrintable (DiscreteObject a) where
        pprint :: DiscreteObject a -> String
pprint (DiscreteObject a
x) = a -> String
forall a. PrettyPrintable a => a -> String
pprint a
x
    
    -- | `DiscreteIdentity` is the morphism of the discrete category.

    data DiscreteIdentity a = DiscreteIdentity a deriving (DiscreteIdentity a -> DiscreteIdentity a -> Bool
(DiscreteIdentity a -> DiscreteIdentity a -> Bool)
-> (DiscreteIdentity a -> DiscreteIdentity a -> Bool)
-> Eq (DiscreteIdentity a)
forall a. Eq a => DiscreteIdentity a -> DiscreteIdentity a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DiscreteIdentity a -> DiscreteIdentity a -> Bool
$c/= :: forall a. Eq a => DiscreteIdentity a -> DiscreteIdentity a -> Bool
== :: DiscreteIdentity a -> DiscreteIdentity a -> Bool
$c== :: forall a. Eq a => DiscreteIdentity a -> DiscreteIdentity a -> Bool
Eq, Int -> DiscreteIdentity a -> ShowS
[DiscreteIdentity a] -> ShowS
DiscreteIdentity a -> String
(Int -> DiscreteIdentity a -> ShowS)
-> (DiscreteIdentity a -> String)
-> ([DiscreteIdentity a] -> ShowS)
-> Show (DiscreteIdentity a)
forall a. Show a => Int -> DiscreteIdentity a -> ShowS
forall a. Show a => [DiscreteIdentity a] -> ShowS
forall a. Show a => DiscreteIdentity a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DiscreteIdentity a] -> ShowS
$cshowList :: forall a. Show a => [DiscreteIdentity a] -> ShowS
show :: DiscreteIdentity a -> String
$cshow :: forall a. Show a => DiscreteIdentity a -> String
showsPrec :: Int -> DiscreteIdentity a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> DiscreteIdentity a -> ShowS
Show)
    
    instance (Eq a) => Morphism (DiscreteIdentity a) (DiscreteObject a) where
        source :: DiscreteIdentity a -> DiscreteObject a
source (DiscreteIdentity a
x) = a -> DiscreteObject a
forall a. a -> DiscreteObject a
DiscreteObject a
x
        target :: DiscreteIdentity a -> DiscreteObject a
target (DiscreteIdentity a
x) = a -> DiscreteObject a
forall a. a -> DiscreteObject a
DiscreteObject a
x
        @ :: DiscreteIdentity a -> DiscreteIdentity a -> DiscreteIdentity a
(@) = (\DiscreteIdentity a
x DiscreteIdentity a
y -> if DiscreteIdentity a
x DiscreteIdentity a -> DiscreteIdentity a -> Bool
forall a. Eq a => a -> a -> Bool
/= DiscreteIdentity a
y then String -> DiscreteIdentity a
forall a. HasCallStack => String -> a
error String
"Composition of incompatible discrete morphisms" else DiscreteIdentity a
x)
    
    instance (PrettyPrintable a) => PrettyPrintable (DiscreteIdentity a) where
        pprint :: DiscreteIdentity a -> String
pprint (DiscreteIdentity a
x) = String
"Id"String -> ShowS
forall a. [a] -> [a] -> [a]
++a -> String
forall a. PrettyPrintable a => a -> String
pprint a
x
    
    -- | The discrete category is just a list of objects.

    data DiscreteCategory a = DiscreteCategory [a] deriving (DiscreteCategory a -> DiscreteCategory a -> Bool
(DiscreteCategory a -> DiscreteCategory a -> Bool)
-> (DiscreteCategory a -> DiscreteCategory a -> Bool)
-> Eq (DiscreteCategory a)
forall a. Eq a => DiscreteCategory a -> DiscreteCategory a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DiscreteCategory a -> DiscreteCategory a -> Bool
$c/= :: forall a. Eq a => DiscreteCategory a -> DiscreteCategory a -> Bool
== :: DiscreteCategory a -> DiscreteCategory a -> Bool
$c== :: forall a. Eq a => DiscreteCategory a -> DiscreteCategory a -> Bool
Eq, Int -> DiscreteCategory a -> ShowS
[DiscreteCategory a] -> ShowS
DiscreteCategory a -> String
(Int -> DiscreteCategory a -> ShowS)
-> (DiscreteCategory a -> String)
-> ([DiscreteCategory a] -> ShowS)
-> Show (DiscreteCategory a)
forall a. Show a => Int -> DiscreteCategory a -> ShowS
forall a. Show a => [DiscreteCategory a] -> ShowS
forall a. Show a => DiscreteCategory a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DiscreteCategory a] -> ShowS
$cshowList :: forall a. Show a => [DiscreteCategory a] -> ShowS
show :: DiscreteCategory a -> String
$cshow :: forall a. Show a => DiscreteCategory a -> String
showsPrec :: Int -> DiscreteCategory a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> DiscreteCategory a -> ShowS
Show)

    instance (Eq a) => FiniteCategory (DiscreteCategory a) (DiscreteIdentity a) (DiscreteObject a) where
        ob :: DiscreteCategory a -> [DiscreteObject a]
ob (DiscreteCategory [a]
objs) = a -> DiscreteObject a
forall a. a -> DiscreteObject a
DiscreteObject (a -> DiscreteObject a) -> [a] -> [DiscreteObject a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
objs
        identity :: Morphism (DiscreteIdentity a) (DiscreteObject a) =>
DiscreteCategory a -> DiscreteObject a -> DiscreteIdentity a
identity (DiscreteCategory [a]
objs) (DiscreteObject a
o) = if a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
o [a]
objs then a -> DiscreteIdentity a
forall a. a -> DiscreteIdentity a
DiscreteIdentity a
o else String -> DiscreteIdentity a
forall a. HasCallStack => String -> a
error String
"Identity of an object not in the discrete category."
        ar :: Morphism (DiscreteIdentity a) (DiscreteObject a) =>
DiscreteCategory a
-> DiscreteObject a -> DiscreteObject a -> [DiscreteIdentity a]
ar DiscreteCategory a
c DiscreteObject a
x DiscreteObject a
y = if DiscreteObject a
x DiscreteObject a -> DiscreteObject a -> Bool
forall a. Eq a => a -> a -> Bool
/= DiscreteObject a
y then [] else [DiscreteCategory a -> DiscreteObject a -> DiscreteIdentity a
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity DiscreteCategory a
c DiscreteObject a
x]
        
    instance (Eq a) => GeneratedFiniteCategory (DiscreteCategory a) (DiscreteIdentity a) (DiscreteObject a) where
        genAr :: Morphism (DiscreteIdentity a) (DiscreteObject a) =>
DiscreteCategory a
-> DiscreteObject a -> DiscreteObject a -> [DiscreteIdentity a]
genAr = DiscreteCategory a
-> DiscreteObject a -> DiscreteObject a -> [DiscreteIdentity a]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
defaultGenAr
        decompose :: Morphism (DiscreteIdentity a) (DiscreteObject a) =>
DiscreteCategory a -> DiscreteIdentity a -> [DiscreteIdentity a]
decompose = DiscreteCategory a -> DiscreteIdentity a -> [DiscreteIdentity a]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> m -> [m]
defaultDecompose
        
    instance (PrettyPrintable a) => PrettyPrintable (DiscreteCategory a) where
        pprint :: DiscreteCategory a -> String
pprint (DiscreteCategory [a]
xs) = String
"DiscreteCategory of " String -> ShowS
forall a. [a] -> [a] -> [a]
++[a] -> String
forall a. PrettyPrintable a => a -> String
pprint [a]
xs