{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, MonadComprehensions  #-}

{-| Module  : FiniteCategories
Description : __'FinCat'__ is the category of finite categories, 'FinFunctor's are the morphisms of __'FinCat'__.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The __FinCat__ category has as objects finite categories and as morphisms homogeneous functors between them.

Functors must be homogeneous because otherwise we would not be able to compose them with the 'Morphism' typeclass.

The 'FinCat' datatype should not be confused with the `FiniteCategory` typeclass. The `FiniteCategory` typeclass describes axioms a structure should follow to be considered a finite category. The 'FinCat' type is itself a 'Category'.

A 'FinFunctor' is a 'Diagram' where the source and target category are the same. The source category of a 'FinFunctor' should be finite.
-}

module Math.Categories.FinCat
(
    -- * Homogeneous functor
    FinFunctor(..),
    -- * __FinCat__
    FinCat(..)
)
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              Math.Category
    import              Math.FiniteCategory
    import              Math.Categories.FunctorCategory
    import              Math.IO.PrettyPrint
    
    -- | A `FinFunctor` /funct/ between two categories is a map between objects and a map between arrows of the two categories such that :
    --
    -- prop> funct ->$ (source f) == source (funct ->£ f)
    -- prop> funct ->$ (target f) == target (funct ->£ f)
    -- prop> funct ->£ (f @ g) = (funct ->£ f) @ (funct ->£ g)
    -- prop> funct ->£ (identity a) = identity (funct ->$ a)
    --
    -- A 'FinFunctor' is a type of 'Diagram'.
    --
    -- It is meant to be a morphism between categories within __`FinCat`__, it is homogeneous, the type of the source category must be the same as the type of the target category.
    --
    -- See 'Diagram' in Math.Categories.FunctorCategory for heterogeneous ones.
    type FinFunctor c m o = Diagram c m o c m o
    
    instance (Eq c, Eq m, Eq o) => Morphism (Diagram c m o c m o) c where
        (@?) Diagram{src=s2,tgt=t2,omap=om2,mmap=fm2} Diagram{src=s1,tgt=t1,omap=om1,mmap=fm1}
            | t1 /= s2 = Nothing
            | otherwise = Just Diagram{src=s1,tgt=t2,omap=om2|.|om1,mmap=fm2|.|fm1}
        source = src
        target = tgt
          
    -- | The __'FinCat'__ category has as objects finite categories and as morphisms homogeneous functors between them.
    data FinCat c m o = FinCat deriving (Eq, Show)
    
    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => Category (FinCat c m o) (Diagram c m o c m o) c where
        identity _ cat = Diagram{src=cat,tgt=cat,omap=memorizeFunction id (ob cat),mmap=memorizeFunction id (arrows cat)}
        ar _ s t = snd.(Set.catEither) $ [diagram s t appO appF | appO <- appObj, appF <- ((fmap $ (Map.unions)).cartesianProductOfSets) [twoObjToMaps a b appO| a <- (setToList $ ob s), b <- (setToList $ ob s)]]
            where
                appObj = Map.enumerateMaps (ob s) (ob t)
                twoObjToMaps a b appO = Map.enumerateMaps (ar s a b) (ar t (appO |!| a) (appO |!| b))