{-# 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 (IsSmallerThan a -> IsSmallerThan a -> Bool
(IsSmallerThan a -> IsSmallerThan a -> Bool)
-> (IsSmallerThan a -> IsSmallerThan a -> Bool)
-> Eq (IsSmallerThan a)
forall a. Eq a => IsSmallerThan a -> IsSmallerThan a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => IsSmallerThan a -> IsSmallerThan a -> Bool
== :: IsSmallerThan a -> IsSmallerThan a -> Bool
$c/= :: forall a. Eq a => IsSmallerThan a -> IsSmallerThan a -> Bool
/= :: IsSmallerThan a -> IsSmallerThan a -> Bool
Eq, Int -> IsSmallerThan a -> ShowS
[IsSmallerThan a] -> ShowS
IsSmallerThan a -> String
(Int -> IsSmallerThan a -> ShowS)
-> (IsSmallerThan a -> String)
-> ([IsSmallerThan a] -> ShowS)
-> Show (IsSmallerThan a)
forall a. Show a => Int -> IsSmallerThan a -> ShowS
forall a. Show a => [IsSmallerThan a] -> ShowS
forall a. Show a => IsSmallerThan a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> IsSmallerThan a -> ShowS
showsPrec :: Int -> IsSmallerThan a -> ShowS
$cshow :: forall a. Show a => IsSmallerThan a -> String
show :: IsSmallerThan a -> String
$cshowList :: forall a. Show a => [IsSmallerThan a] -> ShowS
showList :: [IsSmallerThan a] -> ShowS
Show)
    
    instance (Eq a) => Morphism (IsSmallerThan a) a where
        (IsSmallerThan a
m1 a
t) @? :: IsSmallerThan a -> IsSmallerThan a -> Maybe (IsSmallerThan a)
@? (IsSmallerThan a
s a
m2)
            | a
m1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
m2 = IsSmallerThan a -> Maybe (IsSmallerThan a)
forall a. a -> Maybe a
Just (IsSmallerThan a -> Maybe (IsSmallerThan a))
-> IsSmallerThan a -> Maybe (IsSmallerThan a)
forall a b. (a -> b) -> a -> b
$ a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan a
s a
t
            | Bool
otherwise = Maybe (IsSmallerThan a)
forall a. Maybe a
Nothing
        source :: IsSmallerThan a -> a
source (IsSmallerThan a
s a
_) = a
s
        target :: IsSmallerThan a -> a
target (IsSmallerThan a
_ a
t) = a
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 (TotalOrder a -> TotalOrder a -> Bool
(TotalOrder a -> TotalOrder a -> Bool)
-> (TotalOrder a -> TotalOrder a -> Bool) -> Eq (TotalOrder a)
forall a. TotalOrder a -> TotalOrder a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. TotalOrder a -> TotalOrder a -> Bool
== :: TotalOrder a -> TotalOrder a -> Bool
$c/= :: forall a. TotalOrder a -> TotalOrder a -> Bool
/= :: TotalOrder a -> TotalOrder a -> Bool
Eq,Int -> TotalOrder a -> ShowS
[TotalOrder a] -> ShowS
TotalOrder a -> String
(Int -> TotalOrder a -> ShowS)
-> (TotalOrder a -> String)
-> ([TotalOrder a] -> ShowS)
-> Show (TotalOrder a)
forall a. Int -> TotalOrder a -> ShowS
forall a. [TotalOrder a] -> ShowS
forall a. TotalOrder a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Int -> TotalOrder a -> ShowS
showsPrec :: Int -> TotalOrder a -> ShowS
$cshow :: forall a. TotalOrder a -> String
show :: TotalOrder a -> String
$cshowList :: forall a. [TotalOrder a] -> ShowS
showList :: [TotalOrder a] -> ShowS
Show)
    
    instance (Eq a, Ord a) => Category (TotalOrder a) (IsSmallerThan a) a where
        identity :: Morphism (IsSmallerThan a) a =>
TotalOrder a -> a -> IsSmallerThan a
identity TotalOrder a
_ a
x = a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan a
x a
x
        ar :: Morphism (IsSmallerThan a) a =>
TotalOrder a -> a -> a -> Set (IsSmallerThan a)
ar TotalOrder a
_ a
x a
y
            | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
y = [IsSmallerThan a] -> Set (IsSmallerThan a)
forall a. [a] -> Set a
set [a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan a
x a
y]
            | Bool
otherwise = [IsSmallerThan a] -> Set (IsSmallerThan a)
forall a. [a] -> Set a
set []
    
    instance (PrettyPrint a) => PrettyPrint (IsSmallerThan a) where
        pprint :: IsSmallerThan a -> String
pprint (IsSmallerThan a
x a
y) = a -> String
forall a. PrettyPrint a => a -> String
pprint a
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" <= " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. PrettyPrint a => a -> String
pprint a
y
    
    instance PrettyPrint (TotalOrder a) where
        pprint :: TotalOrder a -> String
pprint = TotalOrder a -> String
forall a. Show a => a -> String
show