{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies  #-}

{-| Module  : FiniteCategories
Description : 'Morphism' and 'Category' typeclasses. 
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A `Morphism` is composable, it has a source and a target.

A `Category` allows to enumerate all arrows between two objects and allows to construct the identity of an object. It is mathematically a locally finite category, we name it 'Category' for simplicity.

See `FiniteCategory` for the ability to enumerate the objects of a category.

We don't reify the `Category` concept because we want to be able to equate categories (functions are not equatable).

A `GeneratedCategory` is a `Category` where some morphisms are selected as generators. Any 'Category' has a trivial set of generators: the set of all of its arrows. You can override the default definition of generators when creating your 'Category' by instantiating 'GeneratedCategory'.
-}

module Math.Category
(
    -- * Morphism

    Morphism(..),
    -- ** Morphism related functions

    compose,
    -- * Category

    Category(..),
    arWithoutId,
    -- ** Morphism predicates

    isIdentity,
    isNotIdentity,
    isIso,
    isSection,
    isRetraction,
    areIsomorphic,
    -- ** Generator predicates

    genArWithoutId,
    isGenerator,
    isComposite,
    -- ** Find special morphisms

    findInverse,
    findIsomorphism,
    findRightInverses,
    findLeftInverses,
)
where
    import              Data.WeakSet             (Set)
    import qualified    Data.WeakSet           as Set
    import              Data.WeakSet.Safe
    
    -- | A `Morphism` can be composed with the ('@?') operator, it has a 'source' and a 'target'.

    --

    -- The ('@?') operator should not be confused with the as-pattern. When using the composition operator, surround the '@?' symbol with spaces.

    --

    -- 'Morphism' is a multiparametrized typeclass where /m/ is the type of the morphism and /o/ the type of the source and target objects.

    --

    -- Source and target are the same type of objects, we distinguish objects not by their type but instead by their values.

    class Morphism m o | m -> o where        
        -- | Unsafe version of ('@?').

        --        

        -- The composition @g '@' f@ may throw an error if @'source' g /= 'target' f@ although it is not garanteed that it will! This is a fast function as it is not supposed to check any compatibility of morphisms.

        --

        -- Composition is associative :

        --

        -- prop> f @ (g @ h) = (f @ g) @ h

        (@) :: m -> m -> m
        
        -- | The composition @g '@?' f@ should return 'Nothing' if @'source' g /= 'target' f@.

        -- This is a consequence of loosing type check at compilation time, we defer the exception handling to execution time.

        --

        -- Composition is associative :

        --

        -- prop> (fmap (f @?)) (g @? h) = fmap (@? h) (f @? g)

        (@?) :: (Eq o) => m -> m -> Maybe m
        (@?) m
g m
f
            | m -> o
forall m o. Morphism m o => m -> o
source m
g o -> o -> Bool
forall a. Eq a => a -> a -> Bool
== m -> o
forall m o. Morphism m o => m -> o
target m
f = m -> Maybe m
forall a. a -> Maybe a
Just (m -> Maybe m) -> m -> Maybe m
forall a b. (a -> b) -> a -> b
$ m
g m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
g
            | Bool
otherwise = Maybe m
forall a. Maybe a
Nothing
        
        -- | Return the source object of the morphism.

        source :: m -> o
        
        -- | Return the target object of the morphism.

        target :: m -> o
    
    -- | Return the composition of a list of morphisms.

    --

    -- For example :

    -- @compose [f,g,h] = f \@ g \@ h@

    --

    -- Return an error if the list is empty : we would have to return an identity but we don't know which one.

    compose :: (Morphism m o) => [m] -> m
    compose :: forall m o. Morphism m o => [m] -> m
compose [] = [Char] -> m
forall a. HasCallStack => [Char] -> a
error [Char]
"Category.compose: empty list to compose"
    compose [m]
l = (m -> m -> m) -> [m] -> m
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 m -> m -> m
forall m o. Morphism m o => m -> m -> m
(@) [m]
l
        
    -- | A `Category` allows to enumerate all arrows between two objects and allows to construct the identity of an object.

    --

    -- A 'Category' is multiparametrized by the type of its morphisms and the type of its objects. 

    --

    -- This typeclass does not assume the category is finite, the number of objects in the category may be infinite.

    --

    -- A category is a set of objects and a set of morphisms which follows the category axioms.

    --

    -- A category also has sets of generating morphisms. A set of generating morphisms is a set of morphism such that every morphism of the category can be constructed by

    -- composing generators. Note that we consider identities should be generators even though they can be constructed as the composition of zero morphism because 'compose' can't compose zero morphism.

    --

    -- Some algorithms are simplified because they only need to deal with generators, the rest of the properties are deduced by composition.

    --

    -- Every `Category` has at least one set of generators : the set of all of its morphisms.

    --

    -- You can override 'genAr' and 'decompose' to define a more interesting set of generating morphisms for a given 'Category'.

    class Category c m o | c -> m, m -> o where
        -- | `identity` should return the identity associated to the object /o/ in the category /c/.

        -- 

        -- The identity morphism is a morphism such that the two following properties are verified :

        --

        -- prop> f '@' 'identity' c ('source' f) = f

        -- prop> 'identity' c ('target' g) '@' g = g

        identity :: (Morphism m o) => c -> o -> m
        
        -- | `ar` should return the set of all arrows between a source and a target.

        --

        -- Arrows with different source or target should not be equal.

        ar :: (Morphism m o) => c -- ^ The category 

            -> o -- ^ The source of the morphisms

            -> o -- ^ The target of the morphisms

            -> Set m -- ^ The set of morphisms in the category c between source and target

            
        {-|# MINIMAL identity, ar #-}
            
        -- | Same as `ar` but only returns the generators. 

        --

        -- prop> @('genAr' c s t) `isIncludedIn` ('ar' c s t)@.

        --

        -- The default implementation is 'ar' because the set of all arrows generates trivially the category.

        genAr :: (Morphism m o) => c -> o -> o -> Set m
        genAr = c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar
        
        -- | `decompose` decomposes a morphism into a list of generators (according to composition) :

        --

        -- prop> m = compose (decompose c m)

        --

        -- An identity should be decomposed into a list containing itself.

        --

        -- The default implementation returns the morphism in a list as all arrows are generators.

        decompose :: (Morphism m o) => c -> m -> [m]
        decompose c
_ = (m -> [m] -> [m]
forall a. a -> [a] -> [a]
:[])
      
    -- | Return the arrows between two objects without the identities.

    arWithoutId :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> o -> o -> Set m
    arWithoutId :: forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> o -> o -> Set m
arWithoutId c
c o
s o
t = (m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity c
c) (Set m -> Set m) -> Set m -> Set m
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c o
s o
t
      
    -- | Return the generators between two objects without the identities.

    genArWithoutId :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> o -> o -> Set m
    genArWithoutId :: forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> o -> o -> Set m
genArWithoutId c
c o
s o
t = (m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity c
c) (Set m -> Set m) -> Set m -> Set m
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
genAr c
c o
s o
t
            
    -- | Return wether a morphism is an identity in a category.

    isIdentity :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
    isIdentity :: forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isIdentity c
c m
m = c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c
c (m -> o
forall m o. Morphism m o => m -> o
source m
m) m -> m -> Bool
forall a. Eq a => a -> a -> Bool
== m
m
    
    -- | Return wether a morphism is not an identity.

    isNotIdentity :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
    isNotIdentity :: forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity c
c m
m = Bool -> Bool
not (c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isIdentity c
c m
m)

    -- | Return Just an inverse of a morphism if possible, Nothing otherwise

    findInverse :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> m -> Maybe m
    findInverse :: forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Maybe m
findInverse c
c m
m = (forall a. Set a -> Maybe a
Set.setToMaybe) (Set m -> Maybe m) -> Set m -> Maybe m
forall a b. (a -> b) -> a -> b
$ (m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\m
f -> c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isIdentity c
c (m
m m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
f) Bool -> Bool -> Bool
&& c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isIdentity c
c (m
f m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
m)) (c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c (m -> o
forall m o. Morphism m o => m -> o
target m
m) (m -> o
forall m o. Morphism m o => m -> o
source m
m))
    
    -- | Return Just an isomorphism from an object to another if possible, Nothing otherwise.

    findIsomorphism :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> o -> o -> Maybe m
    findIsomorphism :: forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> o -> o -> Maybe m
findIsomorphism c
c o
s o
t = (Set m -> Maybe m
forall a. Set a -> Maybe a
Set.setToMaybe)(Set m -> Maybe m)
-> (Set (Maybe m) -> Set m) -> Set (Maybe m) -> Maybe m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Set (Maybe m) -> Set m
forall a. Set (Maybe a) -> Set a
Set.catMaybes) (Set (Maybe m) -> Maybe m) -> Set (Maybe m) -> Maybe m
forall a b. (a -> b) -> a -> b
$ c -> m -> Maybe m
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Maybe m
findInverse c
c (m -> Maybe m) -> Set m -> Set (Maybe m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c o
s o
t
    
    -- | Return wether two objects are isomorphic or not.

    areIsomorphic :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> o -> o -> Bool
    areIsomorphic :: forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> o -> o -> Bool
areIsomorphic c
c o
s o
t = Bool -> Bool
not(Bool -> Bool) -> (Maybe m -> Bool) -> Maybe m -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Maybe m -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Maybe m -> Bool) -> Maybe m -> Bool
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Maybe m
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> o -> o -> Maybe m
findIsomorphism c
c o
s o
t
        
    -- | Return if a morphism is an isomorphism

    isIso :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
    isIso :: forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isIso c
c m
m = Bool -> Bool
not(Bool -> Bool) -> (Maybe m -> Bool) -> Maybe m -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Maybe m -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Maybe m -> Bool) -> Maybe m -> Bool
forall a b. (a -> b) -> a -> b
$ c -> m -> Maybe m
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Maybe m
findInverse c
c m
m

    -- | Find all right inverses.

    findRightInverses :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> m -> Set m
    findRightInverses :: forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Set m
