Safe Haskell	None
Language	Haskell2010

Agda.Utils.SemiRing

Synopsis

class SemiRing a where
- ozero :: a
- oone :: a
- oplus :: a -> a -> a
- otimes :: a -> a -> a
class SemiRing a => StarSemiRing a where
- ostar :: a -> a

Documentation

class SemiRing a where Source #

Semirings (https://en.wikipedia.org/wiki/Semiring).

Methods

ozero :: a Source #

oone :: a Source #

oplus :: a -> a -> a Source #

otimes :: a -> a -> a Source #

Instances

Instances details

SemiRing () Source #
Instance details Defined in Agda.Utils.SemiRing Methods ozero :: () Source # oone :: () Source # oplus :: () -> () -> () Source # otimes :: () -> () -> () Source #
SemiRing Occurrence Source #	`Occurrence` is a complete lattice with least element `Mixed` and greatest element `Unused`. It forms a commutative semiring where `oplus` is meet (glb) and `otimes` is composition. Both operations are idempotent. For `oplus`, `Unused` is neutral (zero) and `Mixed` is dominant. For `otimes`, `StrictPos` is neutral (one) and `Unused` is dominant.
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods ozero :: Occurrence Source # oone :: Occurrence Source # oplus :: Occurrence -> Occurrence -> Occurrence Source # otimes :: Occurrence -> Occurrence -> Occurrence Source #
SemiRing Weight Source #
Instance details Defined in Agda.Utils.Warshall Methods ozero :: Weight Source # oone :: Weight Source # oplus :: Weight -> Weight -> Weight Source # otimes :: Weight -> Weight -> Weight Source #
SemiRing a => SemiRing (Maybe a) Source #
Instance details Defined in Agda.Utils.SemiRing Methods ozero :: Maybe a Source # oone :: Maybe a Source # oplus :: Maybe a -> Maybe a -> Maybe a Source # otimes :: Maybe a -> Maybe a -> Maybe a Source #
SemiRing (Edge (Seq OccursWhere)) Source #	These operations form a semiring if we quotient by the relation "the `Occurrence` components are equal".
Instance details Defined in Agda.TypeChecking.Positivity Methods ozero :: Edge (Seq OccursWhere) Source # oone :: Edge (Seq OccursWhere) Source # oplus :: Edge (Seq OccursWhere) -> Edge (Seq OccursWhere) -> Edge (Seq OccursWhere) Source # otimes :: Edge (Seq OccursWhere) -> Edge (Seq OccursWhere) -> Edge (Seq OccursWhere) Source #

class SemiRing a => StarSemiRing a where Source #

Star semirings (https://en.wikipedia.org/wiki/Semiring#Star_semirings).

Methods

ostar :: a -> a Source #

Instances

Instances details

StarSemiRing () Source #
Instance details Defined in Agda.Utils.SemiRing Methods ostar :: () -> () Source #
StarSemiRing Occurrence Source #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods ostar :: Occurrence -> Occurrence Source #
StarSemiRing a => StarSemiRing (Maybe a) Source #
Instance details Defined in Agda.Utils.SemiRing Methods ostar :: Maybe a -> Maybe a Source #