Safe Haskell	None
Language	GHC2021

Data.InternalCategory

Contents

Path
Internal categories
Reexport

Synopsis

data Path v e where
- UnsafePath v [e] v
- pattern Path :: v -> [e] -> v -> Path v e
- pattern EmptyPath :: v -> Path v e
- pattern NonEmptyPath :: e -> [e] -> Path v e
path :: (Eq v, IQuiver v e) => v -> [e] -> v -> Maybe (Path v e)
emptyPath :: v -> Path v e
singlePath :: IQuiver v e => e -> Path v e
composePath :: Eq v => Path v e -> Path v e -> Maybe (Path v e)
(>?>) :: Eq v => Path v e -> Path v e -> Maybe (Path v e)
concatPath :: Path v (Path v e) -> Path v e
errPath :: (HasCallStack, Eq v, Show v, IQuiver v e) => v -> [e] -> v -> Path v e
errComposePath :: (HasCallStack, Show v, Eq v) => Path v e -> Path v e -> Path v e
(>!>) :: (HasCallStack, Show v, Eq v) => Path v e -> Path v e -> Path v e
injectLeftPath :: Path v e -> Path (Either v w) (Either e f)
injectRightPath :: Path w f -> Path (Either v w) (Either e f)
separateSumPath :: Path (Either v w) (Either e f) -> Either (Path v e) (Path w f)
fstPath :: Path (v, w) (e, f) -> Path v e
sndPath :: Path (v, w) (e, f) -> Path w f
unsafePath :: v -> [e] -> v -> Path v e
class IQuiver ob mor => ICategory ob mor | mor -> ob where
- foldPath :: Path ob mor -> mor
dom :: ICategory ob mor => mor -> ob
cod :: ICategory ob mor => mor -> ob
identity :: ICategory ob mor => ob -> mor
compose :: (Eq ob, ICategory ob mor) => mor -> mor -> Maybe mor
class IQuiver v e | e -> v where
- src :: e -> v
- tgt :: e -> v

Path

data Path v e Source #

Constructors

UnsafePath v [e] v

Bundled Patterns

pattern Path :: v -> [e] -> v -> Path v e
pattern EmptyPath :: v -> Path v e
pattern NonEmptyPath :: e -> [e] -> Path v e

Instances

Instances details

ICategory ob (Path ob mor) Source #	`Path` is the free category
Instance details Defined in Data.InternalCategory Methods foldPath :: Path ob (Path ob mor) -> Path ob mor Source #
IQuiver v (Path v e) Source #
Instance details Defined in Data.InternalCategory Methods src :: Path v e -> v Source # tgt :: Path v e -> v Source #
(Eq e, Eq v) => Eq (Path v e) Source #
Instance details Defined in Data.InternalCategory Methods (==) :: Path v e -> Path v e -> Bool # (/=) :: Path v e -> Path v e -> Bool #
(Ord e, Ord v) => Ord (Path v e) Source #
Instance details Defined in Data.InternalCategory Methods compare :: Path v e -> Path v e -> Ordering # (<) :: Path v e -> Path v e -> Bool # (<=) :: Path v e -> Path v e -> Bool # (>) :: Path v e -> Path v e -> Bool # (>=) :: Path v e -> Path v e -> Bool # max :: Path v e -> Path v e -> Path v e # min :: Path v e -> Path v e -> Path v e #

Constructing path

path :: (Eq v, IQuiver v e) => v -> [e] -> v -> Maybe (Path v e) Source #

emptyPath :: v -> Path v e Source #

singlePath :: IQuiver v e => e -> Path v e Source #

composePath :: Eq v => Path v e -> Path v e -> Maybe (Path v e) Source #

(>?>) :: Eq v => Path v e -> Path v e -> Maybe (Path v e) infixr 1 Source #

concatPath :: Path v (Path v e) -> Path v e Source #

Partial construction functions

errPath :: (HasCallStack, Eq v, Show v, IQuiver v e) => v -> [e] -> v -> Path v e Source #

errComposePath :: (HasCallStack, Show v, Eq v) => Path v e -> Path v e -> Path v e Source #

(>!>) :: (HasCallStack, Show v, Eq v) => Path v e -> Path v e -> Path v e infixr 1 Source #

Sum and Product of paths

injectLeftPath :: Path v e -> Path (Either v w) (Either e f) Source #

injectRightPath :: Path w f -> Path (Either v w) (Either e f) Source #

separateSumPath :: Path (Either v w) (Either e f) -> Either (Path v e) (Path w f) Source #

