{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

{-| Module  : FiniteCategories
Description : An 'OrdinalCategory' is a 'TotalOrder' category where the total order is an order induced by ordinal numbers. 
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

An 'OrdinalCategory' is a 'TotalOrder' category where the total order is an order induced by ordinal numbers. 

Concretely the type parameter must implement the Enum typeclass.

For example, the 'TotalOrder' category induced by (R,<=) is not an 'OrdinalCategory' whereas (N,<=) is.

It induces a non trivial generating set of arrows thanks to the 'succ' function.
-}

module Math.Categories.OrdinalCategory
(
    OrdinalCategory(..),
    module Math.Categories.TotalOrder
    
)
where
    import              Math.Category
    import              Math.Categories.FunctorCategory
    import              Math.Categories.ConeCategory
    import              Math.Categories.TotalOrder
    import              Math.IO.PrettyPrint
    
    import              Data.WeakSet.Safe
    import qualified    Data.WeakMap          as Map
    import              Data.WeakMap.Safe
    
    
    -- | An 'OrdinalCategory' is a 'TotalOrder' where the type /a/ follows the Enum typeclass.

    newtype OrdinalCategory a = OrdinalCategory (TotalOrder a) deriving (OrdinalCategory a -> OrdinalCategory a -> Bool
(OrdinalCategory a -> OrdinalCategory a -> Bool)
-> (OrdinalCategory a -> OrdinalCategory a -> Bool)
-> Eq (OrdinalCategory a)
forall a. OrdinalCategory a -> OrdinalCategory a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. OrdinalCategory a -> OrdinalCategory a -> Bool
== :: OrdinalCategory a -> OrdinalCategory a -> Bool
$c/= :: forall a. OrdinalCategory a -> OrdinalCategory a -> Bool
/= :: OrdinalCategory a -> OrdinalCategory a -> Bool
Eq, Int -> OrdinalCategory a -> ShowS
[OrdinalCategory a] -> ShowS
OrdinalCategory a -> String
(Int -> OrdinalCategory a -> ShowS)
-> (OrdinalCategory a -> String)
-> ([OrdinalCategory a] -> ShowS)
-> Show (OrdinalCategory a)
forall a. Int -> OrdinalCategory a -> ShowS
forall a. [OrdinalCategory a] -> ShowS
forall a. OrdinalCategory a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Int -> OrdinalCategory a -> ShowS
showsPrec :: Int -> OrdinalCategory a -> ShowS
$cshow :: forall a. OrdinalCategory a -> String
show :: OrdinalCategory a -> String
$cshowList :: forall a. [OrdinalCategory a] -> ShowS
showList :: [OrdinalCategory a] -> ShowS
Show)
    
    instance (Enum a, Ord a) => Category (OrdinalCategory a) (IsSmallerThan a) a where
        ar :: Morphism (IsSmallerThan a) a =>
OrdinalCategory a -> a -> a -> Set (IsSmallerThan a)
ar OrdinalCategory 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 []
            
        identity :: Morphism (IsSmallerThan a) a =>
OrdinalCategory a -> a -> IsSmallerThan a
identity OrdinalCategory a
_ a
x = a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan a
x a
x
        
        -- | An 'OrdinalCategory' is generated by morphisms from a number to its successor.

        genAr :: Morphism (IsSmallerThan a) a =>
OrdinalCategory a -> a -> a -> Set (IsSmallerThan a)
genAr OrdinalCategory a
_ a
x a
y
            | a
x a -> a -> Bool
forall a. Eq 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
x]
            | (a -> a
forall a. Enum a => a -> a
succ a
x) a -> a -> Bool
forall a. Eq 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 []
  
        decompose :: Morphism (IsSmallerThan a) a =>
OrdinalCategory a -> IsSmallerThan a -> [IsSmallerThan a]
decompose OrdinalCategory a
_ (IsSmallerThan a
x a
y)
            | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y = [a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan a
x a
y]
            | Bool
otherwise = [IsSmallerThan a] -> [IsSmallerThan a]
forall a. [a] -> [a]
reverse ([IsSmallerThan a] -> [IsSmallerThan a])
-> [IsSmallerThan a] -> [IsSmallerThan a]
forall a b. (a -> b) -> a -> b
$ (\a
n -> a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan a
n (a -> a
forall a. Enum a => a -> a
succ a
n)) (a -> IsSmallerThan a) -> [a] -> [IsSmallerThan a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a
x..(a -> a
forall a. Enum a => a -> a
pred a
y)]
    
    
    instance (Show a) => PrettyPrint (OrdinalCategory a) where
        pprint :: OrdinalCategory a -> String
pprint = OrdinalCategory a -> String
forall a. Show a => a -> String
show