{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

{-| Module  : FiniteCategories
Description : The __'Galaxy'__ category has every objects and no morphism other than identities.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The __'Galaxy'__ category has every objects and no morphism other than identities.

It is called __'Galaxy'__ because its underlying graph is composed of a lot of points with no arrow between them.

It is the biggest 'DiscreteCategory'.
-}

module Math.Categories.Galaxy
(
    StarIdentity(..),
    Galaxy(..),   
)
where
    import          Math.Category
    import          Math.IO.PrettyPrint
    
    import          Data.WeakSet.Safe
    
    -- | 'StarIdentity' is the identity of a star (an object) in a 'Galaxy'.
    data StarIdentity a = StarIdentity a deriving (Eq, Show)
    
    instance (Eq a) => Morphism (StarIdentity a) a where
        (StarIdentity x) @? (StarIdentity y)
            | x == y = Just (StarIdentity x)
            | otherwise = Nothing
        source (StarIdentity x) = x
        target = source
    
    -- | The __'Galaxy'__ category has every objects and no morphism other than identities.
    data Galaxy a = Galaxy deriving (Eq,Show)
    
    instance (Eq a) => Category (Galaxy a) (StarIdentity a) a where
        identity _ = StarIdentity
        ar _ x y
            | x == y = set [StarIdentity x]
            | otherwise = set []
    
    instance (PrettyPrint a) => PrettyPrint (StarIdentity a) where
        pprint (StarIdentity x) = "Id"++ pprint x
    
    instance PrettyPrint (Galaxy a) where
        pprint = show