OAlg.Entity.Diagram.Definition

definition of Diagrams on Oriented structures.

Diagram

data Diagram t n m a where

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:

1. 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.
2. 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.
3. If d matches DiagramParallelLR l r as then holds: orientation a == l:>r for all a in as.
4. If d matches DiagramParallelRL l r as then holds: orientation a == r:>l for all a in as.
5. If d matches DiagramSink e as then holds: e == end a for all a in as.
6. If d matches DiagramSource s as then holds: s == start a for all a in as.
7. If d matches DiagramGeneral ps aijs then holds pi == start aij and pj == 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

HomOriented h => Applicative1 h (Diagram t n m)

Defined in OAlg.Entity.Diagram.Definition

Methods

amap1 :: h a b -> Diagram t n m a -> Diagram t n m b

Oriented a => Show (Diagram t n m a)

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)

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)

Defined in OAlg.Entity.Diagram.Definition

Methods

valid :: Diagram t n m a -> Statement

(Oriented a, XStandardOrtSite 'From a, Attestable m) => XStandard (Diagram ('Chain 'From) ('S m) m a)

Defined in OAlg.Entity.Diagram.Definition

Methods

xStandard :: X (Diagram ('Chain 'From) ('S m) m a)

(Oriented a, XStandardOrtSite 'To a, Attestable m) => XStandard (Diagram ('Chain 'To) ('S m) m a)

Defined in OAlg.Entity.Diagram.Definition

Methods

xStandard :: X (Diagram ('Chain 'To) ('S m) m a)

(Oriented a, m ~ N0, XStandardPoint a, Attestable n) => XStandard (Diagram 'Discrete n m a)

Defined in OAlg.Entity.Diagram.Definition

Methods

xStandard :: X (Diagram 'Discrete n m a)

(Oriented a, n ~ N0, m ~ N0) => XStandard (Diagram 'Empty n m a)

Defined in OAlg.Entity.Diagram.Definition

Methods

xStandard :: X (Diagram 'Empty n m a)

(Oriented a, n ~ N2, XStandardOrtOrientation a, Attestable m) => XStandard (Diagram ('Parallel 'LeftToRight) n m a)

Defined in OAlg.Entity.Diagram.Definition

Methods

xStandard :: X (Diagram ('Parallel 'LeftToRight) n m a)

(Oriented a, n ~ N2, XStandardOrtOrientation a, Attestable m) => XStandard (Diagram ('Parallel 'RightToLeft) n m a)

Defined in OAlg.Entity.Diagram.Definition

Methods

xStandard :: X (Diagram ('Parallel 'RightToLeft) n m a)

(Oriented a, XStandardOrtSite 'From a, Attestable m) => XStandard (Diagram ('Star 'From) ('S m) m a)

Defined in OAlg.Entity.Diagram.Definition

Methods

xStandard :: X (Diagram ('Star 'From) ('S m) m a)

(Oriented a, XStandardOrtSite 'To a, Attestable m) => XStandard (Diagram ('Star 'To) ('S m) m a)

Defined in OAlg.Entity.Diagram.Definition

Methods

xStandard :: X (Diagram ('Star 'To) ('S m) m a)

(Oriented a, Typeable t, Typeable n, Typeable m) => Entity (Diagram t n m a)

Defined in OAlg.Entity.Diagram.Definition

(Oriented a, Typeable t, Typeable n, Typeable m) => Oriented (Diagram ('Chain t) n m a)

Defined in OAlg.Entity.Diagram.Definition

Associated Types

type Point (Diagram ('Chain t) n m a)

Methods

orientation :: Diagram ('Chain t) n m a -> Orientation (Point (Diagram ('Chain t) n m a))

start :: Diagram ('Chain t) n m a -> Point (Diagram ('Chain t) n m a)

end :: Diagram ('Chain t) n m a -> Point (Diagram ('Chain t) n m a)

(Oriented a, Typeable d, Typeable n, Typeable m) => Oriented (Diagram ('Parallel d) n m a)

Defined in OAlg.Entity.Diagram.Definition

Associated Types

type Point (Diagram ('Parallel d) n m a)

Methods

orientation :: Diagram ('Parallel d) n m a -> Orientation (Point (Diagram ('Parallel d) n m a))

start :: Diagram ('Parallel d) n m a -> Point (Diagram ('Parallel d) n m a)

end :: Diagram ('Parallel d) n m a -> Point (Diagram ('Parallel d) n m a)

type Dual (Diagram t n m a :: Type)

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)

Defined in OAlg.Entity.Diagram.Definition

type Point (Diagram ('Chain t) n m a) = Point a

type Point (Diagram ('Parallel d) n m a)

Defined in OAlg.Entity.Diagram.Definition

type Point (Diagram ('Parallel d) n m a) = Point a

data DiagramType

the types of a Diagram.

Constructors

Empty

Discrete

Chain Site

Parallel Direction

Star Site

General

Instances

Show DiagramType

Defined in OAlg.Entity.Diagram.Definition

Methods

showsPrec :: Int -> DiagramType -> ShowS

show :: DiagramType -> String

showList :: [DiagramType] -> ShowS

Eq DiagramType

Defined in OAlg.Entity.Diagram.Definition

Methods

(==) :: DiagramType -> DiagramType -> Bool

(/=) :: DiagramType -> DiagramType -> Bool

Ord DiagramType

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

Defined in OAlg.Entity.Diagram.Definition

type Dual 'Discrete = 'Discrete

type Dual 'Empty

Defined in OAlg.Entity.Diagram.Definition

type Dual 'Empty = 'Empty

type Dual 'General

Defined in OAlg.Entity.Diagram.Definition

type Dual 'General = 'General

type Dual ('Chain 'From)

Defined in OAlg.Entity.Diagram.Definition

type Dual ('Chain 'From) = 'Chain 'To

type Dual ('Chain 'To)

Defined in OAlg.Entity.Diagram.Definition

type Dual ('Chain 'To) = 'Chain 'From

type Dual ('Parallel 'LeftToRight)

Defined in OAlg.Entity.Diagram.Definition

type Dual ('Parallel 'LeftToRight) = 'Parallel 'RightToLeft

type Dual ('Parallel 'RightToLeft)

Defined in OAlg.Entity.Diagram.Definition

type Dual ('Parallel 'RightToLeft) = 'Parallel 'LeftToRight

type Dual ('Star 'From)

Defined in OAlg.Entity.Diagram.Definition

type Dual ('Star 'From) = 'Star 'To

type Dual ('Star 'To)

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

Dual is well defined on diagram types.

dgType :: Diagram t n m a -> DiagramType

the type of a diagram.

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

reflexivity of the underlying diagram type.

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

the points of a diagram.

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

the center point of a Star-diagram.

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

the arrows of a diagram.

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

mapping of a diagram via a homomorphism on Oriented structures.

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

the underlying quiver of a diagram.

Chain

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

the last point of the chain.

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

the first point of the chain.

Parallel

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

adjoins a zero arrow as the first parallel arrow.

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

the _tail__ of a parallel diagram.

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

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

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

Duality

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

to g (Op a).

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

from g (Op a).

data DiagramDuality f g a where

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)

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

from the dual diagram, with inverse of coDiagram.

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

from Op . Op.

SomeDiagram

data SomeDiagram a where

some diagram.

Constructors

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

Instances

Oriented a => Show (SomeDiagram a)

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)

Defined in OAlg.Entity.Diagram.Definition

Methods

valid :: SomeDiagram a -> Statement

type Dual (SomeDiagram a :: Type)

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

mapping of some diagram via a homomorphism on Oriented structures.

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

from Op . Op.

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

the dual of some diagram, with inverse coSomeDiagramInv.

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

from the dual of some diagram, with inverse coSomeDiagram.

X

data XDiagram t n m a where

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

type Dual (XDiagram t n m a :: Type)

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)

the induced random variables of diagrams.

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

the induced random variable of some diagrams.

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

distribution of a random variable of some diagrams.

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

random variable of some diagram of Orientation p.