Copyright	Guillaume Sabbagh 2021
License	GPL-3
Maintainer	guillaumesabbagh@protonmail.com
Stability	experimental
Portability	portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

CompositionGraph.SafeCompositionGraph

Contents

Types for a morphism of composition graph
Types for a composition graph
Construction
Insertion
Modification
Deletion
Utility functions

Description

A SafeCompositionGraph is the quasi-free category generated by a multidigraph quotiented by an equivalence relation on the paths of the graphs. There is a limit on the number of cycles you can have in a morphism. It prevents any infinite loop from occuring. A multidigraph is a directed multigraph which means that edges are oriented and there can be multiple arrows between two objects.

The underlying multidigraph is given by a list of nodes and a list of arrows.

The equivalence relation is given by a function on paths of the inductive graph.

The function mkSafeCompositionGraph checks the structure of the category and is the preferred way of instantiatiating the SafeCompositionGraph type. If the check takes too long because the category is big, you can use the SafeCompositionGraph constructor if you're sure that the category structure is respected.

Morphisms from different composition graphs should not be composed or compared, if they are, the behavior is undefined.

When taking subcategories of a composition graph, the composition law might lead to morphisms not existing anymore. It is not a problem because they are equivalent, it is only counterintuitive for human readability.

Example.ExampleSafeCompositionGraph provides an example of composition graph construction.

Synopsis

