Agda-2.8.0: A dependently typed functional programming language and proof assistant

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 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 () Source # |
Instance details Defined in Agda.Utils.SemiRing Methods ozero :: () Source # oone :: () Source # oplus :: () -> () -> () Source # otimes :: () -> () -> () 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 #
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 #

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