{-# 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(..),
    -- ** Morphism predicates
    isIdentity,
    isNotIdentity,
    isIso,
    isSection,
    isRetraction,
    areIsomorphic,
    -- ** Generator predicates
    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
        -- | 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)
        (@?) :: m -> m -> Maybe m
        
        -- | Return the source object of the morphism.
        source :: m -> o
        
        -- | Return the target object of the morphism.
        target :: m -> o
    
    -- | Unsafe version of '(@?)'.
    (@) :: (Morphism m o) => m -> m -> m
    (@) m2 m1
        | null compo = error "Math.Category.(@): incompatible morphisms"
        | otherwise = r
        where
        compo = m2 @? m1
        Just r = compo
    
    -- | 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 [] = error "Category.compose: empty list to compose"
    compose l = foldr1 (@) 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 = 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 _ = (:[])
            
    -- | 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 c m = identity c (source 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 c m = not (isIdentity c 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 c m = (Set.setToMaybe) $ Set.filter (\f -> isIdentity c (m @ f) && isIdentity c (f @ m)) (ar c (target m) (source 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 c s t = (Set.setToMaybe).(Set.catMaybes) $ findInverse c <$> ar c s 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 c s t = not.null $ findIsomorphism c s t
        
    -- | Return if a morphism is an isomorphism
    isIso :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
    isIso c m = not.null $ findInverse c m

    -- | Find all right inverses.
    findRightInverses :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> m -> Set m
    findRightInverses c f = Set.filter (\g -> isIdentity c (f @ g)) $ ar c (target f) (source f)
    
    -- | Return wether a morphism is a section.
    isSection :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
    isSection c f = not.(Set.null) $ findRightInverses c 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 c f = Set.filter (\g ->  isIdentity c (g @ f)) $ ar c (target f) (source f)
    
    -- | Return wether a morphism is a retraction.
    isRetraction :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
    isRetraction c f = not.(Set.null) $ findLeftInverses c f
        
    -- | Return if a morphism is a generating morphism.
    isGenerator :: (Category c m o, Morphism m o, Eq m) => c -> m -> Bool
    isGenerator c f = f `isIn` (genAr c (source f) (target 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 c f = not (isGenerator c f)