TotalOrder.hs

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

{-| Module  : FiniteCategories
Description : Any total (or linear) order induces a preorder category where elements are objects, there is an arrow between two objects iff the relation is satisfied.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Any total (or linear) order induces a preorder category where elements are objects, there is an arrow between two objects iff the relation is satisfied.

(See Categories for the working mathematican. Saunders Mac Lane. p.11)
-}

module Math.Categories.TotalOrder
(
    IsSmallerThan(..),
    TotalOrder(..),
    
)
where
    import              Math.Category
    import              Math.Categories.FunctorCategory
    import              Math.Categories.ConeCategory
    import              Math.IO.PrettyPrint
    
    import              Data.WeakSet.Safe
    import qualified    Data.WeakMap          as Map
    import              Data.WeakMap.Safe
    
    -- | 'IsSmallerThan' is the type of morphisms in a linear order, it reminds the fact that there is a morphism from a source to a target iff the source is smaller than the target.
    data IsSmallerThan a = IsSmallerThan a a deriving (Eq, Show)
    
    instance (Eq a) => Morphism (IsSmallerThan a) a where
        (IsSmallerThan m1 t) @? (IsSmallerThan s m2)
            | m1 == m2 = Just $ IsSmallerThan s t
            | otherwise = Nothing
        source (IsSmallerThan s _) = s
        target (IsSmallerThan _ t) = t
    
    -- | A 'TotalOrder' category is the category induced by a total order.
    --
    -- (See Categories for the working mathematican. Saunders Mac Lane. p.11)
    data TotalOrder a = TotalOrder deriving (Eq,Show)
    
    instance (Eq a, Ord a) => Category (TotalOrder a) (IsSmallerThan a) a where
        identity _ x = IsSmallerThan x x
        ar _ x y
            | x <= y = set [IsSmallerThan x y]
            | otherwise = set []
    
    instance (PrettyPrint a) => PrettyPrint (IsSmallerThan a) where
        pprint (IsSmallerThan x y) = pprint x ++ " <= " ++ pprint y
    
    instance PrettyPrint (TotalOrder a) where
        pprint = show