data SCGMorphism a b = SCGMorphism {
- pathS :: Path a b
- compositionLawS :: CompositionLaw a b
- maxNbCycles :: Int
}
data SafeCompositionGraph a b = SafeCompositionGraph {
- graphS :: Graph a b
- lawS :: CompositionLaw a b
- maxCycles :: Int
}
mkSafeCompositionGraph :: (Eq a, Eq b, Show a) => Graph a b -> CompositionLaw a b -> Int -> Either (FiniteCategoryError (SCGMorphism a b) a) (SafeCompositionGraph a b)
mkEmptySafeCompositionGraph :: Int -> SafeCompositionGraph a b
finiteCategoryToSafeCompositionGraph :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> (SafeCompositionGraph o m, Diagram c m o (SafeCompositionGraph o m) (SCGMorphism o m) o)
generatedFiniteCategoryToSafeCompositionGraph :: (GeneratedFiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> (SafeCompositionGraph o m, Diagram c m o (SafeCompositionGraph o m) (SCGMorphism o m) o)
insertObjectS :: (Eq a, Eq b) => SafeCompositionGraph a b -> a -> (SafeCompositionGraph a b, PartialFunctor (SafeCompositionGraph a b) (SCGMorphism a b) a)
insertMorphismS :: (Eq a, Eq b) => SafeCompositionGraph a b -> a -> a -> b -> Either (SafeCompositionGraphError a b) (SafeCompositionGraph a b, PartialFunctor (SafeCompositionGraph a b) (SCGMorphism a b) a)
identifyMorphismsS :: (Eq a, Eq b) => SafeCompositionGraph a b -> SCGMorphism a b -> SCGMorphism a b -> Either (SafeCompositionGraphError a b) (SafeCompositionGraph a b, PartialFunctor (SafeCompositionGraph a b) (SCGMorphism a b) a)
unidentifyMorphismS :: (Eq a, Eq b) => SafeCompositionGraph a b -> SCGMorphism a b -> Either (SafeCompositionGraphError a b) (SafeCompositionGraph a b, PartialFunctor (SafeCompositionGraph a b) (SCGMorphism a b) a)
replaceObjectS :: (Eq a, Eq b) => SafeCompositionGraph a b -> a -> a -> Either (SafeCompositionGraphError a b) (SafeCompositionGraph a b, PartialFunctor (SafeCompositionGraph a b) (SCGMorphism a b) a)
replaceMorphismS :: (Eq a, Eq b) => SafeCompositionGraph a b -> SCGMorphism a b -> b -> Either (SafeCompositionGraphError a b) (SafeCompositionGraph a b, PartialFunctor (SafeCompositionGraph a b) (SCGMorphism a b) a)
deleteObjectS :: (Eq a, Eq b) => SafeCompositionGraph a b -> a -> Either (SafeCompositionGraphError a b) (SafeCompositionGraph a b, PartialFunctor (SafeCompositionGraph a b) (SCGMorphism a b) a)
deleteMorphismS :: (Eq a, Eq b) => SafeCompositionGraph a b -> SCGMorphism a b -> Either (SafeCompositionGraphError a b) (SafeCompositionGraph a b, PartialFunctor (SafeCompositionGraph a b) (SCGMorphism a b) a)
isGenS :: Eq a => SCGMorphism a b -> Bool
isCompS :: Eq a => SCGMorphism a b -> Bool
getLabelS :: Eq a => SCGMorphism a b -> Maybe b

Types for a morphism of composition graph

data SCGMorphism a b Source #

The type SCGMorphism is the type of safe composition graph morphisms.

It is a path with a composition law, it is necessary to keep the composition law of the composition graph in every morphism of the graph because we need it to compose two morphisms and the morphisms compose independently of the composition graph. We also store the maximum number of cycles.

Constructors

SCGMorphism
Fields pathS :: Path a b compositionLawS :: CompositionLaw a b maxNbCycles :: Int

Instances

Instances details

(Eq a, Eq b) => Eq (SCGMorphism a b) Source #
Instance details Defined in CompositionGraph.SafeCompositionGraph Methods (==) :: SCGMorphism a b -> SCGMorphism a b -> Bool (/=) :: SCGMorphism a b -> SCGMorphism a b -> Bool
(Show a, Show b) => Show (SCGMorphism a b) Source #
Instance details Defined in CompositionGraph.SafeCompositionGraph Methods showsPrec :: Int -> SCGMorphism a b -> ShowS show :: SCGMorphism a b -> String showList :: [SCGMorphism a b] -> ShowS
(PrettyPrintable a, PrettyPrintable b, Eq a, Eq b) => PrettyPrintable (SCGMorphism a b) Source #
Instance details Defined in CompositionGraph.SafeCompositionGraph Methods pprint :: SCGMorphism a b -> String Source #
(Eq a, Eq b) => Morphism (SCGMorphism a b) a Source #
Instance details Defined in CompositionGraph.SafeCompositionGraph Methods (@) :: SCGMorphism a b -> SCGMorphism a b -> SCGMorphism a b Source # source :: SCGMorphism a b -> a Source # target :: SCGMorphism a b -> a Source #
(Eq a, Eq b) => GeneratedFiniteCategory (SafeCompositionGraph a b) (SCGMorphism a b) a Source #
Instance details Defined in CompositionGraph.SafeCompositionGraph Methods genAr :: SafeCompositionGraph a b -> a -> a -> [SCGMorphism a b] Source # decompose :: SafeCompositionGraph a b -> SCGMorphism a b -> [SCGMorphism a b] Source # genArrows :: SafeCompositionGraph a b -> [SCGMorphism a b] Source #
(Eq a, Eq b) => FiniteCategory (SafeCompositionGraph a b) (SCGMorphism a b) a Source #
Instance details Defined in CompositionGraph.SafeCompositionGraph Methods ob :: SafeCompositionGraph a b -> [a] Source # identity :: SafeCompositionGraph a b -> a -> SCGMorphism a b Source # ar :: SafeCompositionGraph a b -> a -> a -> [SCGMorphism a b] Source # arrows :: SafeCompositionGraph a b -> [SCGMorphism a b] Source #

Types for a composition graph

data SafeCompositionGraph a b Source #

A composition graph is a graph with a composition law. Use mkSafeCompositionGraph to instantiate it unless it takes too long.

Constructors

SafeCompositionGraph
Fields graphS :: Graph a b lawS :: CompositionLaw a b maxCycles :: Int

Instances

Instances details

(Eq a, Eq b) => Eq (SafeCompositionGraph a b) Source #
Instance details Defined in CompositionGraph.SafeCompositionGraph Methods (==) :: SafeCompositionGraph a b -> SafeCompositionGraph a b -> Bool (/=) :: SafeCompositionGraph a b -> SafeCompositionGraph a b -> Bool
(Show a, Show b) => Show (SafeCompositionGraph a b) Source #
Instance details Defined in CompositionGraph.SafeCompositionGraph Methods showsPrec :: Int -> SafeCompositionGraph a b -> ShowS show :: SafeCompositionGraph a b -> String showList :: [SafeCompositionGraph a b] -> ShowS
(PrettyPrintable a, PrettyPrintable b, Eq a, Eq b) => PrettyPrintable (SafeCompositionGraph a b) Source #
Instance details Defined in CompositionGraph.SafeCompositionGraph Methods pprint :: SafeCompositionGraph a b -> String Source #
(Eq a, Eq b) => GeneratedFiniteCategory (SafeCompositionGraph a b) (SCGMorphism a b) a Source #
Instance details Defined in CompositionGraph.SafeCompositionGraph Methods genAr :: SafeCompositionGraph a b -> a -> a -> [SCGMorphism a b] Source # decompose :: SafeCompositionGraph a b -> SCGMorphism a b -> [SCGMorphism a b] Source # genArrows :: SafeCompositionGraph a b -> [SCGMorphism a b] Source #
(Eq a, Eq b) => FiniteCategory (SafeCompositionGraph a b) (SCGMorphism a b) a Source #
Instance details Defined in CompositionGraph.SafeCompositionGraph Methods ob :: SafeCompositionGraph a b -> [a] Source # identity :: SafeCompositionGraph a b -> a -> SCGMorphism a b Source # ar :: SafeCompositionGraph a b -> a -> a -> [SCGMorphism a b] Source # arrows :: SafeCompositionGraph a b -> [SCGMorphism a b] Source #

Construction

mkSafeCompositionGraph :: (Eq a, Eq b, Show a) => Graph a b -> CompositionLaw a b -> Int -> Either (FiniteCategoryError (SCGMorphism a b) a) (SafeCompositionGraph a b) Source #

Constructs a SafeCompositionGraph from a Graph and a CompositionLaw.

This is the preferred way of instantiating a SafeCompositionGraph with mkEmptySafeCompositionGraph. This function checks the category structure, that is why it can return a FiniteCategoryError if the graph and the composition law provided don't produce a valid category. If this function takes too much time, use the SafeCompositionGraph constructor at your own risk (it is your responsability to check the the category structure is valid).

mkEmptySafeCompositionGraph :: Int -> SafeCompositionGraph a b Source #

Constructs an empty SafeCompositionGraph with a maximum number of cycles.

Use insertObject, insertMorphism and identifyMorphisms to build a SafeCompositionGraph from it.

finiteCategoryToSafeCompositionGraph :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> (SafeCompositionGraph o m, Diagram c m o (SafeCompositionGraph o m) (SCGMorphism o m) o) Source #

Transforms any FiniteCategory into a safe composition graph.

The composition graph will take more space in memory compared to the original category because the composition law is stored as a Data.Map.

Returns the SafeCompositionGraph and an isofunctor as a Diagram.

generatedFiniteCategoryToSafeCompositionGraph :: (GeneratedFiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> (SafeCompositionGraph o m, Diagram c m o (SafeCompositionGraph o m) (SCGMorphism o m) o) Source #

Transforms any GeneratedFiniteCategory into a safe composition graph.

The composition graph will take more space in memory compared to the original category because the composition law is stored as a Data.Map.

Returns the SafeCompositionGraph and an isofunctor as a Diagram.

Insertion

insertObjectS :: (Eq a, Eq b) => SafeCompositionGraph a b -> a -> (SafeCompositionGraph a b, PartialFunctor (SafeCompositionGraph a b) (SCGMorphism a b) a) Source #

Inserts an object in a SafeCompositionGraph, returns the new SafeCompositionGraph and a PartialFunctor which is the insertion functor.

insertMorphismS :: (Eq a, Eq b) => SafeCompositionGraph a b -> a -> a -> b -> Either (SafeCompositionGraphError a b) (SafeCompositionGraph a b, PartialFunctor (SafeCompositionGraph a b) (SCGMorphism a b) a) Source #

Inserts a morphism in a SafeCompositionGraph, returns the new SafeCompositionGraph and a PartialFunctor which is the insertion functor if it can, returns Nothing otherwise.

This function fails if the two nodes provided as source and target for the new morphism are not both in the composition graph.

The result may not be a valid SafeCompositionGraph (the new morphism might close a loop creating infinitely many morphisms). You can use the function identifyMorphisms to transform it back into a valid SafeCompositionGraph.

Modification

identifyMorphismsS :: (Eq a, Eq b) => SafeCompositionGraph a b -> SCGMorphism a b -> SCGMorphism a b -> Either (SafeCompositionGraphError a b) (SafeCompositionGraph a b, PartialFunctor (SafeCompositionGraph a b) (SCGMorphism a b) a) Source #

Identify two morphisms if it is possible, if not returns an error in a Left member.

You can only identify a composite morphism to another morphism.

If the resulting composition graph is not associative, it returns Left CompositionNotAssociative.

unidentifyMorphismS :: (Eq a, Eq b) => SafeCompositionGraph a b -> SCGMorphism a b -> Either (SafeCompositionGraphError a b) (SafeCompositionGraph a b, PartialFunctor (SafeCompositionGraph a b) (SCGMorphism a b) a) Source #

Unidentify a morphism if it is possible, if not returns an error in a Left member.

Unidentifying a morphism means removing all entries in the composition law with results the morphism.

replaceObjectS :: (Eq a, Eq b) => SafeCompositionGraph a b -> a -> a -> Either (SafeCompositionGraphError a b) (SafeCompositionGraph a b, PartialFunctor (SafeCompositionGraph a b) (SCGMorphism a b) a) Source #

Replaces an object with a new one, if the object to replace is not in the composition graph, returns Nothing.

It is different from deleting the object and inserting the new one because deleting an object deletes all leaving and coming arrows.

replaceMorphismS :: (Eq a, Eq b) => SafeCompositionGraph a b -> SCGMorphism a b -> b -> Either (SafeCompositionGraphError a b) (SafeCompositionGraph a b, PartialFunctor (SafeCompositionGraph a b) (SCGMorphism a b) a) Source #

Replaces a generating morphism with a new one, if the morphism to replace is not a generator of the composition graph, returns Nothing.

It is different from deleting the morphism and inserting the new one because deleting an object deletes related composition law entries.

Deletion

deleteObjectS :: (Eq a, Eq b) => SafeCompositionGraph a b -> a -> Either (SafeCompositionGraphError a b) (SafeCompositionGraph a b, PartialFunctor (SafeCompositionGraph a b) (SCGMorphism a b) a) Source #

Deletes an object and all morphism coming from it or leaving it.

deleteMorphismS :: (Eq a, Eq b) => SafeCompositionGraph a b -> SCGMorphism a b -> Either (SafeCompositionGraphError a b) (SafeCompositionGraph a b, PartialFunctor (SafeCompositionGraph a b) (SCGMorphism a b) a) Source #

Deletes a generating morphism if it can, the generator should not be an identity.

Utility functions

isGenS :: Eq a => SCGMorphism a b -> Bool Source #

Optimized version of isGenerator for SafeCompositionGraph.

isCompS :: Eq a => SCGMorphism a b -> Bool Source #

Optimized version of isComposite for SafeCompositionGraph.

getLabelS :: Eq a => SCGMorphism a b -> Maybe b Source #

Returns the label of a generator arrow which is not an identity.