Agda.Utils.SemiRing

Documentation

class SemiRing a where

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

Minimal complete definition

ozero, oone, oplus, otimes

Methods

ozero :: a

oone :: a

oplus :: a -> a -> a

otimes :: a -> a -> a

Instances

SemiRing ()

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.

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

ozero :: Occurrence

oone :: Occurrence

oplus :: Occurrence -> Occurrence -> Occurrence

otimes :: Occurrence -> Occurrence -> Occurrence

SemiRing Weight

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".

Defined in Agda.TypeChecking.Positivity

Methods

ozero :: Edge

oone :: Edge

oplus :: Edge -> Edge -> Edge

otimes :: Edge -> Edge -> Edge

SemiRing a => SemiRing (Maybe a)

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

class SemiRing a => StarSemiRing a where

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

Minimal complete definition

ostar

Methods

ostar :: a -> a

Instances

StarSemiRing ()

Defined in Agda.Utils.SemiRing

Methods

ostar :: () -> ()

StarSemiRing Occurrence

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.

Defined in Agda.TypeChecking.Positivity

Methods

ostar :: Edge -> Edge

StarSemiRing a => StarSemiRing (Maybe a)

Defined in Agda.Utils.SemiRing

Methods

ostar :: Maybe a -> Maybe a