Copyright	(c) Erich Gut
License	BSD3
Maintainer	zerich.gut@gmail.com
Safe Haskell	Safe-Inferred
Language	Haskell2010

OAlg.Entity.Diagram.Definition

Contents

Diagram
- Chain
- Parallel
Duality
SomeDiagram
X

Description

definition of Diagrams on Oriented structures.

Synopsis

data Diagram t n m a where
- DiagramEmpty :: Diagram 'Empty N0 N0 a
- DiagramDiscrete :: FinList n (Point a) -> Diagram Discrete n N0 a
- DiagramChainTo :: Point a -> FinList m a -> Diagram (Chain To) (m + 1) m a
- DiagramChainFrom :: Point a -> FinList m a -> Diagram (Chain From) (m + 1) m a
- DiagramParallelLR :: Point a -> Point a -> FinList m a -> Diagram (Parallel LeftToRight) N2 m a
- DiagramParallelRL :: Point a -> Point a -> FinList m a -> Diagram (Parallel RightToLeft) N2 m a
- DiagramSink :: Point a -> FinList m a -> Diagram (Star To) (m + 1) m a
- DiagramSource :: Point a -> FinList m a -> Diagram (Star From) (m + 1) m a
- DiagramGeneral :: FinList n (Point a) -> FinList m (a, Orientation N) -> Diagram General n m a
data DiagramType
- = Empty
- | Discrete
- | Chain Site
- | Parallel Direction
- | Star Site
- | General
rt' :: forall (t :: DiagramType). (Dual (Dual t) :~: t) -> Dual (Dual (Dual t)) :~: Dual t
dgType :: Diagram t n m a -> DiagramType
dgTypeRefl :: Diagram t n m a -> Dual (Dual t) :~: t
dgPoints :: Oriented a => Diagram t n m a -> FinList n (Point a)
dgCenter :: Diagram (Star t) n m c -> Point c
dgArrows :: Diagram t n m a -> FinList m a
dgMap :: Hom Ort h => h a b -> Diagram t n m a -> Diagram t n m b
dgQuiver :: Diagram t n m a -> Quiver n m
chnToStart :: Oriented a => Diagram (Chain To) n m a -> Point a
chnFromStart :: Diagram (Chain From) n m a -> Point a
dgPrlAdjZero :: Distributive a => Diagram (Parallel LeftToRight) n m a -> Diagram (Parallel LeftToRight) n (m + 1) a
dgPrlTail :: Diagram (Parallel d) n (m + 1) a -> Diagram (Parallel d) n m a
dgPrlDiffHead :: Abelian a => Diagram (Parallel d) n (m + 1) a -> Diagram (Parallel d) n (m + 1) a
dgPrlDiffTail :: Abelian a => Diagram (Parallel d) n (m + 1) a -> Diagram (Parallel d) n m a
dgToOp :: DiagramDuality f g a -> f a -> g (Op a)
dgFromOp :: DiagramDuality f g a -> g (Op a) -> f a
data DiagramDuality f g a where
- DiagramDuality :: Oriented a => (f a :~: Diagram t n m a) -> (g (Op a) :~: Dual (Diagram t n m a)) -> (Dual (Dual t) :~: t) -> DiagramDuality f g a
coDiagram :: Diagram t n m a -> Dual (Diagram t n m a)
coDiagramInv :: Oriented a => (Dual (Dual t) :~: t) -> Dual (Diagram t n m a) -> Diagram t n m a
dgFromOpOp :: Oriented a => Diagram t n m (Op (Op a)) -> Diagram t n m a
data SomeDiagram a where
- SomeDiagram :: Diagram t n m a -> SomeDiagram a
sdgMap :: Hom Ort h => h a b -> SomeDiagram a -> SomeDiagram b
sdgFromOpOp :: Oriented a => SomeDiagram (Op (Op a)) -> SomeDiagram a
coSomeDiagram :: SomeDiagram a -> Dual (SomeDiagram a)
coSomeDiagramInv :: Oriented a => Dual (SomeDiagram a) -> SomeDiagram a
data XDiagram t n m a where
- XDiagramEmpty :: XDiagram 'Empty N0 N0 a
- XDiagramDiscrete :: Any n -> X (Point a) -> XDiagram Discrete n N0 a
- XDiagramChainTo :: Any m -> XOrtSite To a -> XDiagram (Chain To) (m + 1) m a
- XDiagramChainFrom :: Any m -> XOrtSite From a -> XDiagram (Chain From) (m + 1) m a
- XDiagramParallelLR :: Any m -> XOrtOrientation a -> XDiagram (Parallel LeftToRight) N2 m a
- XDiagramParallelRL :: Any m -> XOrtOrientation a -> XDiagram (Parallel RightToLeft) N2 m a
- XDiagramSink :: Any m -> XOrtSite To a -> XDiagram (Star To) (m + 1) m a
- XDiagramSource :: Any m -> XOrtSite From a -> XDiagram (Star From) (m + 1) m a
xDiagram :: Oriented a => (Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xSomeDiagram :: Oriented a => X SomeNatural -> XOrtSite To a -> XOrtSite From a -> XOrtOrientation a -> X (SomeDiagram a)
dstSomeDiagram :: Oriented a => Int -> X (SomeDiagram a) -> IO ()
xSomeDiagramOrnt :: Entity p => X SomeNatural -> X p -> X (SomeDiagram (Orientation p))

Diagram

data Diagram t n m a where Source #

diagram for a Oriented structure a of type t having n points and m arrows.

Properties Let d be in Diagram t n m a for a Oriented structure a, then holds:

If d matches DiagramChainTo e as then holds: e == end a0 and start ai == end ai+1 for all i = 0..m-2 where a0:|..:|ai:|..:|am-1:|Nil = as.
If d matches DiagramChainFrom s as then holds: s == start a0 and end ai == start ai+1 for all i = 0..m-2 where a0:|..:|ai:|..:|am-1:|Nil = as.
If d matches DiagramParallelLR l r as then holds: orientation a == l:>r for all a in as.
If d matches DiagramParallelRL l r as then holds: orientation a == r:>l for all a in as.
If d matches DiagramSink e as then holds: e == end a for all a in as.
If d matches DiagramSource s as then holds: s == start a for all a in as.
If d matches DiagramGeneral ps aijs then holds pi == start aijandpj == end aij for all aij in aijs and ps = p0..pn-1@.

Constructors

DiagramEmpty :: Diagram 'Empty N0 N0 a
DiagramDiscrete :: FinList n (Point a) -> Diagram Discrete n N0 a
DiagramChainTo :: Point a -> FinList m a -> Diagram (Chain To) (m + 1) m a
DiagramChainFrom :: Point a -> FinList m a -> Diagram (Chain From) (m + 1) m a
DiagramParallelLR :: Point a -> Point a -> FinList m a -> Diagram (Parallel LeftToRight) N2 m a
DiagramParallelRL :: Point a -> Point a -> FinList m a -> Diagram (Parallel RightToLeft) N2 m a
DiagramSink :: Point a -> FinList m a -> Diagram (Star To) (m + 1) m a
DiagramSource :: Point a -> FinList m a -> Diagram (Star From) (m + 1) m a
DiagramGeneral :: FinList n (Point a) -> FinList m (a, Orientation N) -> Diagram General n m a

Instances

Instances details

HomOriented h => Applicative1 h (Diagram t n m) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition Methods amap1 :: h a b -> Diagram t n m a -> Diagram t n m b Source #
Oriented a => Show (Diagram t n m a) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition Methods showsPrec :: Int -> Diagram t n m a -> ShowS # show :: Diagram t n m a -> String # showList :: [Diagram t n m a] -> ShowS #
Oriented a => Eq (Diagram t n m a) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition Methods (==) :: Diagram t n m a -> Diagram t n m a -> Bool # (/=) :: Diagram t n m a -> Diagram t n m a -> Bool #
Oriented a => Validable (Diagram t n m a) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition Methods valid :: Diagram t n m a -> Statement Source #
(Oriented a, XStandardOrtSite 'From a, Attestable m) => XStandard (Diagram ('Chain 'From) ('S m) m a) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition Methods xStandard :: X (Diagram ('Chain 'From) ('S m) m a) Source #
(Oriented a, XStandardOrtSite 'To a, Attestable m) => XStandard (Diagram ('Chain 'To) ('S m) m a) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition Methods xStandard :: X (Diagram ('Chain 'To) ('S m) m a) Source #
(Oriented a, m ~ N0, XStandardPoint a, Attestable n) => XStandard (Diagram 'Discrete n m a) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition Methods xStandard :: X (Diagram 'Discrete n m a) Source #
(Oriented a, n ~ N0, m ~ N0) => XStandard (Diagram 'Empty n m a) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition Methods xStandard :: X (Diagram 'Empty n m a) Source #
(Oriented a, n ~ N2, XStandardOrtOrientation a, Attestable m) => XStandard (Diagram ('Parallel 'LeftToRight) n m a) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition Methods xStandard :: X (Diagram ('Parallel 'LeftToRight) n m a) Source #
(Oriented a, n ~ N2, XStandardOrtOrientation a, Attestable m) => XStandard (Diagram ('Parallel 'RightToLeft) n m a) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition Methods xStandard :: X (Diagram ('Parallel 'RightToLeft) n m a) Source #
(Oriented a, XStandardOrtSite 'From a, Attestable m) => XStandard (Diagram ('Star 'From) ('S m) m a) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition Methods xStandard :: X (Diagram ('Star 'From) ('S m) m a) Source #
(Oriented a, XStandardOrtSite 'To a, Attestable m) => XStandard (Diagram ('Star 'To) ('S m) m a) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition Methods xStandard :: X (Diagram ('Star 'To) ('S m) m a) Source #
(Oriented a, Typeable t, Typeable n, Typeable m) => Entity (Diagram t n m a) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition
(Oriented a, Typeable t, Typeable n, Typeable m) => Oriented (Diagram ('Chain t) n m a) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition Associated Types type Point (Diagram ('Chain t) n m a) Source # Methods orientation :: Diagram ('Chain t) n m a -> Orientation (Point (Diagram ('Chain t) n m a)) Source # start :: Diagram ('Chain t) n m a -> Point (Diagram ('Chain t) n m a) Source # end :: Diagram ('Chain t) n m a -> Point (Diagram ('Chain t) n m a) Source #
(Oriented a, Typeable d, Typeable n, Typeable m) => Oriented (Diagram ('Parallel d) n m a) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition Associated Types type Point (Diagram ('Parallel d) n m a) Source # Methods orientation :: Diagram ('Parallel d) n m a -> Orientation (Point (Diagram ('Parallel d) n m a)) Source # start :: Diagram ('Parallel d) n m a -> Point (Diagram ('Parallel d) n m a) Source # end :: Diagram ('Parallel d) n m a -> Point (Diagram ('Parallel d) n m a) Source #
type Dual (Diagram t n m a :: Type) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition type Dual (Diagram t n m a :: Type) = Diagram (Dual t) n m (Op a)
type Point (Diagram ('Chain t) n m a) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition type Point (Diagram ('Chain t) n m a) = Point a
type Point (Diagram ('Parallel d) n m a) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition type Point (Diagram ('Parallel d) n m a) = Point a

data DiagramType Source #

the types of a Diagram.

Constructors

Empty
Discrete
Chain Site
Parallel Direction
Star Site
General

Instances

Instances details

Show DiagramType Source #
Instance details Defined in OAlg.Entity.Diagram.Definition Methods showsPrec :: Int -> DiagramType -> ShowS # show :: DiagramType -> String # showList :: [DiagramType] -> ShowS #
Eq DiagramType Source #
Instance details Defined in OAlg.Entity.Diagram.Definition Methods (==) :: DiagramType -> DiagramType -> Bool # (/=) :: DiagramType -> DiagramType -> Bool #
Ord DiagramType Source #
Instance details Defined in OAlg.Entity.Diagram.Definition Methods compare :: DiagramType -> DiagramType -> Ordering # (<) :: DiagramType -> DiagramType -> Bool # (<=) :: DiagramType -> DiagramType -> Bool # (>) :: DiagramType -> DiagramType -> Bool # (>=) :: DiagramType -> DiagramType -> Bool # max :: DiagramType -> DiagramType -> DiagramType # min :: DiagramType -> DiagramType -> DiagramType #
type Dual 'Discrete Source #
Instance details Defined in OAlg.Entity.Diagram.Definition type Dual 'Discrete = 'Discrete
type Dual 'Empty Source #
Instance details Defined in OAlg.Entity.Diagram.Definition type Dual 'Empty = 'Empty
type Dual 'General Source #
Instance details Defined in OAlg.Entity.Diagram.Definition type Dual 'General = 'General
type Dual ('Chain 'From) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition type Dual ('Chain 'From) = 'Chain 'To
type Dual ('Chain 'To) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition type Dual ('Chain 'To) = 'Chain 'From
type Dual ('Parallel 'LeftToRight) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition type Dual ('Parallel 'LeftToRight) = 'Parallel 'RightToLeft
type Dual ('Parallel 'RightToLeft) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition type Dual ('Parallel 'RightToLeft) = 'Parallel 'LeftToRight
type Dual ('Star 'From) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition type Dual ('Star 'From) = 'Star 'To
type Dual ('Star 'To) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition type Dual ('Star 'To) = 'Star 'From

rt' :: forall (t :: DiagramType). (Dual (Dual t) :~: t) -> Dual (Dual (Dual t)) :~: Dual t Source #

Dual is well defined on diagram types.

dgType :: Diagram t n m a -> DiagramType Source #

the type of a diagram.

dgTypeRefl :: Diagram t n m a -> Dual (Dual t) :~: t Source #

reflexivity of the underlying diagram type.

dgPoints :: Oriented a => Diagram t n m a -> FinList n (Point a) Source #

the points of a diagram.

dgCenter :: Diagram (Star t) n m c -> Point c Source #

the center point of a Star-diagram.

dgArrows :: Diagram t n m a -> FinList m a Source #

the arrows of a diagram.

dgMap :: Hom Ort h => h a b -> Diagram t n m a -> Diagram t n m b Source #

mapping of a diagram via a homomorphism on Oriented structures.

dgQuiver :: Diagram t n m a -> Quiver n m Source #

the underlying quiver of a diagram.

Chain

chnToStart :: Oriented a => Diagram (Chain To) n m a -> Point a Source #

the last point of the chain.

chnFromStart :: Diagram (Chain From) n m a -> Point a Source #

the first point of the chain.

Parallel

dgPrlAdjZero :: Distributive a => Diagram (Parallel LeftToRight) n m a -> Diagram (Parallel LeftToRight) n (m + 1) a Source #

adjoins a zero arrow as the first parallel arrow.

dgPrlTail :: Diagram (Parallel d) n (m + 1) a -> Diagram (Parallel d) n m a Source #

the _tail__ of a parallel diagram.

dgPrlDiffHead :: Abelian a => Diagram (Parallel d) n (m + 1) a -> Diagram (Parallel d) n (m + 1) a Source #

subtracts to every arrow of the parallel diagram the first arrow.

dgPrlDiffTail :: Abelian a => Diagram (Parallel d) n (m + 1) a -> Diagram (Parallel d) n m a Source #

subtracts the first arrow to all the others an drops it.

Duality

dgToOp :: DiagramDuality f g a -> f a -> g (Op a) Source #

to g (Op a).

dgFromOp :: DiagramDuality f g a -> g (Op a) -> f a Source #

from g (Op a).

data DiagramDuality f g a where Source #

Op-duality between diagrams.

Constructors

DiagramDuality :: Oriented a => (f a :~: Diagram t n m a) -> (g (Op a) :~: Dual (Diagram t n m a)) -> (Dual (Dual t) :~: t) -> DiagramDuality f g a

coDiagram :: Diagram t n m a -> Dual (Diagram t n m a) Source #

the co diagram with its inverse coDiagramInv.

Property Let d be in Diagram t n m a for a Oriented structure a then holds: dgPoints (coDiagram d) == dgPoints d.

coDiagramInv :: Oriented a => (Dual (Dual t) :~: t) -> Dual (Diagram t n m a) -> Diagram t n m a Source #

from the dual diagram, with inverse of coDiagram.

dgFromOpOp :: Oriented a => Diagram t n m (Op (Op a)) -> Diagram t n m a Source #

from Op . Op.

SomeDiagram

data SomeDiagram a where Source #

some diagram.

Constructors

SomeDiagram :: Diagram t n m a -> SomeDiagram a

Instances

Instances details

Oriented a => Show (SomeDiagram a) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition Methods showsPrec :: Int -> SomeDiagram a -> ShowS # show :: SomeDiagram a -> String # showList :: [SomeDiagram a] -> ShowS #
Oriented a => Validable (SomeDiagram a) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition Methods valid :: SomeDiagram a -> Statement Source #
type Dual (SomeDiagram a :: Type) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition type Dual (SomeDiagram a :: Type) = SomeDiagram (Op a)

sdgMap :: Hom Ort h => h a b -> SomeDiagram a -> SomeDiagram b Source #

mapping of some diagram via a homomorphism on Oriented structures.

sdgFromOpOp :: Oriented a => SomeDiagram (Op (Op a)) -> SomeDiagram a Source #

from Op . Op.

coSomeDiagram :: SomeDiagram a -> Dual (SomeDiagram a) Source #

the dual of some diagram, with inverse coSomeDiagramInv.

coSomeDiagramInv :: Oriented a => Dual (SomeDiagram a) -> SomeDiagram a Source #

from the dual of some diagram, with inverse coSomeDiagram.

X

data XDiagram t n m a where Source #

generator for random variables of diagrams.

Constructors

XDiagramEmpty :: XDiagram 'Empty N0 N0 a
XDiagramDiscrete :: Any n -> X (Point a) -> XDiagram Discrete n N0 a
XDiagramChainTo :: Any m -> XOrtSite To a -> XDiagram (Chain To) (m + 1) m a
XDiagramChainFrom :: Any m -> XOrtSite From a -> XDiagram (Chain From) (m + 1) m a
XDiagramParallelLR :: Any m -> XOrtOrientation a -> XDiagram (Parallel LeftToRight) N2 m a
XDiagramParallelRL :: Any m -> XOrtOrientation a -> XDiagram (Parallel RightToLeft) N2 m a
XDiagramSink :: Any m -> XOrtSite To a -> XDiagram (Star To) (m + 1) m a
XDiagramSource :: Any m -> XOrtSite From a -> XDiagram (Star From) (m + 1) m a

Instances

Instances details

type Dual (XDiagram t n m a :: Type) Source #
Instance details Defined in OAlg.Entity.Diagram.Definition type Dual (XDiagram t n m a :: Type) = XDiagram (Dual t) n m (Op a)

xDiagram :: Oriented a => (Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a) Source #

the induced random variables of diagrams.

xSomeDiagram :: Oriented a => X SomeNatural -> XOrtSite To a -> XOrtSite From a -> XOrtOrientation a -> X (SomeDiagram a) Source #

the induced random variable of some diagrams.

dstSomeDiagram :: Oriented a => Int -> X (SomeDiagram a) -> IO () Source #

distribution of a random variable of some diagrams.

xSomeDiagramOrnt :: Entity p => X SomeNatural -> X p -> X (SomeDiagram (Orientation p)) Source #

random variable of some diagram of Orientation p.