TotalOrder.hs

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MonadComprehensions #-}
{-# LANGUAGE MultiParamTypeClasses #-}

{-| 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.FiniteCategory
    import              Math.Category
    import              Math.Categories.FunctorCategory
    import              Math.Categories.ConeCategory
    import              Math.CompleteCategory
    import              Math.CocompleteCategory
    import              Math.FiniteCategories.Parallel
    import              Math.IO.PrettyPrint
    
    import qualified    Data.WeakSet          as Set
    import              Data.WeakSet.Safe
    import qualified    Data.WeakMap          as Map
    import              Data.WeakMap.Safe
    import              Data.Simplifiable
    
    import              GHC.Generics
    
    -- | '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, Generic, Simplifiable)
    
    instance (Eq a) => Morphism (IsSmallerThan a) a where
        (IsSmallerThan m1 t) @ (IsSmallerThan s m2) = IsSmallerThan s t
        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, Generic, PrettyPrint, Simplifiable)
    
    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 0 (IsSmallerThan x y) = pprint 0 x ++ " <= " ++ pprint 0 y
        pprint v (IsSmallerThan x y) = pprint (v-1) x ++ " <= " ++ pprint (v-1) y
        
        -- pprintWithIndentations 0 ov indent (IsSmallerThan x y) = indentation ov indent ++ pprint 0 x++" <= "++pprint 0 y ++ "\n"
        -- pprintWithIndentations cv ov indent (IsSmallerThan x y) = indentation (ov - cv) indent ++ pprint (cv-1) x++" <= "++pprint (cv-1) y ++ "\n"
        
    instance (Ord a, Eq oIndex) => HasProducts (TotalOrder a) (IsSmallerThan a) a (TotalOrder a) (IsSmallerThan a) a oIndex where
        product diag = unsafeCone apexProduct nat
            where
                apexProduct = Set.minimum $ Map.values $ omap diag
                nat = unsafeNaturalTransformation (constantDiagram (src diag) TotalOrder apexProduct) diag $ Map.weakMapFromSet [(i,IsSmallerThan apexProduct (diag ->$ i)) | i <- ob $ src diag]
                
    instance (Ord a) => HasEqualizers (TotalOrder a) (IsSmallerThan a) a where
        equalize parallelDiag = unsafeCone apexEq nat
            where
                apexEq = parallelDiag ->$ ParallelA
                nat = unsafeNaturalTransformation (constantDiagram Parallel TotalOrder apexEq) parallelDiag (weakMap [(ParallelA, IsSmallerThan apexEq apexEq),(ParallelB, IsSmallerThan (parallelDiag ->$ ParallelB) (parallelDiag ->$ ParallelB))])
                
    instance (Ord a, Eq mIndex, Eq oIndex) => CompleteCategory (TotalOrder a) (IsSmallerThan a) a (TotalOrder a) (IsSmallerThan a) a cIndex mIndex oIndex where
        limit diag = unsafeCone apexProduct nat
            where
                apexProduct = Set.minimum $ Map.values $ omap diag
                nat = unsafeNaturalTransformation (constantDiagram (src diag) TotalOrder apexProduct) diag $ Map.weakMapFromSet [(i,IsSmallerThan apexProduct (diag ->$ i)) | i <- ob $ src diag]
                
        projectBase diag = Diagram{src = tgt diag, tgt = tgt diag, omap = memorizeFunction id (Map.values (omap diag)), mmap = memorizeFunction id (Map.values (mmap diag))}
                
    instance (Ord a, Eq oIndex) => HasCoproducts (TotalOrder a) (IsSmallerThan a) a (TotalOrder a) (IsSmallerThan a) a oIndex where
        coproduct diag = unsafeCocone nadirCoproduct nat
            where
                nadirCoproduct = Set.maximum $ Map.values $ omap diag
                nat = unsafeNaturalTransformation diag (constantDiagram (src diag) TotalOrder nadirCoproduct) $ Map.weakMapFromSet [(i,IsSmallerThan (diag ->$ i) nadirCoproduct) | i <- ob $ src diag]
                
    instance (Ord a) => HasCoequalizers (TotalOrder a) (IsSmallerThan a) a where
        coequalize parallelDiag = unsafeCocone nadirCoeq nat
            where
                nadirCoeq = parallelDiag ->$ ParallelB
                nat = unsafeNaturalTransformation parallelDiag (constantDiagram Parallel TotalOrder nadirCoeq) (weakMap [(ParallelA, IsSmallerThan (parallelDiag ->$ ParallelA) (parallelDiag ->$ ParallelA)),(ParallelB, IsSmallerThan nadirCoeq nadirCoeq)])
                
    instance (Ord a, Eq mIndex, Eq oIndex) => CocompleteCategory (TotalOrder a) (IsSmallerThan a) a (TotalOrder a) (IsSmallerThan a) a cIndex mIndex oIndex where
        colimit diag = unsafeCocone nadirColimit nat
            where
                nadirColimit = Set.maximum $ Map.values $ omap diag
                nat = unsafeNaturalTransformation diag (constantDiagram (src diag) TotalOrder nadirColimit) $ Map.weakMapFromSet [(i,IsSmallerThan (diag ->$ i) nadirColimit) | i <- ob $ src diag]
                
        coprojectBase diag = Diagram{src = tgt diag, tgt = tgt diag, omap = memorizeFunction id (Map.values (omap diag)), mmap = memorizeFunction id (Map.values (mmap diag))}