{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies  #-}

{-| Module  : FiniteCategories
Description : Typeclasses of morphisms and finite categories and general functions on them.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The goal of this module is to represent small finite categories in order to make usual constructions automatically on them (e.g. (co)limits, (co)completion, etc.)
There is a package that deals with categories as a data type (Data.Category) but it does not provide Ar and Ob operators because
the package uses the fact that the language itself is a category to represent categories
(Hask is (almost) a category, Data.Category benefit from type check at compilation time).
The counterpart is that to use Data.Category, you need to create yourself the usual constructions on your category.
To construct automatically (co)limits and other constructions, we require that the category can enumerate every morphisms between two objects.
We also require that the objects are not types because we want to create objects at runtime (that is why we abandon type check at
compilation time for the structure of our categories).
Lastly, we require that morphisms can be equated for usual constructions purposes.

For example, see the FinSet category and the Composition Graph.
-}

module FiniteCategory.FiniteCategory
(
    -- * Morphism typeclass and related functions
    Morphism(..),
    compose,
    -- * FiniteCategory typeclass
    FiniteCategory(..),
    -- * FiniteCategory functions
    arFrom,
    arFrom2,
    arTo,
    arTo2,
    identities,
    isIdentity,
    isNotIdentity,
    isTerminal,
    isInitial,
    terminalObjects,
    initialObjects,
    -- * GeneratedFiniteCategory typeclass and related functions
    GeneratedFiniteCategory(..),
    genArFrom,
    genArFrom2,
    genArTo,
    genArTo2,
    defaultGenAr,
    defaultDecompose,
    bruteForceDecompose,
    isGenerator,
    isComposite,
    -- * Check for category correctness
    FiniteCategoryError(..),
    checkFiniteCategoryProperties,
    checkGeneratedFiniteCategoryProperties
)
where
    
    import Data.List            (elemIndex, elem, concat, nub, intersect, (\\))
    import Data.Maybe           (fromJust)
    import Utils.Tuple
    import IO.PrettyPrint
    
    -- | 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 operator, surround the '@' symbol with spaces.
    --
    -- Morphism is a multiparametrized type class where /m/ is the type of the morphism and /o/ the type of the objects source and target.
    -- 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 throw an error 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> f @ (g @ h) = (f @ g) @ h
        (@) :: m -> m -> m
        source :: m -> o
        target :: m -> o
        
    -- | Returns the composition of the list of morphisms.
    --
    -- For example :
    -- @compose [f,g,h] = f \@ g \@ h@
    compose :: (Morphism m o) => [m] -> m
    compose l = foldr1 (@) l
        
    -- | A category is multiparametrized by the type of its morphisms and the type of its objects. 
    class FiniteCategory c m o | c -> m, m -> o where
        -- | `ob` should return a list of unique objects :
        --
        -- prop> List.nub (ob c) = ob c
        ob :: c -> [o]
        -- | `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 list of all unique arrows between a source and a target :
        --
        -- prop> List.nub (ar c s t) = ar c s t
        --
        -- Arrows with different source or target should not be equal :
        --
        -- prop> (s1 = s2 && t1 = t2) || List.intersect (ar c s1 t1) (ar c s2 t2) = []
        ar :: (Morphism m o) => c -- ^ The category 
            -> o -- ^ The source of the morphisms
            -> o -- ^ The target of the morphisms
            -> [m] -- ^ The list of morphisms in the category c between source and target
        
        {-# MINIMAL ob, identity, ar #-}
        
        -- | `arrows` returns the list of all unique morphisms of a category.
        arrows :: (FiniteCategory c m o, Morphism m o) => c -> [m]
        arrows c = concat [ar c s t | s <- ob c, t <- ob c]
       
        
    -- | `arTo` returns the list of unique morphisms going to a specified target.
    arTo :: (FiniteCategory c m o, Morphism m o) => c -> o -> [m]
    arTo c t = concat [ar c s t | s <- ob c]

    -- | `arTo2` same as `arTo` but for multiple targets.
    arTo2 :: (FiniteCategory c m o, Morphism m o) => c -> [o] -> [m]
    arTo2 c ts = concat [ar c s t | s <- ob c, t <- ts]

    -- | `arFrom` returns the list of unique morphisms going from a specified source.
    arFrom :: (FiniteCategory c m o, Morphism m o) => c -> o -> [m]
    arFrom c s = concat [ar c s t | t <- ob c]

    -- | `arFrom2` same as `arFrom` but for multiple sources.
    arFrom2 :: (FiniteCategory c m o, Morphism m o) => c -> [o] -> [m]
    arFrom2 c ss = concat [ar c s t | t <- ob c, s <- ss]

    -- | `identities` returns all the identities of a category.
    identities :: (FiniteCategory c m o, Morphism m o) => c -> [m]
    identities c = identity c <$> ob c
    
    -- | Returns wether a morphism is an identity in a category.
    isIdentity :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
    isIdentity c m = identity c (source m) == m
    
    -- | Returns wether a morphism is not an identity.
    isNotIdentity :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
    isNotIdentity c m = not (isIdentity c m)

    -- | Returns wether an object is initial in the category.
    isInitial :: (FiniteCategory c m o, Morphism m o) => c -> o -> Bool
    isInitial cat obj = and [(not.null $ ar cat obj t) && (null $ tail (ar cat obj t)) | t <- ob cat]
    
    -- | Returns the list of intial objects in a category.
    initialObjects :: (FiniteCategory c m o, Morphism m o) => c -> [o]
    initialObjects cat = filter (isInitial cat) (ob cat)
    
    -- | Returns wether an object is terminal in the category.
    isTerminal :: (FiniteCategory c m o, Morphism m o) => c -> o -> Bool
    isTerminal cat obj = and [(not.null $ ar cat s obj) && (null $ tail (ar cat s obj)) | s <- ob cat] -- we construct this convoluted condition to avoid length which would compute all the arrows between s and obj even when unnecessary (beyond two arrows it's useless) 
        
    -- | Returns the list of terminal objects in a category.
    terminalObjects :: (FiniteCategory c m o, Morphism m o) => c -> [o]
    terminalObjects cat = filter (isTerminal cat) (ob cat)
        
    -- | `GeneratedFiniteCategory` is a `FiniteCategory` where some morphisms are selected as generators.
    -- The full category is generated by the generating arrows, which means that every morphism can be written as a composition of several generators.
    -- Some algorithms are simplified because they only need to deal with generators, the rest of the properties are deduced by composition.
    -- Every `FiniteCategory` has at least one set of generators : the set of all of its morphisms.
    class (FiniteCategory c m o) => GeneratedFiniteCategory c m o where
        -- | Same as `ar` but only returns the generators. @genAr c s t@ should be included in @ar c s t@. 
        genAr :: (Morphism m o) => c -> o -> o -> [m]
        
        -- | `decompose` decomposes a morphism into a list of generators (according to composition) :
        --
        -- prop> m = compose (decompose c m) 
        decompose :: (Morphism m o) => c -> m -> [m]
        
        {-# MINIMAL genAr, decompose #-}
        
        -- | Same as `arrows` but only returns the generators. @genArrows c@ should be included in @arrows c@.  
        genArrows :: (GeneratedFiniteCategory c m o, Morphism m o) => c -> [m]
        genArrows c = concat [genAr c s t | s <- ob c, t <- ob c]

    -- | Same as `arTo` but only returns the generators. @genArTo c t@ should be included in @arTo c t@.       
    genArTo :: (GeneratedFiniteCategory c m o, Morphism m o) => c -> o -> [m]
    genArTo c t = concat [genAr c s t | s <- ob c] 
        
    -- | Same as `arTo2` but only returns the generators. @genArTo2 c [t]@ should be included in @arTo2 c [t]@.  
    genArTo2 :: (GeneratedFiniteCategory c m o, Morphism m o) => c -> [o] -> [m]
    genArTo2 c ts = concat [genAr c s t | s <- ob c, t <- ts] 
        
    -- | Same as `arFrom` but only returns the generators. @genArFrom c s@ should be included in @arFrom c s@.  
    genArFrom :: (GeneratedFiniteCategory c m o, Morphism m o) => c -> o -> [m]
    genArFrom c s = concat [genAr c s t | t <- ob c] 
        
    -- | Same as `arFrom2` but only returns the generators. @genArFrom2 c [s]@ should be included in @arFrom2 c [t]@.  
    genArFrom2 :: (GeneratedFiniteCategory c m o, Morphism m o) => c -> [o] -> [m]
    genArFrom2 c ss = concat [genAr c s t | t <- ob c, s <- ss] 
        
    -- | Every `FiniteCategory` has at least one set of generators : the set of all of its morphisms.
    --
    -- `defaultGenAr` is a default method for `genAr` in order to transform any `FiniteCategory` into a `GeneratedFiniteCategory`.
    --
    -- Use `defaultGenAr` in conjonction with `defaultDecompose`.
    defaultGenAr :: (GeneratedFiniteCategory c m o, Morphism m o) => c -> o -> o -> [m]
    defaultGenAr = ar
    
    -- | Every `FiniteCategory` has at least one set of generators : the set of all of its morphisms.
    --
    -- `defaultDecompose` is a default method for `decompose` in order to transform any `FiniteCategory` into a `GeneratedFiniteCategory`.
    --
    -- Use `defaultDecompose` in conjonction with `defaultGenAr`.
    defaultDecompose :: (GeneratedFiniteCategory c m o, Morphism m o) => c -> m -> [m]
    defaultDecompose _ m = (m:[])
    
    -- | Helper function for `bruteForceDecompose`.
    bruteForce :: (GeneratedFiniteCategory c m o, Morphism m o, Eq m) => c -> m -> [[m]] -> [m]
    bruteForce c m l = if index == Nothing then bruteForce c m (concat (pathToAugmentedPaths <$> l)) else l !! (fromJust index) where
        index = elemIndex m (compose <$> l)
        leavingMorph path = (genArFrom c) $ target.head $ path
        pathToAugmentedPaths path = (leavingMorph path) >>= (\x -> [(x:path)] )   
    
    -- | If `genAr` is implemented, we can find the decomposition of a morphism by bruteforce search (we compose every arrow until we get the morphism we want).
    --
    -- This method is meant to be used temporarly until a proper decompose method is implemented. (It is very slow.)
    bruteForceDecompose :: (GeneratedFiniteCategory c m o, Morphism m o, Eq m) => c -> m -> [m]
    bruteForceDecompose c m = bruteForce c m ((:[]) <$> genArFrom c (source m))  
    
    -- | Returns if a morphism is a generating morphism.
    -- It can be overloaded to speed it up (for a morphism /f/, it computes every generators between the source and the target of /f/ and checks if /f/ is in the list.)
    isGenerator :: (GeneratedFiniteCategory c m o, Morphism m o, Eq m) => c -> m -> Bool
    isGenerator c f = elem f (genAr c (source f) (target f))
    
    -- | Opposite of `isGenerator`, i.e. returns if the morphism is composite.
    isComposite :: (GeneratedFiniteCategory c m o, Morphism m o, Eq m) => c -> m -> Bool
    isComposite c f = not (isGenerator c f)

    -- | A data type to represent an incoherence inside a category.
    data FiniteCategoryError m o =
                         CompositionNotAssociative {f :: m, g :: m, h :: m, fg_h :: m, f_gh :: m} -- ^ @(h\@g)\@f /= h\@(g\@f)@
                       | ObjectsNotUnique {dupObj :: o} -- ^ `dupObj` was found multiple times in @ob c@.
                       | MorphismsNotUnique {dupMorph :: m} -- ^ `dupMorph` was found multiple times in the category.
                       | ArrowsNotExhaustive {missingAr :: m} -- ^ `missingAr` is an arrow found by calling @ar c@ but is not in @arrows c@.
                       | ArrowBetweenUnknownObjects {f :: m, s :: o, t :: o} -- ^ `f` was found in the category but its source `s` or target `t` is not in @ob c@. 
                       | WrongSource {f :: m, realSource :: o} -- ^ `f` was found by using @ar c s t@ where @s /= source f@.
                       | WrongTarget {f :: m, realTarget :: o} -- ^ `f` was found by using @ar c s t@ where @t /= target f@.
                       | IdentityNotLeftNeutral {idL :: m, f :: m, foidL :: m} -- ^ `idL` is not a valid identity : @f \@ idL /= f@.
                       | IdentityNotRightNeutral {f :: m, idR :: m, idRof :: m} -- ^ `idR` is not a valid identity : @idR \@ f /= f@.
                       | MorphismsShouldNotBeEqual {f :: m, g :: m} -- ^ @f == g@ even though they don'y share the same source or target.
                       | NotTransitive {f :: m, g :: m} -- ^ @f\@g@ is not an element of @ar c (source g) (target g)@.
                       | GeneratorIsNotAMorphism {f :: m} -- ^ `f` is a generator but not a morphism.
                       | MorphismDoesntDecomposesIntoGenerators {f :: m, decomp :: [m], notGen :: m} -- ^ The morphism `f` decomposes into `decomp` where `notGen` is a non generating morphism.
                       | WrongDecomposition {f :: m, decomp :: [m], comp :: m} -- ^ @compose (decompose c f) /= f@.
                       deriving (Eq, Show)

    -- | Checks every properties listed above for a category.
    --
    -- If an error is found in the category, just a `FiniteCategoryError` is returned.
    -- Otherwise, nothing is returned.
    checkFiniteCategoryProperties :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Maybe (FiniteCategoryError m o)
    checkFiniteCategoryProperties c
        | (not.null) dupObjects = Just ObjectsNotUnique {dupObj=head dupObjects}
        | (not.null) incoherentEq = Just MorphismsShouldNotBeEqual {f=(fst.head) incoherentEq, g=(snd.head) incoherentEq}
        | (not.null) wrongSource = Just WrongSource {f = (fst.head) wrongSource, realSource = (snd.head) wrongSource}
        | (not.null) wrongTarget = Just WrongTarget {f = (fst.head) wrongTarget, realTarget = (snd.head) wrongTarget}
        | (not.null) dupMorph = Just MorphismsNotUnique {dupMorph=head dupMorph}
        | (not.null) missingAr = Just ArrowsNotExhaustive {missingAr=head missingAr}
        | (not.null) unknownObjects = Just ArrowBetweenUnknownObjects {f=(fst3.head) unknownObjects, s=(snd3.head) unknownObjects, t=(trd3.head) unknownObjects}
        | (not.null) idNotLNeutral = Just IdentityNotLeftNeutral {idL=(fst3.head) idNotLNeutral, f=(snd3.head) idNotLNeutral,foidL=(trd3.head) idNotLNeutral} 
        | (not.null) idNotRNeutral = Just IdentityNotRightNeutral {f=(fst3.head) idNotRNeutral, idR=(snd3.head) idNotRNeutral,idRof=(trd3.head) idNotRNeutral} 
        | (not.null) notAssociative = Just CompositionNotAssociative {f=(fst3.head) notAssociative,g=(snd3.head) notAssociative,h=(trd3.head) notAssociative, fg_h=(((fst3.head)notAssociative) @ ((snd3.head)notAssociative)) @ ((trd3.head)notAssociative),
                        f_gh=((fst3.head)notAssociative) @ (((snd3.head)notAssociative) @ ((trd3.head)notAssociative))}
        | (not.null) notTransitive = Just NotTransitive {f=(fst.head) notTransitive, g=(snd.head) notTransitive}
        | otherwise = Nothing
        where
            dupObjects = ob c \\ nub (ob c)
            arrowsByAr = concat [ar c s t | s <- (ob c), t <- (ob c)]
            incoherentEq = [(f,g) | f <- arrows c, g <- arrows c, f == g && (source f /= source g || target f /= target g)]
            wrongSource = [(f,s) | s <- ob c, t <- ob c, f <- ar c s t, source f /= s]
            wrongTarget = [(f,t) | s <- ob c, t <- ob c, f <- ar c s t, target f /= t]
            dupMorph = arrowsByAr \\ nub arrowsByAr
            missingAr = arrowsByAr \\ (arrows c)
            unknownObjects = [(f,source f,target f) | f <- arrows c, not ( (source f) `elem` (ob c) && (target f) `elem` (ob c) )]
            idNotLNeutral = [(identity c (source f),f,f @ identity c (source f)) | f <- arrows c, f @ identity c (source f) /= f]
            idNotRNeutral = [(f,identity c (target f), identity c (target f) @ f) | f <- arrows c, identity c (target f) @ f /= f]
            notAssociative = [(x,y,z) | z <- arrows c, y <- arFrom c (target z), x <- arFrom c (target y), (x @ y) @ z /= x @ (y @ z)]
            notTransitive = [(f,g) | g <- arrows c, f <- arFrom c (target g), not (elem (f @ g) (ar c (source g) (target f)))]
            fst3 (x,_,_) = x
            snd3 (_,x,_) = x
            trd3 (_,_,x) = x
        
    -- | Same as `checkFiniteCategoryProperties` but for `GeneratedFiniteCategory`.
    checkGeneratedFiniteCategoryProperties :: (GeneratedFiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Maybe (FiniteCategoryError m o)
    checkGeneratedFiniteCategoryProperties c
        | errCat /= Nothing = errCat
        | (not.null) genNotMorph = Just GeneratorIsNotAMorphism {f=head genNotMorph}
        | (not.null) decompIntoComposite = Just MorphismDoesntDecomposesIntoGenerators {f=(fst3.head) decompIntoComposite, decomp=(snd3.head) decompIntoComposite, notGen=(trd3.head) decompIntoComposite}
        | (not.null) wrongDecomp = Just WrongDecomposition {f=(fst3.head) wrongDecomp, decomp=(snd3.head) wrongDecomp, comp=(trd3.head) wrongDecomp}
        | otherwise = Nothing 
        where 
            errCat = checkFiniteCategoryProperties c
            genNotMorph = genArrows c \\ arrows c
            decompIntoComposite = [(m,decompose c m,f) | m <- arrows c, f <- decompose c m, not (elem f (genAr c (source f) (target f)))]
            wrongDecomp = [(f,decompose c f, compose (decompose c f)) | f <- arrows c, compose (decompose c f) /= f]
            fst3 (x,_,_) = x
            snd3 (_,x,_) = x
            trd3 (_,_,x) = x
            
    instance (Show m, Show o) => PrettyPrintable (FiniteCategoryError m o) where
        pprint = show