{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MonadComprehensions #-}
{-# LANGUAGE MultiParamTypeClasses #-}

{-| Module  : FiniteCategories
Description : Typeclasses for 'Category' with special properties such as being complete.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Typeclasses for 'Category' with special properties such as being complete. 

A 'Category' might have products meaning that any 'discreteDiagram' on it has a limit.

A 'Category' might have equalizers meaning that any 'parallelDiagram' on it has a limit.

If a 'Category' have both products and equalizers, it is complete meaning that it has all small limits.

To compute limits in a custom 'FiniteCategory', see 'limits' in Math.ConeCategory.
-}

module Math.CompleteCategory
(
    -- * Limit type
    Limit(..),
    unproject,
    -- * Helper typeclasses to define a 'CompleteCategory'
    HasProducts(..),
    HasEqualizers(..),
    limitFromProductsAndEqualizers,
    -- * CompleteCategory
    CompleteCategory(..),
    unprojectBase,
)
where
    import              Data.WeakSet             (Set)
    import qualified    Data.WeakSet           as Set
    import              Data.WeakSet.Safe
    import              Data.WeakMap             (Map)
    import qualified    Data.WeakMap           as Map
    import              Data.WeakMap.Safe
    import              Data.List               (intercalate)
    import              Data.Simplifiable
    
    import              Math.Category
    import              Math.FiniteCategory
    import              Math.Functors.DiagonalFunctor
    import              Math.Categories.FunctorCategory
    import              Math.Categories.ConeCategory
    import              Math.Categories.Galaxy
    import              Math.FiniteCategories.DiscreteCategory
    import              Math.FiniteCategories.Parallel
    import              Math.IO.PrettyPrint
    
    import              GHC.Generics
    
    -- | For a 'Category' parametrized over a type t, the apex of the limit of a diagram indexed by a category parametrized over a type i will contain 'ProductElement' constructions (a product element is a tuple). A given tuple can be projected onto a 'Projection' at a given index.
    --
    -- For example, in 'FinSet', let's consider a discrete diagram from 'DiscreteTwo' to ('FinSet' Int) which selects {1,2} and {3,4}. The apex of the limit is obviously {(1,3),(1,4),(2,3),(2,4)}, note that it is not an object of ('Finset' Int) but an object of ('FinSet' (Set (Int,Int))). The 'Limit' type allows to construct type ('FinSet' ('Limit' 'DiscreteTwo' Int)) in which we can consider the original objects with 'Projection' and the new tuples with 'ProductElement'. Here, instead of couples, we will consider the limit to be {ProductElement (weakMap [(A,1),(B,3)]),ProductElement (weakMap [(A,1),(B,4)]),ProductElement (weakMap [(A,2),(B,3)]),ProductElement (weakMap [(A,2),(B,4)])}. We can construct projections in the same category, for example along 'A', which will map 'ProductElement' (weakMap [(A,1),(B,3)]) to ('Projection' 1).
    data Limit oIndex t = Projection t -- ^ A 'Projection' is the parameter type of the original category to project the limits back to them.
                   | ProductElement (Map oIndex t) -- ^ A 'ProductElement' is a mapping from the indexing objects to objects of type t.
                   deriving (Eq, Show, Generic, Simplifiable)
                   
    instance (PrettyPrint oIndex, PrettyPrint t, Eq oIndex) => PrettyPrint (Limit oIndex t) where
        pprint v (Projection x) = pprint v x
        pprint v (ProductElement tuple) = "(" ++ (intercalate "," (pprint v <$> Map.elems tuple)) ++ ")"
        
        pprintWithIndentations cv ov indent (Projection x) = indentation (ov - cv) indent ++ pprint cv x ++ "\n"
        pprintWithIndentations cv ov indent (ProductElement tuple) = indentation (ov - cv) indent ++ "(" ++ (intercalate "," (pprint cv <$> Map.elems tuple)) ++ ")\n"
    
    -- | Remove the constructor 'Projection' from an original object t if possible.
    unproject :: Limit oIndex t -> Maybe t
    unproject (Projection t) = Just t
    unproject (ProductElement _) = Nothing
    
    -- | The typeclass of categories which have all products.
    class (Category c m o, Morphism m o,
           Category cLim mLim oLim, Morphism mLim oLim) =>
           HasProducts c m o cLim mLim oLim oIndex | c -> m, m -> o, cLim -> mLim, mLim -> oLim, c oIndex -> cLim where
        
        -- | Given a 'discreteDiagram' selecting objects, return the product of the selected objects as a 'Cone'.
        product :: Diagram (DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex c m o -> Cone(DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex cLim mLim oLim
        
        
        
    -- | The typeclass of categories which have all equalizers.
    class (Category c m o, Morphism m o) => HasEqualizers c m o | c -> m, m -> o where
        -- | Given a 'parallelDiagram' selecting arrows, return the equalizer of the selected arrows as a 'Cone'.  
        equalize :: Diagram Parallel ParallelAr ParallelOb c m o -> Cone Parallel ParallelAr ParallelOb c m o
        
    -- | The typeclass of categories which have all limits. cLim is the type of the new category in which we can compute limits and their projections. cIndex is the type of the indexing category of the diagrams.
    class (Category c m o, Morphism m o,
           Category cLim mLim oLim, Morphism mLim oLim) =>
           CompleteCategory c m o cLim mLim oLim cIndex mIndex oIndex | c -> m, m -> o, cLim -> mLim, mLim -> oLim, c cIndex mIndex oIndex -> cLim where
        
        -- | Return the limit of a 'Diagram'.
        limit :: (FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq cIndex, Eq mIndex, Eq oIndex) => Diagram cIndex mIndex oIndex c m o -> Cone cIndex mIndex oIndex cLim mLim oLim
        
        -- | A partial 'Diagram' to project objects and morphisms of a base like a call of 'limit' would do.
        --
        -- (coneBase (limit diag)) should equal ((projectBase diag) <-@<- (diag))
        projectBase :: Diagram cIndex mIndex oIndex c m o -> Diagram c m o cLim mLim oLim
       

    -- | A partial 'Diagram' to unproject object and morphism of the base in a 'limit' cone.
    --
    -- unprojectBase and projectBase returned 'Diagram's are inverses.
    unprojectBase :: (CompleteCategory c m o cLim mLim oLim cIndex mIndex oIndex) => Diagram cIndex mIndex oIndex c m o -> Diagram cLim mLim oLim c m o
    unprojectBase = unsafeInverseDiagram.projectBase

    -- | Computes efficiently limits thanks to products and equalizers. Can be used to instantiate 'CompleteCategory'.
    --
    -- The first argument is a function to transform an object of the original category into a limit object.
    --
    -- Most of the time, the original category takes one type parameter and the function uses 'Projection', when the category does not take any type parameter it is 'id'. 
    --
    -- For example, for 'FinSet', the function has to transform a function {1 -> 2} to the function {Projection 1 -> Projection 2}.
    limitFromProductsAndEqualizers :: 
       (Category c m o, Morphism m o,
        Category cLim mLim oLim, Morphism mLim oLim, Eq cLim, Eq mLim, Eq oLim, HasProducts c m o cLim mLim oLim oIndex,HasEqualizers cLim mLim oLim,
        FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq oIndex, Eq mIndex, Eq cIndex) => 
        (m -> mLim) -> Diagram cIndex mIndex oIndex c m o -> Cone cIndex mIndex oIndex cLim mLim oLim
    limitFromProductsAndEqualizers transformMorphismIntoLimMorphism diag = lim
            where
                idxCat = src diag
                discreteDiag = completeDiagram Diagram{src = discreteCategory topObjects, tgt = tgt diag, omap = weakMapFromSet [(o,diag ->$ o) | o <- topObjects], mmap = weakMap[]}
                topObjects = Set.filter (\o -> Set.and [not $ Set.null $ ar idxCat o (source m) | m <- arTo idxCat o]) (ob idxCat)
                objectToAMorphismFromATopObject o
                    | o `Set.elem` topObjects = identity idxCat o
                    | otherwise = anElement [m | m <- arTo idxCat o, source m `Set.elem` topObjects]
                prod = Math.CompleteCategory.product discreteDiag
                newDiag = (completeDiagram Diagram{src = src diag, tgt = (tgt (baseCone prod)), omap = weakMap [], mmap = transformMorphismIntoLimMorphism <$> mmap diag})
                undiscrete = unsafeCone (apex prod) (unsafeNaturalTransformation (constantDiagram (src diag) (tgt (baseCone prod)) (apex prod)) newDiag (weakMapFromSet [(o,(newDiag ->£ (objectToAMorphismFromATopObject o)) @ ((legsCone prod) =>$ (source $ objectToAMorphismFromATopObject o))) | o <- (ob.src $ diag)]))
                equalizeFromMorph fIndex currLim = unsafeCone (apex eq) ((legsCone currLim) @ (diagonal (legsCone eq =>$ ParallelA)))
                    where
                        f = diag ->£ fIndex
                        eq = equalize $ completeDiagram Diagram{src = Parallel, tgt = tgt (baseCone currLim), omap = weakMap [], mmap = weakMap [(ParallelF, (legsCone currLim) =>$ (target fIndex)),(ParallelG, (transformMorphismIntoLimMorphism f) @ ((legsCone currLim) =>$ (source fIndex)))]}
                        diagonal m = unsafeNaturalTransformation (constantDiagram (src diag) (tgt (baseCone undiscrete)) (source m)) (constantDiagram (src diag) (tgt (baseCone undiscrete)) (target m)) (memorizeFunction (const m) (ob (src diag)))
                lim = Set.foldr equalizeFromMorph undiscrete ((set.setToList) (genArrowsWithoutId (src diag)))