findRightInverses c
c m
f = (m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\m
g -> c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isIdentity c
c (m
f m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
g)) (Set m -> Set m) -> Set m -> Set m
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c (m -> o
forall m o. Morphism m o => m -> o
target m
f) (m -> o
forall m o. Morphism m o => m -> o
source m
f)
    
    -- | Return wether a morphism is a section.

    isSection :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
    isSection :: forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isSection c
c m
f = Bool -> Bool
not(Bool -> Bool) -> (Set m -> Bool) -> Set m -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Set m -> Bool
forall a. Set a -> Bool
Set.null) (Set m -> Bool) -> Set m -> Bool
forall a b. (a -> b) -> a -> b
$ c -> m -> Set m
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Set m
findRightInverses c
c m
f
    
    -- | Find a left inverse if it can, returns Nothing otherwise.

    findLeftInverses :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> m -> Set m
    findLeftInverses :: forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Set m
findLeftInverses c
c m
f = (m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\m
g ->  c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isIdentity c
c (m
g m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
f)) (Set m -> Set m) -> Set m -> Set m
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c (m -> o
forall m o. Morphism m o => m -> o
target m
f) (m -> o
forall m o. Morphism m o => m -> o
source m
f)
    
    -- | Return wether a morphism is a retraction.

    isRetraction :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
    isRetraction :: forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isRetraction c
c m
f = Bool -> Bool
not(Bool -> Bool) -> (Set m -> Bool) -> Set m -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Set m -> Bool
forall a. Set a -> Bool
Set.null) (Set m -> Bool) -> Set m -> Bool
forall a b. (a -> b) -> a -> b
$ c -> m -> Set m
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Set m
findLeftInverses c
c m
f
        
    -- | Return if a morphism is a generating morphism.

    isGenerator :: (Category c m o, Morphism m o, Eq m) => c -> m -> Bool
    isGenerator :: forall c m o.
(Category c m o, Morphism m o, Eq m) =>
c -> m -> Bool
isGenerator c
c m
f = m
f m -> Set m -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` (c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
genAr c
c (m -> o
forall m o. Morphism m o => m -> o
source m
f) (m -> o
forall m o. Morphism m o => m -> o
target m
f))
    
    -- | Opposite of `isGenerator`, i.e. returns if the morphism is composite.

    isComposite :: (Category c m o, Morphism m o, Eq m) => c -> m -> Bool
    isComposite :: forall c m o.
(Category c m o, Morphism m o, Eq m) =>
c -> m -> Bool
isComposite c
c m
f = Bool -> Bool
not (c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m) =>
c -> m -> Bool
isGenerator c
c m
f)