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

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

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

A 'Category' might have coproducts meaning that any 'discreteDiagram' on it has a colimit.

A 'Category' might have coequalizers meaning that any 'parallelDiagram' on it has a colimit.

If a 'Category' have both coproducts and coequalizers, it is cocomplete meaning that it has all small colimits.

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

module Math.CocompleteCategory
(
    -- * Colimit type
    Colimit(..),
    uncoproject,
    -- * Helper typeclasses to define a 'CocompleteCategory'
    HasCoproducts(..),
    HasCoequalizers(..),
    colimitFromCoproductsAndCoequalizers,
    -- * Cocomplete Category
    CocompleteCategory(..),
    uncoprojectBase,
)
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 colimit of a diagram indexed by a category parametrized over a type i will contain 'Coproduct' constructions. A given distinguished element can be constructed from a 'Coprojection' 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 nadir of the colimit is obviously {('A',1),('A',2),('B',3),('B',4)}, note that it is not an object of ('Finset' Int) but an object of ('FinSet' (DiscreteTwoOb,Int)). The 'Colimit' type allows to construct type ('FinSet' ('Colimit' 'DiscreteTwo' Int)) in which we can consider the original objects with 'Coprojection' and the new distinguished elements with 'Coproduct'. Thus, the colimit will be {Coproduct 'A' 1,Coproduct 'A' 2,Coproduct 'B' 3,Coproduct 'B' 4}. We can construct coprojections in the same category, for example along 'A', which will map ('Coprojection' 1) to 'Coproduct' 'A' 1.
    data Colimit i t = Coprojection t -- ^ A 'Coprojection' is the parameter type of the original category to coproject them to the colimit.
                     | CoproductElement i t  -- ^ A 'CoproductElement' is a couple containing an indexing object and an object of type t.
                     deriving (Eq, Show, Generic, Simplifiable)
                   
    instance (PrettyPrint i, PrettyPrint t, Eq i) => PrettyPrint (Colimit i t) where
        pprint v (Coprojection x) = pprint v x
        pprint v (CoproductElement idx x) = pprint v x ++ "_" ++ pprint v idx
        
        pprintWithIndentations cv ov indent (Coprojection x) = indentation (ov - cv) indent ++ pprint cv x ++ "\n"
        pprintWithIndentations cv ov indent (CoproductElement idx x) = indentation (ov - cv) indent ++ pprint cv x ++ "_" ++ pprint cv idx ++ "\n"
    
    -- | Remove the constructor 'Coprojection' from an original object t, throws an error if a 'CoproductElement' is given.
    uncoproject :: Colimit oIndex t -> t
    uncoproject (Coprojection t) = t
    uncoproject (CoproductElement _ _) = error "Uncoproject a coproduct element."
    
    -- | The typeclass of categories which have all coproducts.
    class (Category c m o, Morphism m o,
           Category cLim mLim oLim, Morphism mLim oLim) =>
           HasCoproducts 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 coproduct of the selected objects as a 'Cocone'.
        coproduct :: Diagram (DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex c m o  -> Cocone(DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex cLim mLim oLim
        
    -- | The typeclass of categories which have all coequalizers.
    class (Category c m o, Morphism m o) => HasCoequalizers c m o | c -> m, m -> o where
        -- | Given a 'parallelDiagram' selecting arrows, return the coequalizer of the selected arrows as a 'Cocone'.  
        coequalize :: Diagram Parallel ParallelAr ParallelOb c m o -> Cocone Parallel ParallelAr ParallelOb c m o
        
    -- | The typeclass of categories which have all colimits.
    class (Category c m o, Morphism m o,
           Category cLim mLim oLim, Morphism mLim oLim) =>
           CocompleteCategory 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 colimit of a 'Diagram'.
        colimit :: (FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq cIndex, Eq mIndex, Eq oIndex) => Diagram cIndex mIndex oIndex c m o -> Cocone cIndex mIndex oIndex cLim mLim oLim
        
        -- | A partial 'Diagram' to coproject objects and morphisms of a base like a call of 'colimit' would do.
        --
        -- (coconeBase (colimit diag)) should equal ((coprojectBase diag) <-@<- diag)
        coprojectBase :: Diagram cIndex mIndex oIndex c m o -> Diagram c m o cLim mLim oLim
       

    -- | A partial 'Diagram' to uncoproject objects and morphisms of the base in a 'colimit' cocone.
    --
    -- uncoprojectBase and coprojectBase returned 'Diagram's are inverses.
    uncoprojectBase :: (CocompleteCategory c m o cLim mLim oLim cIndex mIndex oIndex) => Diagram cIndex mIndex oIndex c m o -> Diagram cLim mLim oLim c m o
    uncoprojectBase = unsafeInverseDiagram.coprojectBase
        
    
    -- | Computes efficiently colimits thanks to coproducts and coequalizers. Can be used to instantiate 'CocompleteCategory'.
    --
    -- The first argument is a function to transform an object of the original category into a colimit object.
    --
    -- Most of the time, the original category takes one type parameter and the function uses 'Coprojection', 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 {Coprojection 1 -> Coprojection 2}.
    colimitFromCoproductsAndCoequalizers ::
      (Category c m o, Morphism m o,
       Category cLim mLim oLim, Morphism mLim oLim, HasCoproducts c m o cLim mLim oLim oIndex,HasCoequalizers 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 -> Cocone cIndex mIndex oIndex cLim mLim oLim
    colimitFromCoproductsAndCoequalizers transformMorphismIntoColimMorphism diag = colim
            where
                idxCat = src diag
                discreteDiag = completeDiagram Diagram{src = discreteCategory bottomObjects, tgt = tgt diag, omap = weakMapFromSet [(o,diag ->$ o) | o <- bottomObjects], mmap = weakMap []}
                bottomObjects = Set.filter (\o -> Set.and [not $ Set.null $ ar idxCat (target m) o | m <- arFrom idxCat o]) (ob idxCat)
                objectToAMorphismToABottomObject o
                    | o `Set.elem` bottomObjects = identity idxCat o
                    | otherwise = anElement [m | m <- arFrom idxCat o, target m `Set.elem` bottomObjects]
                coprod = coproduct discreteDiag
                newDiag = (completeDiagram Diagram{src = src diag, tgt = (tgt (baseCocone coprod)), omap = weakMap [], mmap = transformMorphismIntoColimMorphism <$> mmap diag})
                undiscrete = unsafeCocone (nadir coprod) (unsafeNaturalTransformation newDiag (constantDiagram (src diag) (tgt (baseCocone coprod)) (nadir coprod)) (weakMapFromSet [(o,((legsCocone coprod) =>$ (target $ objectToAMorphismToABottomObject o)) @ (newDiag ->£ (objectToAMorphismToABottomObject o))) | o <- (ob.src $ diag)]))
                coequalizeFromMorph fIndex currColim = unsafeCocone (nadir coeq) ((diagonal (legsCocone coeq =>$ ParallelB)) @ (legsCocone currColim))
                    where
                        f = diag ->£ fIndex
                        coeq = coequalize $ completeDiagram Diagram{src = Parallel, tgt = tgt (baseCocone currColim), omap = weakMap [], mmap = weakMap [(ParallelF, (legsCocone currColim) =>$ (source fIndex)),(ParallelG, ((legsCocone currColim) =>$ (target fIndex)) @ (transformMorphismIntoColimMorphism f))]}
                        diagonal m = unsafeNaturalTransformation (constantDiagram (src diag) (tgt (baseCocone undiscrete)) (source m)) (constantDiagram (src diag) (tgt (baseCocone undiscrete)) (target m)) (memorizeFunction (const m) (ob (src diag)))
                colim = Set.foldr coequalizeFromMorph undiscrete ((set.setToList) (genArrowsWithoutId idxCat))