{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses  #-}

{-| Module  : FiniteCategories
Description : __FinCat__ is the category of finite categories, functors are the morphisms of __FinCat__.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The __FinCat__ category has as objects finite categories and as morphisms functors between them.
It is itself a large category (therefore not a finite one),
we only construct finite full subcategories of the mathematical infinite __FinCat__ category.
`FinCat` is the type of full finite subcategories of __FinCat__.

To instantiate it, use the `FinCat` constructor on a list of categories.

For example, see ExampleCat.ExampleCat

The `FinCat` type 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 `FiniteCategory` and contains finite categories as objects.

To convert a `FinFunctor` into any other kind of functor, see @Diagram.Conversion@.
-}

module Cat.FinCat
(
    FinFunctor(..),
    FinCat(..)
)
where
    import FiniteCategory.FiniteCategory
    import Utils.EnumerateMaps
    import Utils.CartesianProduct
    import IO.PrettyPrint
    import IO.Show
    import Utils.AssociationList
    
    -- | A `FinFunctor` /F/ between two categories is a map between objects and a map between arrows of the two categories such that :

    --

    -- prop> F (srcF f) = srcF (F f) 

    -- prop> F (tgtF f) = tgtF (F f)

    -- prop> F (f @ g) = F(f) @ F(g)

    -- prop> F (identity a) = identity (F a)

    --

    -- 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/ for heterogeneous ones.

    --

    -- To convert a `FinFunctor` into any other kind of functor, see @Diagram.Conversion@.

    data FinFunctor c m o = FinFunctor {forall c m o. FinFunctor c m o -> c
srcF :: c, forall c m o. FinFunctor c m o -> c
tgtF :: c, forall c m o. FinFunctor c m o -> AssociationList o o
omapF :: AssociationList o o, forall c m o. FinFunctor c m o -> AssociationList m m
mmapF :: AssociationList m m} deriving (FinFunctor c m o -> FinFunctor c m o -> Bool
(FinFunctor c m o -> FinFunctor c m o -> Bool)
-> (FinFunctor c m o -> FinFunctor c m o -> Bool)
-> Eq (FinFunctor c m o)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c m o.
(Eq c, Eq o, Eq m) =>
FinFunctor c m o -> FinFunctor c m o -> Bool
/= :: FinFunctor c m o -> FinFunctor c m o -> Bool
$c/= :: forall c m o.
(Eq c, Eq o, Eq m) =>
FinFunctor c m o -> FinFunctor c m o -> Bool
== :: FinFunctor c m o -> FinFunctor c m o -> Bool
$c== :: forall c m o.
(Eq c, Eq o, Eq m) =>
FinFunctor c m o -> FinFunctor c m o -> Bool
Eq, Int -> FinFunctor c m o -> ShowS
[FinFunctor c m o] -> ShowS
FinFunctor c m o -> String
(Int -> FinFunctor c m o -> ShowS)
-> (FinFunctor c m o -> String)
-> ([FinFunctor c m o] -> ShowS)
-> Show (FinFunctor c m o)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c m o.
(Show c, Show o, Show m) =>
Int -> FinFunctor c m o -> ShowS
forall c m o.
(Show c, Show o, Show m) =>
[FinFunctor c m o] -> ShowS
forall c m o.
(Show c, Show o, Show m) =>
FinFunctor c m o -> String
showList :: [FinFunctor c m o] -> ShowS
$cshowList :: forall c m o.
(Show c, Show o, Show m) =>
[FinFunctor c m o] -> ShowS
show :: FinFunctor c m o -> String
$cshow :: forall c m o.
(Show c, Show o, Show m) =>
FinFunctor c m o -> String
showsPrec :: Int -> FinFunctor c m o -> ShowS
$cshowsPrec :: forall c m o.
(Show c, Show o, Show m) =>
Int -> FinFunctor c m o -> ShowS
Show)
    
    instance (Eq c, Eq m, Eq o) => Morphism (FinFunctor c m o) c where
        @ :: FinFunctor c m o -> FinFunctor c m o -> FinFunctor c m o
(@) FinFunctor{srcF :: forall c m o. FinFunctor c m o -> c
srcF=c
s2,tgtF :: forall c m o. FinFunctor c m o -> c
tgtF=c
t2,omapF :: forall c m o. FinFunctor c m o -> AssociationList o o
omapF=AssociationList o o
om2,mmapF :: forall c m o. FinFunctor c m o -> AssociationList m m
mmapF=AssociationList m m
fm2} FinFunctor{srcF :: forall c m o. FinFunctor c m o -> c
srcF=c
s1,tgtF :: forall c m o. FinFunctor c m o -> c
tgtF=c
t1,omapF :: forall c m o. FinFunctor c m o -> AssociationList o o
omapF=AssociationList o o
om1,mmapF :: forall c m o. FinFunctor c m o -> AssociationList m m
mmapF=AssociationList m m
fm1}
            | c
t1 c -> c -> Bool
forall a. Eq a => a -> a -> Bool
/= c
s2 = String -> FinFunctor c m o
forall a. HasCallStack => String -> a
error String
"Illegal composition of FinFunctors."
            | Bool
otherwise = FinFunctor :: forall c m o.
c
-> c
-> AssociationList o o
-> AssociationList m m
-> FinFunctor c m o
FinFunctor{srcF :: c
srcF=c
s1,tgtF :: c
tgtF=c
t2,omapF :: AssociationList o o
omapF=AssociationList o o
om2AssociationList o o -> AssociationList o o -> AssociationList o o
forall a b c.
(Eq a, Eq b) =>
AssociationList b c -> AssociationList a b -> AssociationList a c
!-.AssociationList o o
om1,mmapF :: AssociationList m m
mmapF=AssociationList m m
fm2AssociationList m m -> AssociationList m m -> AssociationList m m
forall a b c.
(Eq a, Eq b) =>
AssociationList b c -> AssociationList a b -> AssociationList a c
!-.AssociationList m m
fm1}
        source :: FinFunctor c m o -> c
source = FinFunctor c m o -> c
forall c m o. FinFunctor c m o -> c
srcF
        target :: FinFunctor c m o -> c
target = FinFunctor c m o -> c
forall c m o. FinFunctor c m o -> c
tgtF
                    
    instance (FiniteCategory c m o, Morphism m o, PrettyPrintable c, PrettyPrintable m, PrettyPrintable o, Eq m, Eq o) =>
              PrettyPrintable (FinFunctor c m o) where
        pprint :: FinFunctor c m o -> String
pprint FinFunctor{srcF :: forall c m o. FinFunctor c m o -> c
srcF=c
s,tgtF :: forall c m o. FinFunctor c m o -> c
tgtF=c
t,omapF :: forall c m o. FinFunctor c m o -> AssociationList o o
omapF=AssociationList o o
om,mmapF :: forall c m o. FinFunctor c m o -> AssociationList m m
mmapF=AssociationList m m
fm} = String
"FinFunctor ("String -> ShowS
forall a. [a] -> [a] -> [a]
++c -> String
forall a. PrettyPrintable a => a -> String
pprint c
sString -> ShowS
forall a. [a] -> [a] -> [a]
++String
") -> ("String -> ShowS
forall a. [a] -> [a] -> [a]
++c -> String
forall a. PrettyPrintable a => a -> String
pprint c
tString -> ShowS
forall a. [a] -> [a] -> [a]
++String
")\n"String -> ShowS
forall a. [a] -> [a] -> [a]
++AssociationList o o -> String
forall a. PrettyPrintable a => a -> String
pprint AssociationList o o
omString -> ShowS
forall a. [a] -> [a] -> [a]
++String
"\n"String -> ShowS
forall a. [a] -> [a] -> [a]
++AssociationList m m -> String
forall a. PrettyPrintable a => a -> String
pprint AssociationList m m
fm
        
    -- | Checks wether the properties of a FinFunctor are respected.

    checkFinFunctoriality :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => FinFunctor c m o -> Bool
    checkFinFunctoriality :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
FinFunctor c m o -> Bool
checkFinFunctoriality FinFunctor {srcF :: forall c m o. FinFunctor c m o -> c
srcF=c
s,tgtF :: forall c m o. FinFunctor c m o -> c
tgtF=c
t,omapF :: forall c m o. FinFunctor c m o -> AssociationList o o
omapF=AssociationList o o
om,mmapF :: forall c m o. FinFunctor c m o -> AssociationList m m
mmapF=AssociationList m m
fm}
        | Bool -> Bool
not ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
imIdNotId) = Bool
False
        | Bool -> Bool
not ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
errFunct) = Bool
False
        | Bool
otherwise = Bool
True
        where
            imIdNotId :: [Bool]
imIdNotId = [AssociationList m m
fm AssociationList m m -> m -> m
forall a b. Eq a => AssociationList a b -> a -> b
!-! (c -> o -> m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c
s o
a) m -> m -> Bool
forall a. Eq a => a -> a -> Bool
== c -> o -> m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c
t (AssociationList o o
om AssociationList o o -> o -> o
forall a b. Eq a => AssociationList a b -> a -> b
!-! o
a) | o
a <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
s]
            errFunct :: [Bool]
errFunct = [AssociationList m m
fm AssociationList m m -> m -> m
forall a b. Eq a => AssociationList a b -> a -> b
!-! (m
g m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
f) m -> m -> Bool
forall a. Eq a => a -> a -> Bool
== (AssociationList m m
fm AssociationList m m -> m -> m
forall a b. Eq a => AssociationList a b -> a -> b
!-! m
g) m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ (AssociationList m m
fm AssociationList m m -> m -> m
forall a b. Eq a => AssociationList a b -> a -> b
!-! m
f) | m
f <- (c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c
s), m
g <- (c -> o -> [m]
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> [m]
arFrom c
s (m -> o
forall m o. Morphism m o => m -> o
target m
f))]
        
    -- | An instance of `FinCat` is a list of categories of interest.

    --

    -- Listing all arrows between two objects (i.e. listing FinFunctors between two categories) is slow (there are a lot of candidates).

    newtype FinCat c m o = FinCat [c]
    
    -- We are forced to use the language extension FlexibleInstances because of this instance declaration :

    -- The category 'c' could be itself a `FinCat` category therefore not respecting the uniqueness rule of instanciation.

    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => FiniteCategory (FinCat c m o) (FinFunctor c m o) c where
        ob :: FinCat c m o -> [c]
