Copyright | Guillaume Sabbagh 2021 |
---|---|
License | GPL-3 |
Maintainer | guillaumesabbagh@protonmail.com |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
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.
Synopsis
- class Morphism m o | m -> o where
- compose :: Morphism m o => [m] -> m
- class FiniteCategory c m o | c -> m, m -> o where
- arFrom :: (FiniteCategory c m o, Morphism m o) => c -> o -> [m]
- arFrom2 :: (FiniteCategory c m o, Morphism m o) => c -> [o] -> [m]
- arTo :: (FiniteCategory c m o, Morphism m o) => c -> o -> [m]
- arTo2 :: (FiniteCategory c m o, Morphism m o) => c -> [o] -> [m]
- identities :: (FiniteCategory c m o, Morphism m o) => c -> [m]
- isIdentity :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
- isNotIdentity :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
- isTerminal :: (FiniteCategory c m o, Morphism m o) => c -> o -> Bool
- isInitial :: (FiniteCategory c m o, Morphism m o) => c -> o -> Bool
- terminalObjects :: (FiniteCategory c m o, Morphism m o) => c -> [o]
- initialObjects :: (FiniteCategory c m o, Morphism m o) => c -> [o]
- class FiniteCategory c m o => GeneratedFiniteCategory c m o where
- genArFrom :: (GeneratedFiniteCategory c m o, Morphism m o) => c -> o -> [m]
- genArFrom2 :: (GeneratedFiniteCategory c m o, Morphism m o) => c -> [o] -> [m]
- genArTo :: (GeneratedFiniteCategory c m o, Morphism m o) => c -> o -> [m]
- genArTo2 :: (GeneratedFiniteCategory c m o, Morphism m o) => c -> [o] -> [m]
- defaultGenAr :: (GeneratedFiniteCategory c m o, Morphism m o) => c -> o -> o -> [m]
- defaultDecompose :: (GeneratedFiniteCategory c m o, Morphism m o) => c -> m -> [m]
- bruteForceDecompose :: (GeneratedFiniteCategory c m o, Morphism m o, Eq m) => c -> m -> [m]
- isGenerator :: (GeneratedFiniteCategory c m o, Morphism m o, Eq m) => c -> m -> Bool
- isComposite :: (GeneratedFiniteCategory c m o, Morphism m o, Eq m) => c -> m -> Bool
- data FiniteCategoryError m o
- = CompositionNotAssociative { }
- | ObjectsNotUnique {
- dupObj :: o
- | MorphismsNotUnique {
- dupMorph :: m
- | ArrowsNotExhaustive {
- missingAr :: m
- | ArrowBetweenUnknownObjects { }
- | WrongSource {
- f :: m
- realSource :: o
- | WrongTarget {
- f :: m
- realTarget :: o
- | IdentityNotLeftNeutral { }
- | IdentityNotRightNeutral { }
- | MorphismsShouldNotBeEqual { }
- | NotTransitive { }
- | GeneratorIsNotAMorphism {
- f :: m
- | MorphismDoesntDecomposesIntoGenerators { }
- | WrongDecomposition { }
- checkFiniteCategoryProperties :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Maybe (FiniteCategoryError m o)
- checkGeneratedFiniteCategoryProperties :: (GeneratedFiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Maybe (FiniteCategoryError m o)
Morphism typeclass and related functions
class Morphism m o | m -> o where Source #
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.
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 :
f @ (g @ h) = (f @ g) @ h
Instances
compose :: Morphism m o => [m] -> m Source #
Returns the composition of the list of morphisms.
For example :
compose [f,g,h] = f @ g @ h
FiniteCategory typeclass
class FiniteCategory c m o | c -> m, m -> o where Source #
A category is multiparametrized by the type of its morphisms and the type of its objects.
ob
should return a list of unique objects :
List.nub (ob c) = ob c
identity :: Morphism m o => c -> o -> m Source #
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 :
f @ identity c (source f) = f
identity c (target g) @ g = g
:: 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 |
ar
should return the list of all unique arrows between a source and a target :
List.nub (ar c s t) = ar c s t
Arrows with different source or target should not be equal :
(s1 = s2 && t1 = t2) || List.intersect (ar c s1 t1) (ar c s2 t2) = []
arrows :: (FiniteCategory c m o, Morphism m o) => c -> [m] Source #
arrows
returns the list of all unique morphisms of a category.
Instances
FiniteCategory functions
arFrom :: (FiniteCategory c m o, Morphism m o) => c -> o -> [m] Source #
arFrom
returns the list of unique morphisms going from a specified source.
arFrom2 :: (FiniteCategory c m o, Morphism m o) => c -> [o] -> [m] Source #
arTo :: (FiniteCategory c m o, Morphism m o) => c -> o -> [m] Source #
arTo
returns the list of unique morphisms going to a specified target.
arTo2 :: (FiniteCategory c m o, Morphism m o) => c -> [o] -> [m] Source #
identities :: (FiniteCategory c m o, Morphism m o) => c -> [m] Source #
identities
returns all the identities of a category.
isIdentity :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool Source #
Returns wether a morphism is an identity in a category.
isNotIdentity :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool Source #
Returns wether a morphism is not an identity.
isTerminal :: (FiniteCategory c m o, Morphism m o) => c -> o -> Bool Source #
Returns wether an object is terminal in the category.
isInitial :: (FiniteCategory c m o, Morphism m o) => c -> o -> Bool Source #
Returns wether an object is initial in the category.
terminalObjects :: (FiniteCategory c m o, Morphism m o) => c -> [o] Source #
Returns the list of terminal objects in a category.
initialObjects :: (FiniteCategory c m o, Morphism m o) => c -> [o] Source #
Returns the list of intial objects in a category.
GeneratedFiniteCategory typeclass and related functions
class FiniteCategory c m o => GeneratedFiniteCategory c m o where Source #
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.
genAr :: Morphism m o => c -> o -> o -> [m] Source #
Same as ar
but only returns the generators. genAr c s t
should be included in ar c s t
.
decompose :: Morphism m o => c -> m -> [m] Source #
decompose
decomposes a morphism into a list of generators (according to composition) :
m = compose (decompose c m)
genArrows :: (GeneratedFiniteCategory c m o, Morphism m o) => c -> [m] Source #
Same as arrows
but only returns the generators. genArrows c
should be included in arrows c
.
Instances
genArFrom :: (GeneratedFiniteCategory c m o, Morphism m o) => c -> o -> [m] Source #
Same as arFrom
but only returns the generators. genArFrom c s
should be included in arFrom c s
.
genArFrom2 :: (GeneratedFiniteCategory c m o, Morphism m o) => c -> [o] -> [m] Source #
Same as arFrom2
but only returns the generators. genArFrom2 c [s]
should be included in arFrom2 c [t]
.
genArTo :: (GeneratedFiniteCategory c m o, Morphism m o) => c -> o -> [m] Source #
Same as arTo
but only returns the generators. genArTo c t
should be included in arTo c t
.
genArTo2 :: (GeneratedFiniteCategory c m o, Morphism m o) => c -> [o] -> [m] Source #
Same as arTo2
but only returns the generators. genArTo2 c [t]
should be included in arTo2 c [t]
.
defaultGenAr :: (GeneratedFiniteCategory c m o, Morphism m o) => c -> o -> o -> [m] Source #
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
.
defaultDecompose :: (GeneratedFiniteCategory c m o, Morphism m o) => c -> m -> [m] Source #
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
.
bruteForceDecompose :: (GeneratedFiniteCategory c m o, Morphism m o, Eq m) => c -> m -> [m] Source #
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.)
isGenerator :: (GeneratedFiniteCategory c m o, Morphism m o, Eq m) => c -> m -> Bool Source #
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.)
isComposite :: (GeneratedFiniteCategory c m o, Morphism m o, Eq m) => c -> m -> Bool Source #
Opposite of isGenerator
, i.e. returns if the morphism is composite.
Check for category correctness
data FiniteCategoryError m o Source #
A data type to represent an incoherence inside a category.
CompositionNotAssociative | (h@g)@f /= h@(g@f) |
ObjectsNotUnique |
|
| |
MorphismsNotUnique |
|
| |
ArrowsNotExhaustive |
|
| |
ArrowBetweenUnknownObjects |
|
WrongSource |
|
| |
WrongTarget |
|
| |
IdentityNotLeftNeutral |
|
IdentityNotRightNeutral |
|
MorphismsShouldNotBeEqual |
|
NotTransitive |
|
GeneratorIsNotAMorphism |
|
| |
MorphismDoesntDecomposesIntoGenerators | The morphism |
WrongDecomposition |
|
Instances
(Eq m, Eq o) => Eq (FiniteCategoryError m o) Source # | |
Defined in FiniteCategory.FiniteCategory (==) :: FiniteCategoryError m o -> FiniteCategoryError m o -> Bool (/=) :: FiniteCategoryError m o -> FiniteCategoryError m o -> Bool | |
(Show m, Show o) => Show (FiniteCategoryError m o) Source # | |
Defined in FiniteCategory.FiniteCategory showsPrec :: Int -> FiniteCategoryError m o -> ShowS show :: FiniteCategoryError m o -> String showList :: [FiniteCategoryError m o] -> ShowS | |
(Show m, Show o) => PrettyPrintable (FiniteCategoryError m o) Source # | |
Defined in FiniteCategory.FiniteCategory pprint :: FiniteCategoryError m o -> String Source # |
checkFiniteCategoryProperties :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Maybe (FiniteCategoryError m o) Source #
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.
checkGeneratedFiniteCategoryProperties :: (GeneratedFiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Maybe (FiniteCategoryError m o) Source #
Same as checkFiniteCategoryProperties
but for GeneratedFiniteCategory
.