{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
{-| Module : FiniteCategories
Description : 'Morphism' and 'Category' typeclasses.
Copyright : Guillaume Sabbagh 2022
License : GPL-3
Maintainer : guillaumesabbagh@protonmail.com
Stability : experimental
Portability : portable
A `Morphism` is composable, it has a source and a target.
A `Category` allows to enumerate all arrows between two objects and allows to construct the identity of an object. It is mathematically a locally finite category, we name it 'Category' for simplicity.
See `FiniteCategory` for the ability to enumerate the objects of a category.
We don't reify the `Category` concept because we want to be able to equate categories (functions are not equatable).
A `GeneratedCategory` is a `Category` where some morphisms are selected as generators. Any 'Category' has a trivial set of generators: the set of all of its arrows. You can override the default definition of generators when creating your 'Category' by instantiating 'GeneratedCategory'.
-}
module Math.Category
(
-- * Morphism
Morphism(..),
-- ** Morphism related functions
(@),
compose,
-- * Category
Category(..),
-- ** Morphism predicates
isIdentity,
isNotIdentity,
isIso,
isSection,
isRetraction,
areIsomorphic,
-- ** Generator predicates
isGenerator,
isComposite,
-- ** Find special morphisms
findInverse,
findIsomorphism,
findRightInverses,
findLeftInverses,
)
where
import Data.WeakSet (Set)
import qualified Data.WeakSet as Set
import Data.WeakSet.Safe
-- | 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 composition operator, surround the '@?' symbol with spaces.
--
-- 'Morphism' is a multiparametrized typeclass where /m/ is the type of the morphism and /o/ the type of the source and target objects.
--
-- 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 return 'Nothing' 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> (fmap (f @?)) (g @? h) = fmap (@? h) (f @? g)
(@?) :: m -> m -> Maybe m
-- | Return the source object of the morphism.
source :: m -> o
-- | Return the target object of the morphism.
target :: m -> o
-- | Unsafe version of '(@?)'.
(@) :: (Morphism m o) => m -> m -> m
(@) m2 m1
| null compo = error "Math.Category.(@): incompatible morphisms"
| otherwise = r
where
compo = m2 @? m1
Just r = compo
-- | Return the composition of a list of morphisms.
--
-- For example :
-- @compose [f,g,h] = f \@ g \@ h@
--
-- Return an error if the list is empty : we would have to return an identity but we don't know which one.
compose :: (Morphism m o) => [m] -> m
compose [] = error "Category.compose: empty list to compose"
compose l = foldr1 (@) l
-- | A `Category` allows to enumerate all arrows between two objects and allows to construct the identity of an object.
--
-- A 'Category' is multiparametrized by the type of its morphisms and the type of its objects.
--
-- This typeclass does not assume the category is finite, the number of objects in the category may be infinite.
--
-- A category is a set of objects and a set of morphisms which follows the category axioms.
--
-- A category also has sets of generating morphisms. A set of generating morphisms is a set of morphism such that every morphism of the category can be constructed by
-- composing generators. Note that we consider identities should be generators even though they can be constructed as the composition of zero morphism because 'compose' can't compose zero morphism.
--
-- Some algorithms are simplified because they only need to deal with generators, the rest of the properties are deduced by composition.
--
-- Every `Category` has at least one set of generators : the set of all of its morphisms.
--
-- You can override 'genAr' and 'decompose' to define a more interesting set of generating morphisms for a given 'Category'.
class Category c m o | c -> m, m -> o where
-- | `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 set of all arrows between a source and a target.
--
-- Arrows with different source or target should not be equal.
ar :: (Morphism m o) => c -- ^ The category
-> o -- ^ The source of the morphisms
-> o -- ^ The target of the morphisms
-> Set m -- ^ The set of morphisms in the category c between source and target
{-|# MINIMAL identity, ar #-}
-- | Same as `ar` but only returns the generators.
--
-- prop> @('genAr' c s t) `isIncludedIn` ('ar' c s t)@.
--
-- The default implementation is 'ar' because the set of all arrows generates trivially the category.
genAr :: (Morphism m o) => c -> o -> o -> Set m
genAr = ar
-- | `decompose` decomposes a morphism into a list of generators (according to composition) :
--
-- prop> m = compose (decompose c m)
--
-- An identity should be decomposed into a list containing itself.
--
-- The default implementation returns the morphism in a list as all arrows are generators.
decompose :: (Morphism m o) => c -> m -> [m]
decompose _ = (:[])
-- | Return wether a morphism is an identity in a category.
isIdentity :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
isIdentity c m = identity c (source m) == m
-- | Return wether a morphism is not an identity.
isNotIdentity :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
isNotIdentity c m = not (isIdentity c m)
-- | Return Just an inverse of a morphism if possible, Nothing otherwise
findInverse :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> m -> Maybe m
findInverse c m = (Set.setToMaybe) $ Set.filter (\f -> isIdentity c (m @ f) && isIdentity c (f @ m)) (ar c (target m) (source m))
-- | Return Just an isomorphism from an object to another if possible, Nothing otherwise.
findIsomorphism :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> o -> o -> Maybe m
findIsomorphism c s t = (Set.setToMaybe).(Set.catMaybes) $ findInverse c <$> ar c s t
-- | Return wether two objects are isomorphic or not.
areIsomorphic :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> o -> o -> Bool
areIsomorphic c s t = not.null $ findIsomorphism c s t
-- | Return if a morphism is an isomorphism
isIso :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
isIso c m = not.null $ findInverse c m
-- | Find all right inverses.
findRightInverses :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> m -> Set m
findRightInverses c f = Set.filter (\g -> isIdentity c (f @ g)) $ ar c (target f) (source f)
-- | Return wether a morphism is a section.
isSection :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
isSection c f = not.(Set.null) $ findRightInverses c f
-- | Find a left inverse if it can, returns Nothing otherwise.
findLeftInverses :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> m -> Set m
findLeftInverses c f = Set.filter (\g -> isIdentity c (g @ f)) $ ar c (target f) (source f)
-- | Return wether a morphism is a retraction.
isRetraction :: (Category c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
isRetraction c f = not.(Set.null) $ findLeftInverses c f
-- | Return if a morphism is a generating morphism.
isGenerator :: (Category c m o, Morphism m o, Eq m) => c -> m -> Bool
isGenerator c f = f `isIn` (genAr c (source f) (target f))
-- | Opposite of `isGenerator`, i.e. returns if the morphism is composite.
isComposite :: (Category c m o, Morphism m o, Eq m) => c -> m -> Bool
isComposite c f = not (isGenerator c f)