ob (FinCat [c]
xs) = [c]
xs
        identity :: Morphism (FinFunctor c m o) c =>
FinCat c m o -> c -> FinFunctor c m o
identity FinCat c m o
finCat c
catObj = FinFunctor :: forall c m o.
c
-> c
-> AssociationList o o
-> AssociationList m m
-> FinFunctor c m o
FinFunctor {srcF :: c
srcF=c
catObj,tgtF :: c
tgtF=c
catObj,omapF :: AssociationList o o
omapF=(o -> o) -> [o] -> AssociationList o o
forall a b. (a -> b) -> [a] -> AssociationList a b
functToAssocList o -> o
forall a. a -> a
id (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
catObj),mmapF :: AssociationList m m
mmapF=(m -> m) -> [m] -> AssociationList m m
forall a b. (a -> b) -> [a] -> AssociationList a b
functToAssocList m -> m
forall a. a -> a
id (c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c
catObj)}
        ar :: Morphism (FinFunctor c m o) c =>
FinCat c m o -> c -> c -> [FinFunctor c m o]
ar FinCat c m o
finCat c
cat1 c
cat2 = [FinFunctor :: forall c m o.
c
-> c
-> AssociationList o o
-> AssociationList m m
-> FinFunctor c m o
FinFunctor{srcF :: c
srcF=c
cat1,tgtF :: c
tgtF=c
cat2,mmapF :: AssociationList m m
mmapF=AssociationList m m
appF, omapF :: AssociationList o o
omapF=AssociationList o o
appO} | AssociationList o o
appO <- [AssociationList o o]
appObj, AssociationList m m
appF <- [AssociationList m m] -> AssociationList m m
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([AssociationList m m] -> AssociationList m m)
-> [[AssociationList m m]] -> [AssociationList m m]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[AssociationList m m]] -> [[AssociationList m m]]
forall a. [[a]] -> [[a]]
cartesianProduct [o -> o -> AssociationList o o -> [AssociationList m m]
forall {b} {a}.
(FiniteCategory c b a, Morphism b a, Eq a) =>
a -> a -> AssociationList a a -> [AssociationList b b]
twoObjToMaps o
a o
b AssociationList o o
appO| o
a <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
cat1, o
b <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
cat1], FinFunctor c m o -> Bool
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
FinFunctor c m o -> Bool
checkFinFunctoriality FinFunctor :: forall c m o.
c
-> c
-> AssociationList o o
-> AssociationList m m
-> FinFunctor c m o
FinFunctor{srcF :: c
srcF=c
cat1,tgtF :: c
tgtF=c
cat2,mmapF :: AssociationList m m
mmapF=AssociationList m m
appF, omapF :: AssociationList o o
omapF=AssociationList o o
appO}]
            where
                appObj :: [AssociationList o o]
appObj = [o] -> [o] -> [AssociationList o o]
forall a b. [a] -> [b] -> [AssociationList a b]
enumMaps (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
cat1) (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
cat2)
                twoObjToMaps :: a -> a -> AssociationList a a -> [AssociationList b b]
twoObjToMaps a
a a
b AssociationList a a
appO = [b] -> [b] -> [AssociationList b b]
forall a b. [a] -> [b] -> [AssociationList a b]
enumMaps (c -> a -> a -> [b]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
cat1 a
a a
b) (c -> a -> a -> [b]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
cat2 (AssociationList a a
appO AssociationList a a -> a -> a
forall a b. Eq a => AssociationList a b -> a -> b
!-! a
a) (AssociationList a a
appO AssociationList a a -> a -> a
forall a b. Eq a => AssociationList a b -> a -> b
!-! a
b))
                    
    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => GeneratedFiniteCategory (FinCat c m o) (FinFunctor c m o) c where
        genAr :: Morphism (FinFunctor c m o) c =>
FinCat c m o -> c -> c -> [FinFunctor c m o]
genAr = FinCat c m o -> c -> c -> [FinFunctor c m o]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
defaultGenAr
        decompose :: Morphism (FinFunctor c m o) c =>
FinCat c m o -> FinFunctor c m o -> [FinFunctor c m o]
decompose = FinCat c m o -> FinFunctor c m o -> [FinFunctor c m o]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> m -> [m]
defaultDecompose