{-# 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 (Eq, Show)
    
    instance (PrettyPrintable a) => PrettyPrintable (DiscreteObject a) where
        pprint (DiscreteObject x) = pprint x
    
    -- | `DiscreteIdentity` is the morphism of the discrete category.
    data DiscreteIdentity a = DiscreteIdentity a deriving (Eq, Show)
    
    instance (Eq a) => Morphism (DiscreteIdentity a) (DiscreteObject a) where
        source (DiscreteIdentity x) = DiscreteObject x
        target (DiscreteIdentity x) = DiscreteObject x
        (@) = (\x y -> if x /= y then error "Composition of incompatible discrete morphisms" else x)
    
    instance (PrettyPrintable a) => PrettyPrintable (DiscreteIdentity a) where
        pprint (DiscreteIdentity x) = "Id"++pprint x
    
    -- | The discrete category is just a list of objects.
    data DiscreteCategory a = DiscreteCategory [a] deriving (Eq, Show)

    instance (Eq a) => FiniteCategory (DiscreteCategory a) (DiscreteIdentity a) (DiscreteObject a) where
        ob (DiscreteCategory objs) = DiscreteObject <$> objs
        identity (DiscreteCategory objs) (DiscreteObject o) = if elem o objs then DiscreteIdentity o else error "Identity of an object not in the discrete category."
        ar c x y = if x /= y then [] else [identity c x]
        
    instance (Eq a) => GeneratedFiniteCategory (DiscreteCategory a) (DiscreteIdentity a) (DiscreteObject a) where
        genAr = defaultGenAr
        decompose = defaultDecompose
        
    instance (PrettyPrintable a) => PrettyPrintable (DiscreteCategory a) where
        pprint (DiscreteCategory xs) = "DiscreteCategory of " ++pprint xs