fstPath :: Path (v, w) (e, f) -> Path v e Source #

sndPath :: Path (v, w) (e, f) -> Path w f Source #

Unsafe

unsafePath :: v -> [e] -> v -> Path v e Source #

Internal categories

class IQuiver ob mor => ICategory ob mor | mor -> ob where Source #

Methods

foldPath :: Path ob mor -> mor Source #

Instances

Instances details

ICategory Void Void Source #	Empty graph
Instance details Defined in Data.InternalCategory Methods foldPath :: Path Void Void -> Void Source #
ICategory () () Source #	A graph with one vertex and one loop on it
Instance details Defined in Data.InternalCategory Methods foldPath :: Path () () -> () Source #
Eq a => ICategory a (Codisc a) Source #
Instance details Defined in Data.InternalCategory.Codiscrete Methods foldPath :: Path a (Codisc a) -> Codisc a Source #
Eq a => ICategory a (Disc a) Source #
Instance details Defined in Data.InternalCategory.Discrete Methods foldPath :: Path a (Disc a) -> Disc a Source #
ICategory ob (Path ob mor) Source #	`Path` is the free category
Instance details Defined in Data.InternalCategory Methods foldPath :: Path ob (Path ob mor) -> Path ob mor Source #
(Comonad f, Polynomial f, GEq (Tag f)) => ICategory (Pos f) (Dir f) Source #
Instance details Defined in Data.InternalCategory.PolyComonad Methods foldPath :: Path (Pos f) (Dir f) -> Dir f Source #
(Category cat, SDecide k) => ICategory (SomeSing k) (Mor k cat) Source #
Instance details Defined in Data.InternalCategory.Morphism Methods foldPath :: Path (SomeSing k) (Mor k cat) -> Mor k cat Source #
(ICategory v e, ICategory w f) => ICategory (Either v w) (Either e f) Source #
Instance details Defined in Data.InternalCategory Methods foldPath :: Path (Either v w) (Either e f) -> Either e f Source #
(ICategory v e, ICategory w f) => ICategory (v, w) (e, f) Source #
Instance details Defined in Data.InternalCategory Methods foldPath :: Path (v, w) (e, f) -> (e, f) Source #

dom :: ICategory ob mor => mor -> ob Source #

cod :: ICategory ob mor => mor -> ob Source #

identity :: ICategory ob mor => ob -> mor Source #

compose :: (Eq ob, ICategory ob mor) => mor -> mor -> Maybe mor Source #

Reexport

class IQuiver v e | e -> v where Source #

Class for Quiver represented by types of edges and vertices

Methods

src :: e -> v Source #

tgt :: e -> v Source #

Instances

Instances details

IQuiver Void Void Source #	Empty graph
Instance details Defined in Data.InternalQuiver Methods src :: Void -> Void Source # tgt :: Void -> Void Source #
IQuiver () () Source #	A graph with one vertex and one loop on it
Instance details Defined in Data.InternalQuiver Methods src :: () -> () Source # tgt :: () -> () Source #
IQuiver a (Codisc a) Source #
Instance details Defined in Data.InternalCategory.Codiscrete Methods src :: Codisc a -> a Source # tgt :: Codisc a -> a Source #
IQuiver a (Disc a) Source #
Instance details Defined in Data.InternalCategory.Discrete Methods src :: Disc a -> a Source # tgt :: Disc a -> a Source #
IQuiver v (Path v e) Source #
Instance details Defined in Data.InternalCategory Methods src :: Path v e -> v Source # tgt :: Path v e -> v Source #
(Comonad f, Polynomial f, GEq (Tag f)) => IQuiver (Pos f) (Dir f) Source #
Instance details Defined in Data.InternalCategory.PolyComonad Methods src :: Dir f -> Pos f Source # tgt :: Dir f -> Pos f Source #
IQuiver (SomeSing k) (Mor k cat) Source #
Instance details Defined in Data.InternalCategory.Morphism Methods src :: Mor k cat -> SomeSing k Source # tgt :: Mor k cat -> SomeSing k Source #
(IQuiver v e, IQuiver w f) => IQuiver (Either v w) (Either e f) Source #
Instance details Defined in Data.InternalQuiver Methods src :: Either e f -> Either v w Source # tgt :: Either e f -> Either v w Source #
(IQuiver v e, IQuiver w f) => IQuiver (v, w) (e, f) Source #
Instance details Defined in Data.InternalQuiver Methods src :: (e, f) -> (v, w) Source # tgt :: (e, f) -> (v, w) Source #