Safe Haskell	Safe
Language	Haskell2010

Agda.Utils.SemiRing

Synopsis

Documentation

class SemiRing a where #

Minimal complete definition

Methods

oone :: a #

oplus :: a -> a -> a #

otimes :: a -> a -> a #

Instances

SemiRing () #
Instance details Defined in Agda.Utils.SemiRing Methods ozero :: () # oone :: () # oplus :: () -> () -> () # otimes :: () -> () -> () #
SemiRing Occurrence #	`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 # oone :: Occurrence # oplus :: Occurrence -> Occurrence -> Occurrence # otimes :: Occurrence -> Occurrence -> Occurrence #
SemiRing Weight #
Instance details Defined in Agda.Utils.Warshall Methods ozero :: Weight # oone :: Weight # oplus :: Weight -> Weight -> Weight # otimes :: Weight -> Weight -> Weight #
SemiRing Edge #	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 # oone :: Edge # oplus :: Edge -> Edge -> Edge # otimes :: Edge -> Edge -> Edge #
SemiRing a => SemiRing (Maybe a) #
Instance details Defined in Agda.Utils.SemiRing Methods ozero :: Maybe a # oone :: Maybe a # oplus :: Maybe a -> Maybe a -> Maybe a # otimes :: Maybe a -> Maybe a -> Maybe a #

Minimal complete definition

Methods

ostar :: a -> a #

Instances

StarSemiRing () #
Instance details Defined in Agda.Utils.SemiRing Methods ostar :: () -> () #
StarSemiRing Occurrence #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods ostar :: Occurrence -> Occurrence #
StarSemiRing Edge #	As `OccursWhere` does not have an `oplus` we cannot do something meaningful for the `OccursWhere` here. E.g. `ostar (Edge JustNeg w) = Edge Mixed (w oplus (w >*< w))` would probably more sense, if we could do it.
Instance details Defined in Agda.TypeChecking.Positivity Methods ostar :: Edge -> Edge #
StarSemiRing a => StarSemiRing (Maybe a) #
Instance details Defined in Agda.Utils.SemiRing Methods ostar :: Maybe a -> Maybe a #