{-# 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 :: forall m o. Morphism m o => [m] -> m
compose [m]
l = (m -> m -> m) -> [m] -> m
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 m -> m -> m
forall m o. Morphism m o => m -> m -> m
(@) [m]
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
c = [[m]] -> [m]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
c o
s o
t | o
s <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c, o
t <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
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 :: forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> [m]
arTo c
c o
t = [[m]] -> [m]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
c o
s o
t | o
s <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c]

    -- | `arTo2` same as `arTo` but for multiple targets.

    arTo2 :: (FiniteCategory c m o, Morphism m o) => c -> [o] -> [m]
    arTo2 :: forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> [o] -> [m]
arTo2 c
c [o]
ts = [[m]] -> [m]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
c o
s o
t | o
s <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c, o
t <- [o]
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 :: forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> [m]
arFrom c
c o
s = [[m]] -> [m]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
c o
s o
t | o
t <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c]

    -- | `arFrom2` same as `arFrom` but for multiple sources.

    arFrom2 :: (FiniteCategory c m o, Morphism m o) => c -> [o] -> [m]
    arFrom2 :: forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> [o] -> [m]
arFrom2 c
c [o]
ss = [[m]] -> [m]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
c o
s o
t | o
t <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c, o
s <- [o]
ss]

    -- | `identities` returns all the identities of a category.

    identities :: (FiniteCategory c m o, Morphism m o) => c -> [m]
    identities :: forall c m o. (FiniteCategory c m o, Morphism m o) => c -> [m]
identities c
c = c -> o -> m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c
c (o -> m) -> [o] -> [m]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
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 :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isIdentity c
c m
m = c -> o -> m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c
c (m -> o
forall m o. Morphism m o => m -> o
source m
m) m -> m -> Bool
forall a. Eq a => a -> a -> Bool
== 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 :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity c
c m
m = Bool -> Bool
not (c -> m -> Bool
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isIdentity c
c m
m)

    -- | Returns wether an object is initial in the category.

    isInitial :: (FiniteCategory c m o, Morphism m o) => c -> o -> Bool
    isInitial :: forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Bool
isInitial c
cat o
obj = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [(Bool -> Bool
not(Bool -> Bool) -> ([m] -> Bool) -> [m] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[m] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([m] -> Bool) -> [m] -> Bool
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
cat o
obj o
t) Bool -> Bool -> Bool
&& ([m] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([m] -> Bool) -> [m] -> Bool
forall a b. (a -> b) -> a -> b
$ [m] -> [m]
forall a. [a] -> [a]
tail (c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
cat o
obj o
t)) | o
t <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
cat]
    
    -- | Returns the list of intial objects in a category.

    initialObjects :: (FiniteCategory c m o, Morphism m o) => c -> [o]
    initialObjects :: forall c m o. (FiniteCategory c m o, Morphism m o) => c -> [o]
initialObjects c
cat = (o -> Bool) -> [o] -> [o]
forall a. (a -> Bool) -> [a] -> [a]
filter (c -> o -> Bool
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Bool
isInitial c
cat) (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
cat)
    
    -- | Returns wether an object is terminal in the category.

    isTerminal :: (FiniteCategory c m o, Morphism m o) => c -> o -> Bool
    isTerminal :: forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Bool
isTerminal c
cat o
obj = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [(Bool -> Bool
not(Bool -> Bool) -> ([m] -> Bool) -> [m] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[m] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([m] -> Bool) -> [m] -> Bool
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
cat o
s o
obj) Bool -> Bool -> Bool
&& ([m] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([m] -> Bool) -> [m] -> Bool
forall a b. (a -> b) -> a -> b
$ [m] -> [m]
forall a. [a] -> [a]
tail (c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
cat o
s o
obj)) | o
s <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
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 :: forall c m o. (FiniteCategory c m o, Morphism m o) => c -> [o]
terminalObjects c
cat = (o -> Bool) -> [o] -> [o]
forall a. (a -> Bool) -> [a] -> [a]
filter (c -> o -> Bool
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Bool
isTerminal c
cat) (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
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
c = [[m]] -> [m]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [c -> o -> o -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
genAr c
c o
s o
t | o
s <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c, o
t <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
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 :: forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> [m]
genArTo c
c o
t = [[m]] -> [m]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [c -> o -> o -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
genAr c
c o
s o
t | o
s <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
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 :: forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> [o] -> [m]
genArTo2 c
c [o]
ts = [[m]] -> [m]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [c -> o -> o -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
genAr c
c o
s o
t | o
s <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c, o
t <- [o]
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 :: forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> [m]
genArFrom c
c o
s = [[m]] -> [m]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [c -> o -> o -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
genAr c
c o
s o
t | o
t <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
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 :: forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> [o] -> [m]
genArFrom2 c
c [o]
ss = [[m]] -> [m]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [c -> o -> o -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
genAr c
c o
s o
t | o
t <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c, o
s <- [o]
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 :: forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
defaultGenAr = c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
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 :: forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> m -> [m]
defaultDecompose c
_ m
m = (m
mm -> [m] -> [m]
forall a. a -> [a] -> [a]
:[])
    
    -- | Helper function for `bruteForceDecompose`.

    bruteForce :: (GeneratedFiniteCategory c m o, Morphism m o, Eq m) => c -> m -> [[m]] -> [m]
    bruteForce :: forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o, Eq m) =>
c -> m -> [[m]] -> [m]
bruteForce c
c m
m [[m]]
l = if Maybe Int
index Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Int
forall a. Maybe a
Nothing then c -> m -> [[m]] -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o, Eq m) =>
c -> m -> [[m]] -> [m]
bruteForce c
c m
m ([[[m]]] -> [[m]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([m] -> [[m]]
forall {a} {o}.
(GeneratedFiniteCategory c a o, Morphism a o) =>
[a] -> [[a]]
pathToAugmentedPaths ([m] -> [[m]]) -> [[m]] -> [[[m]]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[m]]
l)) else [[m]]
l [[m]] -> Int -> [m]
forall a. [a] -> Int -> a
!! (Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust Maybe Int
index) where
        index :: Maybe Int
index = m -> [m] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex m
m ([m] -> m
forall m o. Morphism m o => [m] -> m
compose ([m] -> m) -> [[m]] -> [m]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[m]]
l)
        leavingMorph :: [b] -> [m]
leavingMorph [b]
path = (c -> o -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> [m]
genArFrom c
c) (o -> [m]) -> o -> [m]
forall a b. (a -> b) -> a -> b
$ b -> o
forall m o. Morphism m o => m -> o
target(b -> o) -> ([b] -> b) -> [b] -> o
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[b] -> b
forall a. [a] -> a
head ([b] -> o) -> [b] -> o
forall a b. (a -> b) -> a -> b
$ [b]
path
        pathToAugmentedPaths :: [a] -> [[a]]
pathToAugmentedPaths [a]
path = ([a] -> [a]
forall {m} {o} {b}.
(GeneratedFiniteCategory c m o, Morphism m o, Morphism b o) =>
[b] -> [m]
leavingMorph [a]
path) [a] -> (a -> [[a]]) -> [[a]]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\a
x -> [(a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
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 :: forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o, Eq m) =>
c -> m -> [m]
bruteForceDecompose c
c m
m = c -> m -> [[m]] -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o, Eq m) =>
c -> m -> [[m]] -> [m]
bruteForce c
c m
m ((m -> [m] -> [m]
forall a. a -> [a] -> [a]
:[]) (m -> [m]) -> [m] -> [[m]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> o -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> [m]
genArFrom c
c (m -> o
forall m o. Morphism m o => m -> o
source m
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 :: forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o, Eq m) =>
c -> m -> Bool
isGenerator c
c m
f = m -> [m] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem m
f (c -> o -> o -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
genAr c
c (m -> o
forall m o. Morphism m o => m -> o
source m
f) (m -> o
forall m o. Morphism m o => m -> o
target m
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 :: forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o, Eq m) =>
c -> m -> Bool
isComposite c
c m
f = Bool -> Bool
not (c -> m -> Bool
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o, Eq m) =>
c -> m -> Bool
isGenerator c
c m
f)

    -- | A data type to represent an incoherence inside a category.

    data FiniteCategoryError m o =
                         CompositionNotAssociative {forall m o. FiniteCategoryError m o -> m
f :: m, forall m o. FiniteCategoryError m o -> m
g :: m, forall m o. FiniteCategoryError m o -> m
h :: m, forall m o. FiniteCategoryError m o -> m
fg_h :: m, forall m o. FiniteCategoryError m o -> m
f_gh :: m} -- ^ @(h\@g)\@f /= h\@(g\@f)@

                       | ObjectsNotUnique {forall m o. FiniteCategoryError m o -> o
dupObj :: o} -- ^ `dupObj` was found multiple times in @ob c@.

                       | MorphismsNotUnique {forall m o. FiniteCategoryError m o -> m
dupMorph :: m} -- ^ `dupMorph` was found multiple times in the category.

                       | ArrowsNotExhaustive {forall m o. FiniteCategoryError m o -> m
missingAr :: m} -- ^ `missingAr` is an arrow found by calling @ar c@ but is not in @arrows c@.

                       | ArrowBetweenUnknownObjects {f :: m, forall m o. FiniteCategoryError m o -> o
s :: o, forall m o. FiniteCategoryError m o -> o
t :: o} -- ^ `f` was found in the category but its source `s` or target `t` is not in @ob c@. 

                       | WrongSource {f :: m, forall m o. FiniteCategoryError m o -> o
realSource :: o} -- ^ `f` was found by using @ar c s t@ where @s /= source f@.

                       | WrongTarget {f :: m, forall m o. FiniteCategoryError m o -> o
realTarget :: o} -- ^ `f` was found by using @ar c s t@ where @t /= target f@.

                       | IdentityNotLeftNeutral {forall m o. FiniteCategoryError m o -> m
idL :: m, f :: m, forall m o. FiniteCategoryError m o -> m
foidL :: m} -- ^ `idL` is not a valid identity : @f \@ idL /= f@.

                       | IdentityNotRightNeutral {f :: m, forall m o. FiniteCategoryError m o -> m
idR :: m, forall m o. FiniteCategoryError m o -> 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, forall m o. FiniteCategoryError m o -> [m]
decomp :: [m], forall m o. FiniteCategoryError m o -> m
notGen :: m} -- ^ The morphism `f` decomposes into `decomp` where `notGen` is a non generating morphism.

                       | WrongDecomposition {f :: m, decomp :: [m], forall m o. FiniteCategoryError m o -> m
comp :: m} -- ^ @compose (decompose c f) /= f@.

                       deriving (FiniteCategoryError m o -> FiniteCategoryError m o -> Bool
(FiniteCategoryError m o -> FiniteCategoryError m o -> Bool)
-> (FiniteCategoryError m o -> FiniteCategoryError m o -> Bool)
-> Eq (FiniteCategoryError m o)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall m o.
(Eq m, Eq o) =>
FiniteCategoryError m o -> FiniteCategoryError m o -> Bool
/= :: FiniteCategoryError m o -> FiniteCategoryError m o -> Bool
$c/= :: forall m o.
(Eq m, Eq o) =>
FiniteCategoryError m o -> FiniteCategoryError m o -> Bool
== :: FiniteCategoryError m o -> FiniteCategoryError m o -> Bool
$c== :: forall m o.
(Eq m, Eq o) =>
FiniteCategoryError m o -> FiniteCategoryError m o -> Bool
Eq, Int -> FiniteCategoryError m o -> ShowS
[FiniteCategoryError m o] -> ShowS
FiniteCategoryError m o -> String
(Int -> FiniteCategoryError m o -> ShowS)
-> (FiniteCategoryError m o -> String)
-> ([FiniteCategoryError m o] -> ShowS)
-> Show (FiniteCategoryError m o)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall m o.
(Show m, Show o) =>
Int -> FiniteCategoryError m o -> ShowS
forall m o. (Show m, Show o) => [FiniteCategoryError m o] -> ShowS
forall m o. (Show m, Show o) => FiniteCategoryError m o -> String
showList :: [FiniteCategoryError m o] -> ShowS
$cshowList :: forall m o. (Show m, Show o) => [FiniteCategoryError m o] -> ShowS
show :: FiniteCategoryError m o -> String
$cshow :: forall m o. (Show m, Show o) => FiniteCategoryError m o -> String
showsPrec :: Int -> FiniteCategoryError m o -> ShowS
$cshowsPrec :: forall m o.
(Show m, Show o) =>
Int -> FiniteCategoryError m o -> ShowS
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 :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Maybe (FiniteCategoryError m o)
checkFiniteCategoryProperties c
c
        | (Bool -> Bool
not(Bool -> Bool) -> ([o] -> Bool) -> [o] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[o] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [o]
dupObjects = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just ObjectsNotUnique :: forall m o. o -> FiniteCategoryError m o
ObjectsNotUnique {dupObj :: o
dupObj=[o] -> o
forall a. [a] -> a
head [o]
dupObjects}
        | (Bool -> Bool
not(Bool -> Bool) -> ([(m, m)] -> Bool) -> [(m, m)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(m, m)]
incoherentEq = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just MorphismsShouldNotBeEqual :: forall m o. m -> m -> FiniteCategoryError m o
MorphismsShouldNotBeEqual {f :: m
f=((m, m) -> m
forall a b. (a, b) -> a
fst((m, m) -> m) -> ([(m, m)] -> (m, m)) -> [(m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m)] -> (m, m)
forall a. [a] -> a
head) [(m, m)]
incoherentEq, g :: m
g=((m, m) -> m
forall a b. (a, b) -> b
snd((m, m) -> m) -> ([(m, m)] -> (m, m)) -> [(m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m)] -> (m, m)
forall a. [a] -> a
head) [(m, m)]
incoherentEq}
        | (Bool -> Bool
not(Bool -> Bool) -> ([(m, o)] -> Bool) -> [(m, o)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, o)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(m, o)]
wrongSource = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just WrongSource :: forall m o. m -> o -> FiniteCategoryError m o
WrongSource {f :: m
f = ((m, o) -> m
forall a b. (a, b) -> a
fst((m, o) -> m) -> ([(m, o)] -> (m, o)) -> [(m, o)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, o)] -> (m, o)
forall a. [a] -> a
head) [(m, o)]
wrongSource, realSource :: o
realSource = ((m, o) -> o
forall a b. (a, b) -> b
snd((m, o) -> o) -> ([(m, o)] -> (m, o)) -> [(m, o)] -> o
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, o)] -> (m, o)
forall a. [a] -> a
head) [(m, o)]
wrongSource}
        | (Bool -> Bool
not(Bool -> Bool) -> ([(m, o)] -> Bool) -> [(m, o)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, o)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(m, o)]
wrongTarget = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just WrongTarget :: forall m o. m -> o -> FiniteCategoryError m o
WrongTarget {f :: m
f = ((m, o) -> m
forall a b. (a, b) -> a
fst((m, o) -> m) -> ([(m, o)] -> (m, o)) -> [(m, o)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, o)] -> (m, o)
forall a. [a] -> a
head) [(m, o)]
wrongTarget, realTarget :: o
realTarget = ((m, o) -> o
forall a b. (a, b) -> b
snd((m, o) -> o) -> ([(m, o)] -> (m, o)) -> [(m, o)] -> o
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, o)] -> (m, o)
forall a. [a] -> a
head) [(m, o)]
wrongTarget}
        | (Bool -> Bool
not(Bool -> Bool) -> ([m] -> Bool) -> [m] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[m] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [m]
dupMorph = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just MorphismsNotUnique :: forall m o. m -> FiniteCategoryError m o
MorphismsNotUnique {dupMorph :: m
dupMorph=[m] -> m
forall a. [a] -> a
head [m]
dupMorph}
        | (Bool -> Bool
not(Bool -> Bool) -> ([m] -> Bool) -> [m] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[m] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [m]
missingAr = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just ArrowsNotExhaustive :: forall m o. m -> FiniteCategoryError m o
ArrowsNotExhaustive {missingAr :: m
missingAr=[m] -> m
forall a. [a] -> a
head [m]
missingAr}
        | (Bool -> Bool
not(Bool -> Bool) -> ([(m, o, o)] -> Bool) -> [(m, o, o)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, o, o)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(m, o, o)]
unknownObjects = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just ArrowBetweenUnknownObjects :: forall m o. m -> o -> o -> FiniteCategoryError m o
ArrowBetweenUnknownObjects {f :: m
f=((m, o, o) -> m
forall {a} {b} {c}. (a, b, c) -> a
fst3((m, o, o) -> m) -> ([(m, o, o)] -> (m, o, o)) -> [(m, o, o)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, o, o)] -> (m, o, o)
forall a. [a] -> a
head) [(m, o, o)]
unknownObjects, s :: o
s=((m, o, o) -> o
forall {a} {b} {c}. (a, b, c) -> b
snd3((m, o, o) -> o) -> ([(m, o, o)] -> (m, o, o)) -> [(m, o, o)] -> o
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, o, o)] -> (m, o, o)
forall a. [a] -> a
head) [(m, o, o)]
unknownObjects, t :: o
t=((m, o, o) -> o
forall {a} {b} {c}. (a, b, c) -> c
trd3((m, o, o) -> o) -> ([(m, o, o)] -> (m, o, o)) -> [(m, o, o)] -> o
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, o, o)] -> (m, o, o)
forall a. [a] -> a
head) [(m, o, o)]
unknownObjects}
        | (Bool -> Bool
not(Bool -> Bool) -> ([(m, m, m)] -> Bool) -> [(m, m, m)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(m, m, m)]
idNotLNeutral = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just IdentityNotLeftNeutral :: forall m o. m -> m -> m -> FiniteCategoryError m o
IdentityNotLeftNeutral {idL :: m
idL=((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> a
fst3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. [a] -> a
head) [(m, m, m)]
idNotLNeutral, f :: m
f=((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> b
snd3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. [a] -> a
head) [(m, m, m)]
idNotLNeutral,foidL :: m
foidL=((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> c
trd3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. [a] -> a
head) [(m, m, m)]
idNotLNeutral} 
        | (Bool -> Bool
not(Bool -> Bool) -> ([(m, m, m)] -> Bool) -> [(m, m, m)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(m, m, m)]
idNotRNeutral = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just IdentityNotRightNeutral :: forall m o. m -> m -> m -> FiniteCategoryError m o
IdentityNotRightNeutral {f :: m
f=((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> a
fst3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. [a] -> a
head) [(m, m, m)]
idNotRNeutral, idR :: m
idR=((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> b
snd3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. [a] -> a
head) [(m, m, m)]
idNotRNeutral,idRof :: m
idRof=((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> c
trd3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. [a] -> a
head) [(m, m, m)]
idNotRNeutral} 
        | (Bool -> Bool
not(Bool -> Bool) -> ([(m, m, m)] -> Bool) -> [(m, m, m)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(m, m, m)]
notAssociative = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just CompositionNotAssociative :: forall m o. m -> m -> m -> m -> m -> FiniteCategoryError m o
CompositionNotAssociative {f :: m
f=((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> a
fst3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. [a] -> a
head) [(m, m, m)]
notAssociative,g :: m
g=((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> b
snd3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. [a] -> a
head) [(m, m, m)]
notAssociative,h :: m
h=((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> c
trd3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. [a] -> a
head) [(m, m, m)]
notAssociative, fg_h :: m
fg_h=((((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> a
fst3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. [a] -> a
head)[(m, m, m)]
notAssociative) m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ (((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> b
snd3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. [a] -> a
head)[(m, m, m)]
notAssociative)) m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ (((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> c
trd3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. [a] -> a
head)[(m, m, m)]
notAssociative),
                        f_gh :: m
f_gh=(((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> a
fst3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. [a] -> a
head)[(m, m, m)]
notAssociative) m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ ((((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> b
snd3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. [a] -> a
head)[(m, m, m)]
notAssociative) m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ (((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> c
trd3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. [a] -> a
head)[(m, m, m)]
notAssociative))}
        | (Bool -> Bool
not(Bool -> Bool) -> ([(m, m)] -> Bool) -> [(m, m)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(m, m)]
notTransitive = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just NotTransitive :: forall m o. m -> m -> FiniteCategoryError m o
NotTransitive {f :: m
f=((m, m) -> m
forall a b. (a, b) -> a
fst((m, m) -> m) -> ([(m, m)] -> (m, m)) -> [(m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m)] -> (m, m)
forall a. [a] -> a
head) [(m, m)]
notTransitive, g :: m
g=((m, m) -> m
forall a b. (a, b) -> b
snd((m, m) -> m) -> ([(m, m)] -> (m, m)) -> [(m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m)] -> (m, m)
forall a. [a] -> a
head) [(m, m)]
notTransitive}
        | Bool
otherwise = Maybe (FiniteCategoryError m o)
forall a. Maybe a
Nothing
        where
            dupObjects :: [o]
dupObjects = c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c [o] -> [o] -> [o]
forall a. Eq a => [a] -> [a] -> [a]
\\ [o] -> [o]
forall a. Eq a => [a] -> [a]
nub (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c)
            arrowsByAr :: [m]
arrowsByAr = [[m]] -> [m]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
c o
s o
t | o
s <- (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c), o
t <- (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c)]
            incoherentEq :: [(m, m)]
incoherentEq = [(m
f,m
g) | m
f <- c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c
c, m
g <- c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c
c, m
f m -> m -> Bool
forall a. Eq a => a -> a -> Bool
== m
g Bool -> Bool -> Bool
&& (m -> o
forall m o. Morphism m o => m -> o
source m
f o -> o -> Bool
forall a. Eq a => a -> a -> Bool
/= m -> o
forall m o. Morphism m o => m -> o
source m
g Bool -> Bool -> Bool
|| m -> o
forall m o. Morphism m o => m -> o
target m
f o -> o -> Bool
forall a. Eq a => a -> a -> Bool
/= m -> o
forall m o. Morphism m o => m -> o
target m
g)]
            wrongSource :: [(m, o)]
wrongSource = [(m
f,o
s) | o
s <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c, o
t <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c, m
f <- c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
c o
s o
t, m -> o
forall m o. Morphism m o => m -> o
source m
f o -> o -> Bool
forall a. Eq a => a -> a -> Bool
/= o
s]
            wrongTarget :: [(m, o)]
wrongTarget = [(m
f,o
t) | o
s <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c, o
t <- c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c, m
f <- c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
c o
s o
t, m -> o
forall m o. Morphism m o => m -> o
target m
f o -> o -> Bool
forall a. Eq a => a -> a -> Bool
/= o
t]
            dupMorph :: [m]
dupMorph = [m]
arrowsByAr [m] -> [m] -> [m]
forall a. Eq a => [a] -> [a] -> [a]
\\ [m] -> [m]
forall a. Eq a => [a] -> [a]
nub [m]
arrowsByAr
            missingAr :: [m]
missingAr = [m]
arrowsByAr [m] -> [m] -> [m]
forall a. Eq a => [a] -> [a] -> [a]
\\ (c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c
c)
            unknownObjects :: [(m, o, o)]
unknownObjects = [(m
f,m -> o
forall m o. Morphism m o => m -> o
source m
f,m -> o
forall m o. Morphism m o => m -> o
target 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
c, Bool -> Bool
not ( (m -> o
forall m o. Morphism m o => m -> o
source m
f) o -> [o] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c) Bool -> Bool -> Bool
&& (m -> o
forall m o. Morphism m o => m -> o
target m
f) o -> [o] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c) )]
            idNotLNeutral :: [(m, m, m)]
idNotLNeutral = [(c -> o -> m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c
c (m -> o
forall m o. Morphism m o => m -> o
source m
f),m
f,m
f m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ c -> o -> m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c
c (m -> o
forall m o. Morphism m o => m -> o
source 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
c, m
f m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ c -> o -> m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c
c (m -> o
forall m o. Morphism m o => m -> o
source m
f) m -> m -> Bool
forall a. Eq a => a -> a -> Bool
/= m
f]
            idNotRNeutral :: [(m, m, m)]
idNotRNeutral = [(m
f,c -> o -> m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c
c (m -> o
forall m o. Morphism m o => m -> o
target m
f), c -> o -> m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c
c (m -> o
forall m o. Morphism m o => m -> o
target m
f) m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ 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
c, c -> o -> m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c
c (m -> o
forall m o. Morphism m o => m -> o
target m
f) m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
f m -> m -> Bool
forall a. Eq a => a -> a -> Bool
/= m
f]
            notAssociative :: [(m, m, m)]
notAssociative = [(m
x,m
y,m
z) | m
z <- c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c
c, m
y <- c -> o -> [m]
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> [m]
arFrom c
c (m -> o
forall m o. Morphism m o => m -> o
target m
z), m
x <- c -> o -> [m]
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> [m]
arFrom c
c (m -> o
forall m o. Morphism m o => m -> o
target m
y), (m
x m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
y) m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
z m -> m -> Bool
forall a. Eq a => a -> a -> Bool
/= m
x m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ (m
y m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
z)]
            notTransitive :: [(m, m)]
notTransitive = [(m
f,m
g) | m
g <- c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c
c, m
f <- c -> o -> [m]
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> [m]
arFrom c
c (m -> o
forall m o. Morphism m o => m -> o
target m
g), Bool -> Bool
not (m -> [m] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (m
f m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
g) (c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
c (m -> o
forall m o. Morphism m o => m -> o
source m
g) (m -> o
forall m o. Morphism m o => m -> o
target m
f)))]
            fst3 :: (a, b, c) -> a
fst3 (a
x,b
_,c
_) = a
x
            snd3 :: (a, b, c) -> b
snd3 (a
_,b
x,c
_) = b
x
            trd3 :: (a, b, c) -> c
trd3 (a
_,b
_,c
x) = c
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 :: forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Maybe (FiniteCategoryError m o)
checkGeneratedFiniteCategoryProperties c
c
        | Maybe (FiniteCategoryError m o)
errCat Maybe (FiniteCategoryError m o)
-> Maybe (FiniteCategoryError m o) -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe (FiniteCategoryError m o)
forall a. Maybe a
Nothing = Maybe (FiniteCategoryError m o)
errCat
        | (Bool -> Bool
not(Bool -> Bool) -> ([m] -> Bool) -> [m] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[m] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [m]
genNotMorph = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just GeneratorIsNotAMorphism :: forall m o. m -> FiniteCategoryError m o
GeneratorIsNotAMorphism {f :: m
f=[m] -> m
forall a. [a] -> a
head [m]
genNotMorph}
        | (Bool -> Bool
not(Bool -> Bool) -> ([(m, [m], m)] -> Bool) -> [(m, [m], m)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, [m], m)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(m, [m], m)]
decompIntoComposite = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just MorphismDoesntDecomposesIntoGenerators :: forall m o. m -> [m] -> m -> FiniteCategoryError m o
MorphismDoesntDecomposesIntoGenerators {f :: m
f=((m, [m], m) -> m
forall {a} {b} {c}. (a, b, c) -> a
fst3((m, [m], m) -> m)
-> ([(m, [m], m)] -> (m, [m], m)) -> [(m, [m], m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, [m], m)] -> (m, [m], m)
forall a. [a] -> a
head) [(m, [m], m)]
decompIntoComposite, decomp :: [m]
decomp=((m, [m], m) -> [m]
forall {a} {b} {c}. (a, b, c) -> b
snd3((m, [m], m) -> [m])
-> ([(m, [m], m)] -> (m, [m], m)) -> [(m, [m], m)] -> [m]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, [m], m)] -> (m, [m], m)
forall a. [a] -> a
head) [(m, [m], m)]
decompIntoComposite, notGen :: m
notGen=((m, [m], m) -> m
forall {a} {b} {c}. (a, b, c) -> c
trd3((m, [m], m) -> m)
-> ([(m, [m], m)] -> (m, [m], m)) -> [(m, [m], m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, [m], m)] -> (m, [m], m)
forall a. [a] -> a
head) [(m, [m], m)]
decompIntoComposite}
        | (Bool -> Bool
not(Bool -> Bool) -> ([(m, [m], m)] -> Bool) -> [(m, [m], m)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, [m], m)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(m, [m], m)]
wrongDecomp = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just WrongDecomposition :: forall m o. m -> [m] -> m -> FiniteCategoryError m o
WrongDecomposition {f :: m
f=((m, [m], m) -> m
forall {a} {b} {c}. (a, b, c) -> a
fst3((m, [m], m) -> m)
-> ([(m, [m], m)] -> (m, [m], m)) -> [(m, [m], m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, [m], m)] -> (m, [m], m)
forall a. [a] -> a
head) [(m, [m], m)]
wrongDecomp, decomp :: [m]
decomp=((m, [m], m) -> [m]
forall {a} {b} {c}. (a, b, c) -> b
snd3((m, [m], m) -> [m])
-> ([(m, [m], m)] -> (m, [m], m)) -> [(m, [m], m)] -> [m]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, [m], m)] -> (m, [m], m)
forall a. [a] -> a
head) [(m, [m], m)]
wrongDecomp, comp :: m
comp=((m, [m], m) -> m
forall {a} {b} {c}. (a, b, c) -> c
trd3((m, [m], m) -> m)
-> ([(m, [m], m)] -> (m, [m], m)) -> [(m, [m], m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, [m], m)] -> (m, [m], m)
forall a. [a] -> a
head) [(m, [m], m)]
wrongDecomp}
        | Bool
otherwise = Maybe (FiniteCategoryError m o)
forall a. Maybe a
Nothing 
        where 
            errCat :: Maybe (FiniteCategoryError m o)
errCat = c -> Maybe (FiniteCategoryError m o)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Maybe (FiniteCategoryError m o)
checkFiniteCategoryProperties c
c
            genNotMorph :: [m]
genNotMorph = c -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, GeneratedFiniteCategory c m o,
 Morphism m o) =>
c -> [m]
genArrows c
c [m] -> [m] -> [m]
forall a. Eq a => [a] -> [a] -> [a]
\\ c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c
c
            decompIntoComposite :: [(m, [m], m)]
decompIntoComposite = [(m
m,c -> m -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> m -> [m]
decompose c
c m
m,m
f) | m
m <- c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c
c, m
f <- c -> m -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> m -> [m]
decompose c
c m
m, Bool -> Bool
not (m -> [m] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem m
f (c -> o -> o -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
genAr c
c (m -> o
forall m o. Morphism m o => m -> o
source m
f) (m -> o
forall m o. Morphism m o => m -> o
target m
f)))]
            wrongDecomp :: [(m, [m], m)]
wrongDecomp = [(m
f,c -> m -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> m -> [m]
decompose c
c m
f, [m] -> m
forall m o. Morphism m o => [m] -> m
compose (c -> m -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> m -> [m]
decompose c
c 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
c, [m] -> m
forall m o. Morphism m o => [m] -> m
compose (c -> m -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> m -> [m]
decompose c
c m
f) m -> m -> Bool
forall a. Eq a => a -> a -> Bool
/= m
f]
            fst3 :: (a, b, c) -> a
fst3 (a
x,b
_,c
_) = a
x
            snd3 :: (a, b, c) -> b
snd3 (a
_,b
x,c
_) = b
x
            trd3 :: (a, b, c) -> c
trd3 (a
_,b
_,c
x) = c
x
            
    instance (Show m, Show o) => PrettyPrintable (FiniteCategoryError m o) where
        pprint :: FiniteCategoryError m o -> String
pprint = FiniteCategoryError m o -> String
forall a. Show a => a -> String
show